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	bilanri	$$⊢\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$$
31	5 8 24 25 28 30	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)$$
32	31	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)$$
33	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)$$
34	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$$
35		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$$
36		eqid	$$⊢X\underset{\dot{}}{\oplus }p=X\underset{\dot{}}{\oplus }p$$
37	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\}$$
38	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$$
39		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)$$
40	1 2 3 4 5 6 7 8 33 34 35 11 36 37 38 39	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$$
41	1 2 3 4 5 6 7 8 33 34 35 11 36 37 38 39	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$$
42	40 41	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)$$
43	42	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)$$
44	43	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)$$
45	32 44	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)$$
46	23 45	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)$$
47	46	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)$$
48	14 47	mpi	$$⊢\phi \to X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)=V$$