Metamath Proof Explorer

Theorem hhssabloi

Description: Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008) (Revised by Mario Carneiro, 23-Dec-2013) (Proof shortened by AV, 27-Aug-2021) (New usage is discouraged.)

Ref Expression
Hypothesis hhssabl.1 
|- H e. SH
Assertion hhssabloi 
|- ( +h |` ( H X. H ) ) e. AbelOp

Proof

Step Hyp Ref Expression
1 hhssabl.1 
 |-  H e. SH
2 1 hhssabloilem 
 |-  ( +h e. GrpOp /\ ( +h |` ( H X. H ) ) e. GrpOp /\ ( +h |` ( H X. H ) ) C_ +h )
3 2 simp2i 
 |-  ( +h |` ( H X. H ) ) e. GrpOp
4 1 shssii 
 |-  H C_ ~H
5 xpss12 
 |-  ( ( H C_ ~H /\ H C_ ~H ) -> ( H X. H ) C_ ( ~H X. ~H ) )
6 4 4 5 mp2an 
 |-  ( H X. H ) C_ ( ~H X. ~H )
7 ax-hfvadd 
 |-  +h : ( ~H X. ~H ) --> ~H
8 7 fdmi 
 |-  dom +h = ( ~H X. ~H )
9 6 8 sseqtrri 
 |-  ( H X. H ) C_ dom +h
10 ssdmres 
 |-  ( ( H X. H ) C_ dom +h <-> dom ( +h |` ( H X. H ) ) = ( H X. H ) )
11 9 10 mpbi 
 |-  dom ( +h |` ( H X. H ) ) = ( H X. H )
12 1 sheli 
 |-  ( x e. H -> x e. ~H )
13 1 sheli 
 |-  ( y e. H -> y e. ~H )
14 ax-hvcom 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x +h y ) = ( y +h x ) )
15 12 13 14 syl2an 
 |-  ( ( x e. H /\ y e. H ) -> ( x +h y ) = ( y +h x ) )
16 ovres 
 |-  ( ( x e. H /\ y e. H ) -> ( x ( +h |` ( H X. H ) ) y ) = ( x +h y ) )
17 ovres 
 |-  ( ( y e. H /\ x e. H ) -> ( y ( +h |` ( H X. H ) ) x ) = ( y +h x ) )
18 17 ancoms 
 |-  ( ( x e. H /\ y e. H ) -> ( y ( +h |` ( H X. H ) ) x ) = ( y +h x ) )
19 15 16 18 3eqtr4d 
 |-  ( ( x e. H /\ y e. H ) -> ( x ( +h |` ( H X. H ) ) y ) = ( y ( +h |` ( H X. H ) ) x ) )
20 3 11 19 isabloi 
 |-  ( +h |` ( H X. H ) ) e. AbelOp