Theorem djhsumss

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

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

Proof

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