Theorem dihsmsnrn

Description: The subspace sum of two singleton spans is closed. (Contributed by NM, 27-Feb-2015)

	Ref	Expression
Hypotheses	dihsmsnrn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihsmsnrn.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dihsmsnrn.v	$$⊢V={\mathrm{Base}}_U$$
	dihsmsnrn.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	dihsmsnrn.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	dihsmsnrn.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dihsmsnrn.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dihsmsnrn.x	$$⊢\phi \to X\in V$$
	dihsmsnrn.y	$$⊢\phi \to Y\in V$$
Assertion	dihsmsnrn	$$⊢\phi \to N\left(\left\{X\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)\in \mathrm{ran}I$$

Proof

Step	Hyp	Ref	Expression
1		dihsmsnrn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dihsmsnrn.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		dihsmsnrn.v	$$⊢V={\mathrm{Base}}_U$$
4		dihsmsnrn.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
5		dihsmsnrn.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
6		dihsmsnrn.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
7		dihsmsnrn.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
8		dihsmsnrn.x	$$⊢\phi \to X\in V$$
9		dihsmsnrn.y	$$⊢\phi \to Y\in V$$
10	1 2 3 5 6	dihlsprn	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in V\right)\to N\left(\left\{X\right\}\right)\in \mathrm{ran}I$$
11	7 8 10	syl2anc	$$⊢\phi \to N\left(\left\{X\right\}\right)\in \mathrm{ran}I$$
12	1 2 3 4 5 6 7 11 9	dihsmsprn	$$⊢\phi \to N\left(\left\{X\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)\in \mathrm{ran}I$$