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 } ) |
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 } ) |