HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-shs Structured version   Visualization version   GIF version

Definition df-shs 28524
Description: Define subspace sum in S. See shsval 28528, shsval2i 28603, and shsval3i 28604 for its value. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.)
Assertion
Ref Expression
df-shs + = (𝑥S , 𝑦S ↦ ( + “ (𝑥 × 𝑦)))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-shs
StepHypRef Expression
1 cph 28145 . 2 class +
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 csh 28142 . . 3 class S
5 cva 28134 . . . 4 class +
62cv 1633 . . . . 5 class 𝑥
73cv 1633 . . . . 5 class 𝑦
86, 7cxp 5261 . . . 4 class (𝑥 × 𝑦)
95, 8cima 5266 . . 3 class ( + “ (𝑥 × 𝑦))
102, 3, 4, 4, 9cmpt2 6814 . 2 class (𝑥S , 𝑦S ↦ ( + “ (𝑥 × 𝑦)))
111, 10wceq 1634 1 wff + = (𝑥S , 𝑦S ↦ ( + “ (𝑥 × 𝑦)))
Colors of variables: wff setvar class
This definition is referenced by:  shsval  28528
  Copyright terms: Public domain W3C validator