| Step | Hyp | Ref
| Expression |
| 1 | | symquadlem.1 |
. . . . . . . 8
⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) |
| 2 | | mirval.p |
. . . . . . . . . . 11
⊢ 𝑃 = (Base‘𝐺) |
| 3 | | mirval.l |
. . . . . . . . . . 11
⊢ 𝐿 = (LineG‘𝐺) |
| 4 | | mirval.i |
. . . . . . . . . . 11
⊢ 𝐼 = (Itv‘𝐺) |
| 5 | | mirval.g |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 6 | | symquadlem.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| 7 | | symquadlem.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 8 | | mirval.d |
. . . . . . . . . . . 12
⊢ − =
(dist‘𝐺) |
| 9 | 2, 8, 4, 5, 6, 7 | tgbtwntriv2 28495 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ (𝐵𝐼𝐴)) |
| 10 | 2, 3, 4, 5, 6, 7, 7, 9 | btwncolg1 28563 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) |
| 11 | 10 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 = 𝐶) → (𝐴 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) |
| 12 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 = 𝐶) → 𝐴 = 𝐶) |
| 13 | 12 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 = 𝐶) → (𝐵𝐿𝐴) = (𝐵𝐿𝐶)) |
| 14 | 13 | eleq2d 2827 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 = 𝐶) → (𝐴 ∈ (𝐵𝐿𝐴) ↔ 𝐴 ∈ (𝐵𝐿𝐶))) |
| 15 | 12 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 = 𝐶) → (𝐵 = 𝐴 ↔ 𝐵 = 𝐶)) |
| 16 | 14, 15 | orbi12d 919 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 = 𝐶) → ((𝐴 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴) ↔ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))) |
| 17 | 11, 16 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 = 𝐶) → (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) |
| 18 | 1, 17 | mtand 816 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝐴 = 𝐶) |
| 19 | 18 | neqned 2947 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 𝐶) |
| 20 | 19 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝐴 ≠ 𝐶) |
| 21 | 20 | necomd 2996 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝐶 ≠ 𝐴) |
| 22 | 21 | neneqd 2945 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → ¬ 𝐶 = 𝐴) |
| 23 | | mirval.s |
. . . . . 6
⊢ 𝑆 = (pInvG‘𝐺) |
| 24 | 5 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝐺 ∈ TarskiG) |
| 25 | | symquadlem.m |
. . . . . 6
⊢ 𝑀 = (𝑆‘𝑋) |
| 26 | | symquadlem.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
| 27 | 26 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝐶 ∈ 𝑃) |
| 28 | 7 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝐴 ∈ 𝑃) |
| 29 | | symquadlem.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
| 30 | 29 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝑋 ∈ 𝑃) |
| 31 | | symquadlem.5 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶)) |
| 32 | 31 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝑋 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶)) |
| 33 | 2, 3, 4, 24, 28, 27, 30, 32 | colcom 28566 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝑋 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴)) |
| 34 | 6 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝐵 ∈ 𝑃) |
| 35 | | symquadlem.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
| 36 | 35 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝐷 ∈ 𝑃) |
| 37 | | eqid 2737 |
. . . . . . . 8
⊢
(cgrG‘𝐺) =
(cgrG‘𝐺) |
| 38 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝑥 ∈ 𝑃) |
| 39 | | symquadlem.6 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ∈ (𝐵𝐿𝐷) ∨ 𝐵 = 𝐷)) |
| 40 | 2, 3, 4, 5, 6, 35,
29, 39 | colrot2 28568 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷 ∈ (𝑋𝐿𝐵) ∨ 𝑋 = 𝐵)) |
| 41 | 2, 3, 4, 5, 29, 6,
35, 40 | colcom 28566 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷 ∈ (𝐵𝐿𝑋) ∨ 𝐵 = 𝑋)) |
| 42 | 41 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝐷 ∈ (𝐵𝐿𝑋) ∨ 𝐵 = 𝑋)) |
| 43 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) |
| 44 | | symquadlem.4 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 − 𝐶) = (𝐷 − 𝐴)) |
| 45 | 44 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝐵 − 𝐶) = (𝐷 − 𝐴)) |
| 46 | | symquadlem.3 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) |
| 47 | 2, 8, 4, 5, 7, 6, 26, 35, 46 | tgcgrcomlr 28488 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) = (𝐷 − 𝐶)) |
| 48 | 47 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝐵 − 𝐴) = (𝐷 − 𝐶)) |
| 49 | 48 | eqcomd 2743 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝐷 − 𝐶) = (𝐵 − 𝐴)) |
| 50 | | symquadlem.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ≠ 𝐷) |
| 51 | 50 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝐵 ≠ 𝐷) |
| 52 | 2, 3, 4, 24, 34, 36, 30, 37, 36, 34, 8, 27, 38, 28, 42, 43, 45, 49, 51 | tgfscgr 28576 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝑋 − 𝐶) = (𝑥 − 𝐴)) |
| 53 | 2, 3, 4, 5, 6, 26,
7, 1 | ncolcom 28569 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵)) |
| 54 | 53 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → ¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵)) |
| 55 | 31 | orcomd 872 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 = 𝐶 ∨ 𝑋 ∈ (𝐴𝐿𝐶))) |
| 56 | 55 | ord 865 |
. . . . . . . . . . 11
⊢ (𝜑 → (¬ 𝐴 = 𝐶 → 𝑋 ∈ (𝐴𝐿𝐶))) |
| 57 | 18, 56 | mpd 15 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝐴𝐿𝐶)) |
| 58 | 57 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝑋 ∈ (𝐴𝐿𝐶)) |
| 59 | 18 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → ¬ 𝐴 = 𝐶) |
| 60 | 45 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝐷 − 𝐴) = (𝐵 − 𝐶)) |
| 61 | 2, 3, 4, 24, 34, 36, 30, 37, 36, 34, 8, 28, 38, 27, 42, 43, 48, 60, 51 | tgfscgr 28576 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝑋 − 𝐴) = (𝑥 − 𝐶)) |
| 62 | 2, 8, 4, 24, 30, 28, 38, 27, 61 | tgcgrcomlr 28488 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝐴 − 𝑋) = (𝐶 − 𝑥)) |
| 63 | 2, 8, 4, 24, 27, 28 | axtgcgrrflx 28470 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝐶 − 𝐴) = (𝐴 − 𝐶)) |
| 64 | 2, 8, 37, 24, 28, 30, 27, 27, 38, 28, 62, 52, 63 | trgcgr 28524 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 〈“𝐴𝑋𝐶”〉(cgrG‘𝐺)〈“𝐶𝑥𝐴”〉) |
| 65 | 2, 3, 4, 24, 28, 30, 27, 37, 27, 38, 28, 32, 64 | lnxfr 28574 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝑥 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴)) |
| 66 | 2, 3, 4, 24, 27, 28, 38, 65 | colcom 28566 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝑥 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶)) |
| 67 | 66 | orcomd 872 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝐴 = 𝐶 ∨ 𝑥 ∈ (𝐴𝐿𝐶))) |
| 68 | 67 | ord 865 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (¬ 𝐴 = 𝐶 → 𝑥 ∈ (𝐴𝐿𝐶))) |
| 69 | 59, 68 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝑥 ∈ (𝐴𝐿𝐶)) |
| 70 | 50 | neneqd 2945 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝐵 = 𝐷) |
| 71 | 39 | orcomd 872 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 = 𝐷 ∨ 𝑋 ∈ (𝐵𝐿𝐷))) |
| 72 | 71 | ord 865 |
. . . . . . . . . . 11
⊢ (𝜑 → (¬ 𝐵 = 𝐷 → 𝑋 ∈ (𝐵𝐿𝐷))) |
| 73 | 70, 72 | mpd 15 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝐵𝐿𝐷)) |
| 74 | 73 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝑋 ∈ (𝐵𝐿𝐷)) |
| 75 | 70 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → ¬ 𝐵 = 𝐷) |
| 76 | 39 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝑋 ∈ (𝐵𝐿𝐷) ∨ 𝐵 = 𝐷)) |
| 77 | 2, 8, 4, 37, 24, 34, 36, 30, 36, 34, 38, 43 | cgr3swap23 28532 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 〈“𝐵𝑋𝐷”〉(cgrG‘𝐺)〈“𝐷𝑥𝐵”〉) |
| 78 | 2, 3, 4, 24, 34, 30, 36, 37, 36, 38, 34, 76, 77 | lnxfr 28574 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝑥 ∈ (𝐷𝐿𝐵) ∨ 𝐷 = 𝐵)) |
| 79 | 2, 3, 4, 24, 36, 34, 38, 78 | colcom 28566 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝑥 ∈ (𝐵𝐿𝐷) ∨ 𝐵 = 𝐷)) |
| 80 | 79 | orcomd 872 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝐵 = 𝐷 ∨ 𝑥 ∈ (𝐵𝐿𝐷))) |
| 81 | 80 | ord 865 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (¬ 𝐵 = 𝐷 → 𝑥 ∈ (𝐵𝐿𝐷))) |
| 82 | 75, 81 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝑥 ∈ (𝐵𝐿𝐷)) |
| 83 | 2, 4, 3, 24, 28, 27, 34, 36, 54, 58, 69, 74, 82 | tglineinteq 28653 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝑋 = 𝑥) |
| 84 | 83 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝑋 − 𝐴) = (𝑥 − 𝐴)) |
| 85 | 52, 84 | eqtr4d 2780 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝑋 − 𝐶) = (𝑋 − 𝐴)) |
| 86 | 2, 8, 4, 3, 23, 24, 25, 27, 28, 30, 33, 85 | colmid 28696 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝐴 = (𝑀‘𝐶) ∨ 𝐶 = 𝐴)) |
| 87 | 86 | orcomd 872 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (𝐶 = 𝐴 ∨ 𝐴 = (𝑀‘𝐶))) |
| 88 | 87 | ord 865 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → (¬ 𝐶 = 𝐴 → 𝐴 = (𝑀‘𝐶))) |
| 89 | 22, 88 | mpd 15 |
. 2
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) → 𝐴 = (𝑀‘𝐶)) |
| 90 | 2, 8, 4, 5, 6, 35 | axtgcgrrflx 28470 |
. . 3
⊢ (𝜑 → (𝐵 − 𝐷) = (𝐷 − 𝐵)) |
| 91 | 2, 3, 4, 5, 6, 35,
29, 37, 35, 6, 8, 41, 90 | lnext 28575 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ 𝑃 〈“𝐵𝐷𝑋”〉(cgrG‘𝐺)〈“𝐷𝐵𝑥”〉) |
| 92 | 89, 91 | r19.29a 3162 |
1
⊢ (𝜑 → 𝐴 = (𝑀‘𝐶)) |