Metamath Proof Explorer

Theorem tglnne

Description: It takes two different points to form a line. (Contributed by Thierry Arnoux, 27-Nov-2019)

Ref Expression
Hypotheses tglineelsb2.p 
|- B = ( Base ` G )
tglineelsb2.i 
|- I = ( Itv ` G )
tglineelsb2.l 
|- L = ( LineG ` G )
tglineelsb2.g 
|- ( ph -> G e. TarskiG )
tglnne.x 
|- ( ph -> X e. B )
tglnne.y 
|- ( ph -> Y e. B )
tglnne.1 
|- ( ph -> ( X L Y ) e. ran L )
Assertion tglnne 
|- ( ph -> X =/= Y )

Proof

Step Hyp Ref Expression
1 tglineelsb2.p 
 |-  B = ( Base ` G )
2 tglineelsb2.i 
 |-  I = ( Itv ` G )
3 tglineelsb2.l 
 |-  L = ( LineG ` G )
4 tglineelsb2.g 
 |-  ( ph -> G e. TarskiG )
5 tglnne.x 
 |-  ( ph -> X e. B )
6 tglnne.y 
 |-  ( ph -> Y e. B )
7 tglnne.1 
 |-  ( ph -> ( X L Y ) e. ran L )
8 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( ( X L Y ) = ( x L y ) /\ x =/= y ) ) -> G e. TarskiG )
9 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( ( X L Y ) = ( x L y ) /\ x =/= y ) ) -> X e. B )
10 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( ( X L Y ) = ( x L y ) /\ x =/= y ) ) -> Y e. B )
11 simpllr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( ( X L Y ) = ( x L y ) /\ x =/= y ) ) -> x e. B )
12 simplr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( ( X L Y ) = ( x L y ) /\ x =/= y ) ) -> y e. B )
13 simprr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( ( X L Y ) = ( x L y ) /\ x =/= y ) ) -> x =/= y )
14 eqid 
 |-  ( dist ` G ) = ( dist ` G )
15 1 14 2 8 11 12 tgbtwntriv1 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( ( X L Y ) = ( x L y ) /\ x =/= y ) ) -> x e. ( x I y ) )
16 1 2 3 8 11 12 11 13 15 btwnlng1 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( ( X L Y ) = ( x L y ) /\ x =/= y ) ) -> x e. ( x L y ) )
17 simprl 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( ( X L Y ) = ( x L y ) /\ x =/= y ) ) -> ( X L Y ) = ( x L y ) )
18 16 17 eleqtrrd 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( ( X L Y ) = ( x L y ) /\ x =/= y ) ) -> x e. ( X L Y ) )
19 1 3 2 8 9 10 18 tglngne 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( ( X L Y ) = ( x L y ) /\ x =/= y ) ) -> X =/= Y )
20 1 2 3 4 7 tgisline 
 |-  ( ph -> E. x e. B E. y e. B ( ( X L Y ) = ( x L y ) /\ x =/= y ) )
21 19 20 r19.29vva 
 |-  ( ph -> X =/= Y )