Proof of Theorem colmid
| Step | Hyp | Ref
| Expression |
| 1 | | animorr 981 |
. 2
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐵 = (𝑀‘𝐴) ∨ 𝐴 = 𝐵)) |
| 2 | | mirval.p |
. . . . 5
⊢ 𝑃 = (Base‘𝐺) |
| 3 | | mirval.d |
. . . . 5
⊢ − =
(dist‘𝐺) |
| 4 | | mirval.i |
. . . . 5
⊢ 𝐼 = (Itv‘𝐺) |
| 5 | | mirval.l |
. . . . 5
⊢ 𝐿 = (LineG‘𝐺) |
| 6 | | mirval.s |
. . . . 5
⊢ 𝑆 = (pInvG‘𝐺) |
| 7 | | mirval.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 8 | 7 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → 𝐺 ∈ TarskiG) |
| 9 | | colmid.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
| 10 | 9 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → 𝑋 ∈ 𝑃) |
| 11 | | colmid.m |
. . . . 5
⊢ 𝑀 = (𝑆‘𝑋) |
| 12 | | colmid.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 13 | 12 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → 𝐴 ∈ 𝑃) |
| 14 | | colmid.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| 15 | 14 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → 𝐵 ∈ 𝑃) |
| 16 | | colmid.d |
. . . . . . 7
⊢ (𝜑 → (𝑋 − 𝐴) = (𝑋 − 𝐵)) |
| 17 | 16 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → (𝑋 − 𝐴) = (𝑋 − 𝐵)) |
| 18 | 17 | eqcomd 2743 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → (𝑋 − 𝐵) = (𝑋 − 𝐴)) |
| 19 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → 𝑋 ∈ (𝐴𝐼𝐵)) |
| 20 | 2, 3, 4, 8, 13, 10, 15, 19 | tgbtwncom 28496 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → 𝑋 ∈ (𝐵𝐼𝐴)) |
| 21 | 2, 3, 4, 5, 6, 8, 10, 11, 13, 15, 18, 20 | ismir 28667 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → 𝐵 = (𝑀‘𝐴)) |
| 22 | 21 | orcd 874 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → (𝐵 = (𝑀‘𝐴) ∨ 𝐴 = 𝐵)) |
| 23 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐺 ∈ TarskiG) |
| 24 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐵 ∈ 𝑃) |
| 25 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐴 ∈ 𝑃) |
| 26 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝑋 ∈ 𝑃) |
| 27 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐴 ∈ (𝑋𝐼𝐵)) |
| 28 | 2, 3, 4, 23, 26, 25, 24, 27 | tgbtwncom 28496 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐴 ∈ (𝐵𝐼𝑋)) |
| 29 | 2, 3, 4, 23, 25, 26 | tgbtwntriv1 28499 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐴 ∈ (𝐴𝐼𝑋)) |
| 30 | 2, 3, 4, 7, 9, 12,
9, 14, 16 | tgcgrcomlr 28488 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 − 𝑋) = (𝐵 − 𝑋)) |
| 31 | 30 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → (𝐴 − 𝑋) = (𝐵 − 𝑋)) |
| 32 | 31 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → (𝐵 − 𝑋) = (𝐴 − 𝑋)) |
| 33 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → (𝐴 − 𝑋) = (𝐴 − 𝑋)) |
| 34 | 2, 3, 4, 23, 24, 25, 26, 25, 25, 26, 28, 29, 32, 33 | tgcgrsub 28517 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → (𝐵 − 𝐴) = (𝐴 − 𝐴)) |
| 35 | 2, 3, 4, 23, 24, 25, 25, 34 | axtgcgrid 28471 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐵 = 𝐴) |
| 36 | 35 | eqcomd 2743 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐴 = 𝐵) |
| 37 | 36 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐴 = 𝐵) |
| 38 | 37 | olcd 875 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → (𝐵 = (𝑀‘𝐴) ∨ 𝐴 = 𝐵)) |
| 39 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝐺 ∈ TarskiG) |
| 40 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝐴 ∈ 𝑃) |
| 41 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝐵 ∈ 𝑃) |
| 42 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝑋 ∈ 𝑃) |
| 43 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝐵 ∈ (𝐴𝐼𝑋)) |
| 44 | 2, 3, 4, 39, 41, 42 | tgbtwntriv1 28499 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝐵 ∈ (𝐵𝐼𝑋)) |
| 45 | 30 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → (𝐴 − 𝑋) = (𝐵 − 𝑋)) |
| 46 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → (𝐵 − 𝑋) = (𝐵 − 𝑋)) |
| 47 | 2, 3, 4, 39, 40, 41, 42, 41, 41, 42, 43, 44, 45, 46 | tgcgrsub 28517 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → (𝐴 − 𝐵) = (𝐵 − 𝐵)) |
| 48 | 2, 3, 4, 39, 40, 41, 41, 47 | axtgcgrid 28471 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝐴 = 𝐵) |
| 49 | 48 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝐴 = 𝐵) |
| 50 | 49 | olcd 875 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → (𝐵 = (𝑀‘𝐴) ∨ 𝐴 = 𝐵)) |
| 51 | | df-ne 2941 |
. . . . 5
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) |
| 52 | | colmid.c |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) |
| 53 | 52 | orcomd 872 |
. . . . . 6
⊢ (𝜑 → (𝐴 = 𝐵 ∨ 𝑋 ∈ (𝐴𝐿𝐵))) |
| 54 | 53 | orcanai 1005 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 = 𝐵) → 𝑋 ∈ (𝐴𝐿𝐵)) |
| 55 | 51, 54 | sylan2b 594 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝑋 ∈ (𝐴𝐿𝐵)) |
| 56 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ TarskiG) |
| 57 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝑃) |
| 58 | 14 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝑃) |
| 59 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐴 ≠ 𝐵) |
| 60 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝑋 ∈ 𝑃) |
| 61 | 2, 5, 4, 56, 57, 58, 59, 60 | tgellng 28561 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝑋 ∈ (𝐴𝐿𝐵) ↔ (𝑋 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝑋𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝑋)))) |
| 62 | 55, 61 | mpbid 232 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝑋 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝑋𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝑋))) |
| 63 | 22, 38, 50, 62 | mpjao3dan 1434 |
. 2
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐵 = (𝑀‘𝐴) ∨ 𝐴 = 𝐵)) |
| 64 | 1, 63 | pm2.61dane 3029 |
1
⊢ (𝜑 → (𝐵 = (𝑀‘𝐴) ∨ 𝐴 = 𝐵)) |