Metamath Proof Explorer


Theorem tglineintmo

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

Ref Expression
Hypotheses tglineintmo.p 𝑃 = ( Base ‘ 𝐺 )
tglineintmo.i 𝐼 = ( Itv ‘ 𝐺 )
tglineintmo.l 𝐿 = ( LineG ‘ 𝐺 )
tglineintmo.g ( 𝜑𝐺 ∈ TarskiG )
tglineintmo.a ( 𝜑𝐴 ∈ ran 𝐿 )
tglineintmo.b ( 𝜑𝐵 ∈ ran 𝐿 )
tglineintmo.c ( 𝜑𝐴𝐵 )
Assertion tglineintmo ( 𝜑 → ∃* 𝑥 ( 𝑥𝐴𝑥𝐵 ) )

Proof

Step Hyp Ref Expression
1 tglineintmo.p 𝑃 = ( Base ‘ 𝐺 )
2 tglineintmo.i 𝐼 = ( Itv ‘ 𝐺 )
3 tglineintmo.l 𝐿 = ( LineG ‘ 𝐺 )
4 tglineintmo.g ( 𝜑𝐺 ∈ TarskiG )
5 tglineintmo.a ( 𝜑𝐴 ∈ ran 𝐿 )
6 tglineintmo.b ( 𝜑𝐵 ∈ ran 𝐿 )
7 tglineintmo.c ( 𝜑𝐴𝐵 )
8 4 ad2antrr ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝐺 ∈ TarskiG )
9 elssuni ( 𝐴 ∈ ran 𝐿𝐴 ran 𝐿 )
10 5 9 syl ( 𝜑𝐴 ran 𝐿 )
11 1 3 2 tglnunirn ( 𝐺 ∈ TarskiG → ran 𝐿𝑃 )
12 4 11 syl ( 𝜑 ran 𝐿𝑃 )
13 10 12 sstrd ( 𝜑𝐴𝑃 )
14 13 ad2antrr ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝐴𝑃 )
15 simplrl ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → ( 𝑥𝐴𝑥𝐵 ) )
16 15 simpld ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝑥𝐴 )
17 14 16 sseldd ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝑥𝑃 )
18 simplrr ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → ( 𝑦𝐴𝑦𝐵 ) )
19 18 simpld ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝑦𝐴 )
20 14 19 sseldd ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝑦𝑃 )
21 simpr ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝑥𝑦 )
22 5 ad2antrr ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝐴 ∈ ran 𝐿 )
23 1 2 3 8 17 20 21 21 22 16 19 tglinethru ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝐴 = ( 𝑥 𝐿 𝑦 ) )
24 6 ad2antrr ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝐵 ∈ ran 𝐿 )
25 15 simprd ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝑥𝐵 )
26 18 simprd ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝑦𝐵 )
27 1 2 3 8 17 20 21 21 24 25 26 tglinethru ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝐵 = ( 𝑥 𝐿 𝑦 ) )
28 23 27 eqtr4d ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝐴 = 𝐵 )
29 7 ad2antrr ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → 𝐴𝐵 )
30 29 neneqd ( ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) ∧ 𝑥𝑦 ) → ¬ 𝐴 = 𝐵 )
31 28 30 pm2.65da ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) → ¬ 𝑥𝑦 )
32 nne ( ¬ 𝑥𝑦𝑥 = 𝑦 )
33 31 32 sylib ( ( 𝜑 ∧ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) ) → 𝑥 = 𝑦 )
34 33 ex ( 𝜑 → ( ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) → 𝑥 = 𝑦 ) )
35 34 alrimivv ( 𝜑 → ∀ 𝑥𝑦 ( ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) → 𝑥 = 𝑦 ) )
36 eleq1w ( 𝑥 = 𝑦 → ( 𝑥𝐴𝑦𝐴 ) )
37 eleq1w ( 𝑥 = 𝑦 → ( 𝑥𝐵𝑦𝐵 ) )
38 36 37 anbi12d ( 𝑥 = 𝑦 → ( ( 𝑥𝐴𝑥𝐵 ) ↔ ( 𝑦𝐴𝑦𝐵 ) ) )
39 38 mo4 ( ∃* 𝑥 ( 𝑥𝐴𝑥𝐵 ) ↔ ∀ 𝑥𝑦 ( ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑦𝐴𝑦𝐵 ) ) → 𝑥 = 𝑦 ) )
40 35 39 sylibr ( 𝜑 → ∃* 𝑥 ( 𝑥𝐴𝑥𝐵 ) )