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 27339
Description: Define subspace sum in S. See shsval 27343, shsval2i 27418, and shsval3i 27419 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 26960 . 2 class +
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 csh 26957 . . 3 class S
5 cva 26949 . . . 4 class +
62cv 1473 . . . . 5 class 𝑥
73cv 1473 . . . . 5 class 𝑦
86, 7cxp 4930 . . . 4 class (𝑥 × 𝑦)
95, 8cima 4935 . . 3 class ( + “ (𝑥 × 𝑦))
102, 3, 4, 4, 9cmpt2 6428 . 2 class (𝑥S , 𝑦S ↦ ( + “ (𝑥 × 𝑦)))
111, 10wceq 1474 1 wff + = (𝑥S , 𝑦S ↦ ( + “ (𝑥 × 𝑦)))
Colors of variables: wff setvar class
This definition is referenced by:  shsval  27343
  Copyright terms: Public domain W3C validator