Metamath Proof Explorer

Theorem coltr

Description: A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019)

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

Proof

Step Hyp Ref Expression
1 tglineintmo.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tglineintmo.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 tglineintmo.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 tglineintmo.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 coltr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 coltr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 coltr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 coltr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 coltr.1 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) )
10 coltr.2 ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
11 4 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → 𝐺 ∈ TarskiG )
12 7 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → 𝐶 ∈ 𝑃 )
13 8 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → 𝐷 ∈ 𝑃 )
14 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → 𝐶 ≠ 𝐷 )
15 1 2 3 11 12 13 14 tglinerflx1 ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → 𝐶 ∈ ( 𝐶 𝐿 𝐷 ) )
16 15 ex ⊢ ( 𝜑 → ( 𝐶 ≠ 𝐷 → 𝐶 ∈ ( 𝐶 𝐿 𝐷 ) ) )
17 16 necon1bd ⊢ ( 𝜑 → ( ¬ 𝐶 ∈ ( 𝐶 𝐿 𝐷 ) → 𝐶 = 𝐷 ) )
18 17 orrd ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐶 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
20 simplr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ 𝐶 ∈ ( 𝐶 𝐿 𝐷 ) ) → 𝐴 = 𝐶 )
21 simpr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ 𝐶 ∈ ( 𝐶 𝐿 𝐷 ) ) → 𝐶 ∈ ( 𝐶 𝐿 𝐷 ) )
22 20 21 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ 𝐶 ∈ ( 𝐶 𝐿 𝐷 ) ) → 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) )
23 22 ex ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐶 ∈ ( 𝐶 𝐿 𝐷 ) → 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ) )
24 23 orim1d ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( ( 𝐶 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) → ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) ) )
25 19 24 mpd ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
26 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) ) → ( 𝐵 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
27 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) ) → 𝐺 ∈ TarskiG )
28 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) ) → 𝐴 ∈ 𝑃 )
29 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) ) → 𝐶 ∈ 𝑃 )
30 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) ) → 𝐷 ∈ 𝑃 )
31 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) ) → 𝐵 ∈ 𝑃 )
32 simpr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) ) → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
33 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐺 ∈ TarskiG )
34 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐴 ∈ 𝑃 )
35 7 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐶 ∈ 𝑃 )
36 6 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐵 ∈ 𝑃 )
37 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐴 ≠ 𝐶 )
38 9 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) )
39 1 3 2 33 36 35 38 tglngne ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐵 ≠ 𝐶 )
40 39 necomd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐶 ≠ 𝐵 )
41 1 2 3 33 35 36 34 40 38 lncom ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) )
42 1 2 3 33 34 35 36 37 41 40 lnrot2 ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) ) → 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) )
44 1 3 2 4 6 7 9 tglngne ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
45 44 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) ) → 𝐵 ≠ 𝐶 )
46 1 2 3 27 28 29 30 31 32 43 45 ncolncol ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) ) → ¬ ( 𝐵 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
47 26 46 condan ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
48 25 47 pm2.61dane ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )