ncolncol

Description: Deduce non-colinearity from non-colinearity and colinearity. (Contributed by Thierry Arnoux, 27-Aug-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}$
	tglineinteq.a	$⊢ φ \to A \in P$
	tglineinteq.b	$⊢ φ \to B \in P$
	tglineinteq.c	$⊢ φ \to C \in P$
	tglineinteq.d	$⊢ φ \to D \in P$
	tglineinteq.e	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
	ncolncol.1	$⊢ φ \to D \in (A L B)$
	ncolncol.2	$⊢ φ \to D \neq B$
Assertion	ncolncol	$⊢ φ \to \neg (D \in (B L C) \lor B = 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		tglineinteq.a	$⊢ φ \to A \in P$
6		tglineinteq.b	$⊢ φ \to B \in P$
7		tglineinteq.c	$⊢ φ \to C \in P$
8		tglineinteq.d	$⊢ φ \to D \in P$
9		tglineinteq.e	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
10		ncolncol.1	$⊢ φ \to D \in (A L B)$
11		ncolncol.2	$⊢ φ \to D \neq B$
12	4	adantr	$⊢ (φ \land (D \in (B L C) \lor B = C)) \to G \in 𝒢_{Tarski}$
13	5	adantr	$⊢ (φ \land (D \in (B L C) \lor B = C)) \to A \in P$
14	6	adantr	$⊢ (φ \land (D \in (B L C) \lor B = C)) \to B \in P$
15	7	adantr	$⊢ (φ \land (D \in (B L C) \lor B = C)) \to C \in P$
16	4	ad2antrr	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land C \in (D L B)) \to G \in 𝒢_{Tarski}$
17	5	ad2antrr	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land C \in (D L B)) \to A \in P$
18	6	ad2antrr	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land C \in (D L B)) \to B \in P$
19	7	ad2antrr	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land C \in (D L B)) \to C \in P$
20	1 3 2 4 5 6 10	tglngne	$⊢ φ \to A \neq B$
21	20	ad2antrr	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land C \in (D L B)) \to A \neq B$
22	8	ad2antrr	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land C \in (D L B)) \to D \in P$
23	11	necomd	$⊢ φ \to B \neq D$
24	23	ad2antrr	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land C \in (D L B)) \to B \neq D$
25		simpr	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land C \in (D L B)) \to C \in (D L B)$
26	1 2 3 16 18 22 19 24 25	lncom	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land C \in (D L B)) \to C \in (B L D)$
27	20	necomd	$⊢ φ \to B \neq A$
28	1 2 3 4 6 5 8 27 10	lncom	$⊢ φ \to D \in (B L A)$
29	1 2 3 4 6 5 27 8 11 28	tglineelsb2	$⊢ φ \to B L A = B L D$
30	29	ad2antrr	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land C \in (D L B)) \to B L A = B L D$
31	26 30	eleqtrrd	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land C \in (D L B)) \to C \in (B L A)$
32	1 2 3 16 17 18 19 21 31	lncom	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land C \in (D L B)) \to C \in (A L B)$
33	32	orcd	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land C \in (D L B)) \to (C \in (A L B) \lor A = B)$
34		simpr	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land D = B) \to D = B$
35	11	ad2antrr	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land D = B) \to D \neq B$
36	34 35	pm2.21ddne	$⊢ ((φ \land (D \in (B L C) \lor B = C)) \land D = B) \to (C \in (A L B) \lor A = B)$
37	8	adantr	$⊢ (φ \land (D \in (B L C) \lor B = C)) \to D \in P$
38		simpr	$⊢ (φ \land (D \in (B L C) \lor B = C)) \to (D \in (B L C) \lor B = C)$
39	1 3 2 12 14 15 37 38	colrot2	$⊢ (φ \land (D \in (B L C) \lor B = C)) \to (C \in (D L B) \lor D = B)$
40	33 36 39	mpjaodan	$⊢ (φ \land (D \in (B L C) \lor B = C)) \to (C \in (A L B) \lor A = B)$
41	1 3 2 12 13 14 15 40	colrot1	$⊢ (φ \land (D \in (B L C) \lor B = C)) \to (A \in (B L C) \lor B = C)$
42	9 41	mtand	$⊢ φ \to \neg (D \in (B L C) \lor B = C)$

Metamath Proof Explorer

Theorem ncolncol

Proof