Metamath Proof Explorer

Theorem ncolncol

Description: Deduce non-colinearity from non-colinearity and colinearity. (Contributed by Thierry Arnoux, 27-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 ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
ncolncol.1 ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 𝐿 𝐵 ) )
ncolncol.2 ⊢ ( 𝜑 → 𝐷 ≠ 𝐵 )
Assertion ncolncol ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )

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 ncolncol.1 ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 𝐿 𝐵 ) )
11 ncolncol.2 ⊢ ( 𝜑 → 𝐷 ≠ 𝐵 )
12 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) → 𝐺 ∈ TarskiG )
13 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) → 𝐴 ∈ 𝑃 )
14 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) → 𝐵 ∈ 𝑃 )
15 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) → 𝐶 ∈ 𝑃 )
16 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) ) → 𝐺 ∈ TarskiG )
17 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) ) → 𝐴 ∈ 𝑃 )
18 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) ) → 𝐵 ∈ 𝑃 )
19 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) ) → 𝐶 ∈ 𝑃 )
20 1 3 2 4 5 6 10 tglngne ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
21 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) ) → 𝐴 ≠ 𝐵 )
22 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) ) → 𝐷 ∈ 𝑃 )
23 11 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐷 )
24 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) ) → 𝐵 ≠ 𝐷 )
25 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) ) → 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) )
26 1 2 3 16 18 22 19 24 25 lncom ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) ) → 𝐶 ∈ ( 𝐵 𝐿 𝐷 ) )
27 20 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
28 1 2 3 4 6 5 8 27 10 lncom ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐵 𝐿 𝐴 ) )
29 1 2 3 4 6 5 27 8 11 28 tglineelsb2 ⊢ ( 𝜑 → ( 𝐵 𝐿 𝐴 ) = ( 𝐵 𝐿 𝐷 ) )
30 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) ) → ( 𝐵 𝐿 𝐴 ) = ( 𝐵 𝐿 𝐷 ) )
31 26 30 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) ) → 𝐶 ∈ ( 𝐵 𝐿 𝐴 ) )
32 1 2 3 16 17 18 19 21 31 lncom ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) ) → 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) )
33 32 orcd ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) ) → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
34 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐷 = 𝐵 ) → 𝐷 = 𝐵 )
35 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐷 = 𝐵 ) → 𝐷 ≠ 𝐵 )
36 34 35 pm2.21ddne ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) ∧ 𝐷 = 𝐵 ) → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
37 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) → 𝐷 ∈ 𝑃 )
38 simpr ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) → ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
39 1 3 2 12 14 15 37 38 colrot2 ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) → ( 𝐶 ∈ ( 𝐷 𝐿 𝐵 ) ∨ 𝐷 = 𝐵 ) )
40 33 36 39 mpjaodan ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
41 1 3 2 12 13 14 15 40 colrot1 ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) → ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
42 9 41 mtand ⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )