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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
tglnpt2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tglnpt2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tglnpt2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tglnpt2.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
tglnpt3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
tglnpt3.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
tglnpt3.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
Assertion tglnpt3 ( 𝜑 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑋 ∧ 𝑧 ≠ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 tglnpt2.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tglnpt2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 tglnpt2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 tglnpt2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tglnpt2.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
6 tglnpt3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
7 tglnpt3.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
8 tglnpt3.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
9 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
10 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) → 𝐺 ∈ TarskiG )
11 1 3 2 4 5 7 tglnpt ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
12 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) → 𝑌 ∈ 𝑃 )
13 1 3 2 4 5 6 tglnpt ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
14 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) → 𝑋 ∈ 𝑃 )
15 1 fvexi ⊢ 𝑃 ∈ V
16 15 a1i ⊢ ( 𝜑 → 𝑃 ∈ V )
17 16 13 11 8 nehash2 ⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
18 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
19 1 9 2 10 12 14 18 tgbtwndiff ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) → ∃ 𝑧 ∈ 𝑃 ( 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑧 ) )
20 4 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → 𝐺 ∈ TarskiG )
21 13 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → 𝑋 ∈ 𝑃 )
22 11 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → 𝑌 ∈ 𝑃 )
23 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → 𝑧 ∈ 𝑃 )
24 8 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → 𝑋 ≠ 𝑌 )
25 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → 𝑋 ≠ 𝑧 )
26 20 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑌 = 𝑧 ) → 𝐺 ∈ TarskiG )
27 23 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑌 = 𝑧 ) → 𝑧 ∈ 𝑃 )
28 21 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑌 = 𝑧 ) → 𝑋 ∈ 𝑃 )
29 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑌 = 𝑧 ) → 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) )
30 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑌 = 𝑧 ) → 𝑌 = 𝑧 )
31 30 oveq1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑌 = 𝑧 ) → ( 𝑌 𝐼 𝑧 ) = ( 𝑧 𝐼 𝑧 ) )
32 29 31 eleqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑌 = 𝑧 ) → 𝑋 ∈ ( 𝑧 𝐼 𝑧 ) )
33 1 9 2 26 27 28 32 axtgbtwnid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑌 = 𝑧 ) → 𝑧 = 𝑋 )
34 33 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑌 = 𝑧 ) → 𝑋 = 𝑧 )
35 25 34 mteqand ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → 𝑌 ≠ 𝑧 )
36 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) )
37 1 2 3 20 22 23 21 35 36 btwnlng1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → 𝑋 ∈ ( 𝑌 𝐿 𝑧 ) )
38 1 2 3 20 21 22 23 24 37 35 lnrot2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) )
39 1 2 3 4 13 11 8 8 5 6 7 tglinethru ⊢ ( 𝜑 → 𝐴 = ( 𝑋 𝐿 𝑌 ) )
40 39 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → 𝐴 = ( 𝑋 𝐿 𝑌 ) )
41 38 40 eleqtrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → 𝑧 ∈ 𝐴 )
42 25 necomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → 𝑧 ≠ 𝑋 )
43 35 necomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → 𝑧 ≠ 𝑌 )
44 41 42 43 jca32 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ) ∧ 𝑋 ≠ 𝑧 ) → ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝑋 ∧ 𝑧 ≠ 𝑌 ) ) )
45 44 anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑧 ) ) → ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝑋 ∧ 𝑧 ≠ 𝑌 ) ) )
46 45 expl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) → ( ( 𝑧 ∈ 𝑃 ∧ ( 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑧 ) ) → ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝑋 ∧ 𝑧 ≠ 𝑌 ) ) ) )
47 46 reximdv2 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) → ( ∃ 𝑧 ∈ 𝑃 ( 𝑋 ∈ ( 𝑌 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑧 ) → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑋 ∧ 𝑧 ≠ 𝑌 ) ) )
48 19 47 mpd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑡 ) → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑋 ∧ 𝑧 ≠ 𝑌 ) )
49 1 2 3 4 5 6 tglnpt2 ⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝐴 𝑋 ≠ 𝑡 )
50 48 49 r19.29a ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑋 ∧ 𝑧 ≠ 𝑌 ) )