Metamath Proof Explorer


Theorem sshjval2

Description: Value of join in the set of closed subspaces of Hilbert space CH . (Contributed by NM, 1-Nov-2000) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion sshjval2
|- ( ( A C_ ~H /\ B C_ ~H ) -> ( A vH B ) = |^| { x e. CH | ( A u. B ) C_ x } )

Proof

Step Hyp Ref Expression
1 sshjval
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
2 unss
 |-  ( ( A C_ ~H /\ B C_ ~H ) <-> ( A u. B ) C_ ~H )
3 ococin
 |-  ( ( A u. B ) C_ ~H -> ( _|_ ` ( _|_ ` ( A u. B ) ) ) = |^| { x e. CH | ( A u. B ) C_ x } )
4 2 3 sylbi
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( _|_ ` ( _|_ ` ( A u. B ) ) ) = |^| { x e. CH | ( A u. B ) C_ x } )
5 1 4 eqtrd
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A vH B ) = |^| { x e. CH | ( A u. B ) C_ x } )