Theorem dochexmidlem8

Description: Lemma for dochexmid . The contradiction of dochexmidlem6 and dochexmidlem7 shows that there can be no atom p that is not in X + ( ._|_X ) , which is therefore the whole atom space. (Contributed by NM, 15-Jan-2015)

	Ref	Expression
Hypotheses	dochexmidlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dochexmidlem1.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	dochexmidlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dochexmidlem1.v	$$⊢V={\mathrm{Base}}_U$$
	dochexmidlem1.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
	dochexmidlem1.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	dochexmidlem1.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	dochexmidlem1.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
	dochexmidlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dochexmidlem1.x	$$⊢\phi \to X\in S$$
	dochexmidlem8.z	$$⊢\underset{\dot{}}{0}=0_U$$
	dochexmidlem8.xn	$$⊢\phi \to X\ne \left\{\underset{\dot{}}{0}\right\}$$
	dochexmidlem8.c	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X$$
Assertion	dochexmidlem8	$$⊢\phi \to X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)=V$$

Proof

Step	Hyp	Ref	Expression
1		dochexmidlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochexmidlem1.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		dochexmidlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		dochexmidlem1.v	$$⊢V={\mathrm{Base}}_U$$
5		dochexmidlem1.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
6		dochexmidlem1.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
7		dochexmidlem1.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
8		dochexmidlem1.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
9		dochexmidlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		dochexmidlem1.x	$$⊢\phi \to X\in S$$
11		dochexmidlem8.z	$$⊢\underset{\dot{}}{0}=0_U$$
12		dochexmidlem8.xn	$$⊢\phi \to X\ne \left\{\underset{\dot{}}{0}\right\}$$
13		dochexmidlem8.c	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X$$
14		nonconne	$$⊢\neg \left(X=X\wedge X\ne X\right)$$
15	1 3 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
16	4 5	lssss	$$⊢X\in S\to X\subseteq V$$
17	10 16	syl	$$⊢\phi \to X\subseteq V$$
18	1 3 4 5 2	dochlss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\subseteq V\right)\to \underset{\dot{}}{\perp }\left(X\right)\in S$$
19	9 17 18	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(X\right)\in S$$
20	5 7	lsmcl	$$⊢\left(U\in \mathrm{LMod}\wedge X\in S\wedge \underset{\dot{}}{\perp }\left(X\right)\in S\right)\to X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\in S$$
21	15 10 19 20	syl3anc	$$⊢\phi \to X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\in S$$
22	4 5	lssss	$$⊢X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\in S\to X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\subseteq V$$
23	21 22	syl	$$⊢\phi \to X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\subseteq V$$
24	15	adantr	$$⊢\left(\phi \wedge \left(X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\subseteq V\wedge X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\ne V\right)\right)\to U\in \mathrm{LMod}$$
25	21	adantr	$$⊢\left(\phi \wedge \left(X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\subseteq V\wedge X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\ne V\right)\right)\to X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\in S$$
26	4 5	lss1	$$⊢U\in \mathrm{LMod}\to V\in S$$
27	15 26	syl	$$⊢\phi \to V\in S$$
28	27	adantr	$$⊢\left(\phi \wedge \left(X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\subseteq V\wedge X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\ne V\right)\right)\to V\in S$$
29		df-pss	$$⊢X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\subset V\leftrightarrow \left(X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\subseteq V\wedge X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\ne V\right)$$
30	29	biimpri	$$⊢\left(X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\subseteq V\wedge X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\ne V\right)\to X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\subset V$$
31	30	adantl	$$⊢\left(\phi \wedge \left(X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\subseteq V\wedge X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\ne V\right)\right)\to X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\subset V$$
32	5 8 24 25 28 31	lpssat	$$⊢\left(\phi \wedge \left(X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\subseteq V\wedge X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\ne V\right)\right)\to \exists p\in A\left(p\subseteq V\wedge \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)$$
33	32	ex	$$⊢\phi \to \left(\left(X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\subseteq V\wedge X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\ne V\right)\to \exists p\in A\left(p\subseteq V\wedge \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)\right)$$
34	9	3ad2ant1	$$⊢\left(\phi \wedge p\in A\wedge \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
35	10	3ad2ant1	$$⊢\left(\phi \wedge p\in A\wedge \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)\to X\in S$$
36		simp2	$$⊢\left(\phi \wedge p\in A\wedge \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)\to p\in A$$
37		eqid	$$⊢X\underset{\dot{}}{\oplus }p=X\underset{\dot{}}{\oplus }p$$
38	12	3ad2ant1	$$⊢\left(\phi \wedge p\in A\wedge \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)\to X\ne \left\{\underset{\dot{}}{0}\right\}$$
39	13	3ad2ant1	$$⊢\left(\phi \wedge p\in A\wedge \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X$$
40		simp3	$$⊢\left(\phi \wedge p\in A\wedge \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)\to \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$
41	1 2 3 4 5 6 7 8 34 35 36 11 37 38 39 40	dochexmidlem6	$$⊢\left(\phi \wedge p\in A\wedge \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)\to X\underset{\dot{}}{\oplus }p=X$$
42	1 2 3 4 5 6 7 8 34 35 36 11 37 38 39 40	dochexmidlem7	$$⊢\left(\phi \wedge p\in A\wedge \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)\to X\underset{\dot{}}{\oplus }p\ne X$$
43	41 42	pm2.21ddne	$$⊢\left(\phi \wedge p\in A\wedge \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)\to \left(X=X\wedge X\ne X\right)$$
44	43	3adant3l	$$⊢\left(\phi \wedge p\in A\wedge \left(p\subseteq V\wedge \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)\right)\to \left(X=X\wedge X\ne X\right)$$
45	44	rexlimdv3a	$$⊢\phi \to \left(\exists p\in A\left(p\subseteq V\wedge \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)\to \left(X=X\wedge X\ne X\right)\right)$$
46	33 45	syld	$$⊢\phi \to \left(\left(X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\subseteq V\wedge X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\ne V\right)\to \left(X=X\wedge X\ne X\right)\right)$$
47	23 46	mpand	$$⊢\phi \to \left(X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\ne V\to \left(X=X\wedge X\ne X\right)\right)$$
48	47	necon1bd	$$⊢\phi \to \left(\neg \left(X=X\wedge X\ne X\right)\to X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)=V\right)$$
49	14 48	mpi	$$⊢\phi \to X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)=V$$