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 ℤRHom fld = I

Proof

Step Hyp Ref Expression
1 1re 1
2 remulg n 1 n fld 1 = n 1
3 1 2 mpan2 n n fld 1 = n 1
4 zre n n
5 ax-1rid n n 1 = n
6 4 5 syl n n 1 = n
7 3 6 eqtrd n n fld 1 = n
8 7 mpteq2ia n n fld 1 = n n
9 resubdrg SubRing fld fld DivRing
10 9 simpri fld DivRing
11 drngring fld DivRing fld Ring
12 eqid ℤRHom fld = ℤRHom fld
13 eqid fld = fld
14 re1r 1 = 1 fld
15 12 13 14 zrhval2 fld Ring ℤRHom fld = n n fld 1
16 10 11 15 mp2b ℤRHom fld = n n fld 1
17 mptresid I = n n
18 8 16 17 3eqtr4i ℤRHom fld = I