Metamath Proof Explorer


Theorem tglineneq

Description: Given three non-colinear points, build two different lines. (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 ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
Assertion tglineneq ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ≠ ( 𝐶 𝐿 𝐷 ) )

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 1 2 3 4 5 6 7 9 ncolne1 ( 𝜑𝐴𝐵 )
11 1 2 3 4 5 6 10 tglinerflx1 ( 𝜑𝐴 ∈ ( 𝐴 𝐿 𝐵 ) )
12 simplr ( ( ( 𝜑𝐶 = 𝐷 ) ∧ 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ) → 𝐶 = 𝐷 )
13 4 adantr ( ( 𝜑𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ) → 𝐺 ∈ TarskiG )
14 7 adantr ( ( 𝜑𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ) → 𝐶𝑃 )
15 8 adantr ( ( 𝜑𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ) → 𝐷𝑃 )
16 simpr ( ( 𝜑𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ) → 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) )
17 1 3 2 13 14 15 16 tglngne ( ( 𝜑𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ) → 𝐶𝐷 )
18 17 adantlr ( ( ( 𝜑𝐶 = 𝐷 ) ∧ 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ) → 𝐶𝐷 )
19 18 neneqd ( ( ( 𝜑𝐶 = 𝐷 ) ∧ 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ) → ¬ 𝐶 = 𝐷 )
20 12 19 pm2.65da ( ( 𝜑𝐶 = 𝐷 ) → ¬ 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) )
21 nelne1 ( ( 𝐴 ∈ ( 𝐴 𝐿 𝐵 ) ∧ ¬ 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ) → ( 𝐴 𝐿 𝐵 ) ≠ ( 𝐶 𝐿 𝐷 ) )
22 11 20 21 syl2an2r ( ( 𝜑𝐶 = 𝐷 ) → ( 𝐴 𝐿 𝐵 ) ≠ ( 𝐶 𝐿 𝐷 ) )
23 4 ad2antrr ( ( ( 𝜑𝐶𝐷 ) ∧ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) ) → 𝐺 ∈ TarskiG )
24 6 ad2antrr ( ( ( 𝜑𝐶𝐷 ) ∧ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) ) → 𝐵𝑃 )
25 7 ad2antrr ( ( ( 𝜑𝐶𝐷 ) ∧ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) ) → 𝐶𝑃 )
26 5 ad2antrr ( ( ( 𝜑𝐶𝐷 ) ∧ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) ) → 𝐴𝑃 )
27 pm2.46 ( ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) → ¬ 𝐵 = 𝐶 )
28 9 27 syl ( 𝜑 → ¬ 𝐵 = 𝐶 )
29 28 neqned ( 𝜑𝐵𝐶 )
30 29 ad2antrr ( ( ( 𝜑𝐶𝐷 ) ∧ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) ) → 𝐵𝐶 )
31 8 ad2antrr ( ( ( 𝜑𝐶𝐷 ) ∧ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) ) → 𝐷𝑃 )
32 simplr ( ( ( 𝜑𝐶𝐷 ) ∧ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) ) → 𝐶𝐷 )
33 1 2 3 23 25 31 32 tglinerflx1 ( ( ( 𝜑𝐶𝐷 ) ∧ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) ) → 𝐶 ∈ ( 𝐶 𝐿 𝐷 ) )
34 simpr ( ( ( 𝜑𝐶𝐷 ) ∧ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) ) → ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) )
35 33 34 eleqtrrd ( ( ( 𝜑𝐶𝐷 ) ∧ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) ) → 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) )
36 1 3 2 23 26 24 35 tglngne ( ( ( 𝜑𝐶𝐷 ) ∧ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) ) → 𝐴𝐵 )
37 1 2 3 23 24 25 26 30 35 36 lnrot1 ( ( ( 𝜑𝐶𝐷 ) ∧ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) ) → 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) )
38 37 orcd ( ( ( 𝜑𝐶𝐷 ) ∧ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) ) → ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
39 9 ad2antrr ( ( ( 𝜑𝐶𝐷 ) ∧ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) ) → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
40 38 39 pm2.65da ( ( 𝜑𝐶𝐷 ) → ¬ ( 𝐴 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) )
41 40 neqned ( ( 𝜑𝐶𝐷 ) → ( 𝐴 𝐿 𝐵 ) ≠ ( 𝐶 𝐿 𝐷 ) )
42 22 41 pm2.61dane ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ≠ ( 𝐶 𝐿 𝐷 ) )