Theorem shscom

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

	Ref	Expression
Assertion	shscom	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to A{+}_{\mathscr{H}}B=B{+}_{\mathscr{H}}A$$

Proof

Step	Hyp	Ref	Expression
1		shel	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge y\in A\right)\to y\in \mathscr{H}$$
2		shel	$$⊢\left(B\in {\mathbf{S}}_{\mathscr{H}}\wedge z\in B\right)\to z\in \mathscr{H}$$
3	1 2	anim12i	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge y\in A\right)\wedge \left(B\in {\mathbf{S}}_{\mathscr{H}}\wedge z\in B\right)\right)\to \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)$$
4	3	an4s	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge \left(y\in A\wedge z\in B\right)\right)\to \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)$$
5		ax-hvcom	$$⊢\left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\to y{+}_{ℎ}z=z{+}_{ℎ}y$$
6	4 5	syl	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge \left(y\in A\wedge z\in B\right)\right)\to y{+}_{ℎ}z=z{+}_{ℎ}y$$
7	6	eqeq2d	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge \left(y\in A\wedge z\in B\right)\right)\to \left(x=y{+}_{ℎ}z\leftrightarrow x=z{+}_{ℎ}y\right)$$
8	7	2rexbidva	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(\exists y\in A\exists z\in Bx=y{+}_{ℎ}z\leftrightarrow \exists y\in A\exists z\in Bx=z{+}_{ℎ}y\right)$$
9		rexcom	$$⊢\exists y\in A\exists z\in Bx=z{+}_{ℎ}y\leftrightarrow \exists z\in B\exists y\in Ax=z{+}_{ℎ}y$$
10	8 9	bitrdi	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(\exists y\in A\exists z\in Bx=y{+}_{ℎ}z\leftrightarrow \exists z\in B\exists y\in Ax=z{+}_{ℎ}y\right)$$
11		shsel	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(x\in \left(A{+}_{\mathscr{H}}B\right)\leftrightarrow \exists y\in A\exists z\in Bx=y{+}_{ℎ}z\right)$$
12		shsel	$$⊢\left(B\in {\mathbf{S}}_{\mathscr{H}}\wedge A\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(x\in \left(B{+}_{\mathscr{H}}A\right)\leftrightarrow \exists z\in B\exists y\in Ax=z{+}_{ℎ}y\right)$$
13	12	ancoms	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(x\in \left(B{+}_{\mathscr{H}}A\right)\leftrightarrow \exists z\in B\exists y\in Ax=z{+}_{ℎ}y\right)$$
14	10 11 13	3bitr4d	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(x\in \left(A{+}_{\mathscr{H}}B\right)\leftrightarrow x\in \left(B{+}_{\mathscr{H}}A\right)\right)$$
15	14	eqrdv	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to A{+}_{\mathscr{H}}B=B{+}_{\mathscr{H}}A$$