Theorem dochexmidlem5

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$$
	dochexmidlem5.pp	$$⊢\phi \to p\in A$$
	dochexmidlem5.z	$$⊢\underset{\dot{}}{0}=0_U$$
	dochexmidlem5.m	$$⊢M=X\underset{\dot{}}{\oplus }p$$
	dochexmidlem5.xn	$$⊢\phi \to X\ne \left\{\underset{\dot{}}{0}\right\}$$
	dochexmidlem5.pl	$$⊢\phi \to \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$
Assertion	dochexmidlem5	$$⊢\phi \to \underset{\dot{}}{\perp }\left(X\right)\cap M=\left\{\underset{\dot{}}{0}\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		dochexmidlem5.pp	$$⊢\phi \to p\in A$$
12		dochexmidlem5.z	$$⊢\underset{\dot{}}{0}=0_U$$
13		dochexmidlem5.m	$$⊢M=X\underset{\dot{}}{\oplus }p$$
14		dochexmidlem5.xn	$$⊢\phi \to X\ne \left\{\underset{\dot{}}{0}\right\}$$
15		dochexmidlem5.pl	$$⊢\phi \to \neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$
16	1 3 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
17	16	adantr	$$⊢\left(\phi \wedge \underset{\dot{}}{\perp }\left(X\right)\cap M\ne \left\{\underset{\dot{}}{0}\right\}\right)\to U\in \mathrm{LMod}$$
18	4 5	lssss	$$⊢X\in S\to X\subseteq V$$
19	10 18	syl	$$⊢\phi \to X\subseteq V$$
20	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$$
21	9 19 20	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(X\right)\in S$$
22	5 8 16 11	lsatlssel	$$⊢\phi \to p\in S$$
23	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$$
24	16 10 22 23	syl3anc	$$⊢\phi \to X\underset{\dot{}}{\oplus }p\in S$$
25	13 24	eqeltrid	$$⊢\phi \to M\in S$$
26	5	lssincl	$$⊢\left(U\in \mathrm{LMod}\wedge \underset{\dot{}}{\perp }\left(X\right)\in S\wedge M\in S\right)\to \underset{\dot{}}{\perp }\left(X\right)\cap M\in S$$
27	16 21 25 26	syl3anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(X\right)\cap M\in S$$
28	27	adantr	$$⊢\left(\phi \wedge \underset{\dot{}}{\perp }\left(X\right)\cap M\ne \left\{\underset{\dot{}}{0}\right\}\right)\to \underset{\dot{}}{\perp }\left(X\right)\cap M\in S$$
29		simpr	$$⊢\left(\phi \wedge \underset{\dot{}}{\perp }\left(X\right)\cap M\ne \left\{\underset{\dot{}}{0}\right\}\right)\to \underset{\dot{}}{\perp }\left(X\right)\cap M\ne \left\{\underset{\dot{}}{0}\right\}$$
30	5 12 8 17 28 29	lssatomic	$$⊢\left(\phi \wedge \underset{\dot{}}{\perp }\left(X\right)\cap M\ne \left\{\underset{\dot{}}{0}\right\}\right)\to \exists q\in Aq\subseteq \underset{\dot{}}{\perp }\left(X\right)\cap M$$
31	30	ex	$$⊢\phi \to \left(\underset{\dot{}}{\perp }\left(X\right)\cap M\ne \left\{\underset{\dot{}}{0}\right\}\to \exists q\in Aq\subseteq \underset{\dot{}}{\perp }\left(X\right)\cap M\right)$$
32	9	3ad2ant1	$$⊢\left(\phi \wedge q\in A\wedge q\subseteq \underset{\dot{}}{\perp }\left(X\right)\cap M\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
33	10	3ad2ant1	$$⊢\left(\phi \wedge q\in A\wedge q\subseteq \underset{\dot{}}{\perp }\left(X\right)\cap M\right)\to X\in S$$
34	11	3ad2ant1	$$⊢\left(\phi \wedge q\in A\wedge q\subseteq \underset{\dot{}}{\perp }\left(X\right)\cap M\right)\to p\in A$$
35		simp2	$$⊢\left(\phi \wedge q\in A\wedge q\subseteq \underset{\dot{}}{\perp }\left(X\right)\cap M\right)\to q\in A$$
36	14	3ad2ant1	$$⊢\left(\phi \wedge q\in A\wedge q\subseteq \underset{\dot{}}{\perp }\left(X\right)\cap M\right)\to X\ne \left\{\underset{\dot{}}{0}\right\}$$
37		simp3	$$⊢\left(\phi \wedge q\in A\wedge q\subseteq \underset{\dot{}}{\perp }\left(X\right)\cap M\right)\to q\subseteq \underset{\dot{}}{\perp }\left(X\right)\cap M$$
38	1 2 3 4 5 6 7 8 32 33 34 35 12 13 36 37	dochexmidlem4	$$⊢\left(\phi \wedge q\in A\wedge q\subseteq \underset{\dot{}}{\perp }\left(X\right)\cap M\right)\to p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$
39	38	rexlimdv3a	$$⊢\phi \to \left(\exists q\in Aq\subseteq \underset{\dot{}}{\perp }\left(X\right)\cap M\to p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)$$
40	31 39	syld	$$⊢\phi \to \left(\underset{\dot{}}{\perp }\left(X\right)\cap M\ne \left\{\underset{\dot{}}{0}\right\}\to p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\right)$$
41	40	necon1bd	$$⊢\phi \to \left(\neg p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)\to \underset{\dot{}}{\perp }\left(X\right)\cap M=\left\{\underset{\dot{}}{0}\right\}\right)$$
42	15 41	mpd	$$⊢\phi \to \underset{\dot{}}{\perp }\left(X\right)\cap M=\left\{\underset{\dot{}}{0}\right\}$$