This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hilid

Description: The group identity element of Hilbert space vector addition is the zero vector. (Contributed by NM, 16-Apr-2007) (New usage is discouraged.)

Ref Expression
Assertion hilid 
|- ( GId ` +h ) = 0h

Proof

Step Hyp Ref Expression
1 hilablo 
 |-  +h e. AbelOp
2 ablogrpo 
 |-  ( +h e. AbelOp -> +h e. GrpOp )
3 1 2 ax-mp 
 |-  +h e. GrpOp
4 ax-hfvadd 
 |-  +h : ( ~H X. ~H ) --> ~H
5 4 fdmi 
 |-  dom +h = ( ~H X. ~H )
6 3 5 grporn 
 |-  ~H = ran +h
7 eqid 
 |-  ( GId ` +h ) = ( GId ` +h )
8 6 7 grpoidval 
 |-  ( +h e. GrpOp -> ( GId ` +h ) = ( iota_ y e. ~H A. x e. ~H ( y +h x ) = x ) )
9 3 8 ax-mp 
 |-  ( GId ` +h ) = ( iota_ y e. ~H A. x e. ~H ( y +h x ) = x )
10 hvaddlid 
 |-  ( x e. ~H -> ( 0h +h x ) = x )
11 10 rgen 
 |-  A. x e. ~H ( 0h +h x ) = x
12 ax-hv0cl 
 |-  0h e. ~H
13 6 grpoideu 
 |-  ( +h e. GrpOp -> E! y e. ~H A. x e. ~H ( y +h x ) = x )
14 3 13 ax-mp 
 |-  E! y e. ~H A. x e. ~H ( y +h x ) = x
15 oveq1 
 |-  ( y = 0h -> ( y +h x ) = ( 0h +h x ) )
16 15 eqeq1d 
 |-  ( y = 0h -> ( ( y +h x ) = x <-> ( 0h +h x ) = x ) )
17 16 ralbidv 
 |-  ( y = 0h -> ( A. x e. ~H ( y +h x ) = x <-> A. x e. ~H ( 0h +h x ) = x ) )
18 17 riota2 
 |-  ( ( 0h e. ~H /\ E! y e. ~H A. x e. ~H ( y +h x ) = x ) -> ( A. x e. ~H ( 0h +h x ) = x <-> ( iota_ y e. ~H A. x e. ~H ( y +h x ) = x ) = 0h ) )
19 12 14 18 mp2an 
 |-  ( A. x e. ~H ( 0h +h x ) = x <-> ( iota_ y e. ~H A. x e. ~H ( y +h x ) = x ) = 0h )
20 11 19 mpbi 
 |-  ( iota_ y e. ~H A. x e. ~H ( y +h x ) = x ) = 0h
21 9 20 eqtri 
 |-  ( GId ` +h ) = 0h