Database
BASIC TOPOLOGY
Metric subcomplex vector spaces
Subcomplex vector spaces
cnlmodlem2
Next ⟩
cnlmodlem3
Metamath Proof Explorer
Ascii
Unicode
Theorem
cnlmodlem2
Description:
Lemma 2 for
cnlmod
.
(Contributed by
AV
, 20-Sep-2021)
Ref
Expression
Hypothesis
cnlmod.w
⊢
W
=
Base
ndx
ℂ
+
ndx
+
∪
Scalar
⁡
ndx
ℂ
fld
⋅
ndx
×
Assertion
cnlmodlem2
⊢
+
W
=
+
Proof
Step
Hyp
Ref
Expression
1
cnlmod.w
⊢
W
=
Base
ndx
ℂ
+
ndx
+
∪
Scalar
⁡
ndx
ℂ
fld
⋅
ndx
×
2
addex
⊢
+
∈
V
3
qdass
⊢
Base
ndx
ℂ
+
ndx
+
∪
Scalar
⁡
ndx
ℂ
fld
⋅
ndx
×
=
Base
ndx
ℂ
+
ndx
+
Scalar
⁡
ndx
ℂ
fld
∪
⋅
ndx
×
4
1
3
eqtri
⊢
W
=
Base
ndx
ℂ
+
ndx
+
Scalar
⁡
ndx
ℂ
fld
∪
⋅
ndx
×
5
4
lmodplusg
⊢
+
∈
V
→
+
=
+
W
6
5
eqcomd
⊢
+
∈
V
→
+
W
=
+
7
2
6
ax-mp
⊢
+
W
=
+