Definition df-shs

Description: Define subspace sum in SH . See shsval , shsval2i , and shsval3i for its value. (Contributed by NM, 16-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	df-shs	$$⊢{+}_{\mathscr{H}}=\left(x\in {\mathbf{S}}_{\mathscr{H}},y\in {\mathbf{S}}_{\mathscr{H}}⟼{+}_{ℎ}\left[x\times y\right]\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cph	$$class{+}_{\mathscr{H}}$$
1		vx	$$setvarx$$
2		csh	$$class{\mathbf{S}}_{\mathscr{H}}$$
3		vy	$$setvary$$
4		cva	$$class{+}_{ℎ}$$
5	1	cv	$$setvarx$$
6	3	cv	$$setvary$$
7	5 6	cxp	$$class\left(x\times y\right)$$
8	4 7	cima	$$class{+}_{ℎ}\left[x\times y\right]$$
9	1 3 2 2 8	cmpo	$$class\left(x\in {\mathbf{S}}_{\mathscr{H}},y\in {\mathbf{S}}_{\mathscr{H}}⟼{+}_{ℎ}\left[x\times y\right]\right)$$
10	0 9	wceq	$$wff{+}_{\mathscr{H}}=\left(x\in {\mathbf{S}}_{\mathscr{H}},y\in {\mathbf{S}}_{\mathscr{H}}⟼{+}_{ℎ}\left[x\times y\right]\right)$$