Theorem dochexmidlem4

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$$
	dochexmidlem4.pp	$$⊢\phi \to p\in A$$
	dochexmidlem4.qq	$$⊢\phi \to q\in A$$
	dochexmidlem4.z	$$⊢\underset{\dot{}}{0}=0_U$$
	dochexmidlem4.m	$$⊢M=X\underset{\dot{}}{\oplus }p$$
	dochexmidlem4.xn	$$⊢\phi \to X\ne \left\{\underset{\dot{}}{0}\right\}$$
	dochexmidlem4.pl	$$⊢\phi \to q\subseteq \underset{\dot{}}{\perp }\left(X\right)\cap M$$
Assertion	dochexmidlem4	$$⊢\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		dochexmidlem4.pp	$$⊢\phi \to p\in A$$
12		dochexmidlem4.qq	$$⊢\phi \to q\in A$$
13		dochexmidlem4.z	$$⊢\underset{\dot{}}{0}=0_U$$
14		dochexmidlem4.m	$$⊢M=X\underset{\dot{}}{\oplus }p$$
15		dochexmidlem4.xn	$$⊢\phi \to X\ne \left\{\underset{\dot{}}{0}\right\}$$
16		dochexmidlem4.pl	$$⊢\phi \to q\subseteq \underset{\dot{}}{\perp }\left(X\right)\cap M$$
17	1 3 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
18	5 8 17 11	lsatlssel	$$⊢\phi \to p\in S$$
19		inss2	$$⊢\underset{\dot{}}{\perp }\left(X\right)\cap M\subseteq M$$
20	16 19	sstrdi	$$⊢\phi \to q\subseteq M$$
21	20 14	sseqtrdi	$$⊢\phi \to q\subseteq X\underset{\dot{}}{\oplus }p$$
22	13 5 7 8 17 10 18 12 15 21	lsmsat	$$⊢\phi \to \exists r\in A\left(r\subseteq X\wedge q\subseteq r\underset{\dot{}}{\oplus }p\right)$$
23	9	3ad2ant1	$$⊢\left(\phi \wedge r\in A\wedge \left(r\subseteq X\wedge q\subseteq r\underset{\dot{}}{\oplus }p\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
24	10	3ad2ant1	$$⊢\left(\phi \wedge r\in A\wedge \left(r\subseteq X\wedge q\subseteq r\underset{\dot{}}{\oplus }p\right)\right)\to X\in S$$
25	11	3ad2ant1	$$⊢\left(\phi \wedge r\in A\wedge \left(r\subseteq X\wedge q\subseteq r\underset{\dot{}}{\oplus }p\right)\right)\to p\in A$$
26	12	3ad2ant1	$$⊢\left(\phi \wedge r\in A\wedge \left(r\subseteq X\wedge q\subseteq r\underset{\dot{}}{\oplus }p\right)\right)\to q\in A$$
27		simp2	$$⊢\left(\phi \wedge r\in A\wedge \left(r\subseteq X\wedge q\subseteq r\underset{\dot{}}{\oplus }p\right)\right)\to r\in A$$
28		inss1	$$⊢\underset{\dot{}}{\perp }\left(X\right)\cap M\subseteq \underset{\dot{}}{\perp }\left(X\right)$$
29	16 28	sstrdi	$$⊢\phi \to q\subseteq \underset{\dot{}}{\perp }\left(X\right)$$
30	29	3ad2ant1	$$⊢\left(\phi \wedge r\in A\wedge \left(r\subseteq X\wedge q\subseteq r\underset{\dot{}}{\oplus }p\right)\right)\to q\subseteq \underset{\dot{}}{\perp }\left(X\right)$$
31		simp3l	$$⊢\left(\phi \wedge r\in A\wedge \left(r\subseteq X\wedge q\subseteq r\underset{\dot{}}{\oplus }p\right)\right)\to r\subseteq X$$
32		simp3r	$$⊢\left(\phi \wedge r\in A\wedge \left(r\subseteq X\wedge q\subseteq r\underset{\dot{}}{\oplus }p\right)\right)\to q\subseteq r\underset{\dot{}}{\oplus }p$$
33	1 2 3 4 5 6 7 8 23 24 25 26 27 30 31 32	dochexmidlem3	$$⊢\left(\phi \wedge r\in A\wedge \left(r\subseteq X\wedge q\subseteq r\underset{\dot{}}{\oplus }p\right)\right)\to p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$
34	33	rexlimdv3a	$$⊢\phi \to \left(\exists r\in A\left(r\subseteq X\wedge q\subseteq r\underset{\dot{}}{\oplus }p\right)\to p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)$$
35	22 34	mpd	$$⊢\phi \to p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$