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𝑊 )
lspsn0.n 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lsp0 ( 𝑊 ∈ LMod → ( 𝑁 ‘ ∅ ) = { 0 } )

Proof

Step Hyp Ref Expression
1 lspsn0.z 0 = ( 0g𝑊 )
2 lspsn0.n 𝑁 = ( LSpan ‘ 𝑊 )
3 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
4 1 3 lsssn0 ( 𝑊 ∈ LMod → { 0 } ∈ ( LSubSp ‘ 𝑊 ) )
5 0ss ∅ ⊆ { 0 }
6 3 2 lspssp ( ( 𝑊 ∈ LMod ∧ { 0 } ∈ ( LSubSp ‘ 𝑊 ) ∧ ∅ ⊆ { 0 } ) → ( 𝑁 ‘ ∅ ) ⊆ { 0 } )
7 5 6 mp3an3 ( ( 𝑊 ∈ LMod ∧ { 0 } ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑁 ‘ ∅ ) ⊆ { 0 } )
8 4 7 mpdan ( 𝑊 ∈ LMod → ( 𝑁 ‘ ∅ ) ⊆ { 0 } )
9 0ss ∅ ⊆ ( Base ‘ 𝑊 )
10 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
11 10 3 2 lspcl ( ( 𝑊 ∈ LMod ∧ ∅ ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ ∅ ) ∈ ( LSubSp ‘ 𝑊 ) )
12 9 11 mpan2 ( 𝑊 ∈ LMod → ( 𝑁 ‘ ∅ ) ∈ ( LSubSp ‘ 𝑊 ) )
13 1 3 lss0ss ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ ∅ ) ∈ ( LSubSp ‘ 𝑊 ) ) → { 0 } ⊆ ( 𝑁 ‘ ∅ ) )
14 12 13 mpdan ( 𝑊 ∈ LMod → { 0 } ⊆ ( 𝑁 ‘ ∅ ) )
15 8 14 eqssd ( 𝑊 ∈ LMod → ( 𝑁 ‘ ∅ ) = { 0 } )