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

Metamath Proof Explorer

Theorem cnfld1

Description: One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014) Avoid ax-mulf . (Revised by GG, 31-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 ovmpot 
 |-  ( ( 1 e. CC /\ x e. CC ) -> ( 1 ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = ( 1 x. x ) )
3 2 eqcomd 
 |-  ( ( 1 e. CC /\ x e. CC ) -> ( 1 x. x ) = ( 1 ( u e. CC , v e. CC |-> ( u x. v ) ) x ) )
4 1 3 mpan 
 |-  ( x e. CC -> ( 1 x. x ) = ( 1 ( u e. CC , v e. CC |-> ( u x. v ) ) x ) )
5 mullid 
 |-  ( x e. CC -> ( 1 x. x ) = x )
6 4 5 eqtr3d 
 |-  ( x e. CC -> ( 1 ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = x )
7 ovmpot 
 |-  ( ( x e. CC /\ 1 e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) 1 ) = ( x x. 1 ) )
8 1 7 mpan2 
 |-  ( x e. CC -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) 1 ) = ( x x. 1 ) )
9 mulrid 
 |-  ( x e. CC -> ( x x. 1 ) = x )
10 8 9 eqtrd 
 |-  ( x e. CC -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) 1 ) = x )
11 6 10 jca 
 |-  ( x e. CC -> ( ( 1 ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = x /\ ( x ( u e. CC , v e. CC |-> ( u x. v ) ) 1 ) = x ) )
12 11 rgen 
 |-  A. x e. CC ( ( 1 ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = x /\ ( x ( u e. CC , v e. CC |-> ( u x. v ) ) 1 ) = x )
13 1 12 pm3.2i 
 |-  ( 1 e. CC /\ A. x e. CC ( ( 1 ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = x /\ ( x ( u e. CC , v e. CC |-> ( u x. v ) ) 1 ) = x ) )
14 cnring 
 |-  CCfld e. Ring
15 cnfldbas 
 |-  CC = ( Base ` CCfld )
16 mpocnfldmul 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) = ( .r ` CCfld )
17 eqid 
 |-  ( 1r ` CCfld ) = ( 1r ` CCfld )
18 15 16 17 isringid 
 |-  ( CCfld e. Ring -> ( ( 1 e. CC /\ A. x e. CC ( ( 1 ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = x /\ ( x ( u e. CC , v e. CC |-> ( u x. v ) ) 1 ) = x ) ) <-> ( 1r ` CCfld ) = 1 ) )
19 14 18 ax-mp 
 |-  ( ( 1 e. CC /\ A. x e. CC ( ( 1 ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = x /\ ( x ( u e. CC , v e. CC |-> ( u x. v ) ) 1 ) = x ) ) <-> ( 1r ` CCfld ) = 1 )
20 13 19 mpbi 
 |-  ( 1r ` CCfld ) = 1
21 20 eqcomi 
 |-  1 = ( 1r ` CCfld )