Metamath Proof Explorer


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 + = x S , y S + x × y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cph class +
1 vx setvar x
2 csh class S
3 vy setvar y
4 cva class +
5 1 cv setvar x
6 3 cv setvar y
7 5 6 cxp class x × y
8 4 7 cima class + x × y
9 1 3 2 2 8 cmpo class x S , y S + x × y
10 0 9 wceq wff + = x S , y S + x × y