Metamath Proof Explorer


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 )