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