Metamath Proof Explorer


Theorem coltr

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

Ref Expression
Hypotheses tglineintmo.p P = Base G
tglineintmo.i I = Itv G
tglineintmo.l L = Line 𝒢 G
tglineintmo.g φ G 𝒢 Tarski
coltr.a φ A P
coltr.b φ B P
coltr.c φ C P
coltr.d φ D P
coltr.1 φ A B L C
coltr.2 φ B C L D C = D
Assertion coltr φ A C L D C = D

Proof

Step Hyp Ref Expression
1 tglineintmo.p P = Base G
2 tglineintmo.i I = Itv G
3 tglineintmo.l L = Line 𝒢 G
4 tglineintmo.g φ G 𝒢 Tarski
5 coltr.a φ A P
6 coltr.b φ B P
7 coltr.c φ C P
8 coltr.d φ D P
9 coltr.1 φ A B L C
10 coltr.2 φ B C L D C = D
11 4 adantr φ C D G 𝒢 Tarski
12 7 adantr φ C D C P
13 8 adantr φ C D D P
14 simpr φ C D C D
15 1 2 3 11 12 13 14 tglinerflx1 φ C D C C L D
16 15 ex φ C D C C L D
17 16 necon1bd φ ¬ C C L D C = D
18 17 orrd φ C C L D C = D
19 18 adantr φ A = C C C L D C = D
20 simplr φ A = C C C L D A = C
21 simpr φ A = C C C L D C C L D
22 20 21 eqeltrd φ A = C C C L D A C L D
23 22 ex φ A = C C C L D A C L D
24 23 orim1d φ A = C C C L D C = D A C L D C = D
25 19 24 mpd φ A = C A C L D C = D
26 10 ad2antrr φ A C ¬ A C L D C = D B C L D C = D
27 4 ad2antrr φ A C ¬ A C L D C = D G 𝒢 Tarski
28 5 ad2antrr φ A C ¬ A C L D C = D A P
29 7 ad2antrr φ A C ¬ A C L D C = D C P
30 8 ad2antrr φ A C ¬ A C L D C = D D P
31 6 ad2antrr φ A C ¬ A C L D C = D B P
32 simpr φ A C ¬ A C L D C = D ¬ A C L D C = D
33 4 adantr φ A C G 𝒢 Tarski
34 5 adantr φ A C A P
35 7 adantr φ A C C P
36 6 adantr φ A C B P
37 simpr φ A C A C
38 9 adantr φ A C A B L C
39 1 3 2 33 36 35 38 tglngne φ A C B C
40 39 necomd φ A C C B
41 1 2 3 33 35 36 34 40 38 lncom φ A C A C L B
42 1 2 3 33 34 35 36 37 41 40 lnrot2 φ A C B A L C
43 42 adantr φ A C ¬ A C L D C = D B A L C
44 1 3 2 4 6 7 9 tglngne φ B C
45 44 ad2antrr φ A C ¬ A C L D C = D B C
46 1 2 3 27 28 29 30 31 32 43 45 ncolncol φ A C ¬ A C L D C = D ¬ B C L D C = D
47 26 46 condan φ A C A C L D C = D
48 25 47 pm2.61dane φ A C L D C = D