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

Metamath Proof Explorer

Theorem lss0v

Description: The zero vector in a submodule equals the zero vector in the including module. (Contributed by NM, 15-Mar-2015)

Ref Expression
Hypotheses lss0v.x 
|- X = ( W |`s U )
lss0v.o 
|- .0. = ( 0g ` W )
lss0v.z 
|- Z = ( 0g ` X )
lss0v.l 
|- L = ( LSubSp ` W )
Assertion lss0v 
|- ( ( W e. LMod /\ U e. L ) -> Z = .0. )

Proof

Step Hyp Ref Expression
1 lss0v.x 
 |-  X = ( W |`s U )
2 lss0v.o 
 |-  .0. = ( 0g ` W )
3 lss0v.z 
 |-  Z = ( 0g ` X )
4 lss0v.l 
 |-  L = ( LSubSp ` W )
5 0ss 
 |-  (/) C_ U
6 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
7 eqid 
 |-  ( LSpan ` X ) = ( LSpan ` X )
8 1 6 7 4 lsslsp 
 |-  ( ( W e. LMod /\ U e. L /\ (/) C_ U ) -> ( ( LSpan ` X ) ` (/) ) = ( ( LSpan ` W ) ` (/) ) )
9 5 8 mp3an3 
 |-  ( ( W e. LMod /\ U e. L ) -> ( ( LSpan ` X ) ` (/) ) = ( ( LSpan ` W ) ` (/) ) )
10 1 4 lsslmod 
 |-  ( ( W e. LMod /\ U e. L ) -> X e. LMod )
11 3 7 lsp0 
 |-  ( X e. LMod -> ( ( LSpan ` X ) ` (/) ) = { Z } )
12 10 11 syl 
 |-  ( ( W e. LMod /\ U e. L ) -> ( ( LSpan ` X ) ` (/) ) = { Z } )
13 2 6 lsp0 
 |-  ( W e. LMod -> ( ( LSpan ` W ) ` (/) ) = { .0. } )
14 13 adantr 
 |-  ( ( W e. LMod /\ U e. L ) -> ( ( LSpan ` W ) ` (/) ) = { .0. } )
15 9 12 14 3eqtr3d 
 |-  ( ( W e. LMod /\ U e. L ) -> { Z } = { .0. } )
16 15 unieqd 
 |-  ( ( W e. LMod /\ U e. L ) -> U. { Z } = U. { .0. } )
17 3 fvexi 
 |-  Z e. _V
18 17 unisn 
 |-  U. { Z } = Z
19 2 fvexi 
 |-  .0. e. _V
20 19 unisn 
 |-  U. { .0. } = .0.
21 16 18 20 3eqtr3g 
 |-  ( ( W e. LMod /\ U e. L ) -> Z = .0. )