Theorem dihsmsnrn

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

	Ref	Expression
Hypotheses	dihsmsnrn.h	|- H = ( LHyp ` K )
	dihsmsnrn.u	|- U = ( ( DVecH ` K ) ` W )
	dihsmsnrn.v	|- V = ( Base ` U )
	dihsmsnrn.p	|- .(+) = ( LSSum ` U )
	dihsmsnrn.n	|- N = ( LSpan ` U )
	dihsmsnrn.i	|- I = ( ( DIsoH ` K ) ` W )
	dihsmsnrn.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dihsmsnrn.x	|- ( ph -> X e. V )
	dihsmsnrn.y	|- ( ph -> Y e. V )
Assertion	dihsmsnrn	|- ( ph -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) e. ran I )

Proof

Step	Hyp	Ref	Expression
1		dihsmsnrn.h	|- H = ( LHyp ` K )
2		dihsmsnrn.u	|- U = ( ( DVecH ` K ) ` W )
3		dihsmsnrn.v	|- V = ( Base ` U )
4		dihsmsnrn.p	|- .(+) = ( LSSum ` U )
5		dihsmsnrn.n	|- N = ( LSpan ` U )
6		dihsmsnrn.i	|- I = ( ( DIsoH ` K ) ` W )
7		dihsmsnrn.k	|- ( ph -> ( K e. HL /\ W e. H ) )
8		dihsmsnrn.x	|- ( ph -> X e. V )
9		dihsmsnrn.y	|- ( ph -> Y e. V )
10	1 2 3 5 6	dihlsprn	|- ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( N ` { X } ) e. ran I )
11	7 8 10	syl2anc	|- ( ph -> ( N ` { X } ) e. ran I )
12	1 2 3 4 5 6 7 11 9	dihsmsprn	|- ( ph -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) e. ran I )