coltr3

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	$⊢ φ \to G \in 𝒢_{Tarski}$
	coltr.a	$⊢ φ \to A \in P$
	coltr.b	$⊢ φ \to B \in P$
	coltr.c	$⊢ φ \to C \in P$
	coltr.d	$⊢ φ \to D \in P$
	coltr.1	$⊢ φ \to A \in (B L C)$
	coltr3.2	$⊢ φ \to D \in (A I C)$
Assertion	coltr3	$⊢ φ \to D \in (B L C)$

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	$⊢ φ \to G \in 𝒢_{Tarski}$
5		coltr.a	$⊢ φ \to A \in P$
6		coltr.b	$⊢ φ \to B \in P$
7		coltr.c	$⊢ φ \to C \in P$
8		coltr.d	$⊢ φ \to D \in P$
9		coltr.1	$⊢ φ \to A \in (B L C)$
10		coltr3.2	$⊢ φ \to D \in (A I C)$
11		eqid	$⊢ dist (G) = dist (G)$
12	4	adantr	$⊢ (φ \land A = C) \to G \in 𝒢_{Tarski}$
13	5	adantr	$⊢ (φ \land A = C) \to A \in P$
14	8	adantr	$⊢ (φ \land A = C) \to D \in P$
15	10	adantr	$⊢ (φ \land A = C) \to D \in (A I C)$
16		simpr	$⊢ (φ \land A = C) \to A = C$
17	16	oveq2d	$⊢ (φ \land A = C) \to A I A = A I C$
18	15 17	eleqtrrd	$⊢ (φ \land A = C) \to D \in (A I A)$
19	1 11 2 12 13 14 18	axtgbtwnid	$⊢ (φ \land A = C) \to A = D$
20	9	adantr	$⊢ (φ \land A = C) \to A \in (B L C)$
21	19 20	eqeltrrd	$⊢ (φ \land A = C) \to D \in (B L C)$
22	4	adantr	$⊢ (φ \land A \neq C) \to G \in 𝒢_{Tarski}$
23	5	adantr	$⊢ (φ \land A \neq C) \to A \in P$
24	7	adantr	$⊢ (φ \land A \neq C) \to C \in P$
25	8	adantr	$⊢ (φ \land A \neq C) \to D \in P$
26		simpr	$⊢ (φ \land A \neq C) \to A \neq C$
27	10	adantr	$⊢ (φ \land A \neq C) \to D \in (A I C)$
28	1 2 3 22 23 24 25 26 27	btwnlng1	$⊢ (φ \land A \neq C) \to D \in (A L C)$
29	26	necomd	$⊢ (φ \land A \neq C) \to C \neq A$
30	6	adantr	$⊢ (φ \land A \neq C) \to B \in P$
31	1 3 2 4 6 7 9	tglngne	$⊢ φ \to B \neq C$
32	31	adantr	$⊢ (φ \land A \neq C) \to B \neq C$
33	9	adantr	$⊢ (φ \land A \neq C) \to A \in (B L C)$
34	1 2 3 22 24 23 30 29 33 32	lnrot1	$⊢ (φ \land A \neq C) \to B \in (C L A)$
35	1 2 3 22 24 23 29 30 32 34	tglineelsb2	$⊢ (φ \land A \neq C) \to C L A = C L B$
36	1 2 3 22 23 24 26	tglinecom	$⊢ (φ \land A \neq C) \to A L C = C L A$
37	1 2 3 4 6 7 31	tglinecom	$⊢ φ \to B L C = C L B$
38	37	adantr	$⊢ (φ \land A \neq C) \to B L C = C L B$
39	35 36 38	3eqtr4d	$⊢ (φ \land A \neq C) \to A L C = B L C$
40	28 39	eleqtrd	$⊢ (φ \land A \neq C) \to D \in (B L C)$
41	21 40	pm2.61dane	$⊢ φ \to D \in (B L C)$

Metamath Proof Explorer

Theorem coltr3

Proof