tglowdim2ln

Description: There is always one point outside of any line. Theorem 6.25 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 16-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}$
	tglowdim2l.1	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
	tglowdim2ln.a	$⊢ φ \to A \in P$
	tglowdim2ln.b	$⊢ φ \to B \in P$
	tglowdim2ln.1	$⊢ φ \to A \neq B$
Assertion	tglowdim2ln	$⊢ φ \to \exists c \in P \neg c \in (A L B)$

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		tglowdim2l.1	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
6		tglowdim2ln.a	$⊢ φ \to A \in P$
7		tglowdim2ln.b	$⊢ φ \to B \in P$
8		tglowdim2ln.1	$⊢ φ \to A \neq B$
9	1 2 3 4 5	tglowdim2l	$⊢ φ \to \exists a \in P \exists b \in P \exists z \in P \neg (z \in (a L b) \lor a = b)$
10	9	adantr	$⊢ (φ \land \forall c \in P c \in (A L B)) \to \exists a \in P \exists b \in P \exists z \in P \neg (z \in (a L b) \lor a = b)$
11		eleq1w	$⊢ c = z \to (c \in (A L B) \leftrightarrow z \in (A L B))$
12		simpllr	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to \forall c \in P c \in (A L B)$
13		simplr3	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to z \in P$
14	11 12 13	rspcdva	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to z \in (A L B)$
15	4	ad3antrrr	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to G \in 𝒢_{Tarski}$
16		simplr1	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to a \in P$
17		simplr2	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to b \in P$
18		simpr	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to \neg a = b$
19	18	neqned	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to a \neq b$
20	6	ad3antrrr	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to A \in P$
21	7	ad3antrrr	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to B \in P$
22	8	ad3antrrr	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to A \neq B$
23	1 2 3 15 20 21 22	tgelrnln	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to A L B \in ran L$
24		eleq1w	$⊢ c = a \to (c \in (A L B) \leftrightarrow a \in (A L B))$
25	24 12 16	rspcdva	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to a \in (A L B)$
26		eleq1w	$⊢ c = b \to (c \in (A L B) \leftrightarrow b \in (A L B))$
27	26 12 17	rspcdva	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to b \in (A L B)$
28	1 2 3 15 16 17 19 19 23 25 27	tglinethru	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to A L B = a L b$
29	14 28	eleqtrd	$⊢ (((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \land \neg a = b) \to z \in (a L b)$
30	29	ex	$⊢ ((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \to (\neg a = b \to z \in (a L b))$
31	30	orrd	$⊢ ((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \to (a = b \lor z \in (a L b))$
32	31	orcomd	$⊢ ((φ \land \forall c \in P c \in (A L B)) \land (a \in P \land b \in P \land z \in P)) \to (z \in (a L b) \lor a = b)$
33	32	ralrimivvva	$⊢ (φ \land \forall c \in P c \in (A L B)) \to \forall a \in P \forall b \in P \forall z \in P (z \in (a L b) \lor a = b)$
34		dfral2	$⊢ \forall z \in P (z \in (a L b) \lor a = b) \leftrightarrow \neg \exists z \in P \neg (z \in (a L b) \lor a = b)$
35	34	ralbii	$⊢ \forall b \in P \forall z \in P (z \in (a L b) \lor a = b) \leftrightarrow \forall b \in P \neg \exists z \in P \neg (z \in (a L b) \lor a = b)$
36		ralnex	$⊢ \forall b \in P \neg \exists z \in P \neg (z \in (a L b) \lor a = b) \leftrightarrow \neg \exists b \in P \exists z \in P \neg (z \in (a L b) \lor a = b)$
37	35 36	bitri	$⊢ \forall b \in P \forall z \in P (z \in (a L b) \lor a = b) \leftrightarrow \neg \exists b \in P \exists z \in P \neg (z \in (a L b) \lor a = b)$
38	37	ralbii	$⊢ \forall a \in P \forall b \in P \forall z \in P (z \in (a L b) \lor a = b) \leftrightarrow \forall a \in P \neg \exists b \in P \exists z \in P \neg (z \in (a L b) \lor a = b)$
39		ralnex	$⊢ \forall a \in P \neg \exists b \in P \exists z \in P \neg (z \in (a L b) \lor a = b) \leftrightarrow \neg \exists a \in P \exists b \in P \exists z \in P \neg (z \in (a L b) \lor a = b)$
40	38 39	bitri	$⊢ \forall a \in P \forall b \in P \forall z \in P (z \in (a L b) \lor a = b) \leftrightarrow \neg \exists a \in P \exists b \in P \exists z \in P \neg (z \in (a L b) \lor a = b)$
41	33 40	sylib	$⊢ (φ \land \forall c \in P c \in (A L B)) \to \neg \exists a \in P \exists b \in P \exists z \in P \neg (z \in (a L b) \lor a = b)$
42	10 41	pm2.65da	$⊢ φ \to \neg \forall c \in P c \in (A L B)$
43		rexnal	$⊢ \exists c \in P \neg c \in (A L B) \leftrightarrow \neg \forall c \in P c \in (A L B)$
44	42 43	sylibr	$⊢ φ \to \exists c \in P \neg c \in (A L B)$

Metamath Proof Explorer

Theorem tglowdim2ln

Proof