Metamath Proof Explorer


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 } ) )