Metamath Proof Explorer

Theorem lsppr

Description: Span of a pair of vectors. (Contributed by NM, 22-Aug-2014)

Ref Expression
Hypotheses lsppr.v 
|- V = ( Base ` W )
lsppr.a 
|- .+ = ( +g ` W )
lsppr.f 
|- F = ( Scalar ` W )
lsppr.k 
|- K = ( Base ` F )
lsppr.t 
|- .x. = ( .s ` W )
lsppr.n 
|- N = ( LSpan ` W )
lsppr.w 
|- ( ph -> W e. LMod )
lsppr.x 
|- ( ph -> X e. V )
lsppr.y 
|- ( ph -> Y e. V )
Assertion lsppr 
|- ( ph -> ( N ` { X , Y } ) = { v | E. k e. K E. l e. K v = ( ( k .x. X ) .+ ( l .x. Y ) ) } )

Proof

Step Hyp Ref Expression
1 lsppr.v 
 |-  V = ( Base ` W )
2 lsppr.a 
 |-  .+ = ( +g ` W )
3 lsppr.f 
 |-  F = ( Scalar ` W )
4 lsppr.k 
 |-  K = ( Base ` F )
5 lsppr.t 
 |-  .x. = ( .s ` W )
6 lsppr.n 
 |-  N = ( LSpan ` W )
7 lsppr.w 
 |-  ( ph -> W e. LMod )
8 lsppr.x 
 |-  ( ph -> X e. V )
9 lsppr.y 
 |-  ( ph -> Y e. V )
10 df-pr 
 |-  { X , Y } = ( { X } u. { Y } )
11 10 fveq2i 
 |-  ( N ` { X , Y } ) = ( N ` ( { X } u. { Y } ) )
12 8 snssd 
 |-  ( ph -> { X } C_ V )
13 9 snssd 
 |-  ( ph -> { Y } C_ V )
14 1 6 lspun 
 |-  ( ( W e. LMod /\ { X } C_ V /\ { Y } C_ V ) -> ( N ` ( { X } u. { Y } ) ) = ( N ` ( ( N ` { X } ) u. ( N ` { Y } ) ) ) )
15 7 12 13 14 syl3anc 
 |-  ( ph -> ( N ` ( { X } u. { Y } ) ) = ( N ` ( ( N ` { X } ) u. ( N ` { Y } ) ) ) )
16 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
17 1 16 6 lspsncl 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
18 7 8 17 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ( LSubSp ` W ) )
19 1 16 6 lspsncl 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
20 7 9 19 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) )
21 eqid 
 |-  ( LSSum ` W ) = ( LSSum ` W )
22 16 6 21 lsmsp 
 |-  ( ( W e. LMod /\ ( N ` { X } ) e. ( LSubSp ` W ) /\ ( N ` { Y } ) e. ( LSubSp ` W ) ) -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) = ( N ` ( ( N ` { X } ) u. ( N ` { Y } ) ) ) )
23 7 18 20 22 syl3anc 
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) = ( N ` ( ( N ` { X } ) u. ( N ` { Y } ) ) ) )
24 1 2 3 4 5 21 6 7 8 9 lsmspsn 
 |-  ( ph -> ( v e. ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) <-> E. k e. K E. l e. K v = ( ( k .x. X ) .+ ( l .x. Y ) ) ) )
25 24 abbi2dv 
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) = { v | E. k e. K E. l e. K v = ( ( k .x. X ) .+ ( l .x. Y ) ) } )
26 15 23 25 3eqtr2d 
 |-  ( ph -> ( N ` ( { X } u. { Y } ) ) = { v | E. k e. K E. l e. K v = ( ( k .x. X ) .+ ( l .x. Y ) ) } )
27 11 26 syl5eq 
 |-  ( ph -> ( N ` { X , Y } ) = { v | E. k e. K E. l e. K v = ( ( k .x. X ) .+ ( l .x. Y ) ) } )