Theorem lspvadd

Description: The span of a vector sum is included in the span of its arguments. (Contributed by NM, 22-Feb-2014) (Proof shortened by Mario Carneiro, 21-Jun-2014)

	Ref	Expression
Hypotheses	lspvadd.v	|- V = ( Base ` W )
	lspvadd.a	|- .+ = ( +g ` W )
	lspvadd.n	|- N = ( LSpan ` W )
Assertion	lspvadd	|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X .+ Y ) } ) C_ ( N ` { X , Y } ) )

Proof

Step	Hyp	Ref	Expression
1		lspvadd.v	|- V = ( Base ` W )
2		lspvadd.a	|- .+ = ( +g ` W )
3		lspvadd.n	|- N = ( LSpan ` W )
4		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
5		simp1	|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> W e. LMod )
6		prssi	|- ( ( X e. V /\ Y e. V ) -> { X , Y } C_ V )
7	6	3adant1	|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> { X , Y } C_ V )
8	1 4 3	lspcl	|- ( ( W e. LMod /\ { X , Y } C_ V ) -> ( N ` { X , Y } ) e. ( LSubSp ` W ) )
9	5 7 8	syl2anc	|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { X , Y } ) e. ( LSubSp ` W ) )
10	1 3	lspssid	|- ( ( W e. LMod /\ { X , Y } C_ V ) -> { X , Y } C_ ( N ` { X , Y } ) )
11	5 7 10	syl2anc	|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> { X , Y } C_ ( N ` { X , Y } ) )
12		prssg	|- ( ( X e. V /\ Y e. V ) -> ( ( X e. ( N ` { X , Y } ) /\ Y e. ( N ` { X , Y } ) ) <-> { X , Y } C_ ( N ` { X , Y } ) ) )
13	12	3adant1	|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( ( X e. ( N ` { X , Y } ) /\ Y e. ( N ` { X , Y } ) ) <-> { X , Y } C_ ( N ` { X , Y } ) ) )
14	11 13	mpbird	|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X e. ( N ` { X , Y } ) /\ Y e. ( N ` { X , Y } ) ) )
15	2 4	lssvacl	|- ( ( ( W e. LMod /\ ( N ` { X , Y } ) e. ( LSubSp ` W ) ) /\ ( X e. ( N ` { X , Y } ) /\ Y e. ( N ` { X , Y } ) ) ) -> ( X .+ Y ) e. ( N ` { X , Y } ) )
16	5 9 14 15	syl21anc	|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) e. ( N ` { X , Y } ) )
17	4 3 5 9 16	lspsnel5a	|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X .+ Y ) } ) C_ ( N ` { X , Y } ) )