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	$⊢ φ \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)$
	coltr.2	$⊢ φ \to (B \in (C L D) \lor C = D)$
Assertion	coltr	$⊢ φ \to (A \in (C L D) \lor 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	$⊢ φ \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		coltr.2	$⊢ φ \to (B \in (C L D) \lor C = D)$
11	4	adantr	$⊢ (φ \land C \neq D) \to G \in 𝒢_{Tarski}$
12	7	adantr	$⊢ (φ \land C \neq D) \to C \in P$
13	8	adantr	$⊢ (φ \land C \neq D) \to D \in P$
14		simpr	$⊢ (φ \land C \neq D) \to C \neq D$
15	1 2 3 11 12 13 14	tglinerflx1	$⊢ (φ \land C \neq D) \to C \in (C L D)$
16	15	ex	$⊢ φ \to (C \neq D \to C \in (C L D))$
17	16	necon1bd	$⊢ φ \to (\neg C \in (C L D) \to C = D)$
18	17	orrd	$⊢ φ \to (C \in (C L D) \lor C = D)$
19	18	adantr	$⊢ (φ \land A = C) \to (C \in (C L D) \lor C = D)$
20		simplr	$⊢ ((φ \land A = C) \land C \in (C L D)) \to A = C$
21		simpr	$⊢ ((φ \land A = C) \land C \in (C L D)) \to C \in (C L D)$
22	20 21	eqeltrd	$⊢ ((φ \land A = C) \land C \in (C L D)) \to A \in (C L D)$
23	22	ex	$⊢ (φ \land A = C) \to (C \in (C L D) \to A \in (C L D))$
24	23	orim1d	$⊢ (φ \land A = C) \to ((C \in (C L D) \lor C = D) \to (A \in (C L D) \lor C = D))$
25	19 24	mpd	$⊢ (φ \land A = C) \to (A \in (C L D) \lor C = D)$
26	10	ad2antrr	$⊢ ((φ \land A \neq C) \land \neg (A \in (C L D) \lor C = D)) \to (B \in (C L D) \lor C = D)$
27	4	ad2antrr	$⊢ ((φ \land A \neq C) \land \neg (A \in (C L D) \lor C = D)) \to G \in 𝒢_{Tarski}$
28	5	ad2antrr	$⊢ ((φ \land A \neq C) \land \neg (A \in (C L D) \lor C = D)) \to A \in P$
29	7	ad2antrr	$⊢ ((φ \land A \neq C) \land \neg (A \in (C L D) \lor C = D)) \to C \in P$
30	8	ad2antrr	$⊢ ((φ \land A \neq C) \land \neg (A \in (C L D) \lor C = D)) \to D \in P$
31	6	ad2antrr	$⊢ ((φ \land A \neq C) \land \neg (A \in (C L D) \lor C = D)) \to B \in P$
32		simpr	$⊢ ((φ \land A \neq C) \land \neg (A \in (C L D) \lor C = D)) \to \neg (A \in (C L D) \lor C = D)$
33	4	adantr	$⊢ (φ \land A \neq C) \to G \in 𝒢_{Tarski}$
34	5	adantr	$⊢ (φ \land A \neq C) \to A \in P$
35	7	adantr	$⊢ (φ \land A \neq C) \to C \in P$
36	6	adantr	$⊢ (φ \land A \neq C) \to B \in P$
37		simpr	$⊢ (φ \land A \neq C) \to A \neq C$
38	9	adantr	$⊢ (φ \land A \neq C) \to A \in (B L C)$
39	1 3 2 33 36 35 38	tglngne	$⊢ (φ \land A \neq C) \to B \neq C$
40	39	necomd	$⊢ (φ \land A \neq C) \to C \neq B$
41	1 2 3 33 35 36 34 40 38	lncom	$⊢ (φ \land A \neq C) \to A \in (C L B)$
42	1 2 3 33 34 35 36 37 41 40	lnrot2	$⊢ (φ \land A \neq C) \to B \in (A L C)$
43	42	adantr	$⊢ ((φ \land A \neq C) \land \neg (A \in (C L D) \lor C = D)) \to B \in (A L C)$
44	1 3 2 4 6 7 9	tglngne	$⊢ φ \to B \neq C$
45	44	ad2antrr	$⊢ ((φ \land A \neq C) \land \neg (A \in (C L D) \lor C = D)) \to B \neq C$
46	1 2 3 27 28 29 30 31 32 43 45	ncolncol	$⊢ ((φ \land A \neq C) \land \neg (A \in (C L D) \lor C = D)) \to \neg (B \in (C L D) \lor C = D)$
47	26 46	condan	$⊢ (φ \land A \neq C) \to (A \in (C L D) \lor C = D)$
48	25 47	pm2.61dane	$⊢ φ \to (A \in (C L D) \lor C = D)$

Metamath Proof Explorer

Theorem coltr

Proof