Theorem lspprvacl

Description: The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015)

	Ref	Expression
Hypotheses	lspprvacl.v	|- V = ( Base ` W )
	lspprvacl.p	|- .+ = ( +g ` W )
	lspprvacl.n	|- N = ( LSpan ` W )
	lspprvacl.w	|- ( ph -> W e. LMod )
	lspprvacl.x	|- ( ph -> X e. V )
	lspprvacl.y	|- ( ph -> Y e. V )
Assertion	lspprvacl	|- ( ph -> ( X .+ Y ) e. ( N ` { X , Y } ) )

Proof

Step	Hyp	Ref	Expression
1		lspprvacl.v	|- V = ( Base ` W )
2		lspprvacl.p	|- .+ = ( +g ` W )
3		lspprvacl.n	|- N = ( LSpan ` W )
4		lspprvacl.w	|- ( ph -> W e. LMod )
5		lspprvacl.x	|- ( ph -> X e. V )
6		lspprvacl.y	|- ( ph -> Y e. V )
7		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
8	1 7 3 4 5 6	lspprcl	|- ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` W ) )
9	1 3 4 5 6	lspprid1	|- ( ph -> X e. ( N ` { X , Y } ) )
10	1 3 4 5 6	lspprid2	|- ( ph -> Y e. ( N ` { X , Y } ) )
11	2 7	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 } ) )
12	4 8 9 10 11	syl22anc	|- ( ph -> ( X .+ Y ) e. ( N ` { X , Y } ) )