# 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 )`
` |-  +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`