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

Metamath Proof Explorer

Theorem lsssn0

Description: The singleton of the zero vector is a subspace. (Contributed by NM, 13-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lss0cl.z 
|- .0. = ( 0g ` W )
lss0cl.s 
|- S = ( LSubSp ` W )
Assertion lsssn0 
|- ( W e. LMod -> { .0. } e. S )

Proof

Step Hyp Ref Expression
1 lss0cl.z 
 |-  .0. = ( 0g ` W )
2 lss0cl.s 
 |-  S = ( LSubSp ` W )
3 eqidd 
 |-  ( W e. LMod -> ( Scalar ` W ) = ( Scalar ` W ) )
4 eqidd 
 |-  ( W e. LMod -> ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) )
5 eqidd 
 |-  ( W e. LMod -> ( Base ` W ) = ( Base ` W ) )
6 eqidd 
 |-  ( W e. LMod -> ( +g ` W ) = ( +g ` W ) )
7 eqidd 
 |-  ( W e. LMod -> ( .s ` W ) = ( .s ` W ) )
8 2 a1i 
 |-  ( W e. LMod -> S = ( LSubSp ` W ) )
9 eqid 
 |-  ( Base ` W ) = ( Base ` W )
10 9 1 lmod0vcl 
 |-  ( W e. LMod -> .0. e. ( Base ` W ) )
11 10 snssd 
 |-  ( W e. LMod -> { .0. } C_ ( Base ` W ) )
12 1 fvexi 
 |-  .0. e. _V
13 12 snnz 
 |-  { .0. } =/= (/)
14 13 a1i 
 |-  ( W e. LMod -> { .0. } =/= (/) )
15 simpr2 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. { .0. } /\ b e. { .0. } ) ) -> a e. { .0. } )
16 elsni 
 |-  ( a e. { .0. } -> a = .0. )
17 15 16 syl 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. { .0. } /\ b e. { .0. } ) ) -> a = .0. )
18 17 oveq2d 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. { .0. } /\ b e. { .0. } ) ) -> ( x ( .s ` W ) a ) = ( x ( .s ` W ) .0. ) )
19 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
20 eqid 
 |-  ( .s ` W ) = ( .s ` W )
21 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
22 19 20 21 1 lmodvs0 
 |-  ( ( W e. LMod /\ x e. ( Base ` ( Scalar ` W ) ) ) -> ( x ( .s ` W ) .0. ) = .0. )
23 22 3ad2antr1 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. { .0. } /\ b e. { .0. } ) ) -> ( x ( .s ` W ) .0. ) = .0. )
24 18 23 eqtrd 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. { .0. } /\ b e. { .0. } ) ) -> ( x ( .s ` W ) a ) = .0. )
25 simpr3 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. { .0. } /\ b e. { .0. } ) ) -> b e. { .0. } )
26 elsni 
 |-  ( b e. { .0. } -> b = .0. )
27 25 26 syl 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. { .0. } /\ b e. { .0. } ) ) -> b = .0. )
28 24 27 oveq12d 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. { .0. } /\ b e. { .0. } ) ) -> ( ( x ( .s ` W ) a ) ( +g ` W ) b ) = ( .0. ( +g ` W ) .0. ) )
29 eqid 
 |-  ( +g ` W ) = ( +g ` W )
30 9 29 1 lmod0vlid 
 |-  ( ( W e. LMod /\ .0. e. ( Base ` W ) ) -> ( .0. ( +g ` W ) .0. ) = .0. )
31 10 30 mpdan 
 |-  ( W e. LMod -> ( .0. ( +g ` W ) .0. ) = .0. )
32 31 adantr 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. { .0. } /\ b e. { .0. } ) ) -> ( .0. ( +g ` W ) .0. ) = .0. )
33 28 32 eqtrd 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. { .0. } /\ b e. { .0. } ) ) -> ( ( x ( .s ` W ) a ) ( +g ` W ) b ) = .0. )
34 ovex 
 |-  ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. _V
35 34 elsn 
 |-  ( ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. { .0. } <-> ( ( x ( .s ` W ) a ) ( +g ` W ) b ) = .0. )
36 33 35 sylibr 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. { .0. } /\ b e. { .0. } ) ) -> ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. { .0. } )
37 3 4 5 6 7 8 11 14 36 islssd 
 |-  ( W e. LMod -> { .0. } e. S )