Metamath Proof Explorer

Theorem ncolncol

Description: Deduce non-colinearity from non-colinearity and colinearity. (Contributed by Thierry Arnoux, 27-Aug-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 )
tglineinteq.a 
|- ( ph -> A e. P )
tglineinteq.b 
|- ( ph -> B e. P )
tglineinteq.c 
|- ( ph -> C e. P )
tglineinteq.d 
|- ( ph -> D e. P )
tglineinteq.e 
|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
ncolncol.1 
|- ( ph -> D e. ( A L B ) )
ncolncol.2 
|- ( ph -> D =/= B )
Assertion ncolncol 
|- ( ph -> -. ( D e. ( B L C ) \/ B = 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 tglineinteq.a 
 |-  ( ph -> A e. P )
6 tglineinteq.b 
 |-  ( ph -> B e. P )
7 tglineinteq.c 
 |-  ( ph -> C e. P )
8 tglineinteq.d 
 |-  ( ph -> D e. P )
9 tglineinteq.e 
 |-  ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
10 ncolncol.1 
 |-  ( ph -> D e. ( A L B ) )
11 ncolncol.2 
 |-  ( ph -> D =/= B )
12 4 adantr 
 |-  ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) -> G e. TarskiG )
13 5 adantr 
 |-  ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) -> A e. P )
14 6 adantr 
 |-  ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) -> B e. P )
15 7 adantr 
 |-  ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) -> C e. P )
16 4 ad2antrr 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ C e. ( D L B ) ) -> G e. TarskiG )
17 5 ad2antrr 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ C e. ( D L B ) ) -> A e. P )
18 6 ad2antrr 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ C e. ( D L B ) ) -> B e. P )
19 7 ad2antrr 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ C e. ( D L B ) ) -> C e. P )
20 1 3 2 4 5 6 10 tglngne 
 |-  ( ph -> A =/= B )
21 20 ad2antrr 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ C e. ( D L B ) ) -> A =/= B )
22 8 ad2antrr 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ C e. ( D L B ) ) -> D e. P )
23 11 necomd 
 |-  ( ph -> B =/= D )
24 23 ad2antrr 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ C e. ( D L B ) ) -> B =/= D )
25 simpr 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ C e. ( D L B ) ) -> C e. ( D L B ) )
26 1 2 3 16 18 22 19 24 25 lncom 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ C e. ( D L B ) ) -> C e. ( B L D ) )
27 20 necomd 
 |-  ( ph -> B =/= A )
28 1 2 3 4 6 5 8 27 10 lncom 
 |-  ( ph -> D e. ( B L A ) )
29 1 2 3 4 6 5 27 8 11 28 tglineelsb2 
 |-  ( ph -> ( B L A ) = ( B L D ) )
30 29 ad2antrr 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ C e. ( D L B ) ) -> ( B L A ) = ( B L D ) )
31 26 30 eleqtrrd 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ C e. ( D L B ) ) -> C e. ( B L A ) )
32 1 2 3 16 17 18 19 21 31 lncom 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ C e. ( D L B ) ) -> C e. ( A L B ) )
33 32 orcd 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ C e. ( D L B ) ) -> ( C e. ( A L B ) \/ A = B ) )
34 simpr 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ D = B ) -> D = B )
35 11 ad2antrr 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ D = B ) -> D =/= B )
36 34 35 pm2.21ddne 
 |-  ( ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) /\ D = B ) -> ( C e. ( A L B ) \/ A = B ) )
37 8 adantr 
 |-  ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) -> D e. P )
38 simpr 
 |-  ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) -> ( D e. ( B L C ) \/ B = C ) )
39 1 3 2 12 14 15 37 38 colrot2 
 |-  ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) -> ( C e. ( D L B ) \/ D = B ) )
40 33 36 39 mpjaodan 
 |-  ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) -> ( C e. ( A L B ) \/ A = B ) )
41 1 3 2 12 13 14 15 40 colrot1 
 |-  ( ( ph /\ ( D e. ( B L C ) \/ B = C ) ) -> ( A e. ( B L C ) \/ B = C ) )
42 9 41 mtand 
 |-  ( ph -> -. ( D e. ( B L C ) \/ B = C ) )