Step |
Hyp |
Ref |
Expression |
1 |
|
ax-hilex |
|- ~H e. _V |
2 |
|
ax-hfvadd |
|- +h : ( ~H X. ~H ) --> ~H |
3 |
|
ax-hvass |
|- ( ( x e. ~H /\ y e. ~H /\ z e. ~H ) -> ( ( x +h y ) +h z ) = ( x +h ( y +h z ) ) ) |
4 |
|
ax-hv0cl |
|- 0h e. ~H |
5 |
|
hvaddid2 |
|- ( x e. ~H -> ( 0h +h x ) = x ) |
6 |
|
neg1cn |
|- -u 1 e. CC |
7 |
|
hvmulcl |
|- ( ( -u 1 e. CC /\ x e. ~H ) -> ( -u 1 .h x ) e. ~H ) |
8 |
6 7
|
mpan |
|- ( x e. ~H -> ( -u 1 .h x ) e. ~H ) |
9 |
|
ax-hvcom |
|- ( ( ( -u 1 .h x ) e. ~H /\ x e. ~H ) -> ( ( -u 1 .h x ) +h x ) = ( x +h ( -u 1 .h x ) ) ) |
10 |
8 9
|
mpancom |
|- ( x e. ~H -> ( ( -u 1 .h x ) +h x ) = ( x +h ( -u 1 .h x ) ) ) |
11 |
|
hvnegid |
|- ( x e. ~H -> ( x +h ( -u 1 .h x ) ) = 0h ) |
12 |
10 11
|
eqtrd |
|- ( x e. ~H -> ( ( -u 1 .h x ) +h x ) = 0h ) |
13 |
1 2 3 4 5 8 12
|
isgrpoi |
|- +h e. GrpOp |
14 |
2
|
fdmi |
|- dom +h = ( ~H X. ~H ) |
15 |
|
ax-hvcom |
|- ( ( x e. ~H /\ y e. ~H ) -> ( x +h y ) = ( y +h x ) ) |
16 |
13 14 15
|
isabloi |
|- +h e. AbelOp |