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