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