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 = ( Base ` G )
mirval.d 
|- .- = ( dist ` G )
mirval.i 
|- I = ( Itv ` G )
mirval.l 
|- L = ( LineG ` G )
mirval.s 
|- S = ( pInvG ` G )
mirval.g 
|- ( ph -> G e. TarskiG )
colmid.m 
|- M = ( S ` X )
colmid.a 
|- ( ph -> A e. P )
colmid.b 
|- ( ph -> B e. P )
colmid.x 
|- ( ph -> X e. P )
colmid.c 
|- ( ph -> ( X e. ( A L B ) \/ A = B ) )
colmid.d 
|- ( ph -> ( X .- A ) = ( X .- B ) )
Assertion colmid 
|- ( ph -> ( B = ( M ` A ) \/ A = B ) )

Proof

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