This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sshjval

Description: Value of join for subsets of Hilbert space. (Contributed by NM, 1-Nov-2000) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion sshjval 
|- ( ( A C_ ~H /\ B C_ ~H ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-hilex 
 |-  ~H e. _V
2 1 elpw2 
 |-  ( A e. ~P ~H <-> A C_ ~H )
3 1 elpw2 
 |-  ( B e. ~P ~H <-> B C_ ~H )
4 uneq12 
 |-  ( ( x = A /\ y = B ) -> ( x u. y ) = ( A u. B ) )
5 4 fveq2d 
 |-  ( ( x = A /\ y = B ) -> ( _|_ ` ( x u. y ) ) = ( _|_ ` ( A u. B ) ) )
6 5 fveq2d 
 |-  ( ( x = A /\ y = B ) -> ( _|_ ` ( _|_ ` ( x u. y ) ) ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
7 df-chj 
 |-  vH = ( x e. ~P ~H , y e. ~P ~H |-> ( _|_ ` ( _|_ ` ( x u. y ) ) ) )
8 fvex 
 |-  ( _|_ ` ( _|_ ` ( A u. B ) ) ) e. _V
9 6 7 8 ovmpoa 
 |-  ( ( A e. ~P ~H /\ B e. ~P ~H ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
10 2 3 9 syl2anbr 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )