Theorem shjcom

Description: Commutative law for Hilbert lattice join of subspaces. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	shjcom	|- ( ( A e. SH /\ B e. SH ) -> ( A vH B ) = ( B vH A ) )

Proof

Step	Hyp	Ref	Expression
1		shjval	|- ( ( A e. SH /\ B e. SH ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
2		shjval	|- ( ( B e. SH /\ A e. SH ) -> ( B vH A ) = ( _|_ ` ( _|_ ` ( B u. A ) ) ) )
3	2	ancoms	|- ( ( A e. SH /\ B e. SH ) -> ( B vH A ) = ( _|_ ` ( _|_ ` ( B u. A ) ) ) )
4		uncom	|- ( B u. A ) = ( A u. B )
5	4	fveq2i	|- ( _|_ ` ( B u. A ) ) = ( _|_ ` ( A u. B ) )
6	5	fveq2i	|- ( _|_ ` ( _|_ ` ( B u. A ) ) ) = ( _|_ ` ( _|_ ` ( A u. B ) ) )
7	3 6	eqtrdi	|- ( ( A e. SH /\ B e. SH ) -> ( B vH A ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
8	1 7	eqtr4d	|- ( ( A e. SH /\ B e. SH ) -> ( A vH B ) = ( B vH A ) )