PA008O · theorem

scaled_inverse_transport_right

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

A scaled inverse survives replacement by a congruent right factor.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ p. ∀ a. ∀ x. ∀ y. ∀ z. ModEq(p,x · y,a) → ModEq(p,y,z) → ModEq(p,x · z,a)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0008 ModEq

3 occurrences

In local proof propositions

PD0008 ModEq

2 occurrences

Exact expanded native-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)

Proof neighborhood

Direct theorem prerequisites

PA0020 mod_eq_mul_left PA003L mod_eq_symm PA0024 mod_eq_trans

Direct theorem dependents

PA008Q prime_scaled_inverse_exists

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

27 script commands · 4 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
mod eq mul leftmod eq symmmod eq trans
01Fix variables and assumptionsL1–7

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro z
  6. L6
    intro hxy
  7. L7
    intro hyz
02Establish hscaledL8–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq mul left.

  1. L8
    have hscaled : ModEq(p,x · y,x · z)Definitions: ModEq(p,x · y,x · z)Original native command in the exact edition
  2. L9
    specialize mod_eq_mul_left p
  3. L10
    specialize mod_eq_mul_left y
  4. L11
    specialize mod_eq_mul_left z
  5. L12
    specialize mod_eq_mul_left x
  6. L13
    apply mod_eq_mul_left
  7. L14
    exact hyz
03Establish hreverseL15–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L15
    have hreverse : ModEq(p,x · z,x · y)Definitions: ModEq(p,x · z,x · y)Original native command in the exact edition
  2. L16
    specialize mod_eq_symm p
  3. L17
    specialize mod_eq_symm (x * y)
  4. L18
    specialize mod_eq_symm (x * z)
  5. L19
    apply mod_eq_symm
  6. L20
    exact hscaled
  7. L21
    specialize mod_eq_trans p
  8. L22
    specialize mod_eq_trans (x * z)
  9. L23
    specialize mod_eq_trans (x * y)
  10. L24
    specialize mod_eq_trans a
04Use earlier factsL25–27

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L25
    apply mod_eq_trans
  2. L26
    exact hreverse
  3. L27
    exact hxy

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro x
  4. 0004intro y
  5. 0005intro z
  6. 0006intro hxy
  7. 0007intro hyz
  8. 0008have hscaled : ModEq(p,x · y,x · z)
    Exact native replay linehave 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 : ModEq(p,x · z,x · y)
    Exact native replay linehave 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