Metamath Proof Explorer

Theorem coltr3

Description: A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019)

Ref Expression
Hypotheses tglineintmo.p 
|- P = ( Base ` G )
tglineintmo.i 
|- I = ( Itv ` G )
tglineintmo.l 
|- L = ( LineG ` G )
tglineintmo.g 
|- ( ph -> G e. TarskiG )
coltr.a 
|- ( ph -> A e. P )
coltr.b 
|- ( ph -> B e. P )
coltr.c 
|- ( ph -> C e. P )
coltr.d 
|- ( ph -> D e. P )
coltr.1 
|- ( ph -> A e. ( B L C ) )
coltr3.2 
|- ( ph -> D e. ( A I C ) )
Assertion coltr3 
|- ( ph -> D e. ( B L C ) )

Proof

Step Hyp Ref Expression
1 tglineintmo.p 
 |-  P = ( Base ` G )
2 tglineintmo.i 
 |-  I = ( Itv ` G )
3 tglineintmo.l 
 |-  L = ( LineG ` G )
4 tglineintmo.g 
 |-  ( ph -> G e. TarskiG )
5 coltr.a 
 |-  ( ph -> A e. P )
6 coltr.b 
 |-  ( ph -> B e. P )
7 coltr.c 
 |-  ( ph -> C e. P )
8 coltr.d 
 |-  ( ph -> D e. P )
9 coltr.1 
 |-  ( ph -> A e. ( B L C ) )
10 coltr3.2 
 |-  ( ph -> D e. ( A I C ) )
11 eqid 
 |-  ( dist ` G ) = ( dist ` G )
12 4 adantr 
 |-  ( ( ph /\ A = C ) -> G e. TarskiG )
13 5 adantr 
 |-  ( ( ph /\ A = C ) -> A e. P )
14 8 adantr 
 |-  ( ( ph /\ A = C ) -> D e. P )
15 10 adantr 
 |-  ( ( ph /\ A = C ) -> D e. ( A I C ) )
16 simpr 
 |-  ( ( ph /\ A = C ) -> A = C )
17 16 oveq2d 
 |-  ( ( ph /\ A = C ) -> ( A I A ) = ( A I C ) )
18 15 17 eleqtrrd 
 |-  ( ( ph /\ A = C ) -> D e. ( A I A ) )
19 1 11 2 12 13 14 18 axtgbtwnid 
 |-  ( ( ph /\ A = C ) -> A = D )
20 9 adantr 
 |-  ( ( ph /\ A = C ) -> A e. ( B L C ) )
21 19 20 eqeltrrd 
 |-  ( ( ph /\ A = C ) -> D e. ( B L C ) )
22 4 adantr 
 |-  ( ( ph /\ A =/= C ) -> G e. TarskiG )
23 5 adantr 
 |-  ( ( ph /\ A =/= C ) -> A e. P )
24 7 adantr 
 |-  ( ( ph /\ A =/= C ) -> C e. P )
25 8 adantr 
 |-  ( ( ph /\ A =/= C ) -> D e. P )
26 simpr 
 |-  ( ( ph /\ A =/= C ) -> A =/= C )
27 10 adantr 
 |-  ( ( ph /\ A =/= C ) -> D e. ( A I C ) )
28 1 2 3 22 23 24 25 26 27 btwnlng1 
 |-  ( ( ph /\ A =/= C ) -> D e. ( A L C ) )
29 26 necomd 
 |-  ( ( ph /\ A =/= C ) -> C =/= A )
30 6 adantr 
 |-  ( ( ph /\ A =/= C ) -> B e. P )
31 1 3 2 4 6 7 9 tglngne 
 |-  ( ph -> B =/= C )
32 31 adantr 
 |-  ( ( ph /\ A =/= C ) -> B =/= C )
33 9 adantr 
 |-  ( ( ph /\ A =/= C ) -> A e. ( B L C ) )
34 1 2 3 22 24 23 30 29 33 32 lnrot1 
 |-  ( ( ph /\ A =/= C ) -> B e. ( C L A ) )
35 1 2 3 22 24 23 29 30 32 34 tglineelsb2 
 |-  ( ( ph /\ A =/= C ) -> ( C L A ) = ( C L B ) )
36 1 2 3 22 23 24 26 tglinecom 
 |-  ( ( ph /\ A =/= C ) -> ( A L C ) = ( C L A ) )
37 1 2 3 4 6 7 31 tglinecom 
 |-  ( ph -> ( B L C ) = ( C L B ) )
38 37 adantr 
 |-  ( ( ph /\ A =/= C ) -> ( B L C ) = ( C L B ) )
39 35 36 38 3eqtr4d 
 |-  ( ( ph /\ A =/= C ) -> ( A L C ) = ( B L C ) )
40 28 39 eleqtrd 
 |-  ( ( ph /\ A =/= C ) -> D e. ( B L C ) )
41 21 40 pm2.61dane 
 |-  ( ph -> D e. ( B L C ) )