Metamath Proof Explorer

Theorem tgcolg

Description: We choose the notation ( Z e. ( X L Y ) \/ X = Y ) instead of "colinear" in order to avoid defining an additional symbol for colinearity because LineG is a common structure slot for other axiomatizations of geometry. (Contributed by Thierry Arnoux, 25-May-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 )
Assertion tgcolg 
|- ( ph -> ( ( Z e. ( X L Y ) \/ X = Y ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )

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 animorr 
 |-  ( ( ph /\ X = Y ) -> ( Z e. ( X L Y ) \/ X = Y ) )
9 eqid 
 |-  ( dist ` G ) = ( dist ` G )
10 4 adantr 
 |-  ( ( ph /\ X = Y ) -> G e. TarskiG )
11 7 adantr 
 |-  ( ( ph /\ X = Y ) -> Z e. P )
12 5 adantr 
 |-  ( ( ph /\ X = Y ) -> X e. P )
13 1 9 3 10 11 12 tgbtwntriv2 
 |-  ( ( ph /\ X = Y ) -> X e. ( Z I X ) )
14 simpr 
 |-  ( ( ph /\ X = Y ) -> X = Y )
15 14 oveq2d 
 |-  ( ( ph /\ X = Y ) -> ( Z I X ) = ( Z I Y ) )
16 13 15 eleqtrd 
 |-  ( ( ph /\ X = Y ) -> X e. ( Z I Y ) )
17 16 3mix2d 
 |-  ( ( ph /\ X = Y ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )
18 8 17 2thd 
 |-  ( ( ph /\ X = Y ) -> ( ( Z e. ( X L Y ) \/ X = Y ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
19 simpr 
 |-  ( ( ph /\ X =/= Y ) -> X =/= Y )
20 19 neneqd 
 |-  ( ( ph /\ X =/= Y ) -> -. X = Y )
21 biorf 
 |-  ( -. X = Y -> ( Z e. ( X L Y ) <-> ( X = Y \/ Z e. ( X L Y ) ) ) )
22 20 21 syl 
 |-  ( ( ph /\ X =/= Y ) -> ( Z e. ( X L Y ) <-> ( X = Y \/ Z e. ( X L Y ) ) ) )
23 orcom 
 |-  ( ( X = Y \/ Z e. ( X L Y ) ) <-> ( Z e. ( X L Y ) \/ X = Y ) )
24 22 23 bitrdi 
 |-  ( ( ph /\ X =/= Y ) -> ( Z e. ( X L Y ) <-> ( Z e. ( X L Y ) \/ X = Y ) ) )
25 4 adantr 
 |-  ( ( ph /\ X =/= Y ) -> G e. TarskiG )
26 5 adantr 
 |-  ( ( ph /\ X =/= Y ) -> X e. P )
27 6 adantr 
 |-  ( ( ph /\ X =/= Y ) -> Y e. P )
28 7 adantr 
 |-  ( ( ph /\ X =/= Y ) -> Z e. P )
29 1 2 3 25 26 27 19 28 tgellng 
 |-  ( ( ph /\ X =/= Y ) -> ( Z e. ( X L Y ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
30 24 29 bitr3d 
 |-  ( ( ph /\ X =/= Y ) -> ( ( Z e. ( X L Y ) \/ X = Y ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
31 18 30 pm2.61dane 
 |-  ( ph -> ( ( Z e. ( X L Y ) \/ X = Y ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )