Metamath Proof Explorer

Theorem tglineinteq

Description: Two distinct lines intersect in at most one point. Theorem 6.21 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 6-Aug-2019)

Ref Expression
Hypotheses tglineintmo.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tglineintmo.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tglineintmo.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tglineintmo.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tglineinteq.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tglineinteq.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tglineinteq.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tglineinteq.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tglineinteq.e ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
tglineinteq.1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) )
tglineinteq.2 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 𝐿 𝐵 ) )
tglineinteq.3 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 𝐿 𝐷 ) )
tglineinteq.4 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 𝐿 𝐷 ) )
Assertion tglineinteq ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step Hyp Ref Expression
1 tglineintmo.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tglineintmo.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 tglineintmo.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 tglineintmo.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tglineinteq.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 tglineinteq.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 tglineinteq.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 tglineinteq.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 tglineinteq.e ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
10 tglineinteq.1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) )
11 tglineinteq.2 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 𝐿 𝐵 ) )
12 tglineinteq.3 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 𝐿 𝐷 ) )
13 tglineinteq.4 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 𝐿 𝐷 ) )
14 1 3 2 4 5 6 10 tglngne ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
15 1 2 3 4 5 6 14 tgelrnln ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 )
16 1 3 2 4 7 8 12 tglngne ⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
17 1 2 3 4 7 8 16 tgelrnln ⊢ ( 𝜑 → ( 𝐶 𝐿 𝐷 ) ∈ ran 𝐿 )
18 1 2 3 4 5 6 7 8 9 tglineneq ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ≠ ( 𝐶 𝐿 𝐷 ) )
19 1 2 3 4 15 17 18 tglineintmo ⊢ ( 𝜑 → ∃* 𝑥 ( 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ∧ 𝑥 ∈ ( 𝐶 𝐿 𝐷 ) ) )
20 10 12 jca ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) ∧ 𝑋 ∈ ( 𝐶 𝐿 𝐷 ) ) )
21 11 13 jca ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐴 𝐿 𝐵 ) ∧ 𝑌 ∈ ( 𝐶 𝐿 𝐷 ) ) )
22 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ↔ 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) ) )
23 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ ( 𝐶 𝐿 𝐷 ) ↔ 𝑋 ∈ ( 𝐶 𝐿 𝐷 ) ) )
24 22 23 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ∧ 𝑥 ∈ ( 𝐶 𝐿 𝐷 ) ) ↔ ( 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) ∧ 𝑋 ∈ ( 𝐶 𝐿 𝐷 ) ) ) )
25 eleq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ↔ 𝑌 ∈ ( 𝐴 𝐿 𝐵 ) ) )
26 eleq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 ∈ ( 𝐶 𝐿 𝐷 ) ↔ 𝑌 ∈ ( 𝐶 𝐿 𝐷 ) ) )
27 25 26 anbi12d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ∧ 𝑥 ∈ ( 𝐶 𝐿 𝐷 ) ) ↔ ( 𝑌 ∈ ( 𝐴 𝐿 𝐵 ) ∧ 𝑌 ∈ ( 𝐶 𝐿 𝐷 ) ) ) )
28 24 27 moi ⊢ ( ( ( 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ∃* 𝑥 ( 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ∧ 𝑥 ∈ ( 𝐶 𝐿 𝐷 ) ) ∧ ( ( 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) ∧ 𝑋 ∈ ( 𝐶 𝐿 𝐷 ) ) ∧ ( 𝑌 ∈ ( 𝐴 𝐿 𝐵 ) ∧ 𝑌 ∈ ( 𝐶 𝐿 𝐷 ) ) ) ) → 𝑋 = 𝑌 )
29 10 11 19 20 21 28 syl212anc ⊢ ( 𝜑 → 𝑋 = 𝑌 )