Metamath Proof Explorer

Theorem lsmpr

Description: The span of a pair of vectors equals the sum of the spans of their singletons. (Contributed by NM, 13-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 lsmpr.v 
 |-  V = ( Base ` W )
2 lsmpr.n 
 |-  N = ( LSpan ` W )
3 lsmpr.p 
 |-  .(+) = ( LSSum ` W )
4 lsmpr.w 
 |-  ( ph -> W e. LMod )
5 lsmpr.x 
 |-  ( ph -> X e. V )
6 lsmpr.y 
 |-  ( ph -> Y e. V )
7 5 snssd 
 |-  ( ph -> { X } C_ V )
8 6 snssd 
 |-  ( ph -> { Y } C_ V )
9 1 2 lspun 
 |-  ( ( W e. LMod /\ { X } C_ V /\ { Y } C_ V ) -> ( N ` ( { X } u. { Y } ) ) = ( N ` ( ( N ` { X } ) u. ( N ` { Y } ) ) ) )
10 4 7 8 9 syl3anc 
 |-  ( ph -> ( N ` ( { X } u. { Y } ) ) = ( N ` ( ( N ` { X } ) u. ( N ` { Y } ) ) ) )
11 df-pr 
 |-  { X , Y } = ( { X } u. { Y } )
12 11 fveq2i 
 |-  ( N ` { X , Y } ) = ( N ` ( { X } u. { Y } ) )
13 12 a1i 
 |-  ( ph -> ( N ` { X , Y } ) = ( N ` ( { X } u. { Y } ) ) )
14 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
15 1 14 2 lspsncl 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
16 4 5 15 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ( LSubSp ` W ) )
17 1 14 2 lspsncl 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
18 4 6 17 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) )
19 14 2 3 lsmsp 
 |-  ( ( W e. LMod /\ ( N ` { X } ) e. ( LSubSp ` W ) /\ ( N ` { Y } ) e. ( LSubSp ` W ) ) -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) = ( N ` ( ( N ` { X } ) u. ( N ` { Y } ) ) ) )
20 4 16 18 19 syl3anc 
 |-  ( ph -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) = ( N ` ( ( N ` { X } ) u. ( N ` { Y } ) ) ) )
21 10 13 20 3eqtr4d 
 |-  ( ph -> ( N ` { X , Y } ) = ( ( N ` { X } ) .(+) ( N ` { Y } ) ) )