Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > df-shs | Structured version Visualization version GIF version |
Description: Define subspace sum in Sℋ. See shsval 29089, shsval2i 29164, and shsval3i 29165 for its value. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-shs | ⊢ +ℋ = (𝑥 ∈ Sℋ , 𝑦 ∈ Sℋ ↦ ( +ℎ “ (𝑥 × 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cph 28708 | . 2 class +ℋ | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | csh 28705 | . . 3 class Sℋ | |
5 | cva 28697 | . . . 4 class +ℎ | |
6 | 2 | cv 1536 | . . . . 5 class 𝑥 |
7 | 3 | cv 1536 | . . . . 5 class 𝑦 |
8 | 6, 7 | cxp 5553 | . . . 4 class (𝑥 × 𝑦) |
9 | 5, 8 | cima 5558 | . . 3 class ( +ℎ “ (𝑥 × 𝑦)) |
10 | 2, 3, 4, 4, 9 | cmpo 7158 | . 2 class (𝑥 ∈ Sℋ , 𝑦 ∈ Sℋ ↦ ( +ℎ “ (𝑥 × 𝑦))) |
11 | 1, 10 | wceq 1537 | 1 wff +ℋ = (𝑥 ∈ Sℋ , 𝑦 ∈ Sℋ ↦ ( +ℎ “ (𝑥 × 𝑦))) |
Colors of variables: wff setvar class |
This definition is referenced by: shsval 29089 |
Copyright terms: Public domain | W3C validator |