Metamath Proof Explorer

Theorem colmid

Description: Colinearity and equidistance implies midpoint. Theorem 7.20 of Schwabhauser p. 52. (Contributed by Thierry Arnoux, 30-Jul-2019)

Ref Expression
Hypotheses mirval.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
mirval.d
mirval.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
mirval.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
mirval.s ${⊢}{S}={pInv}_{𝒢}\left({G}\right)$
mirval.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
colmid.m ${⊢}{M}={S}\left({X}\right)$
colmid.a ${⊢}{\phi }\to {A}\in {P}$
colmid.b ${⊢}{\phi }\to {B}\in {P}$
colmid.x ${⊢}{\phi }\to {X}\in {P}$
colmid.c ${⊢}{\phi }\to \left({X}\in \left({A}{L}{B}\right)\vee {A}={B}\right)$
colmid.d
Assertion colmid ${⊢}{\phi }\to \left({B}={M}\left({A}\right)\vee {A}={B}\right)$

Proof

Step Hyp Ref Expression
1 mirval.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
2 mirval.d
3 mirval.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
4 mirval.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
5 mirval.s ${⊢}{S}={pInv}_{𝒢}\left({G}\right)$
6 mirval.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
7 colmid.m ${⊢}{M}={S}\left({X}\right)$
8 colmid.a ${⊢}{\phi }\to {A}\in {P}$
9 colmid.b ${⊢}{\phi }\to {B}\in {P}$
10 colmid.x ${⊢}{\phi }\to {X}\in {P}$
11 colmid.c ${⊢}{\phi }\to \left({X}\in \left({A}{L}{B}\right)\vee {A}={B}\right)$
12 colmid.d
13 animorr ${⊢}\left({\phi }\wedge {A}={B}\right)\to \left({B}={M}\left({A}\right)\vee {A}={B}\right)$
14 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {A}\ne {B}\right)\wedge {X}\in \left({A}{I}{B}\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
15 10 ad2antrr ${⊢}\left(\left({\phi }\wedge {A}\ne {B}\right)\wedge {X}\in \left({A}{I}{B}\right)\right)\to {X}\in {P}$
16 8 ad2antrr ${⊢}\left(\left({\phi }\wedge {A}\ne {B}\right)\wedge {X}\in \left({A}{I}{B}\right)\right)\to {A}\in {P}$
17 9 ad2antrr ${⊢}\left(\left({\phi }\wedge {A}\ne {B}\right)\wedge {X}\in \left({A}{I}{B}\right)\right)\to {B}\in {P}$
19 18 eqcomd
20 simpr ${⊢}\left(\left({\phi }\wedge {A}\ne {B}\right)\wedge {X}\in \left({A}{I}{B}\right)\right)\to {X}\in \left({A}{I}{B}\right)$
21 1 2 3 14 16 15 17 20 tgbtwncom ${⊢}\left(\left({\phi }\wedge {A}\ne {B}\right)\wedge {X}\in \left({A}{I}{B}\right)\right)\to {X}\in \left({B}{I}{A}\right)$
22 1 2 3 4 5 14 15 7 16 17 19 21 ismir ${⊢}\left(\left({\phi }\wedge {A}\ne {B}\right)\wedge {X}\in \left({A}{I}{B}\right)\right)\to {B}={M}\left({A}\right)$
23 22 orcd ${⊢}\left(\left({\phi }\wedge {A}\ne {B}\right)\wedge {X}\in \left({A}{I}{B}\right)\right)\to \left({B}={M}\left({A}\right)\vee {A}={B}\right)$
24 6 adantr ${⊢}\left({\phi }\wedge {A}\in \left({X}{I}{B}\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
25 9 adantr ${⊢}\left({\phi }\wedge {A}\in \left({X}{I}{B}\right)\right)\to {B}\in {P}$
26 8 adantr ${⊢}\left({\phi }\wedge {A}\in \left({X}{I}{B}\right)\right)\to {A}\in {P}$
27 10 adantr ${⊢}\left({\phi }\wedge {A}\in \left({X}{I}{B}\right)\right)\to {X}\in {P}$
28 simpr ${⊢}\left({\phi }\wedge {A}\in \left({X}{I}{B}\right)\right)\to {A}\in \left({X}{I}{B}\right)$
29 1 2 3 24 27 26 25 28 tgbtwncom ${⊢}\left({\phi }\wedge {A}\in \left({X}{I}{B}\right)\right)\to {A}\in \left({B}{I}{X}\right)$
30 1 2 3 24 26 27 tgbtwntriv1 ${⊢}\left({\phi }\wedge {A}\in \left({X}{I}{B}\right)\right)\to {A}\in \left({A}{I}{X}\right)$
31 1 2 3 6 10 8 10 9 12 tgcgrcomlr
33 32 eqcomd
34 eqidd
35 1 2 3 24 25 26 27 26 26 27 29 30 33 34 tgcgrsub
36 1 2 3 24 25 26 26 35 axtgcgrid ${⊢}\left({\phi }\wedge {A}\in \left({X}{I}{B}\right)\right)\to {B}={A}$
37 36 eqcomd ${⊢}\left({\phi }\wedge {A}\in \left({X}{I}{B}\right)\right)\to {A}={B}$
38 37 adantlr ${⊢}\left(\left({\phi }\wedge {A}\ne {B}\right)\wedge {A}\in \left({X}{I}{B}\right)\right)\to {A}={B}$
39 38 olcd ${⊢}\left(\left({\phi }\wedge {A}\ne {B}\right)\wedge {A}\in \left({X}{I}{B}\right)\right)\to \left({B}={M}\left({A}\right)\vee {A}={B}\right)$
40 6 adantr ${⊢}\left({\phi }\wedge {B}\in \left({A}{I}{X}\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
41 8 adantr ${⊢}\left({\phi }\wedge {B}\in \left({A}{I}{X}\right)\right)\to {A}\in {P}$
42 9 adantr ${⊢}\left({\phi }\wedge {B}\in \left({A}{I}{X}\right)\right)\to {B}\in {P}$
43 10 adantr ${⊢}\left({\phi }\wedge {B}\in \left({A}{I}{X}\right)\right)\to {X}\in {P}$
44 simpr ${⊢}\left({\phi }\wedge {B}\in \left({A}{I}{X}\right)\right)\to {B}\in \left({A}{I}{X}\right)$
45 1 2 3 40 42 43 tgbtwntriv1 ${⊢}\left({\phi }\wedge {B}\in \left({A}{I}{X}\right)\right)\to {B}\in \left({B}{I}{X}\right)$
47 eqidd
48 1 2 3 40 41 42 43 42 42 43 44 45 46 47 tgcgrsub
49 1 2 3 40 41 42 42 48 axtgcgrid ${⊢}\left({\phi }\wedge {B}\in \left({A}{I}{X}\right)\right)\to {A}={B}$
50 49 adantlr ${⊢}\left(\left({\phi }\wedge {A}\ne {B}\right)\wedge {B}\in \left({A}{I}{X}\right)\right)\to {A}={B}$
51 50 olcd ${⊢}\left(\left({\phi }\wedge {A}\ne {B}\right)\wedge {B}\in \left({A}{I}{X}\right)\right)\to \left({B}={M}\left({A}\right)\vee {A}={B}\right)$
52 df-ne ${⊢}{A}\ne {B}↔¬{A}={B}$
53 11 orcomd ${⊢}{\phi }\to \left({A}={B}\vee {X}\in \left({A}{L}{B}\right)\right)$
54 53 orcanai ${⊢}\left({\phi }\wedge ¬{A}={B}\right)\to {X}\in \left({A}{L}{B}\right)$
55 52 54 sylan2b ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {X}\in \left({A}{L}{B}\right)$
56 6 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
57 8 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {A}\in {P}$
58 9 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {B}\in {P}$
59 simpr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {A}\ne {B}$
60 10 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {X}\in {P}$
61 1 4 3 56 57 58 59 60 tgellng ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to \left({X}\in \left({A}{L}{B}\right)↔\left({X}\in \left({A}{I}{B}\right)\vee {A}\in \left({X}{I}{B}\right)\vee {B}\in \left({A}{I}{X}\right)\right)\right)$
62 55 61 mpbid ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to \left({X}\in \left({A}{I}{B}\right)\vee {A}\in \left({X}{I}{B}\right)\vee {B}\in \left({A}{I}{X}\right)\right)$
63 23 39 51 62 mpjao3dan ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to \left({B}={M}\left({A}\right)\vee {A}={B}\right)$
64 13 63 pm2.61dane ${⊢}{\phi }\to \left({B}={M}\left({A}\right)\vee {A}={B}\right)$