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

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 } )