Theorem shscom

Description: Commutative law for subspace sum. (Contributed by NM, 15-Dec-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	shscom	|- ( ( A e. SH /\ B e. SH ) -> ( A +H B ) = ( B +H A ) )

Proof

Step	Hyp	Ref	Expression
1		shel	|- ( ( A e. SH /\ y e. A ) -> y e. ~H )
2		shel	|- ( ( B e. SH /\ z e. B ) -> z e. ~H )
3	1 2	anim12i	|- ( ( ( A e. SH /\ y e. A ) /\ ( B e. SH /\ z e. B ) ) -> ( y e. ~H /\ z e. ~H ) )
4	3	an4s	|- ( ( ( A e. SH /\ B e. SH ) /\ ( y e. A /\ z e. B ) ) -> ( y e. ~H /\ z e. ~H ) )
5		ax-hvcom	|- ( ( y e. ~H /\ z e. ~H ) -> ( y +h z ) = ( z +h y ) )
6	4 5	syl	|- ( ( ( A e. SH /\ B e. SH ) /\ ( y e. A /\ z e. B ) ) -> ( y +h z ) = ( z +h y ) )
7	6	eqeq2d	|- ( ( ( A e. SH /\ B e. SH ) /\ ( y e. A /\ z e. B ) ) -> ( x = ( y +h z ) <-> x = ( z +h y ) ) )
8	7	2rexbidva	|- ( ( A e. SH /\ B e. SH ) -> ( E. y e. A E. z e. B x = ( y +h z ) <-> E. y e. A E. z e. B x = ( z +h y ) ) )
9		rexcom	|- ( E. y e. A E. z e. B x = ( z +h y ) <-> E. z e. B E. y e. A x = ( z +h y ) )
10	8 9	bitrdi	|- ( ( A e. SH /\ B e. SH ) -> ( E. y e. A E. z e. B x = ( y +h z ) <-> E. z e. B E. y e. A x = ( z +h y ) ) )
11		shsel	|- ( ( A e. SH /\ B e. SH ) -> ( x e. ( A +H B ) <-> E. y e. A E. z e. B x = ( y +h z ) ) )
12		shsel	|- ( ( B e. SH /\ A e. SH ) -> ( x e. ( B +H A ) <-> E. z e. B E. y e. A x = ( z +h y ) ) )
13	12	ancoms	|- ( ( A e. SH /\ B e. SH ) -> ( x e. ( B +H A ) <-> E. z e. B E. y e. A x = ( z +h y ) ) )
14	10 11 13	3bitr4d	|- ( ( A e. SH /\ B e. SH ) -> ( x e. ( A +H B ) <-> x e. ( B +H A ) ) )
15	14	eqrdv	|- ( ( A e. SH /\ B e. SH ) -> ( A +H B ) = ( B +H A ) )