Metamath Proof Explorer

Theorem lnxfr

Description: Transfer law for colinearity. Theorem 4.13 of Schwabhauser p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019)

Ref Expression
Hypotheses tglngval.p 
|- P = ( Base ` G )
tglngval.l 
|- L = ( LineG ` G )
tglngval.i 
|- I = ( Itv ` G )
tglngval.g 
|- ( ph -> G e. TarskiG )
tglngval.x 
|- ( ph -> X e. P )
tglngval.y 
|- ( ph -> Y e. P )
tgcolg.z 
|- ( ph -> Z e. P )
lnxfr.r 
|- .~ = ( cgrG ` G )
lnxfr.a 
|- ( ph -> A e. P )
lnxfr.b 
|- ( ph -> B e. P )
lnxfr.c 
|- ( ph -> C e. P )
lnxfr.1 
|- ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )
lnxfr.2 
|- ( ph -> <" X Y Z "> .~ <" A B C "> )
Assertion lnxfr 
|- ( ph -> ( B e. ( A L C ) \/ A = C ) )

Proof

Step Hyp Ref Expression
1 tglngval.p 
 |-  P = ( Base ` G )
2 tglngval.l 
 |-  L = ( LineG ` G )
3 tglngval.i 
 |-  I = ( Itv ` G )
4 tglngval.g 
 |-  ( ph -> G e. TarskiG )
5 tglngval.x 
 |-  ( ph -> X e. P )
6 tglngval.y 
 |-  ( ph -> Y e. P )
7 tgcolg.z 
 |-  ( ph -> Z e. P )
8 lnxfr.r 
 |-  .~ = ( cgrG ` G )
9 lnxfr.a 
 |-  ( ph -> A e. P )
10 lnxfr.b 
 |-  ( ph -> B e. P )
11 lnxfr.c 
 |-  ( ph -> C e. P )
12 lnxfr.1 
 |-  ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )
13 lnxfr.2 
 |-  ( ph -> <" X Y Z "> .~ <" A B C "> )
14 4 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> G e. TarskiG )
15 9 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> A e. P )
16 11 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> C e. P )
17 10 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> B e. P )
18 eqid 
 |-  ( dist ` G ) = ( dist ` G )
19 5 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> X e. P )
20 6 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Y e. P )
21 7 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Z e. P )
22 13 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> <" X Y Z "> .~ <" A B C "> )
23 simpr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Y e. ( X I Z ) )
24 1 18 3 8 14 19 20 21 15 17 16 22 23 tgbtwnxfr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> B e. ( A I C ) )
25 1 2 3 14 15 16 17 24 btwncolg1 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> ( B e. ( A L C ) \/ A = C ) )
26 4 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> G e. TarskiG )
27 9 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> A e. P )
28 11 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> C e. P )
29 10 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> B e. P )
30 6 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> Y e. P )
31 5 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> X e. P )
32 7 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> Z e. P )
33 13 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> <" X Y Z "> .~ <" A B C "> )
34 1 18 3 8 26 31 30 32 27 29 28 33 cgr3swap12 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> <" Y X Z "> .~ <" B A C "> )
35 simpr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> X e. ( Y I Z ) )
36 1 18 3 8 26 30 31 32 29 27 28 34 35 tgbtwnxfr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> A e. ( B I C ) )
37 1 2 3 26 27 28 29 36 btwncolg2 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> ( B e. ( A L C ) \/ A = C ) )
38 4 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> G e. TarskiG )
39 9 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> A e. P )
40 11 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> C e. P )
41 10 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> B e. P )
42 5 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> X e. P )
43 7 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Z e. P )
44 6 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Y e. P )
45 13 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> <" X Y Z "> .~ <" A B C "> )
46 1 18 3 8 38 42 44 43 39 41 40 45 cgr3swap23 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> <" X Z Y "> .~ <" A C B "> )
47 simpr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Z e. ( X I Y ) )
48 1 18 3 8 38 42 43 44 39 40 41 46 47 tgbtwnxfr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> C e. ( A I B ) )
49 1 2 3 38 39 40 41 48 btwncolg3 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> ( B e. ( A L C ) \/ A = C ) )
50 1 2 3 4 5 7 6 tgcolg 
 |-  ( ph -> ( ( Y e. ( X L Z ) \/ X = Z ) <-> ( Y e. ( X I Z ) \/ X e. ( Y I Z ) \/ Z e. ( X I Y ) ) ) )
51 12 50 mpbid 
 |-  ( ph -> ( Y e. ( X I Z ) \/ X e. ( Y I Z ) \/ Z e. ( X I Y ) ) )
52 25 37 49 51 mpjao3dan 
 |-  ( ph -> ( B e. ( A L C ) \/ A = C ) )