Metamath Proof Explorer

Theorem tglnpt3

Description: Find a third point on a 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 )
tglnpt3.x 
|- ( ph -> X e. A )
tglnpt3.y 
|- ( ph -> Y e. A )
tglnpt3.1 
|- ( ph -> X =/= Y )
Assertion tglnpt3 
|- ( ph -> E. z e. A ( z =/= X /\ z =/= 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 tglnpt3.x 
 |-  ( ph -> X e. A )
7 tglnpt3.y 
 |-  ( ph -> Y e. A )
8 tglnpt3.1 
 |-  ( ph -> X =/= Y )
9 eqid 
 |-  ( dist ` G ) = ( dist ` G )
10 4 ad2antrr 
 |-  ( ( ( ph /\ t e. A ) /\ X =/= t ) -> G e. TarskiG )
11 1 3 2 4 5 7 tglnpt 
 |-  ( ph -> Y e. P )
12 11 ad2antrr 
 |-  ( ( ( ph /\ t e. A ) /\ X =/= t ) -> Y e. P )
13 1 3 2 4 5 6 tglnpt 
 |-  ( ph -> X e. P )
14 13 ad2antrr 
 |-  ( ( ( ph /\ t e. A ) /\ X =/= t ) -> X e. P )
15 1 fvexi 
 |-  P e. _V
16 15 a1i 
 |-  ( ph -> P e. _V )
17 16 13 11 8 nehash2 
 |-  ( ph -> 2 <_ ( # ` P ) )
18 17 ad2antrr 
 |-  ( ( ( ph /\ t e. A ) /\ X =/= t ) -> 2 <_ ( # ` P ) )
19 1 9 2 10 12 14 18 tgbtwndiff 
 |-  ( ( ( ph /\ t e. A ) /\ X =/= t ) -> E. z e. P ( X e. ( Y I z ) /\ X =/= z ) )
20 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> G e. TarskiG )
21 13 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> X e. P )
22 11 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> Y e. P )
23 simpllr 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> z e. P )
24 8 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> X =/= Y )
25 simpr 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> X =/= z )
26 20 adantr 
 |-  ( ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) /\ Y = z ) -> G e. TarskiG )
27 23 adantr 
 |-  ( ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) /\ Y = z ) -> z e. P )
28 21 adantr 
 |-  ( ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) /\ Y = z ) -> X e. P )
29 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) /\ Y = z ) -> X e. ( Y I z ) )
30 simpr 
 |-  ( ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) /\ Y = z ) -> Y = z )
31 30 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) /\ Y = z ) -> ( Y I z ) = ( z I z ) )
32 29 31 eleqtrd 
 |-  ( ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) /\ Y = z ) -> X e. ( z I z ) )
33 1 9 2 26 27 28 32 axtgbtwnid 
 |-  ( ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) /\ Y = z ) -> z = X )
34 33 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) /\ Y = z ) -> X = z )
35 25 34 mteqand 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> Y =/= z )
36 simplr 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> X e. ( Y I z ) )
37 1 2 3 20 22 23 21 35 36 btwnlng1 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> X e. ( Y L z ) )
38 1 2 3 20 21 22 23 24 37 35 lnrot2 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> z e. ( X L Y ) )
39 1 2 3 4 13 11 8 8 5 6 7 tglinethru 
 |-  ( ph -> A = ( X L Y ) )
40 39 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> A = ( X L Y ) )
41 38 40 eleqtrrd 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> z e. A )
42 25 necomd 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> z =/= X )
43 35 necomd 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> z =/= Y )
44 41 42 43 jca32 
 |-  ( ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ X e. ( Y I z ) ) /\ X =/= z ) -> ( z e. A /\ ( z =/= X /\ z =/= Y ) ) )
45 44 anasss 
 |-  ( ( ( ( ( ph /\ t e. A ) /\ X =/= t ) /\ z e. P ) /\ ( X e. ( Y I z ) /\ X =/= z ) ) -> ( z e. A /\ ( z =/= X /\ z =/= Y ) ) )
46 45 expl 
 |-  ( ( ( ph /\ t e. A ) /\ X =/= t ) -> ( ( z e. P /\ ( X e. ( Y I z ) /\ X =/= z ) ) -> ( z e. A /\ ( z =/= X /\ z =/= Y ) ) ) )
47 46 reximdv2 
 |-  ( ( ( ph /\ t e. A ) /\ X =/= t ) -> ( E. z e. P ( X e. ( Y I z ) /\ X =/= z ) -> E. z e. A ( z =/= X /\ z =/= Y ) ) )
48 19 47 mpd 
 |-  ( ( ( ph /\ t e. A ) /\ X =/= t ) -> E. z e. A ( z =/= X /\ z =/= Y ) )
49 1 2 3 4 5 6 tglnpt2 
 |-  ( ph -> E. t e. A X =/= t )
50 48 49 r19.29a 
 |-  ( ph -> E. z e. A ( z =/= X /\ z =/= Y ) )