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

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 
 |-  + e. AbelOp
2 ablogrpo 
 |-  ( + e. AbelOp -> + e. GrpOp )
3 1 2 ax-mp 
 |-  + e. GrpOp
4 ax-addf 
 |-  + : ( CC X. CC ) --> CC
5 4 fdmi 
 |-  dom + = ( CC X. CC )
6 3 5 grporn 
 |-  CC = ran +
7 eqid 
 |-  ( GId ` + ) = ( GId ` + )
8 6 7 grpoidval 
 |-  ( + e. GrpOp -> ( GId ` + ) = ( iota_ y e. CC A. x e. CC ( y + x ) = x ) )
9 3 8 ax-mp 
 |-  ( GId ` + ) = ( iota_ y e. CC A. x e. CC ( y + x ) = x )
10 addlid 
 |-  ( x e. CC -> ( 0 + x ) = x )
11 10 rgen 
 |-  A. x e. CC ( 0 + x ) = x
12 0cn 
 |-  0 e. CC
13 6 grpoideu 
 |-  ( + e. GrpOp -> E! y e. CC A. x e. CC ( y + x ) = x )
14 3 13 ax-mp 
 |-  E! y e. CC A. x e. CC ( 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 -> ( A. x e. CC ( y + x ) = x <-> A. x e. CC ( 0 + x ) = x ) )
18 17 riota2 
 |-  ( ( 0 e. CC /\ E! y e. CC A. x e. CC ( y + x ) = x ) -> ( A. x e. CC ( 0 + x ) = x <-> ( iota_ y e. CC A. x e. CC ( y + x ) = x ) = 0 ) )
19 12 14 18 mp2an 
 |-  ( A. x e. CC ( 0 + x ) = x <-> ( iota_ y e. CC A. x e. CC ( y + x ) = x ) = 0 )
20 11 19 mpbi 
 |-  ( iota_ y e. CC A. x e. CC ( y + x ) = x ) = 0
21 9 20 eqtr2i 
 |-  0 = ( GId ` + )