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

Metamath Proof Explorer

Theorem lsppreli

Description: A vector expressed as a sum belongs to the span of its components. (Contributed by NM, 9-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 lsppreli.v 
 |-  V = ( Base ` W )
2 lsppreli.p 
 |-  .+ = ( +g ` W )
3 lsppreli.t 
 |-  .x. = ( .s ` W )
4 lsppreli.f 
 |-  F = ( Scalar ` W )
5 lsppreli.k 
 |-  K = ( Base ` F )
6 lsppreli.n 
 |-  N = ( LSpan ` W )
7 lsppreli.w 
 |-  ( ph -> W e. LMod )
8 lsppreli.a 
 |-  ( ph -> A e. K )
9 lsppreli.b 
 |-  ( ph -> B e. K )
10 lsppreli.x 
 |-  ( ph -> X e. V )
11 lsppreli.y 
 |-  ( ph -> Y e. V )
12 1 6 lspsnsubg 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( SubGrp ` W ) )
13 7 10 12 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ( SubGrp ` W ) )
14 1 6 lspsnsubg 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( SubGrp ` W ) )
15 7 11 14 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( SubGrp ` W ) )
16 1 3 4 5 6 7 8 10 ellspsni 
 |-  ( ph -> ( A .x. X ) e. ( N ` { X } ) )
17 1 3 4 5 6 7 9 11 ellspsni 
 |-  ( ph -> ( B .x. Y ) e. ( N ` { Y } ) )
18 eqid 
 |-  ( LSSum ` W ) = ( LSSum ` W )
19 2 18 lsmelvali 
 |-  ( ( ( ( N ` { X } ) e. ( SubGrp ` W ) /\ ( N ` { Y } ) e. ( SubGrp ` W ) ) /\ ( ( A .x. X ) e. ( N ` { X } ) /\ ( B .x. Y ) e. ( N ` { Y } ) ) ) -> ( ( A .x. X ) .+ ( B .x. Y ) ) e. ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
20 13 15 16 17 19 syl22anc 
 |-  ( ph -> ( ( A .x. X ) .+ ( B .x. Y ) ) e. ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
21 1 6 18 7 10 11 lsmpr 
 |-  ( ph -> ( N ` { X , Y } ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
22 20 21 eleqtrrd 
 |-  ( ph -> ( ( A .x. X ) .+ ( B .x. Y ) ) e. ( N ` { X , Y } ) )