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 ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ≠ ( 𝐶 𝐿 𝐷 ) )