Theorem dochexmidlem2

Description: Lemma for dochexmid . (Contributed by NM, 14-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$$
	dochexmidlem2.pp	$$⊢\phi \to p\in A$$
	dochexmidlem2.qq	$$⊢\phi \to q\in A$$
	dochexmidlem2.rr	$$⊢\phi \to r\in A$$
	dochexmidlem2.ql	$$⊢\phi \to q\subseteq \underset{\dot{}}{\perp }\left(X\right)$$
	dochexmidlem2.rl	$$⊢\phi \to r\subseteq X$$
	dochexmidlem2.pl	$$⊢\phi \to p\subseteq r\underset{\dot{}}{\oplus }q$$
Assertion	dochexmidlem2	$$⊢\phi \to p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$

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		dochexmidlem2.pp	$$⊢\phi \to p\in A$$
12		dochexmidlem2.qq	$$⊢\phi \to q\in A$$
13		dochexmidlem2.rr	$$⊢\phi \to r\in A$$
14		dochexmidlem2.ql	$$⊢\phi \to q\subseteq \underset{\dot{}}{\perp }\left(X\right)$$
15		dochexmidlem2.rl	$$⊢\phi \to r\subseteq X$$
16		dochexmidlem2.pl	$$⊢\phi \to p\subseteq r\underset{\dot{}}{\oplus }q$$
17	1 3 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
18	5	lsssssubg	$$⊢U\in \mathrm{LMod}\to S\subseteq \mathrm{SubGrp}\left(U\right)$$
19	17 18	syl	$$⊢\phi \to S\subseteq \mathrm{SubGrp}\left(U\right)$$
20	19 10	sseldd	$$⊢\phi \to X\in \mathrm{SubGrp}\left(U\right)$$
21	4 5	lssss	$$⊢X\in S\to X\subseteq V$$
22	10 21	syl	$$⊢\phi \to X\subseteq V$$
23	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$$
24	9 22 23	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(X\right)\in S$$
25	19 24	sseldd	$$⊢\phi \to \underset{\dot{}}{\perp }\left(X\right)\in \mathrm{SubGrp}\left(U\right)$$
26	7	lsmless12	$$⊢\left(\left(X\in \mathrm{SubGrp}\left(U\right)\wedge \underset{\dot{}}{\perp }\left(X\right)\in \mathrm{SubGrp}\left(U\right)\right)\wedge \left(r\subseteq X\wedge q\subseteq \underset{\dot{}}{\perp }\left(X\right)\right)\right)\to r\underset{\dot{}}{\oplus }q\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$
27	20 25 15 14 26	syl22anc	$$⊢\phi \to r\underset{\dot{}}{\oplus }q\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$
28	16 27	sstrd	$$⊢\phi \to p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$