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

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 tglnpt2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
7 neeq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑋 ≠ 𝑦 ↔ 𝑋 ≠ 𝑧 ) )
8 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 = 𝑥 ) → 𝐺 ∈ TarskiG )
9 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 = 𝑥 ) → 𝑥 ∈ 𝑃 )
10 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 = 𝑥 ) → 𝑧 ∈ 𝑃 )
11 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 = 𝑥 ) → 𝑥 ≠ 𝑧 )
12 1 2 3 8 9 10 11 tglinerflx2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 = 𝑥 ) → 𝑧 ∈ ( 𝑥 𝐿 𝑧 ) )
13 simplrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 = 𝑥 ) → 𝐴 = ( 𝑥 𝐿 𝑧 ) )
14 12 13 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 = 𝑥 ) → 𝑧 ∈ 𝐴 )
15 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 = 𝑥 ) → 𝑋 = 𝑥 )
16 15 11 eqnetrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 = 𝑥 ) → 𝑋 ≠ 𝑧 )
17 7 14 16 rspcedvdw ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 = 𝑥 ) → ∃ 𝑦 ∈ 𝐴 𝑋 ≠ 𝑦 )
18 neeq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑋 ≠ 𝑦 ↔ 𝑋 ≠ 𝑥 ) )
19 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 ≠ 𝑥 ) → 𝐺 ∈ TarskiG )
20 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 ≠ 𝑥 ) → 𝑥 ∈ 𝑃 )
21 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 ≠ 𝑥 ) → 𝑧 ∈ 𝑃 )
22 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 ≠ 𝑥 ) → 𝑥 ≠ 𝑧 )
23 1 2 3 19 20 21 22 tglinerflx1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 ≠ 𝑥 ) → 𝑥 ∈ ( 𝑥 𝐿 𝑧 ) )
24 simplrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 ≠ 𝑥 ) → 𝐴 = ( 𝑥 𝐿 𝑧 ) )
25 23 24 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 ≠ 𝑥 ) → 𝑥 ∈ 𝐴 )
26 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 ≠ 𝑥 ) → 𝑋 ≠ 𝑥 )
27 18 25 26 rspcedvdw ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) ∧ 𝑋 ≠ 𝑥 ) → ∃ 𝑦 ∈ 𝐴 𝑋 ≠ 𝑦 )
28 17 27 pm2.61dane ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) ) → ∃ 𝑦 ∈ 𝐴 𝑋 ≠ 𝑦 )
29 1 2 3 4 5 tgisline ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝐴 = ( 𝑥 𝐿 𝑧 ) ∧ 𝑥 ≠ 𝑧 ) )
30 28 29 r19.29vva ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐴 𝑋 ≠ 𝑦 )