Theorem hhssablo

Description: Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	hhssablo	⊢ ( 𝐻 ∈ Sℋ → ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ AbelOp )

Proof

Step	Hyp	Ref	Expression
1		xpeq1	⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) → ( 𝐻 × 𝐻 ) = ( if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) × 𝐻 ) )
2		xpeq2	⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) → ( if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) × 𝐻 ) = ( if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) ) )
3	1 2	eqtrd	⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) → ( 𝐻 × 𝐻 ) = ( if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) ) )
4	3	reseq2d	⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) → ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( +ℎ ↾ ( if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) ) ) )
5	4	eleq1d	⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) → ( ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ AbelOp ↔ ( +ℎ ↾ ( if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) ) ) ∈ AbelOp ) )
6		helsh	⊢ ℋ ∈ Sℋ
7	6	elimel	⊢ if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) ∈ Sℋ
8	7	hhssabloi	⊢ ( +ℎ ↾ ( if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , ℋ ) ) ) ∈ AbelOp
9	5 8	dedth	⊢ ( 𝐻 ∈ Sℋ → ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ AbelOp )