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 ` W ) ` (/) ) = ( ( LSpan ` X ) ` (/) ) )
9 5 8 mp3an3
 |-  ( ( W e. LMod /\ U e. L ) -> ( ( LSpan ` W ) ` (/) ) = ( ( LSpan ` X ) ` (/) ) )
10 2 6 lsp0
 |-  ( W e. LMod -> ( ( LSpan ` W ) ` (/) ) = { .0. } )
11 10 adantr
 |-  ( ( W e. LMod /\ U e. L ) -> ( ( LSpan ` W ) ` (/) ) = { .0. } )
12 1 4 lsslmod
 |-  ( ( W e. LMod /\ U e. L ) -> X e. LMod )
13 3 7 lsp0
 |-  ( X e. LMod -> ( ( LSpan ` X ) ` (/) ) = { Z } )
14 12 13 syl
 |-  ( ( W e. LMod /\ U e. L ) -> ( ( LSpan ` X ) ` (/) ) = { Z } )
15 9 11 14 3eqtr3rd
 |-  ( ( 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. )