Metamath Proof Explorer

Theorem cnfld1

Description: One is the unit element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Assertion cnfld1 
|- 1 = ( 1r ` CCfld )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 mulid2 
 |-  ( x e. CC -> ( 1 x. x ) = x )
3 mulid1 
 |-  ( x e. CC -> ( x x. 1 ) = x )
4 2 3 jca 
 |-  ( x e. CC -> ( ( 1 x. x ) = x /\ ( x x. 1 ) = x ) )
5 4 rgen 
 |-  A. x e. CC ( ( 1 x. x ) = x /\ ( x x. 1 ) = x )
6 1 5 pm3.2i 
 |-  ( 1 e. CC /\ A. x e. CC ( ( 1 x. x ) = x /\ ( x x. 1 ) = x ) )
7 cnring 
 |-  CCfld e. Ring
8 cnfldbas 
 |-  CC = ( Base ` CCfld )
9 cnfldmul 
 |-  x. = ( .r ` CCfld )
10 eqid 
 |-  ( 1r ` CCfld ) = ( 1r ` CCfld )
11 8 9 10 isringid 
 |-  ( CCfld e. Ring -> ( ( 1 e. CC /\ A. x e. CC ( ( 1 x. x ) = x /\ ( x x. 1 ) = x ) ) <-> ( 1r ` CCfld ) = 1 ) )
12 7 11 ax-mp 
 |-  ( ( 1 e. CC /\ A. x e. CC ( ( 1 x. x ) = x /\ ( x x. 1 ) = x ) ) <-> ( 1r ` CCfld ) = 1 )
13 6 12 mpbi 
 |-  ( 1r ` CCfld ) = 1
14 13 eqcomi 
 |-  1 = ( 1r ` CCfld )