Database
BASIC ALGEBRAIC STRUCTURES
Left modules
Subspaces and spans in a left module
lsp0
Next ⟩
lspuni0
Metamath Proof Explorer
Ascii
Unicode
Theorem
lsp0
Description:
Span of the empty set.
(Contributed by
Mario Carneiro
, 5-Sep-2014)
Ref
Expression
Hypotheses
lspsn0.z
⊢
0
˙
=
0
W
lspsn0.n
⊢
N
=
LSpan
⁡
W
Assertion
lsp0
⊢
W
∈
LMod
→
N
⁡
∅
=
0
˙
Proof
Step
Hyp
Ref
Expression
1
lspsn0.z
⊢
0
˙
=
0
W
2
lspsn0.n
⊢
N
=
LSpan
⁡
W
3
eqid
⊢
LSubSp
⁡
W
=
LSubSp
⁡
W
4
1
3
lsssn0
⊢
W
∈
LMod
→
0
˙
∈
LSubSp
⁡
W
5
0ss
⊢
∅
⊆
0
˙
6
3
2
lspssp
⊢
W
∈
LMod
∧
0
˙
∈
LSubSp
⁡
W
∧
∅
⊆
0
˙
→
N
⁡
∅
⊆
0
˙
7
5
6
mp3an3
⊢
W
∈
LMod
∧
0
˙
∈
LSubSp
⁡
W
→
N
⁡
∅
⊆
0
˙
8
4
7
mpdan
⊢
W
∈
LMod
→
N
⁡
∅
⊆
0
˙
9
0ss
⊢
∅
⊆
Base
W
10
eqid
⊢
Base
W
=
Base
W
11
10
3
2
lspcl
⊢
W
∈
LMod
∧
∅
⊆
Base
W
→
N
⁡
∅
∈
LSubSp
⁡
W
12
9
11
mpan2
⊢
W
∈
LMod
→
N
⁡
∅
∈
LSubSp
⁡
W
13
1
3
lss0ss
⊢
W
∈
LMod
∧
N
⁡
∅
∈
LSubSp
⁡
W
→
0
˙
⊆
N
⁡
∅
14
12
13
mpdan
⊢
W
∈
LMod
→
0
˙
⊆
N
⁡
∅
15
8
14
eqssd
⊢
W
∈
LMod
→
N
⁡
∅
=
0
˙