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

Definition df-shs 27551
 Description: Define subspace sum in Sℋ. See shsval 27555, shsval2i 27630, and shsval3i 27631 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 27172 . 2 class +
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 csh 27169 . . 3 class S
5 cva 27161 . . . 4 class +
62cv 1474 . . . . 5 class 𝑥
73cv 1474 . . . . 5 class 𝑦
86, 7cxp 5036 . . . 4 class (𝑥 × 𝑦)
95, 8cima 5041 . . 3 class ( + “ (𝑥 × 𝑦))
102, 3, 4, 4, 9cmpt2 6551 . 2 class (𝑥S , 𝑦S ↦ ( + “ (𝑥 × 𝑦)))
111, 10wceq 1475 1 wff + = (𝑥S , 𝑦S ↦ ( + “ (𝑥 × 𝑦)))
 Colors of variables: wff setvar class This definition is referenced by:  shsval  27555
 Copyright terms: Public domain W3C validator