Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
dihsmsnrn
Next ⟩
dihsmatrn
Metamath Proof Explorer
Ascii
Unicode
Theorem
dihsmsnrn
Description:
The subspace sum of two singleton spans is closed.
(Contributed by
NM
, 27-Feb-2015)
Ref
Expression
Hypotheses
dihsmsnrn.h
⊢
H
=
LHyp
⁡
K
dihsmsnrn.u
⊢
U
=
DVecH
⁡
K
⁡
W
dihsmsnrn.v
⊢
V
=
Base
U
dihsmsnrn.p
⊢
⊕
˙
=
LSSum
⁡
U
dihsmsnrn.n
⊢
N
=
LSpan
⁡
U
dihsmsnrn.i
⊢
I
=
DIsoH
⁡
K
⁡
W
dihsmsnrn.k
⊢
φ
→
K
∈
HL
∧
W
∈
H
dihsmsnrn.x
⊢
φ
→
X
∈
V
dihsmsnrn.y
⊢
φ
→
Y
∈
V
Assertion
dihsmsnrn
⊢
φ
→
N
⁡
X
⊕
˙
N
⁡
Y
∈
ran
⁡
I
Proof
Step
Hyp
Ref
Expression
1
dihsmsnrn.h
⊢
H
=
LHyp
⁡
K
2
dihsmsnrn.u
⊢
U
=
DVecH
⁡
K
⁡
W
3
dihsmsnrn.v
⊢
V
=
Base
U
4
dihsmsnrn.p
⊢
⊕
˙
=
LSSum
⁡
U
5
dihsmsnrn.n
⊢
N
=
LSpan
⁡
U
6
dihsmsnrn.i
⊢
I
=
DIsoH
⁡
K
⁡
W
7
dihsmsnrn.k
⊢
φ
→
K
∈
HL
∧
W
∈
H
8
dihsmsnrn.x
⊢
φ
→
X
∈
V
9
dihsmsnrn.y
⊢
φ
→
Y
∈
V
10
1
2
3
5
6
dihlsprn
⊢
K
∈
HL
∧
W
∈
H
∧
X
∈
V
→
N
⁡
X
∈
ran
⁡
I
11
7
8
10
syl2anc
⊢
φ
→
N
⁡
X
∈
ran
⁡
I
12
1
2
3
4
5
6
7
11
9
dihsmsprn
⊢
φ
→
N
⁡
X
⊕
˙
N
⁡
Y
∈
ran
⁡
I