Theorem djhunssN

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

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

Proof

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