Metamath Proof Explorer


Theorem cnidOLD

Description: Obsolete version of cnaddid . The group identity element of complex number addition is zero. (Contributed by Steve Rodriguez, 3-Dec-2006) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion cnidOLD 0 = GId +

Proof

Step Hyp Ref Expression
1 cnaddabloOLD + AbelOp
2 ablogrpo + AbelOp + GrpOp
3 1 2 ax-mp + GrpOp
4 ax-addf + : ×
5 4 fdmi dom + = ×
6 3 5 grporn = ran +
7 eqid GId + = GId +
8 6 7 grpoidval + GrpOp GId + = ι y | x y + x = x
9 3 8 ax-mp GId + = ι y | x y + x = x
10 addid2 x 0 + x = x
11 10 rgen x 0 + x = x
12 0cn 0
13 6 grpoideu + GrpOp ∃! y x y + x = x
14 3 13 ax-mp ∃! y x y + x = x
15 oveq1 y = 0 y + x = 0 + x
16 15 eqeq1d y = 0 y + x = x 0 + x = x
17 16 ralbidv y = 0 x y + x = x x 0 + x = x
18 17 riota2 0 ∃! y x y + x = x x 0 + x = x ι y | x y + x = x = 0
19 12 14 18 mp2an x 0 + x = x ι y | x y + x = x = 0
20 11 19 mpbi ι y | x y + x = x = 0
21 9 20 eqtr2i 0 = GId +