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		addid2	|- ( 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 ` + )