Metamath Proof Explorer


Theorem chsupval

Description: The value of the supremum of a set of closed subspaces of Hilbert space. For an alternate version of the value, see chsupval2 . (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

Ref Expression
Assertion chsupval ( 𝐴C → ( 𝐴 ) = ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 chsspwh C ⊆ 𝒫 ℋ
2 sstr2 ( 𝐴C → ( C ⊆ 𝒫 ℋ → 𝐴 ⊆ 𝒫 ℋ ) )
3 1 2 mpi ( 𝐴C𝐴 ⊆ 𝒫 ℋ )
4 hsupval ( 𝐴 ⊆ 𝒫 ℋ → ( 𝐴 ) = ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
5 3 4 syl ( 𝐴C → ( 𝐴 ) = ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )