Metamath Proof Explorer

Theorem qqhre

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

Ref Expression
Assertion qqhre 
|- ( QQHom ` RRfld ) = ( _I |` QQ )

Proof

Step Hyp Ref Expression
1 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
2 1 simpri 
 |-  RRfld e. DivRing
3 drngring 
 |-  ( RRfld e. DivRing -> RRfld e. Ring )
4 f1oi 
 |-  ( _I |` ZZ ) : ZZ -1-1-onto-> ZZ
5 f1of1 
 |-  ( ( _I |` ZZ ) : ZZ -1-1-onto-> ZZ -> ( _I |` ZZ ) : ZZ -1-1-> ZZ )
6 4 5 ax-mp 
 |-  ( _I |` ZZ ) : ZZ -1-1-> ZZ
7 zssre 
 |-  ZZ C_ RR
8 f1ss 
 |-  ( ( ( _I |` ZZ ) : ZZ -1-1-> ZZ /\ ZZ C_ RR ) -> ( _I |` ZZ ) : ZZ -1-1-> RR )
9 6 7 8 mp2an 
 |-  ( _I |` ZZ ) : ZZ -1-1-> RR
10 zrhre 
 |-  ( ZRHom ` RRfld ) = ( _I |` ZZ )
11 f1eq1 
 |-  ( ( ZRHom ` RRfld ) = ( _I |` ZZ ) -> ( ( ZRHom ` RRfld ) : ZZ -1-1-> RR <-> ( _I |` ZZ ) : ZZ -1-1-> RR ) )
12 10 11 ax-mp 
 |-  ( ( ZRHom ` RRfld ) : ZZ -1-1-> RR <-> ( _I |` ZZ ) : ZZ -1-1-> RR )
13 9 12 mpbir 
 |-  ( ZRHom ` RRfld ) : ZZ -1-1-> RR
14 rebase 
 |-  RR = ( Base ` RRfld )
15 eqid 
 |-  ( ZRHom ` RRfld ) = ( ZRHom ` RRfld )
16 re0g 
 |-  0 = ( 0g ` RRfld )
17 14 15 16 zrhchr 
 |-  ( RRfld e. Ring -> ( ( chr ` RRfld ) = 0 <-> ( ZRHom ` RRfld ) : ZZ -1-1-> RR ) )
18 13 17 mpbiri 
 |-  ( RRfld e. Ring -> ( chr ` RRfld ) = 0 )
19 2 3 18 mp2b 
 |-  ( chr ` RRfld ) = 0
20 eqid 
 |-  ( /r ` RRfld ) = ( /r ` RRfld )
21 14 20 15 qqhvval 
 |-  ( ( ( RRfld e. DivRing /\ ( chr ` RRfld ) = 0 ) /\ q e. QQ ) -> ( ( QQHom ` RRfld ) ` q ) = ( ( ( ZRHom ` RRfld ) ` ( numer ` q ) ) ( /r ` RRfld ) ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) ) )
22 2 19 21 mpanl12 
 |-  ( q e. QQ -> ( ( QQHom ` RRfld ) ` q ) = ( ( ( ZRHom ` RRfld ) ` ( numer ` q ) ) ( /r ` RRfld ) ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) ) )
23 f1f 
 |-  ( ( ZRHom ` RRfld ) : ZZ -1-1-> RR -> ( ZRHom ` RRfld ) : ZZ --> RR )
24 13 23 ax-mp 
 |-  ( ZRHom ` RRfld ) : ZZ --> RR
25 24 a1i 
 |-  ( q e. QQ -> ( ZRHom ` RRfld ) : ZZ --> RR )
26 qnumcl 
 |-  ( q e. QQ -> ( numer ` q ) e. ZZ )
27 25 26 ffvelrnd 
 |-  ( q e. QQ -> ( ( ZRHom ` RRfld ) ` ( numer ` q ) ) e. RR )
28 qdencl 
 |-  ( q e. QQ -> ( denom ` q ) e. NN )
29 28 nnzd 
 |-  ( q e. QQ -> ( denom ` q ) e. ZZ )
30 25 29 ffvelrnd 
 |-  ( q e. QQ -> ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) e. RR )
31 29 anim1i 
 |-  ( ( q e. QQ /\ ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) = 0 ) -> ( ( denom ` q ) e. ZZ /\ ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) = 0 ) )
32 14 15 16 zrhf1ker 
 |-  ( RRfld e. Ring -> ( ( ZRHom ` RRfld ) : ZZ -1-1-> RR <-> ( `' ( ZRHom ` RRfld ) " { 0 } ) = { 0 } ) )
33 2 3 32 mp2b 
 |-  ( ( ZRHom ` RRfld ) : ZZ -1-1-> RR <-> ( `' ( ZRHom ` RRfld ) " { 0 } ) = { 0 } )
34 13 33 mpbi 
 |-  ( `' ( ZRHom ` RRfld ) " { 0 } ) = { 0 }
35 34 eleq2i 
 |-  ( ( denom ` q ) e. ( `' ( ZRHom ` RRfld ) " { 0 } ) <-> ( denom ` q ) e. { 0 } )
36 ffn 
 |-  ( ( ZRHom ` RRfld ) : ZZ --> RR -> ( ZRHom ` RRfld ) Fn ZZ )
37 fniniseg 
 |-  ( ( ZRHom ` RRfld ) Fn ZZ -> ( ( denom ` q ) e. ( `' ( ZRHom ` RRfld ) " { 0 } ) <-> ( ( denom ` q ) e. ZZ /\ ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) = 0 ) ) )
38 24 36 37 mp2b 
 |-  ( ( denom ` q ) e. ( `' ( ZRHom ` RRfld ) " { 0 } ) <-> ( ( denom ` q ) e. ZZ /\ ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) = 0 ) )
39 fvex 
 |-  ( denom ` q ) e. _V
40 39 elsn 
 |-  ( ( denom ` q ) e. { 0 } <-> ( denom ` q ) = 0 )
41 35 38 40 3bitr3ri 
 |-  ( ( denom ` q ) = 0 <-> ( ( denom ` q ) e. ZZ /\ ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) = 0 ) )
42 31 41 sylibr 
 |-  ( ( q e. QQ /\ ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) = 0 ) -> ( denom ` q ) = 0 )
43 28 nnne0d 
 |-  ( q e. QQ -> ( denom ` q ) =/= 0 )
44 43 adantr 
 |-  ( ( q e. QQ /\ ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) = 0 ) -> ( denom ` q ) =/= 0 )
45 44 neneqd 
 |-  ( ( q e. QQ /\ ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) = 0 ) -> -. ( denom ` q ) = 0 )
46 42 45 pm2.65da 
 |-  ( q e. QQ -> -. ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) = 0 )
47 46 neqned 
 |-  ( q e. QQ -> ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) =/= 0 )
48 redvr 
 |-  ( ( ( ( ZRHom ` RRfld ) ` ( numer ` q ) ) e. RR /\ ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) e. RR /\ ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) =/= 0 ) -> ( ( ( ZRHom ` RRfld ) ` ( numer ` q ) ) ( /r ` RRfld ) ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) ) = ( ( ( ZRHom ` RRfld ) ` ( numer ` q ) ) / ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) ) )
49 27 30 47 48 syl3anc 
 |-  ( q e. QQ -> ( ( ( ZRHom ` RRfld ) ` ( numer ` q ) ) ( /r ` RRfld ) ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) ) = ( ( ( ZRHom ` RRfld ) ` ( numer ` q ) ) / ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) ) )
50 10 fveq1i 
 |-  ( ( ZRHom ` RRfld ) ` ( numer ` q ) ) = ( ( _I |` ZZ ) ` ( numer ` q ) )
51 fvresi 
 |-  ( ( numer ` q ) e. ZZ -> ( ( _I |` ZZ ) ` ( numer ` q ) ) = ( numer ` q ) )
52 50 51 syl5eq 
 |-  ( ( numer ` q ) e. ZZ -> ( ( ZRHom ` RRfld ) ` ( numer ` q ) ) = ( numer ` q ) )
53 26 52 syl 
 |-  ( q e. QQ -> ( ( ZRHom ` RRfld ) ` ( numer ` q ) ) = ( numer ` q ) )
54 10 fveq1i 
 |-  ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) = ( ( _I |` ZZ ) ` ( denom ` q ) )
55 fvresi 
 |-  ( ( denom ` q ) e. ZZ -> ( ( _I |` ZZ ) ` ( denom ` q ) ) = ( denom ` q ) )
56 54 55 syl5eq 
 |-  ( ( denom ` q ) e. ZZ -> ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) = ( denom ` q ) )
57 29 56 syl 
 |-  ( q e. QQ -> ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) = ( denom ` q ) )
58 53 57 oveq12d 
 |-  ( q e. QQ -> ( ( ( ZRHom ` RRfld ) ` ( numer ` q ) ) / ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) ) = ( ( numer ` q ) / ( denom ` q ) ) )
59 qeqnumdivden 
 |-  ( q e. QQ -> q = ( ( numer ` q ) / ( denom ` q ) ) )
60 58 59 eqtr4d 
 |-  ( q e. QQ -> ( ( ( ZRHom ` RRfld ) ` ( numer ` q ) ) / ( ( ZRHom ` RRfld ) ` ( denom ` q ) ) ) = q )
61 22 49 60 3eqtrd 
 |-  ( q e. QQ -> ( ( QQHom ` RRfld ) ` q ) = q )
62 61 mpteq2ia 
 |-  ( q e. QQ |-> ( ( QQHom ` RRfld ) ` q ) ) = ( q e. QQ |-> q )
63 14 20 15 qqhf 
 |-  ( ( RRfld e. DivRing /\ ( chr ` RRfld ) = 0 ) -> ( QQHom ` RRfld ) : QQ --> RR )
64 2 19 63 mp2an 
 |-  ( QQHom ` RRfld ) : QQ --> RR
65 64 a1i 
 |-  ( T. -> ( QQHom ` RRfld ) : QQ --> RR )
66 65 feqmptd 
 |-  ( T. -> ( QQHom ` RRfld ) = ( q e. QQ |-> ( ( QQHom ` RRfld ) ` q ) ) )
67 66 mptru 
 |-  ( QQHom ` RRfld ) = ( q e. QQ |-> ( ( QQHom ` RRfld ) ` q ) )
68 mptresid 
 |-  ( _I |` QQ ) = ( q e. QQ |-> q )
69 62 67 68 3eqtr4i 
 |-  ( QQHom ` RRfld ) = ( _I |` QQ )