Metamath Proof Explorer


Theorem chsupval2

Description: The value of the supremum of a set of closed subspaces of Hilbert space. Definition of supremum in Proposition 1 of Kalmbach p. 65. (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

Ref Expression
Assertion chsupval2
|- ( A C_ CH -> ( \/H ` A ) = |^| { x e. CH | U. A C_ x } )

Proof

Step Hyp Ref Expression
1 chsspwh
 |-  CH C_ ~P ~H
2 sstr2
 |-  ( A C_ CH -> ( CH C_ ~P ~H -> A C_ ~P ~H ) )
3 1 2 mpi
 |-  ( A C_ CH -> A C_ ~P ~H )
4 hsupval2
 |-  ( A C_ ~P ~H -> ( \/H ` A ) = |^| { x e. CH | U. A C_ x } )
5 3 4 syl
 |-  ( A C_ CH -> ( \/H ` A ) = |^| { x e. CH | U. A C_ x } )