This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-shs

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 +ℋ = ( 𝑥 ∈ Sℋ , 𝑦 ∈ Sℋ ↦ ( +ℎ “ ( 𝑥 × 𝑦 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cph ⊢ +ℋ
1 vx ⊢ 𝑥
2 csh ⊢ Sℋ
3 vy ⊢ 𝑦
4 cva ⊢ +ℎ
5 1 cv ⊢ 𝑥
6 3 cv ⊢ 𝑦
7 5 6 cxp ⊢ ( 𝑥 × 𝑦 )
8 4 7 cima ⊢ ( +ℎ “ ( 𝑥 × 𝑦 ) )
9 1 3 2 2 8 cmpo ⊢ ( 𝑥 ∈ Sℋ , 𝑦 ∈ Sℋ ↦ ( +ℎ “ ( 𝑥 × 𝑦 ) ) )
10 0 9 wceq ⊢ +ℋ = ( 𝑥 ∈ Sℋ , 𝑦 ∈ Sℋ ↦ ( +ℎ “ ( 𝑥 × 𝑦 ) ) )