Database
BASIC ALGEBRAIC STRUCTURES
Left modules
Subspaces and spans in a left module
lspprvacl
Next ⟩
lssats2
Metamath Proof Explorer
Ascii
Unicode
Theorem
lspprvacl
Description:
The sum of two vectors belongs to their span.
(Contributed by
NM
, 20-May-2015)
Ref
Expression
Hypotheses
lspprvacl.v
⊢
V
=
Base
W
lspprvacl.p
⊢
+
˙
=
+
W
lspprvacl.n
⊢
N
=
LSpan
⁡
W
lspprvacl.w
⊢
φ
→
W
∈
LMod
lspprvacl.x
⊢
φ
→
X
∈
V
lspprvacl.y
⊢
φ
→
Y
∈
V
Assertion
lspprvacl
⊢
φ
→
X
+
˙
Y
∈
N
⁡
X
Y
Proof
Step
Hyp
Ref
Expression
1
lspprvacl.v
⊢
V
=
Base
W
2
lspprvacl.p
⊢
+
˙
=
+
W
3
lspprvacl.n
⊢
N
=
LSpan
⁡
W
4
lspprvacl.w
⊢
φ
→
W
∈
LMod
5
lspprvacl.x
⊢
φ
→
X
∈
V
6
lspprvacl.y
⊢
φ
→
Y
∈
V
7
eqid
⊢
LSubSp
⁡
W
=
LSubSp
⁡
W
8
1
7
3
4
5
6
lspprcl
⊢
φ
→
N
⁡
X
Y
∈
LSubSp
⁡
W
9
1
3
4
5
6
lspprid1
⊢
φ
→
X
∈
N
⁡
X
Y
10
1
3
4
5
6
lspprid2
⊢
φ
→
Y
∈
N
⁡
X
Y
11
2
7
lssvacl
⊢
W
∈
LMod
∧
N
⁡
X
Y
∈
LSubSp
⁡
W
∧
X
∈
N
⁡
X
Y
∧
Y
∈
N
⁡
X
Y
→
X
+
˙
Y
∈
N
⁡
X
Y
12
4
8
9
10
11
syl22anc
⊢
φ
→
X
+
˙
Y
∈
N
⁡
X
Y