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 4 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> G e. TarskiG )
8 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> x e. P )
9 simpllr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> z e. P )
10 simplrr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> x =/= z )
11 1 2 3 7 8 9 10 tglinerflx2 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> z e. ( x L z ) )
12 simplrl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> A = ( x L z ) )
13 11 12 eleqtrrd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> z e. A )
14 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> X = x )
15 14 10 eqnetrd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> X =/= z )
16 neeq2 
 |-  ( y = z -> ( X =/= y <-> X =/= z ) )
17 16 rspcev 
 |-  ( ( z e. A /\ X =/= z ) -> E. y e. A X =/= y )
18 13 15 17 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X = x ) -> E. y e. A X =/= y )
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 neeq2 
 |-  ( y = x -> ( X =/= y <-> X =/= x ) )
28 27 rspcev 
 |-  ( ( x e. A /\ X =/= x ) -> E. y e. A X =/= y )
29 25 26 28 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) /\ X =/= x ) -> E. y e. A X =/= y )
30 18 29 pm2.61dane 
 |-  ( ( ( ( ph /\ x e. P ) /\ z e. P ) /\ ( A = ( x L z ) /\ x =/= z ) ) -> E. y e. A X =/= y )
31 1 2 3 4 5 tgisline 
 |-  ( ph -> E. x e. P E. z e. P ( A = ( x L z ) /\ x =/= z ) )
32 30 31 r19.29vva 
 |-  ( ph -> E. y e. A X =/= y )