# 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
`|- ( H e. SH -> ( +h |` ( H X. H ) ) e. AbelOp )`

### Proof

Step Hyp Ref Expression
1 xpeq1
` |-  ( H = if ( H e. SH , H , ~H ) -> ( H X. H ) = ( if ( H e. SH , H , ~H ) X. H ) )`
2 xpeq2
` |-  ( H = if ( H e. SH , H , ~H ) -> ( if ( H e. SH , H , ~H ) X. H ) = ( if ( H e. SH , H , ~H ) X. if ( H e. SH , H , ~H ) ) )`
3 1 2 eqtrd
` |-  ( H = if ( H e. SH , H , ~H ) -> ( H X. H ) = ( if ( H e. SH , H , ~H ) X. if ( H e. SH , H , ~H ) ) )`
4 3 reseq2d
` |-  ( H = if ( H e. SH , H , ~H ) -> ( +h |` ( H X. H ) ) = ( +h |` ( if ( H e. SH , H , ~H ) X. if ( H e. SH , H , ~H ) ) ) )`
5 4 eleq1d
` |-  ( H = if ( H e. SH , H , ~H ) -> ( ( +h |` ( H X. H ) ) e. AbelOp <-> ( +h |` ( if ( H e. SH , H , ~H ) X. if ( H e. SH , H , ~H ) ) ) e. AbelOp ) )`
6 helsh
` |-  ~H e. SH`
7 6 elimel
` |-  if ( H e. SH , H , ~H ) e. SH`
8 7 hhssabloi
` |-  ( +h |` ( if ( H e. SH , H , ~H ) X. if ( H e. SH , H , ~H ) ) ) e. AbelOp`
9 5 8 dedth
` |-  ( H e. SH -> ( +h |` ( H X. H ) ) e. AbelOp )`