Theorem hhssablo

Description: Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	hhssablo	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to {{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)}\in \mathrm{AbelOp}$$

Proof

Step	Hyp	Ref	Expression
1		xpeq1	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\to H\times H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\times H$$
2		xpeq2	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\to if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\times H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)$$
3	1 2	eqtrd	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\to H\times H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)$$
4	3	reseq2d	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\to {{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)}={{+}_{ℎ}\upharpoonright }_{\left(if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\right)}$$
5	4	eleq1d	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\to \left({{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)}\in \mathrm{AbelOp}\leftrightarrow {{+}_{ℎ}\upharpoonright }_{\left(if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\right)}\in \mathrm{AbelOp}\right)$$
6		helsh	$$⊢\mathscr{H}\in {\mathbf{S}}_{\mathscr{H}}$$
7	6	elimel	$$⊢if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\in {\mathbf{S}}_{\mathscr{H}}$$
8	7	hhssabloi	$$⊢{{+}_{ℎ}\upharpoonright }_{\left(if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,\mathscr{H}\right)\right)}\in \mathrm{AbelOp}$$
9	5 8	dedth	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to {{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)}\in \mathrm{AbelOp}$$