tglineneq

Description: Given three non-colinear points, build two different lines. (Contributed by Thierry Arnoux, 6-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)$
Assertion	tglineneq	$⊢ φ \to A L B \neq C L 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		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	1 2 3 4 5 6 7 9	ncolne1	$⊢ φ \to A \neq B$
11	1 2 3 4 5 6 10	tglinerflx1	$⊢ φ \to A \in (A L B)$
12		simplr	$⊢ ((φ \land C = D) \land A \in (C L D)) \to C = D$
13	4	adantr	$⊢ (φ \land A \in (C L D)) \to G \in 𝒢_{Tarski}$
14	7	adantr	$⊢ (φ \land A \in (C L D)) \to C \in P$
15	8	adantr	$⊢ (φ \land A \in (C L D)) \to D \in P$
16		simpr	$⊢ (φ \land A \in (C L D)) \to A \in (C L D)$
17	1 3 2 13 14 15 16	tglngne	$⊢ (φ \land A \in (C L D)) \to C \neq D$
18	17	adantlr	$⊢ ((φ \land C = D) \land A \in (C L D)) \to C \neq D$
19	18	neneqd	$⊢ ((φ \land C = D) \land A \in (C L D)) \to \neg C = D$
20	12 19	pm2.65da	$⊢ (φ \land C = D) \to \neg A \in (C L D)$
21		nelne1	$⊢ (A \in (A L B) \land \neg A \in (C L D)) \to A L B \neq C L D$
22	11 20 21	syl2an2r	$⊢ (φ \land C = D) \to A L B \neq C L D$
23	4	ad2antrr	$⊢ ((φ \land C \neq D) \land A L B = C L D) \to G \in 𝒢_{Tarski}$
24	6	ad2antrr	$⊢ ((φ \land C \neq D) \land A L B = C L D) \to B \in P$
25	7	ad2antrr	$⊢ ((φ \land C \neq D) \land A L B = C L D) \to C \in P$
26	5	ad2antrr	$⊢ ((φ \land C \neq D) \land A L B = C L D) \to A \in P$
27		pm2.46	$⊢ \neg (A \in (B L C) \lor B = C) \to \neg B = C$
28	9 27	syl	$⊢ φ \to \neg B = C$
29	28	neqned	$⊢ φ \to B \neq C$
30	29	ad2antrr	$⊢ ((φ \land C \neq D) \land A L B = C L D) \to B \neq C$
31	8	ad2antrr	$⊢ ((φ \land C \neq D) \land A L B = C L D) \to D \in P$
32		simplr	$⊢ ((φ \land C \neq D) \land A L B = C L D) \to C \neq D$
33	1 2 3 23 25 31 32	tglinerflx1	$⊢ ((φ \land C \neq D) \land A L B = C L D) \to C \in (C L D)$
34		simpr	$⊢ ((φ \land C \neq D) \land A L B = C L D) \to A L B = C L D$
35	33 34	eleqtrrd	$⊢ ((φ \land C \neq D) \land A L B = C L D) \to C \in (A L B)$
36	1 3 2 23 26 24 35	tglngne	$⊢ ((φ \land C \neq D) \land A L B = C L D) \to A \neq B$
37	1 2 3 23 24 25 26 30 35 36	lnrot1	$⊢ ((φ \land C \neq D) \land A L B = C L D) \to A \in (B L C)$
38	37	orcd	$⊢ ((φ \land C \neq D) \land A L B = C L D) \to (A \in (B L C) \lor B = C)$
39	9	ad2antrr	$⊢ ((φ \land C \neq D) \land A L B = C L D) \to \neg (A \in (B L C) \lor B = C)$
40	38 39	pm2.65da	$⊢ (φ \land C \neq D) \to \neg A L B = C L D$
41	40	neqned	$⊢ (φ \land C \neq D) \to A L B \neq C L D$
42	22 41	pm2.61dane	$⊢ φ \to A L B \neq C L D$

Metamath Proof Explorer

Theorem tglineneq

Proof