Theorem dvhdimlem

Description: Lemma for dvh2dim and dvh3dim . TODO: make this obsolete and use dvh4dimlem directly? (Contributed by NM, 24-Apr-2015)

	Ref	Expression
Hypotheses	dvh3dim.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dvh3dim.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dvh3dim.v	$$⊢V={\mathrm{Base}}_U$$
	dvh3dim.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	dvh3dim.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dvh3dim.x	$$⊢\phi \to X\in V$$
	dvhdim.y	$$⊢\phi \to Y\in V$$
	dvhdim.o	$$⊢\underset{\dot{}}{0}=0_U$$
	dvhdim.x	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
	dvhdimlem.y	$$⊢\phi \to Y\ne \underset{\dot{}}{0}$$
Assertion	dvhdimlem	$$⊢\phi \to \exists z\in V\neg z\in N\left(\left\{X,Y\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvh3dim.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvh3dim.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		dvh3dim.v	$$⊢V={\mathrm{Base}}_U$$
4		dvh3dim.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
5		dvh3dim.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
6		dvh3dim.x	$$⊢\phi \to X\in V$$
7		dvhdim.y	$$⊢\phi \to Y\in V$$
8		dvhdim.o	$$⊢\underset{\dot{}}{0}=0_U$$
9		dvhdim.x	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
10		dvhdimlem.y	$$⊢\phi \to Y\ne \underset{\dot{}}{0}$$
11	1 2 3 4 5 6 7 7 8 9 10 10	dvh4dimlem	$$⊢\phi \to \exists z\in V\neg z\in N\left(\left\{X,Y,Y\right\}\right)$$
12	1 2 5	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
13		df-tp	$$⊢\left\{X,Y,Y\right\}=\left\{X,Y\right\}\cup \left\{Y\right\}$$
14		prssi	$$⊢\left(X\in V\wedge Y\in V\right)\to \left\{X,Y\right\}\subseteq V$$
15	6 7 14	syl2anc	$$⊢\phi \to \left\{X,Y\right\}\subseteq V$$
16	7	snssd	$$⊢\phi \to \left\{Y\right\}\subseteq V$$
17	15 16	unssd	$$⊢\phi \to \left\{X,Y\right\}\cup \left\{Y\right\}\subseteq V$$
18	13 17	eqsstrid	$$⊢\phi \to \left\{X,Y,Y\right\}\subseteq V$$
19		ssun1	$$⊢\left\{X,Y\right\}\subseteq \left\{X,Y\right\}\cup \left\{Y\right\}$$
20	19 13	sseqtrri	$$⊢\left\{X,Y\right\}\subseteq \left\{X,Y,Y\right\}$$
21	20	a1i	$$⊢\phi \to \left\{X,Y\right\}\subseteq \left\{X,Y,Y\right\}$$
22	3 4	lspss	$$⊢\left(U\in \mathrm{LMod}\wedge \left\{X,Y,Y\right\}\subseteq V\wedge \left\{X,Y\right\}\subseteq \left\{X,Y,Y\right\}\right)\to N\left(\left\{X,Y\right\}\right)\subseteq N\left(\left\{X,Y,Y\right\}\right)$$
23	12 18 21 22	syl3anc	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\subseteq N\left(\left\{X,Y,Y\right\}\right)$$
24	23	ssneld	$$⊢\phi \to \left(\neg z\in N\left(\left\{X,Y,Y\right\}\right)\to \neg z\in N\left(\left\{X,Y\right\}\right)\right)$$
25	24	reximdv	$$⊢\phi \to \left(\exists z\in V\neg z\in N\left(\left\{X,Y,Y\right\}\right)\to \exists z\in V\neg z\in N\left(\left\{X,Y\right\}\right)\right)$$
26	11 25	mpd	$$⊢\phi \to \exists z\in V\neg z\in N\left(\left\{X,Y\right\}\right)$$