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 | |- +H = ( x e. SH , y e. SH |-> ( +h " ( x X. y ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cph | |- +H |
|
| 1 | vx | |- x |
|
| 2 | csh | |- SH |
|
| 3 | vy | |- y |
|
| 4 | cva | |- +h |
|
| 5 | 1 | cv | |- x |
| 6 | 3 | cv | |- y |
| 7 | 5 6 | cxp | |- ( x X. y ) |
| 8 | 4 7 | cima | |- ( +h " ( x X. y ) ) |
| 9 | 1 3 2 2 8 | cmpo | |- ( x e. SH , y e. SH |-> ( +h " ( x X. y ) ) ) |
| 10 | 0 9 | wceq | |- +H = ( x e. SH , y e. SH |-> ( +h " ( x X. y ) ) ) |