Theorem dochexmidlem6

Description: Lemma for dochexmid . (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$$
	dochexmidlem6.pp	$$⊢\phi \to p\in A$$
	dochexmidlem6.z	$$⊢\underset{\dot{}}{0}=0_U$$
	dochexmidlem6.m	$$⊢M=X\underset{\dot{}}{\oplus }p$$
	dochexmidlem6.xn	$$⊢\phi \to X\ne \left\{\underset{\dot{}}{0}\right\}$$
	dochexmidlem6.c	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X$$
	dochexmidlem6.pl	$$⊢\phi \to \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$
Assertion	dochexmidlem6	$$⊢\phi \to M=X$$

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		dochexmidlem6.pp	$$⊢\phi \to p\in A$$
12		dochexmidlem6.z	$$⊢\underset{\dot{}}{0}=0_U$$
13		dochexmidlem6.m	$$⊢M=X\underset{\dot{}}{\oplus }p$$
14		dochexmidlem6.xn	$$⊢\phi \to X\ne \left\{\underset{\dot{}}{0}\right\}$$
15		dochexmidlem6.c	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X$$
16		dochexmidlem6.pl	$$⊢\phi \to \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$
17	1 2 3 4 5 6 7 8 9 10 11 12 13 14 16	dochexmidlem5	$$⊢\phi \to \underset{\dot{}}{\perp }\left(X\right)\cap M=\left\{\underset{\dot{}}{0}\right\}$$
18	17	fveq2d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\cap M\right)=\underset{\dot{}}{\perp }\left(\left\{\underset{\dot{}}{0}\right\}\right)$$
19	1 3 2 4 12	doch0	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{\perp }\left(\left\{\underset{\dot{}}{0}\right\}\right)=V$$
20	9 19	syl	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{\underset{\dot{}}{0}\right\}\right)=V$$
21	18 20	eqtrd	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\cap M\right)=V$$
22	21	ineq1d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\cap M\right)\cap M=V\cap M$$
23		eqid	$$⊢\mathrm{DIsoH}\left(K\right)\left(W\right)=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
24	4 5	lssss	$$⊢X\in S\to X\subseteq V$$
25	10 24	syl	$$⊢\phi \to X\subseteq V$$
26	1 3 4 2	dochssv	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\subseteq V\right)\to \underset{\dot{}}{\perp }\left(X\right)\subseteq V$$
27	9 25 26	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(X\right)\subseteq V$$
28	1 23 3 4 2	dochcl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \underset{\dot{}}{\perp }\left(X\right)\subseteq V\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
29	9 27 28	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
30	15 29	eqeltrrd	$$⊢\phi \to X\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
31	1 23 3 7 8 9 30 11	dihsmatrn	$$⊢\phi \to X\underset{\dot{}}{\oplus }p\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
32	13 31	eqeltrid	$$⊢\phi \to M\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
33	1 3 23 5	dihrnlss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge M\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)\right)\to M\in S$$
34	9 32 33	syl2anc	$$⊢\phi \to M\in S$$
35	1 3 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
36	5 8 35 11	lsatlssel	$$⊢\phi \to p\in S$$
37	5 7	lsmcl	$$⊢\left(U\in \mathrm{LMod}\wedge X\in S\wedge p\in S\right)\to X\underset{\dot{}}{\oplus }p\in S$$
38	35 10 36 37	syl3anc	$$⊢\phi \to X\underset{\dot{}}{\oplus }p\in S$$
39	4 5	lssss	$$⊢X\underset{\dot{}}{\oplus }p\in S\to X\underset{\dot{}}{\oplus }p\subseteq V$$
40	38 39	syl	$$⊢\phi \to X\underset{\dot{}}{\oplus }p\subseteq V$$
41	13 40	eqsstrid	$$⊢\phi \to M\subseteq V$$
42	1 23 3 4 2 9 41	dochoccl	$$⊢\phi \to \left(M\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(M\right)\right)=M\right)$$
43	32 42	mpbid	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(M\right)\right)=M$$
44	5	lsssssubg	$$⊢U\in \mathrm{LMod}\to S\subseteq \mathrm{SubGrp}\left(U\right)$$
45	35 44	syl	$$⊢\phi \to S\subseteq \mathrm{SubGrp}\left(U\right)$$
46	45 10	sseldd	$$⊢\phi \to X\in \mathrm{SubGrp}\left(U\right)$$
47	45 36	sseldd	$$⊢\phi \to p\in \mathrm{SubGrp}\left(U\right)$$
48	7	lsmub1	$$⊢\left(X\in \mathrm{SubGrp}\left(U\right)\wedge p\in \mathrm{SubGrp}\left(U\right)\right)\to X\subseteq X\underset{\dot{}}{\oplus }p$$
49	46 47 48	syl2anc	$$⊢\phi \to X\subseteq X\underset{\dot{}}{\oplus }p$$
50	49 13	sseqtrrdi	$$⊢\phi \to X\subseteq M$$
51	1 3 5 2 9 10 34 43 50	dihoml4	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\cap M\right)\cap M=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)$$
52		sseqin2	$$⊢M\subseteq V\leftrightarrow V\cap M=M$$
53	41 52	sylib	$$⊢\phi \to V\cap M=M$$
54	22 51 53	3eqtr3rd	$$⊢\phi \to M=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)$$
55	54 15	eqtrd	$$⊢\phi \to M=X$$