Definition df-shs 26091

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

Assertion

Ref	Expression
df-shs	|- +H = ( x e. SH , y e. SH |-> ( +h " ( x X. y ) ) )

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-shs

Step	Hyp	Ref	Expression
1		cph 25713	. 2 class +H
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		csh 25710	. . 3 class SH
5		cva 25702	. . . 4 class +h
6	2	cv 1380	. . . . 5 class x
7	3	cv 1380	. . . . 5 class y
8	6, 7	cxp 4983	. . . 4 class ( x X. y )
9	5, 8	cima 4988	. . 3 class ( +h " ( x X. y ) )
10	2, 3, 4, 4, 9	cmpt2 6279	. 2 class ( x e. SH , y e. SH |-> ( +h " ( x X. y ) ) )
11	1, 10	wceq 1381	1 wff +H = ( x e. SH , y e. SH |-> ( +h " ( x X. y ) ) )

This definition is referenced by:  shsval  26095