Metamath Proof Explorer

Theorem zrhre

Description: The ZRHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017)

Ref Expression
Assertion zrhre 
|- ( ZRHom ` RRfld ) = ( _I |` ZZ )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 remulg 
 |-  ( ( n e. ZZ /\ 1 e. RR ) -> ( n ( .g ` RRfld ) 1 ) = ( n x. 1 ) )
3 1 2 mpan2 
 |-  ( n e. ZZ -> ( n ( .g ` RRfld ) 1 ) = ( n x. 1 ) )
4 zre 
 |-  ( n e. ZZ -> n e. RR )
5 ax-1rid 
 |-  ( n e. RR -> ( n x. 1 ) = n )
6 4 5 syl 
 |-  ( n e. ZZ -> ( n x. 1 ) = n )
7 3 6 eqtrd 
 |-  ( n e. ZZ -> ( n ( .g ` RRfld ) 1 ) = n )
8 7 mpteq2ia 
 |-  ( n e. ZZ |-> ( n ( .g ` RRfld ) 1 ) ) = ( n e. ZZ |-> n )
9 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
10 9 simpri 
 |-  RRfld e. DivRing
11 drngring 
 |-  ( RRfld e. DivRing -> RRfld e. Ring )
12 eqid 
 |-  ( ZRHom ` RRfld ) = ( ZRHom ` RRfld )
13 eqid 
 |-  ( .g ` RRfld ) = ( .g ` RRfld )
14 re1r 
 |-  1 = ( 1r ` RRfld )
15 12 13 14 zrhval2 
 |-  ( RRfld e. Ring -> ( ZRHom ` RRfld ) = ( n e. ZZ |-> ( n ( .g ` RRfld ) 1 ) ) )
16 10 11 15 mp2b 
 |-  ( ZRHom ` RRfld ) = ( n e. ZZ |-> ( n ( .g ` RRfld ) 1 ) )
17 mptresid 
 |-  ( _I |` ZZ ) = ( n e. ZZ |-> n )
18 8 16 17 3eqtr4i 
 |-  ( ZRHom ` RRfld ) = ( _I |` ZZ )