Metamath Proof Explorer

Theorem tglnpt4

Description: Find a second point on a line, outside of a second line. (Contributed by Thierry Arnoux, 17-Jun-2026)

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 )
tglnpt4.y 
|- ( ph -> B e. ran L )
tglnpt4.x 
|- ( ph -> X e. A )
tglnpt4.1 
|- ( ph -> A =/= B )
Assertion tglnpt4 
|- ( ph -> E. z e. ( A \ B ) z =/= X )

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 tglnpt4.y 
 |-  ( ph -> B e. ran L )
7 tglnpt4.x 
 |-  ( ph -> X e. A )
8 tglnpt4.1 
 |-  ( ph -> A =/= B )
9 4 adantr 
 |-  ( ( ph /\ X e. B ) -> G e. TarskiG )
10 5 adantr 
 |-  ( ( ph /\ X e. B ) -> A e. ran L )
11 7 adantr 
 |-  ( ( ph /\ X e. B ) -> X e. A )
12 1 2 3 9 10 11 tglnpt2 
 |-  ( ( ph /\ X e. B ) -> E. z e. A X =/= z )
13 simplr 
 |-  ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) -> z e. A )
14 simpr 
 |-  ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) -> X =/= z )
15 14 neneqd 
 |-  ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) -> -. X = z )
16 4 ad4antr 
 |-  ( ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> G e. TarskiG )
17 5 ad4antr 
 |-  ( ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> A e. ran L )
18 6 ad4antr 
 |-  ( ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> B e. ran L )
19 8 ad4antr 
 |-  ( ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> A =/= B )
20 7 ad4antr 
 |-  ( ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> X e. A )
21 simp-4r 
 |-  ( ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> X e. B )
22 20 21 elind 
 |-  ( ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> X e. ( A i^i B ) )
23 simpllr 
 |-  ( ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> z e. A )
24 simpr 
 |-  ( ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> z e. B )
25 23 24 elind 
 |-  ( ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> z e. ( A i^i B ) )
26 1 2 3 16 17 18 19 22 25 tglineineq 
 |-  ( ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> X = z )
27 15 26 mtand 
 |-  ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) -> -. z e. B )
28 13 27 eldifd 
 |-  ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) -> z e. ( A \ B ) )
29 14 necomd 
 |-  ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) -> z =/= X )
30 28 29 jca 
 |-  ( ( ( ( ph /\ X e. B ) /\ z e. A ) /\ X =/= z ) -> ( z e. ( A \ B ) /\ z =/= X ) )
31 30 expl 
 |-  ( ( ph /\ X e. B ) -> ( ( z e. A /\ X =/= z ) -> ( z e. ( A \ B ) /\ z =/= X ) ) )
32 31 reximdv2 
 |-  ( ( ph /\ X e. B ) -> ( E. z e. A X =/= z -> E. z e. ( A \ B ) z =/= X ) )
33 12 32 mpd 
 |-  ( ( ph /\ X e. B ) -> E. z e. ( A \ B ) z =/= X )
34 4 adantr 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> G e. TarskiG )
35 5 adantr 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> A e. ran L )
36 7 adantr 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> X e. A )
37 1 2 3 34 35 36 tglnpt2 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> E. z e. A X =/= z )
38 simplr 
 |-  ( ( ( ( ph /\ ( A i^i B ) = (/) ) /\ z e. A ) /\ X =/= z ) -> z e. A )
39 simp-4r 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) = (/) ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> ( A i^i B ) = (/) )
40 simpllr 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) = (/) ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> z e. A )
41 simpr 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) = (/) ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> z e. B )
42 40 41 elind 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) = (/) ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> z e. ( A i^i B ) )
43 42 ne0d 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) = (/) ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> ( A i^i B ) =/= (/) )
44 43 neneqd 
 |-  ( ( ( ( ( ph /\ ( A i^i B ) = (/) ) /\ z e. A ) /\ X =/= z ) /\ z e. B ) -> -. ( A i^i B ) = (/) )
45 39 44 pm2.65da 
 |-  ( ( ( ( ph /\ ( A i^i B ) = (/) ) /\ z e. A ) /\ X =/= z ) -> -. z e. B )
46 38 45 eldifd 
 |-  ( ( ( ( ph /\ ( A i^i B ) = (/) ) /\ z e. A ) /\ X =/= z ) -> z e. ( A \ B ) )
47 simpr 
 |-  ( ( ( ( ph /\ ( A i^i B ) = (/) ) /\ z e. A ) /\ X =/= z ) -> X =/= z )
48 47 necomd 
 |-  ( ( ( ( ph /\ ( A i^i B ) = (/) ) /\ z e. A ) /\ X =/= z ) -> z =/= X )
49 46 48 jca 
 |-  ( ( ( ( ph /\ ( A i^i B ) = (/) ) /\ z e. A ) /\ X =/= z ) -> ( z e. ( A \ B ) /\ z =/= X ) )
50 49 expl 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> ( ( z e. A /\ X =/= z ) -> ( z e. ( A \ B ) /\ z =/= X ) ) )
51 50 reximdv2 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> ( E. z e. A X =/= z -> E. z e. ( A \ B ) z =/= X ) )
52 37 51 mpd 
 |-  ( ( ph /\ ( A i^i B ) = (/) ) -> E. z e. ( A \ B ) z =/= X )
53 52 adantlr 
 |-  ( ( ( ph /\ -. X e. B ) /\ ( A i^i B ) = (/) ) -> E. z e. ( A \ B ) z =/= X )
54 simpr 
 |-  ( ( ( ph /\ -. X e. B ) /\ ( A i^i B ) =/= (/) ) -> ( A i^i B ) =/= (/) )
55 4 ad2antrr 
 |-  ( ( ( ph /\ -. X e. B ) /\ y e. ( A i^i B ) ) -> G e. TarskiG )
56 5 ad2antrr 
 |-  ( ( ( ph /\ -. X e. B ) /\ y e. ( A i^i B ) ) -> A e. ran L )
57 7 ad2antrr 
 |-  ( ( ( ph /\ -. X e. B ) /\ y e. ( A i^i B ) ) -> X e. A )
58 simpr 
 |-  ( ( ( ph /\ -. X e. B ) /\ y e. ( A i^i B ) ) -> y e. ( A i^i B ) )
59 58 elin1d 
 |-  ( ( ( ph /\ -. X e. B ) /\ y e. ( A i^i B ) ) -> y e. A )
60 simpr 
 |-  ( ( ph /\ y e. ( A i^i B ) ) -> y e. ( A i^i B ) )
61 60 elin2d 
 |-  ( ( ph /\ y e. ( A i^i B ) ) -> y e. B )
62 61 adantlr 
 |-  ( ( ( ph /\ -. X e. B ) /\ y e. ( A i^i B ) ) -> y e. B )
63 simplr 
 |-  ( ( ( ph /\ -. X e. B ) /\ y e. ( A i^i B ) ) -> -. X e. B )
64 nelne2 
 |-  ( ( y e. B /\ -. X e. B ) -> y =/= X )
65 62 63 64 syl2anc 
 |-  ( ( ( ph /\ -. X e. B ) /\ y e. ( A i^i B ) ) -> y =/= X )
66 65 necomd 
 |-  ( ( ( ph /\ -. X e. B ) /\ y e. ( A i^i B ) ) -> X =/= y )
67 1 2 3 55 56 57 59 66 tglnpt3 
 |-  ( ( ( ph /\ -. X e. B ) /\ y e. ( A i^i B ) ) -> E. z e. A ( z =/= X /\ z =/= y ) )
68 simpllr 
 |-  ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) -> z e. A )
69 simpr 
 |-  ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) -> z =/= y )
70 69 neneqd 
 |-  ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) -> -. z = y )
71 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) /\ z e. B ) -> G e. TarskiG )
72 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) /\ z e. B ) -> A e. ran L )
73 6 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) /\ z e. B ) -> B e. ran L )
74 8 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) /\ z e. B ) -> A =/= B )
75 68 adantr 
 |-  ( ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) /\ z e. B ) -> z e. A )
76 simpr 
 |-  ( ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) /\ z e. B ) -> z e. B )
77 75 76 elind 
 |-  ( ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) /\ z e. B ) -> z e. ( A i^i B ) )
78 60 ad4antr 
 |-  ( ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) /\ z e. B ) -> y e. ( A i^i B ) )
79 1 2 3 71 72 73 74 77 78 tglineineq 
 |-  ( ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) /\ z e. B ) -> z = y )
80 70 79 mtand 
 |-  ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) -> -. z e. B )
81 68 80 eldifd 
 |-  ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) -> z e. ( A \ B ) )
82 simplr 
 |-  ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) -> z =/= X )
83 81 82 jca 
 |-  ( ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ z =/= X ) /\ z =/= y ) -> ( z e. ( A \ B ) /\ z =/= X ) )
84 83 anasss 
 |-  ( ( ( ( ph /\ y e. ( A i^i B ) ) /\ z e. A ) /\ ( z =/= X /\ z =/= y ) ) -> ( z e. ( A \ B ) /\ z =/= X ) )
85 84 expl 
 |-  ( ( ph /\ y e. ( A i^i B ) ) -> ( ( z e. A /\ ( z =/= X /\ z =/= y ) ) -> ( z e. ( A \ B ) /\ z =/= X ) ) )
86 85 reximdv2 
 |-  ( ( ph /\ y e. ( A i^i B ) ) -> ( E. z e. A ( z =/= X /\ z =/= y ) -> E. z e. ( A \ B ) z =/= X ) )
87 86 adantlr 
 |-  ( ( ( ph /\ -. X e. B ) /\ y e. ( A i^i B ) ) -> ( E. z e. A ( z =/= X /\ z =/= y ) -> E. z e. ( A \ B ) z =/= X ) )
88 67 87 mpd 
 |-  ( ( ( ph /\ -. X e. B ) /\ y e. ( A i^i B ) ) -> E. z e. ( A \ B ) z =/= X )
89 88 adantlr 
 |-  ( ( ( ( ph /\ -. X e. B ) /\ ( A i^i B ) =/= (/) ) /\ y e. ( A i^i B ) ) -> E. z e. ( A \ B ) z =/= X )
90 54 89 n0limd 
 |-  ( ( ( ph /\ -. X e. B ) /\ ( A i^i B ) =/= (/) ) -> E. z e. ( A \ B ) z =/= X )
91 53 90 pm2.61dane 
 |-  ( ( ph /\ -. X e. B ) -> E. z e. ( A \ B ) z =/= X )
92 33 91 pm2.61dan 
 |-  ( ph -> E. z e. ( A \ B ) z =/= X )