| Step | Hyp | Ref
| Expression |
| 1 | | legval.p |
. . 3
⊢ 𝑃 = (Base‘𝐺) |
| 2 | | legval.d |
. . 3
⊢ − =
(dist‘𝐺) |
| 3 | | legval.i |
. . 3
⊢ 𝐼 = (Itv‘𝐺) |
| 4 | | legval.l |
. . 3
⊢ ≤ =
(≤G‘𝐺) |
| 5 | | legval.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 6 | | legov.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 7 | | legov.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| 8 | | legov.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
| 9 | | legov.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
| 10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | legov 28593 |
. 2
⊢ (𝜑 → ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ↔ ∃𝑦 ∈ 𝑃 (𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦)))) |
| 11 | | eqid 2737 |
. . . . . . 7
⊢
(LineG‘𝐺) =
(LineG‘𝐺) |
| 12 | 5 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) → 𝐺 ∈ TarskiG) |
| 13 | 8 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) → 𝐶 ∈ 𝑃) |
| 14 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) → 𝑧 ∈ 𝑃) |
| 15 | 9 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) → 𝐷 ∈ 𝑃) |
| 16 | | eqid 2737 |
. . . . . . 7
⊢
(cgrG‘𝐺) =
(cgrG‘𝐺) |
| 17 | 6 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) → 𝐴 ∈ 𝑃) |
| 18 | 7 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) → 𝐵 ∈ 𝑃) |
| 19 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) → 𝑧 ∈ (𝐶𝐼𝐷)) |
| 20 | 1, 11, 3, 12, 13, 15, 14, 19 | btwncolg1 28563 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) → (𝑧 ∈ (𝐶(LineG‘𝐺)𝐷) ∨ 𝐶 = 𝐷)) |
| 21 | | simprr 773 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) → (𝐴 − 𝐵) = (𝐶 − 𝑧)) |
| 22 | 21 | eqcomd 2743 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) → (𝐶 − 𝑧) = (𝐴 − 𝐵)) |
| 23 | 1, 11, 3, 12, 13, 14, 15, 16, 17, 18, 2, 20, 22 | lnext 28575 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) → ∃𝑥 ∈ 𝑃 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) |
| 24 | 12 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → 𝐺 ∈ TarskiG) |
| 25 | 13 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → 𝐶 ∈ 𝑃) |
| 26 | 14 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → 𝑧 ∈ 𝑃) |
| 27 | 15 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → 𝐷 ∈ 𝑃) |
| 28 | 17 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → 𝐴 ∈ 𝑃) |
| 29 | 18 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → 𝐵 ∈ 𝑃) |
| 30 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → 𝑥 ∈ 𝑃) |
| 31 | | simpr 484 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) |
| 32 | | simpllr 776 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) |
| 33 | 32 | simpld 494 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → 𝑧 ∈ (𝐶𝐼𝐷)) |
| 34 | 1, 2, 3, 16, 24, 25, 26, 27, 28, 29, 30, 31, 33 | tgbtwnxfr 28538 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → 𝐵 ∈ (𝐴𝐼𝑥)) |
| 35 | 1, 2, 3, 16, 24, 25, 26, 27, 28, 29, 30, 31 | trgcgrcom 28536 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐶𝑧𝐷”〉) |
| 36 | 1, 2, 3, 16, 24, 28, 29, 30, 25, 26, 27, 35 | cgr3simp3 28530 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → (𝑥 − 𝐴) = (𝐷 − 𝐶)) |
| 37 | 1, 2, 3, 24, 30, 28, 27, 25, 36 | tgcgrcomlr 28488 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → (𝐴 − 𝑥) = (𝐶 − 𝐷)) |
| 38 | 34, 37 | jca 511 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉) → (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷))) |
| 39 | 38 | ex 412 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) ∧ 𝑥 ∈ 𝑃) → (〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉 → (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷)))) |
| 40 | 39 | reximdva 3168 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) → (∃𝑥 ∈ 𝑃 〈“𝐶𝑧𝐷”〉(cgrG‘𝐺)〈“𝐴𝐵𝑥”〉 → ∃𝑥 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷)))) |
| 41 | 23, 40 | mpd 15 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) → ∃𝑥 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷))) |
| 42 | 41 | adantllr 719 |
. . . 4
⊢ ((((𝜑 ∧ ∃𝑦 ∈ 𝑃 (𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) → ∃𝑥 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷))) |
| 43 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ ∃𝑦 ∈ 𝑃 (𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦))) → ∃𝑦 ∈ 𝑃 (𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦))) |
| 44 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (𝑦 ∈ (𝐶𝐼𝐷) ↔ 𝑧 ∈ (𝐶𝐼𝐷))) |
| 45 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝐶 − 𝑦) = (𝐶 − 𝑧)) |
| 46 | 45 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ((𝐴 − 𝐵) = (𝐶 − 𝑦) ↔ (𝐴 − 𝐵) = (𝐶 − 𝑧))) |
| 47 | 44, 46 | anbi12d 632 |
. . . . . 6
⊢ (𝑦 = 𝑧 → ((𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦)) ↔ (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧)))) |
| 48 | 47 | cbvrexvw 3238 |
. . . . 5
⊢
(∃𝑦 ∈
𝑃 (𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦)) ↔ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) |
| 49 | 43, 48 | sylib 218 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑦 ∈ 𝑃 (𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦))) → ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))) |
| 50 | 42, 49 | r19.29a 3162 |
. . 3
⊢ ((𝜑 ∧ ∃𝑦 ∈ 𝑃 (𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦))) → ∃𝑥 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷))) |
| 51 | 5 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) → 𝐺 ∈ TarskiG) |
| 52 | 6 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) → 𝐴 ∈ 𝑃) |
| 53 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) → 𝑧 ∈ 𝑃) |
| 54 | 7 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) → 𝐵 ∈ 𝑃) |
| 55 | 8 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) → 𝐶 ∈ 𝑃) |
| 56 | 9 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) → 𝐷 ∈ 𝑃) |
| 57 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) → 𝐵 ∈ (𝐴𝐼𝑧)) |
| 58 | 1, 11, 3, 51, 52, 54, 53, 57 | btwncolg3 28565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) → (𝑧 ∈ (𝐴(LineG‘𝐺)𝐵) ∨ 𝐴 = 𝐵)) |
| 59 | | simprr 773 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) → (𝐴 − 𝑧) = (𝐶 − 𝐷)) |
| 60 | 1, 11, 3, 51, 52, 53, 54, 16, 55, 56, 2, 58, 59 | lnext 28575 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) → ∃𝑦 ∈ 𝑃 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) |
| 61 | 51 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → 𝐺 ∈ TarskiG) |
| 62 | 52 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → 𝐴 ∈ 𝑃) |
| 63 | 54 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → 𝐵 ∈ 𝑃) |
| 64 | 53 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → 𝑧 ∈ 𝑃) |
| 65 | 55 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → 𝐶 ∈ 𝑃) |
| 66 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → 𝑦 ∈ 𝑃) |
| 67 | 56 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → 𝐷 ∈ 𝑃) |
| 68 | | simpr 484 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) |
| 69 | 1, 2, 3, 16, 61, 62, 64, 63, 65, 67, 66, 68 | cgr3swap23 28532 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → 〈“𝐴𝐵𝑧”〉(cgrG‘𝐺)〈“𝐶𝑦𝐷”〉) |
| 70 | | simpllr 776 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) |
| 71 | 70 | simpld 494 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → 𝐵 ∈ (𝐴𝐼𝑧)) |
| 72 | 1, 2, 3, 16, 61, 62, 63, 64, 65, 66, 67, 69, 71 | tgbtwnxfr 28538 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → 𝑦 ∈ (𝐶𝐼𝐷)) |
| 73 | 1, 2, 3, 16, 61, 62, 64, 63, 65, 67, 66, 68 | cgr3simp3 28530 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → (𝐵 − 𝐴) = (𝑦 − 𝐶)) |
| 74 | 1, 2, 3, 61, 63, 62, 66, 65, 73 | tgcgrcomlr 28488 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → (𝐴 − 𝐵) = (𝐶 − 𝑦)) |
| 75 | 72, 74 | jca 511 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉) → (𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦))) |
| 76 | 75 | ex 412 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) ∧ 𝑦 ∈ 𝑃) → (〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉 → (𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦)))) |
| 77 | 76 | reximdva 3168 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) → (∃𝑦 ∈ 𝑃 〈“𝐴𝑧𝐵”〉(cgrG‘𝐺)〈“𝐶𝐷𝑦”〉 → ∃𝑦 ∈ 𝑃 (𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦)))) |
| 78 | 60, 77 | mpd 15 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) → ∃𝑦 ∈ 𝑃 (𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦))) |
| 79 | 78 | adantllr 719 |
. . . 4
⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷))) ∧ 𝑧 ∈ 𝑃) ∧ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) → ∃𝑦 ∈ 𝑃 (𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦))) |
| 80 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷))) → ∃𝑥 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷))) |
| 81 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝐴𝐼𝑥) = (𝐴𝐼𝑧)) |
| 82 | 81 | eleq2d 2827 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝐵 ∈ (𝐴𝐼𝑥) ↔ 𝐵 ∈ (𝐴𝐼𝑧))) |
| 83 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝐴 − 𝑥) = (𝐴 − 𝑧)) |
| 84 | 83 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝐴 − 𝑥) = (𝐶 − 𝐷) ↔ (𝐴 − 𝑧) = (𝐶 − 𝐷))) |
| 85 | 82, 84 | anbi12d 632 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷)) ↔ (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷)))) |
| 86 | 85 | cbvrexvw 3238 |
. . . . 5
⊢
(∃𝑥 ∈
𝑃 (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷)) ↔ ∃𝑧 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) |
| 87 | 80, 86 | sylib 218 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷))) → ∃𝑧 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑧) ∧ (𝐴 − 𝑧) = (𝐶 − 𝐷))) |
| 88 | 79, 87 | r19.29a 3162 |
. . 3
⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷))) → ∃𝑦 ∈ 𝑃 (𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦))) |
| 89 | 50, 88 | impbida 801 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ 𝑃 (𝑦 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑦)) ↔ ∃𝑥 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷)))) |
| 90 | 10, 89 | bitrd 279 |
1
⊢ (𝜑 → ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ↔ ∃𝑥 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷)))) |