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