Metamath Proof Explorer

Theorem tglnpt2

Description: Find a second point on a line. (Contributed by Thierry Arnoux, 18-Oct-2019)

Ref Expression
Hypotheses tglnpt2.p 
|- P = ( Base ` G )
tglnpt2.i 
|- I = ( Itv ` G )
tglnpt2.l 
|- L = ( LineG ` G )
tglnpt2.g 
|- ( ph -> G e. TarskiG )
tglnpt2.a 
|- ( ph -> A e. ran L )
tglnpt2.x 
|- ( ph -> X e. A )
Assertion tglnpt2 
|- ( ph -> E. y e. A X =/= y )

Proof

Step Hyp Ref Expression
1 tglnpt2.p 
 |-  P = ( Base ` G )
2 tglnpt2.i 
 |-  I = ( Itv ` G )
3 tglnpt2.l 
 |-  L = ( LineG ` G )
4 tglnpt2.g 
 |-  ( ph -> G e. TarskiG )
5 tglnpt2.a 
 |-  ( ph -> A e. ran L )
6 tglnpt2.x 
 |-  ( ph -> X e. A )
7 neeq2 
 |-  ( y = z -> ( X =/= y <-> X =/= z ) )
8 4 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> G e. TarskiG )
9 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> x e. P )
10 simpllr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> z e. P )
11 simplrr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> x =/= z )
12 1 2 3 8 9 10 11 tglinerflx2 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> z e. ( x L z ) )
13 simplrl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> A = ( x L z ) )
14 12 13 eleqtrrd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> z e. A )
15 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> X = x )
16 15 11 eqnetrd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> X =/= z )
17 7 14 16 rspcedvdw 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> E. y e. A X =/= y )
18 neeq2 
 |-  ( y = x -> ( X =/= y <-> X =/= x ) )
19 4 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X =/= x ) -> G e. TarskiG )
20 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X =/= x ) -> x e. P )
21 simpllr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X =/= x ) -> z e. P )
22 simplrr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X =/= x ) -> x =/= z )
23 1 2 3 19 20 21 22 tglinerflx1 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X =/= x ) -> x e. ( x L z ) )
24 simplrl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X =/= x ) -> A = ( x L z ) )
25 23 24 eleqtrrd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X =/= x ) -> x e. A )
26 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X =/= x ) -> X =/= x )
27 18 25 26 rspcedvdw 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X =/= x ) -> E. y e. A X =/= y )
28 17 27 pm2.61dane 
 |-  ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) -> E. y e. A X =/= y )
29 1 2 3 4 5 tgisline 
 |-  ( ph -> E. x e. P E. z e. P ( A = ( x L z ) /\ x =/= z ) )
30 28 29 r19.29vva 
 |-  ( ph -> E. y e. A X =/= y )