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 )