| Step | Hyp | Ref
| Expression |
| 1 | | simpllr 776 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) |
| 2 | 1 | simprd 495 |
. . . 4
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → (𝐴 − 𝐵) = (𝐶 − 𝑥)) |
| 3 | | legval.p |
. . . . . 6
⊢ 𝑃 = (Base‘𝐺) |
| 4 | | legval.d |
. . . . . 6
⊢ − =
(dist‘𝐺) |
| 5 | | legval.i |
. . . . . 6
⊢ 𝐼 = (Itv‘𝐺) |
| 6 | | legval.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 7 | 6 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝐺 ∈ TarskiG) |
| 8 | | simp-4r 784 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝑥 ∈ 𝑃) |
| 9 | | legtrd.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
| 10 | 9 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝐷 ∈ 𝑃) |
| 11 | | legtrd.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
| 12 | 11 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝐶 ∈ 𝑃) |
| 13 | 1 | simpld 494 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝑥 ∈ (𝐶𝐼𝐷)) |
| 14 | 3, 4, 5, 7, 12, 8,
10, 13 | tgbtwncom 28496 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝑥 ∈ (𝐷𝐼𝐶)) |
| 15 | | simpr 484 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) |
| 16 | 15 | simpld 494 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝐷 ∈ (𝐶𝐼𝑦)) |
| 17 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝑦 ∈ 𝑃) |
| 18 | | legid.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| 19 | 18 | ad4antr 732 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝐵 ∈ 𝑃) |
| 20 | | legid.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 21 | 20 | ad4antr 732 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝐴 ∈ 𝑃) |
| 22 | 3, 4, 5, 7, 12, 10, 17, 16 | tgbtwncom 28496 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝐷 ∈ (𝑦𝐼𝐶)) |
| 23 | 3, 4, 5, 7, 17, 10, 8, 12, 22, 14 | tgbtwnexch2 28504 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝑥 ∈ (𝑦𝐼𝐶)) |
| 24 | 3, 4, 5, 7, 19, 21 | tgbtwntriv1 28499 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝐵 ∈ (𝐵𝐼𝐴)) |
| 25 | 15 | simprd 495 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → (𝐶 − 𝑦) = (𝐴 − 𝐵)) |
| 26 | 3, 4, 5, 7, 12, 17, 21, 19, 25 | tgcgrcomlr 28488 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → (𝑦 − 𝐶) = (𝐵 − 𝐴)) |
| 27 | 2 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → (𝐶 − 𝑥) = (𝐴 − 𝐵)) |
| 28 | 3, 4, 5, 7, 12, 8,
21, 19, 27 | tgcgrcomlr 28488 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → (𝑥 − 𝐶) = (𝐵 − 𝐴)) |
| 29 | 3, 4, 5, 7, 17, 8,
12, 19, 19, 21, 23, 24, 26, 28 | tgcgrsub 28517 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → (𝑦 − 𝑥) = (𝐵 − 𝐵)) |
| 30 | 3, 4, 5, 7, 17, 8,
19, 29 | axtgcgrid 28471 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝑦 = 𝑥) |
| 31 | 30 | oveq2d 7447 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → (𝐶𝐼𝑦) = (𝐶𝐼𝑥)) |
| 32 | 16, 31 | eleqtrd 2843 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝐷 ∈ (𝐶𝐼𝑥)) |
| 33 | 3, 4, 5, 7, 12, 10, 8, 32 | tgbtwncom 28496 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝐷 ∈ (𝑥𝐼𝐶)) |
| 34 | 3, 4, 5, 7, 8, 10,
12, 14, 33 | tgbtwnswapid 28500 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → 𝑥 = 𝐷) |
| 35 | 34 | oveq2d 7447 |
. . . 4
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → (𝐶 − 𝑥) = (𝐶 − 𝐷)) |
| 36 | 2, 35 | eqtrd 2777 |
. . 3
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) → (𝐴 − 𝐵) = (𝐶 − 𝐷)) |
| 37 | | legtri3.2 |
. . . . 5
⊢ (𝜑 → (𝐶 − 𝐷) ≤ (𝐴 − 𝐵)) |
| 38 | | legval.l |
. . . . . 6
⊢ ≤ =
(≤G‘𝐺) |
| 39 | 3, 4, 5, 38, 6, 11, 9, 20, 18 | legov2 28594 |
. . . . 5
⊢ (𝜑 → ((𝐶 − 𝐷) ≤ (𝐴 − 𝐵) ↔ ∃𝑦 ∈ 𝑃 (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵)))) |
| 40 | 37, 39 | mpbid 232 |
. . . 4
⊢ (𝜑 → ∃𝑦 ∈ 𝑃 (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) |
| 41 | 40 | ad2antrr 726 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) → ∃𝑦 ∈ 𝑃 (𝐷 ∈ (𝐶𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐴 − 𝐵))) |
| 42 | 36, 41 | r19.29a 3162 |
. 2
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) → (𝐴 − 𝐵) = (𝐶 − 𝐷)) |
| 43 | | legtri3.1 |
. . 3
⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐶 − 𝐷)) |
| 44 | 3, 4, 5, 38, 6, 20, 18, 11, 9 | legov 28593 |
. . 3
⊢ (𝜑 → ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ↔ ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥)))) |
| 45 | 43, 44 | mpbid 232 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) |
| 46 | 42, 45 | r19.29a 3162 |
1
⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) |