Theorem djhspss

Description: Subspace span of union is a subset of subspace join. (Contributed by NM, 6-Aug-2014)

	Ref	Expression
Hypotheses	djhspss.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	djhspss.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	djhspss.v	$$⊢V={\mathrm{Base}}_U$$
	djhspss.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	djhspss.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{joinH}\left(K\right)\left(W\right)$$
	djhspss.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	djhspss.x	$$⊢\phi \to X\subseteq V$$
	djhspss.y	$$⊢\phi \to Y\subseteq V$$
Assertion	djhspss	$$⊢\phi \to N\left(X\cup Y\right)\subseteq X\underset{\dot{}}{\vee }Y$$

Proof

Step	Hyp	Ref	Expression
1		djhspss.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		djhspss.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		djhspss.v	$$⊢V={\mathrm{Base}}_U$$
4		djhspss.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
5		djhspss.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{joinH}\left(K\right)\left(W\right)$$
6		djhspss.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7		djhspss.x	$$⊢\phi \to X\subseteq V$$
8		djhspss.y	$$⊢\phi \to Y\subseteq V$$
9		eqid	$$⊢\mathrm{ocH}\left(K\right)\left(W\right)=\mathrm{ocH}\left(K\right)\left(W\right)$$
10	7 8	unssd	$$⊢\phi \to X\cup Y\subseteq V$$
11	1 2 9 3 4 6 10	dochspss	$$⊢\phi \to N\left(X\cup Y\right)\subseteq \mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(X\cup Y\right)\right)$$
12	1 2 3 9 5	djhval2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\subseteq V\wedge Y\subseteq V\right)\to X\underset{\dot{}}{\vee }Y=\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(X\cup Y\right)\right)$$
13	6 7 8 12	syl3anc	$$⊢\phi \to X\underset{\dot{}}{\vee }Y=\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(X\cup Y\right)\right)$$
14	11 13	sseqtrrd	$$⊢\phi \to N\left(X\cup Y\right)\subseteq X\underset{\dot{}}{\vee }Y$$