PA008O

scaled_inverse_transport_right

Alpha v16 checked-use theorem · independently closed; not Stable

A scaled inverse survives replacement by a congruent right factor.

Exact expanded PA statement

forall p a x y z. (exists esi_mod_left_transport_source esi_mod_right_transport_source. (x * y) + p * esi_mod_left_transport_source = (a) + p * esi_mod_right_transport_source) -> (exists esi_mod_left_transport_argument esi_mod_right_transport_argument. (y) + p * esi_mod_left_transport_argument = (z) + p * esi_mod_right_transport_argument) -> (exists esi_mod_left_transport_result esi_mod_right_transport_result. (x * z) + p * esi_mod_left_transport_result = (a) + p * esi_mod_right_transport_result)

Structural proof guide

Generated structural guide

A scaled inverse survives replacement by a congruent right factor.

Use the direct prerequisites mod_eq_mul_left, mod_eq_symm, mod_eq_trans as previously established PA formulas.

The proof proceeds by intermediate claims (2).

Referenced ingredients

PA0020 mod_eq_mul_left PA003L mod_eq_symm PA0024 mod_eq_trans

Proof neighborhood

Direct dependencies

PA0020 mod_eq_mul_left PA003L mod_eq_symm PA0024 mod_eq_trans

Direct dependents

PA008Q prime_scaled_inverse_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro p
  2. 0002intro a
  3. 0003intro x
  4. 0004intro y
  5. 0005intro z
  6. 0006intro hxy
  7. 0007intro hyz
  8. 0008have hscaled : exists esi_mod_left_transport_scaled esi_mod_right_transport_scaled. (x * y) + p * esi_mod_left_transport_scaled = (x * z) + p * esi_mod_right_transport_scaled
  9. 0009specialize mod_eq_mul_left p
  10. 0010specialize mod_eq_mul_left y
  11. 0011specialize mod_eq_mul_left z
  12. 0012specialize mod_eq_mul_left x
  13. 0013apply mod_eq_mul_left
  14. 0014exact hyz
  15. 0015have hreverse : exists esi_mod_left_transport_reverse esi_mod_right_transport_reverse. (x * z) + p * esi_mod_left_transport_reverse = (x * y) + p * esi_mod_right_transport_reverse
  16. 0016specialize mod_eq_symm p
  17. 0017specialize mod_eq_symm (x * y)
  18. 0018specialize mod_eq_symm (x * z)
  19. 0019apply mod_eq_symm
  20. 0020exact hscaled
  21. 0021specialize mod_eq_trans p
  22. 0022specialize mod_eq_trans (x * z)
  23. 0023specialize mod_eq_trans (x * y)
  24. 0024specialize mod_eq_trans a
  25. 0025apply mod_eq_trans
  26. 0026exact hreverse
  27. 0027exact hxy