Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Linear algebra (extension)
Linear combinations
lspsslco
Next ⟩
lcosslsp
Metamath Proof Explorer
Ascii
Unicode
Theorem
lspsslco
Description:
Lemma for
lspeqlco
.
(Contributed by
AV
, 17-Apr-2019)
Ref
Expression
Hypothesis
lspeqvlco.b
⊢
B
=
Base
M
Assertion
lspsslco
⊢
M
∈
LMod
∧
V
∈
𝒫
B
→
LSpan
⁡
M
⁡
V
⊆
M
LinCo
V
Proof
Step
Hyp
Ref
Expression
1
lspeqvlco.b
⊢
B
=
Base
M
2
simpl
⊢
M
∈
LMod
∧
V
∈
𝒫
B
→
M
∈
LMod
3
1
pweqi
⊢
𝒫
B
=
𝒫
Base
M
4
3
eleq2i
⊢
V
∈
𝒫
B
↔
V
∈
𝒫
Base
M
5
lincolss
⊢
M
∈
LMod
∧
V
∈
𝒫
Base
M
→
M
LinCo
V
∈
LSubSp
⁡
M
6
4
5
sylan2b
⊢
M
∈
LMod
∧
V
∈
𝒫
B
→
M
LinCo
V
∈
LSubSp
⁡
M
7
lcoss
⊢
M
∈
LMod
∧
V
∈
𝒫
Base
M
→
V
⊆
M
LinCo
V
8
4
7
sylan2b
⊢
M
∈
LMod
∧
V
∈
𝒫
B
→
V
⊆
M
LinCo
V
9
eqid
⊢
LSubSp
⁡
M
=
LSubSp
⁡
M
10
eqid
⊢
LSpan
⁡
M
=
LSpan
⁡
M
11
9
10
lspssp
⊢
M
∈
LMod
∧
M
LinCo
V
∈
LSubSp
⁡
M
∧
V
⊆
M
LinCo
V
→
LSpan
⁡
M
⁡
V
⊆
M
LinCo
V
12
2
6
8
11
syl3anc
⊢
M
∈
LMod
∧
V
∈
𝒫
B
→
LSpan
⁡
M
⁡
V
⊆
M
LinCo
V