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

Metamath Proof Explorer

Theorem cnaddid

Description: The group identity element of complex number addition is zero. See also cnfld0 . (Contributed by Steve Rodriguez, 3-Dec-2006) (Revised by AV, 26-Aug-2021) (New usage is discouraged.)

Ref Expression
Hypothesis cnaddabl.g 
|- G = { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. }
Assertion cnaddid 
|- ( 0g ` G ) = 0

Proof

Step Hyp Ref Expression
1 cnaddabl.g 
 |-  G = { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. }
2 0cn 
 |-  0 e. CC
3 cnex 
 |-  CC e. _V
4 1 grpbase 
 |-  ( CC e. _V -> CC = ( Base ` G ) )
5 3 4 ax-mp 
 |-  CC = ( Base ` G )
6 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
7 addex 
 |-  + e. _V
8 1 grpplusg 
 |-  ( + e. _V -> + = ( +g ` G ) )
9 7 8 ax-mp 
 |-  + = ( +g ` G )
10 id 
 |-  ( 0 e. CC -> 0 e. CC )
11 addlid 
 |-  ( x e. CC -> ( 0 + x ) = x )
12 11 adantl 
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( 0 + x ) = x )
13 addrid 
 |-  ( x e. CC -> ( x + 0 ) = x )
14 13 adantl 
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( x + 0 ) = x )
15 5 6 9 10 12 14 ismgmid2 
 |-  ( 0 e. CC -> 0 = ( 0g ` G ) )
16 2 15 ax-mp 
 |-  0 = ( 0g ` G )
17 16 eqcomi 
 |-  ( 0g ` G ) = 0