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