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