This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ellspsn5 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X .+ Y ) } ) C_ ( N ` { X , Y } ) )