Metamath Proof Explorer

Theorem coltr

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 ) )
coltr.2 
|- ( ph -> ( B e. ( C L D ) \/ C = D ) )
Assertion coltr 
|- ( ph -> ( A e. ( C L D ) \/ C = D ) )

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 coltr.2 
 |-  ( ph -> ( B e. ( C L D ) \/ C = D ) )
11 4 adantr 
 |-  ( ( ph /\ C =/= D ) -> G e. TarskiG )
12 7 adantr 
 |-  ( ( ph /\ C =/= D ) -> C e. P )
13 8 adantr 
 |-  ( ( ph /\ C =/= D ) -> D e. P )
14 simpr 
 |-  ( ( ph /\ C =/= D ) -> C =/= D )
15 1 2 3 11 12 13 14 tglinerflx1 
 |-  ( ( ph /\ C =/= D ) -> C e. ( C L D ) )
16 15 ex 
 |-  ( ph -> ( C =/= D -> C e. ( C L D ) ) )
17 16 necon1bd 
 |-  ( ph -> ( -. C e. ( C L D ) -> C = D ) )
18 17 orrd 
 |-  ( ph -> ( C e. ( C L D ) \/ C = D ) )
19 18 adantr 
 |-  ( ( ph /\ A = C ) -> ( C e. ( C L D ) \/ C = D ) )
20 simplr 
 |-  ( ( ( ph /\ A = C ) /\ C e. ( C L D ) ) -> A = C )
21 simpr 
 |-  ( ( ( ph /\ A = C ) /\ C e. ( C L D ) ) -> C e. ( C L D ) )
22 20 21 eqeltrd 
 |-  ( ( ( ph /\ A = C ) /\ C e. ( C L D ) ) -> A e. ( C L D ) )
23 22 ex 
 |-  ( ( ph /\ A = C ) -> ( C e. ( C L D ) -> A e. ( C L D ) ) )
24 23 orim1d 
 |-  ( ( ph /\ A = C ) -> ( ( C e. ( C L D ) \/ C = D ) -> ( A e. ( C L D ) \/ C = D ) ) )
25 19 24 mpd 
 |-  ( ( ph /\ A = C ) -> ( A e. ( C L D ) \/ C = D ) )
26 10 ad2antrr 
 |-  ( ( ( ph /\ A =/= C ) /\ -. ( A e. ( C L D ) \/ C = D ) ) -> ( B e. ( C L D ) \/ C = D ) )
27 4 ad2antrr 
 |-  ( ( ( ph /\ A =/= C ) /\ -. ( A e. ( C L D ) \/ C = D ) ) -> G e. TarskiG )
28 5 ad2antrr 
 |-  ( ( ( ph /\ A =/= C ) /\ -. ( A e. ( C L D ) \/ C = D ) ) -> A e. P )
29 7 ad2antrr 
 |-  ( ( ( ph /\ A =/= C ) /\ -. ( A e. ( C L D ) \/ C = D ) ) -> C e. P )
30 8 ad2antrr 
 |-  ( ( ( ph /\ A =/= C ) /\ -. ( A e. ( C L D ) \/ C = D ) ) -> D e. P )
31 6 ad2antrr 
 |-  ( ( ( ph /\ A =/= C ) /\ -. ( A e. ( C L D ) \/ C = D ) ) -> B e. P )
32 simpr 
 |-  ( ( ( ph /\ A =/= C ) /\ -. ( A e. ( C L D ) \/ C = D ) ) -> -. ( A e. ( C L D ) \/ C = D ) )
33 4 adantr 
 |-  ( ( ph /\ A =/= C ) -> G e. TarskiG )
34 5 adantr 
 |-  ( ( ph /\ A =/= C ) -> A e. P )
35 7 adantr 
 |-  ( ( ph /\ A =/= C ) -> C e. P )
36 6 adantr 
 |-  ( ( ph /\ A =/= C ) -> B e. P )
37 simpr 
 |-  ( ( ph /\ A =/= C ) -> A =/= C )
38 9 adantr 
 |-  ( ( ph /\ A =/= C ) -> A e. ( B L C ) )
39 1 3 2 33 36 35 38 tglngne 
 |-  ( ( ph /\ A =/= C ) -> B =/= C )
40 39 necomd 
 |-  ( ( ph /\ A =/= C ) -> C =/= B )
41 1 2 3 33 35 36 34 40 38 lncom 
 |-  ( ( ph /\ A =/= C ) -> A e. ( C L B ) )
42 1 2 3 33 34 35 36 37 41 40 lnrot2 
 |-  ( ( ph /\ A =/= C ) -> B e. ( A L C ) )
43 42 adantr 
 |-  ( ( ( ph /\ A =/= C ) /\ -. ( A e. ( C L D ) \/ C = D ) ) -> B e. ( A L C ) )
44 1 3 2 4 6 7 9 tglngne 
 |-  ( ph -> B =/= C )
45 44 ad2antrr 
 |-  ( ( ( ph /\ A =/= C ) /\ -. ( A e. ( C L D ) \/ C = D ) ) -> B =/= C )
46 1 2 3 27 28 29 30 31 32 43 45 ncolncol 
 |-  ( ( ( ph /\ A =/= C ) /\ -. ( A e. ( C L D ) \/ C = D ) ) -> -. ( B e. ( C L D ) \/ C = D ) )
47 26 46 condan 
 |-  ( ( ph /\ A =/= C ) -> ( A e. ( C L D ) \/ C = D ) )
48 25 47 pm2.61dane 
 |-  ( ph -> ( A e. ( C L D ) \/ C = D ) )