Metamath Proof Explorer

Theorem tglineneq

Description: Given three non-colinear points, build two different lines. (Contributed by Thierry Arnoux, 6-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 ) )
Assertion tglineneq 
|- ( ph -> ( A L B ) =/= ( C L 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 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 1 2 3 4 5 6 7 9 ncolne1 
 |-  ( ph -> A =/= B )
11 1 2 3 4 5 6 10 tglinerflx1 
 |-  ( ph -> A e. ( A L B ) )
12 simplr 
 |-  ( ( ( ph /\ C = D ) /\ A e. ( C L D ) ) -> C = D )
13 4 adantr 
 |-  ( ( ph /\ A e. ( C L D ) ) -> G e. TarskiG )
14 7 adantr 
 |-  ( ( ph /\ A e. ( C L D ) ) -> C e. P )
15 8 adantr 
 |-  ( ( ph /\ A e. ( C L D ) ) -> D e. P )
16 simpr 
 |-  ( ( ph /\ A e. ( C L D ) ) -> A e. ( C L D ) )
17 1 3 2 13 14 15 16 tglngne 
 |-  ( ( ph /\ A e. ( C L D ) ) -> C =/= D )
18 17 adantlr 
 |-  ( ( ( ph /\ C = D ) /\ A e. ( C L D ) ) -> C =/= D )
19 18 neneqd 
 |-  ( ( ( ph /\ C = D ) /\ A e. ( C L D ) ) -> -. C = D )
20 12 19 pm2.65da 
 |-  ( ( ph /\ C = D ) -> -. A e. ( C L D ) )
21 nelne1 
 |-  ( ( A e. ( A L B ) /\ -. A e. ( C L D ) ) -> ( A L B ) =/= ( C L D ) )
22 11 20 21 syl2an2r 
 |-  ( ( ph /\ C = D ) -> ( A L B ) =/= ( C L D ) )
23 4 ad2antrr 
 |-  ( ( ( ph /\ C =/= D ) /\ ( A L B ) = ( C L D ) ) -> G e. TarskiG )
24 6 ad2antrr 
 |-  ( ( ( ph /\ C =/= D ) /\ ( A L B ) = ( C L D ) ) -> B e. P )
25 7 ad2antrr 
 |-  ( ( ( ph /\ C =/= D ) /\ ( A L B ) = ( C L D ) ) -> C e. P )
26 5 ad2antrr 
 |-  ( ( ( ph /\ C =/= D ) /\ ( A L B ) = ( C L D ) ) -> A e. P )
27 pm2.46 
 |-  ( -. ( A e. ( B L C ) \/ B = C ) -> -. B = C )
28 9 27 syl 
 |-  ( ph -> -. B = C )
29 28 neqned 
 |-  ( ph -> B =/= C )
30 29 ad2antrr 
 |-  ( ( ( ph /\ C =/= D ) /\ ( A L B ) = ( C L D ) ) -> B =/= C )
31 8 ad2antrr 
 |-  ( ( ( ph /\ C =/= D ) /\ ( A L B ) = ( C L D ) ) -> D e. P )
32 simplr 
 |-  ( ( ( ph /\ C =/= D ) /\ ( A L B ) = ( C L D ) ) -> C =/= D )
33 1 2 3 23 25 31 32 tglinerflx1 
 |-  ( ( ( ph /\ C =/= D ) /\ ( A L B ) = ( C L D ) ) -> C e. ( C L D ) )
34 simpr 
 |-  ( ( ( ph /\ C =/= D ) /\ ( A L B ) = ( C L D ) ) -> ( A L B ) = ( C L D ) )
35 33 34 eleqtrrd 
 |-  ( ( ( ph /\ C =/= D ) /\ ( A L B ) = ( C L D ) ) -> C e. ( A L B ) )
36 1 3 2 23 26 24 35 tglngne 
 |-  ( ( ( ph /\ C =/= D ) /\ ( A L B ) = ( C L D ) ) -> A =/= B )
37 1 2 3 23 24 25 26 30 35 36 lnrot1 
 |-  ( ( ( ph /\ C =/= D ) /\ ( A L B ) = ( C L D ) ) -> A e. ( B L C ) )
38 37 orcd 
 |-  ( ( ( ph /\ C =/= D ) /\ ( A L B ) = ( C L D ) ) -> ( A e. ( B L C ) \/ B = C ) )
39 9 ad2antrr 
 |-  ( ( ( ph /\ C =/= D ) /\ ( A L B ) = ( C L D ) ) -> -. ( A e. ( B L C ) \/ B = C ) )
40 38 39 pm2.65da 
 |-  ( ( ph /\ C =/= D ) -> -. ( A L B ) = ( C L D ) )
41 40 neqned 
 |-  ( ( ph /\ C =/= D ) -> ( A L B ) =/= ( C L D ) )
42 22 41 pm2.61dane 
 |-  ( ph -> ( A L B ) =/= ( C L D ) )