This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database COMPLEX HILBERT SPACE EXPLORER (DEPRECATED) Subspaces and projections Subspace sum, span, lattice join, lattice supremum hsupval
Description: Value of supremum of set of subsets of Hilbert space. For an alternate
version of the value, see hsupval2 . (Contributed by NM , 9-Dec-2003)
(Revised by Mario Carneiro , 23-Dec-2013)
(New usage is discouraged.)
Ref
Expression
Assertion
hsupval ⊢ A ⊆ 𝒫 ℋ → ⋁ ℋ A = ⊥ ⊥ ⋃ A
Proof
Step
Hyp
Ref
Expression
1
ax-hilex ⊢ ℋ ∈ V
2
1
pwex ⊢ 𝒫 ℋ ∈ V
3
2
elpw2 ⊢ A ∈ 𝒫 𝒫 ℋ ↔ A ⊆ 𝒫 ℋ
4
unieq ⊢ x = A → ⋃ x = ⋃ A
5
4
fveq2d ⊢ x = A → ⊥ ⋃ x = ⊥ ⋃ A
6
5
fveq2d ⊢ x = A → ⊥ ⊥ ⋃ x = ⊥ ⊥ ⋃ A
7
df-chsup ⊢ ⋁ ℋ = x ∈ 𝒫 𝒫 ℋ ⟼ ⊥ ⊥ ⋃ x
8
fvex ⊢ ⊥ ⊥ ⋃ A ∈ V
9
6 7 8
fvmpt ⊢ A ∈ 𝒫 𝒫 ℋ → ⋁ ℋ A = ⊥ ⊥ ⋃ A
10
3 9
sylbir ⊢ A ⊆ 𝒫 ℋ → ⋁ ℋ A = ⊥ ⊥ ⋃ A