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

Metamath Proof Explorer

Theorem lsppr0

Description: The span of a vector paired with zero equals the span of the singleton of the vector. (Contributed by NM, 29-Aug-2014)

Ref Expression
Hypotheses lsppr0.v 
|- V = ( Base ` W )
lsppr0.z 
|- .0. = ( 0g ` W )
lsppr0.n 
|- N = ( LSpan ` W )
lsppr0.w 
|- ( ph -> W e. LMod )
lsppr0.x 
|- ( ph -> X e. V )
Assertion lsppr0 
|- ( ph -> ( N ` { X , .0. } ) = ( N ` { X } ) )

Proof

Step Hyp Ref Expression
1 lsppr0.v 
 |-  V = ( Base ` W )
2 lsppr0.z 
 |-  .0. = ( 0g ` W )
3 lsppr0.n 
 |-  N = ( LSpan ` W )
4 lsppr0.w 
 |-  ( ph -> W e. LMod )
5 lsppr0.x 
 |-  ( ph -> X e. V )
6 eqid 
 |-  ( LSSum ` W ) = ( LSSum ` W )
7 1 2 lmod0vcl 
 |-  ( W e. LMod -> .0. e. V )
8 4 7 syl 
 |-  ( ph -> .0. e. V )
9 1 3 6 4 5 8 lsmpr 
 |-  ( ph -> ( N ` { X , .0. } ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { .0. } ) ) )
10 2 3 lspsn0 
 |-  ( W e. LMod -> ( N ` { .0. } ) = { .0. } )
11 4 10 syl 
 |-  ( ph -> ( N ` { .0. } ) = { .0. } )
12 11 oveq2d 
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { .0. } ) ) = ( ( N ` { X } ) ( LSSum ` W ) { .0. } ) )
13 1 3 lspsnsubg 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( SubGrp ` W ) )
14 4 5 13 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ( SubGrp ` W ) )
15 2 6 lsm01 
 |-  ( ( N ` { X } ) e. ( SubGrp ` W ) -> ( ( N ` { X } ) ( LSSum ` W ) { .0. } ) = ( N ` { X } ) )
16 14 15 syl 
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) { .0. } ) = ( N ` { X } ) )
17 9 12 16 3eqtrd 
 |-  ( ph -> ( N ` { X , .0. } ) = ( N ` { X } ) )