Metamath Proof Explorer

Theorem hilablo

Description: Hilbert space vector addition is an Abelian group operation. (Contributed by NM, 15-Apr-2007) (New usage is discouraged.)

Ref Expression
Assertion hilablo 
|- +h e. AbelOp

Proof

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 hvaddlid 
 |-  ( 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