Database
COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
Subspaces and projections
Subspace sum, span, lattice join, lattice supremum
df-shs
Metamath Proof Explorer
Description: Define subspace sum in SH . See shsval , shsval2i , and
shsval3i for its value. (Contributed by NM , 16-Oct-1999)
(New usage is discouraged.)
Ref
Expression
Assertion
df-shs
⊢ + ℋ = x ∈ S ℋ , y ∈ S ℋ ⟼ + ℎ x × y
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cph
class + ℋ
1
vx
setvar x
2
csh
class S ℋ
3
vy
setvar y
4
cva
class + ℎ
5
1
cv
setvar x
6
3
cv
setvar y
7
5 6
cxp
class x × y
8
4 7
cima
class + ℎ x × y
9
1 3 2 2 8
cmpo
class x ∈ S ℋ , y ∈ S ℋ ⟼ + ℎ x × y
10
0 9
wceq
wff + ℋ = x ∈ S ℋ , y ∈ S ℋ ⟼ + ℎ x × y