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+=0

Proof

Step Hyp Ref Expression
1 hilablo +AbelOp
2 ablogrpo +AbelOp+GrpOp
3 1 2 ax-mp +GrpOp
4 ax-hfvadd +:×
5 4 fdmi dom+=×
6 3 5 grporn =ran+
7 eqid GId+=GId+
8 6 7 grpoidval +GrpOpGId+=ιy|xy+x=x
9 3 8 ax-mp GId+=ιy|xy+x=x
10 hvaddid2 x0+x=x
11 10 rgen x0+x=x
12 ax-hv0cl 0
13 6 grpoideu +GrpOp∃!yxy+x=x
14 3 13 ax-mp ∃!yxy+x=x
15 oveq1 y=0y+x=0+x
16 15 eqeq1d y=0y+x=x0+x=x
17 16 ralbidv y=0xy+x=xx0+x=x
18 17 riota2 0∃!yxy+x=xx0+x=xιy|xy+x=x=0
19 12 14 18 mp2an x0+x=xιy|xy+x=x=0
20 11 19 mpbi ιy|xy+x=x=0
21 9 20 eqtri GId+=0