Metamath Proof Explorer

Theorem lsp0

Description: Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014)

Ref Expression
Hypotheses lspsn0.z 
|- .0. = ( 0g ` W )
lspsn0.n 
|- N = ( LSpan ` W )
Assertion lsp0 
|- ( W e. LMod -> ( N ` (/) ) = { .0. } )

Proof

Step Hyp Ref Expression
1 lspsn0.z 
 |-  .0. = ( 0g ` W )
2 lspsn0.n 
 |-  N = ( LSpan ` W )
3 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
4 1 3 lsssn0 
 |-  ( W e. LMod -> { .0. } e. ( LSubSp ` W ) )
5 0ss 
 |-  (/) C_ { .0. }
6 3 2 lspssp 
 |-  ( ( W e. LMod /\ { .0. } e. ( LSubSp ` W ) /\ (/) C_ { .0. } ) -> ( N ` (/) ) C_ { .0. } )
7 5 6 mp3an3 
 |-  ( ( W e. LMod /\ { .0. } e. ( LSubSp ` W ) ) -> ( N ` (/) ) C_ { .0. } )
8 4 7 mpdan 
 |-  ( W e. LMod -> ( N ` (/) ) C_ { .0. } )
9 0ss 
 |-  (/) C_ ( Base ` W )
10 eqid 
 |-  ( Base ` W ) = ( Base ` W )
11 10 3 2 lspcl 
 |-  ( ( W e. LMod /\ (/) C_ ( Base ` W ) ) -> ( N ` (/) ) e. ( LSubSp ` W ) )
12 9 11 mpan2 
 |-  ( W e. LMod -> ( N ` (/) ) e. ( LSubSp ` W ) )
13 1 3 lss0ss 
 |-  ( ( W e. LMod /\ ( N ` (/) ) e. ( LSubSp ` W ) ) -> { .0. } C_ ( N ` (/) ) )
14 12 13 mpdan 
 |-  ( W e. LMod -> { .0. } C_ ( N ` (/) ) )
15 8 14 eqssd 
 |-  ( W e. LMod -> ( N ` (/) ) = { .0. } )