Metamath Proof Explorer

Theorem qqhval

Description: Value of the canonical homormorphism from the rational number to a field. (Contributed by Thierry Arnoux, 22-Oct-2017)

Ref Expression
Hypotheses qqhval.1 
|- ./ = ( /r ` R )
qqhval.2 
|- .1. = ( 1r ` R )
qqhval.3 
|- L = ( ZRHom ` R )
Assertion qqhval 
|- ( R e. _V -> ( QQHom ` R ) = ran ( x e. ZZ , y e. ( `' L " ( Unit ` R ) ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) )

Proof

Step Hyp Ref Expression
1 qqhval.1 
 |-  ./ = ( /r ` R )
2 qqhval.2 
 |-  .1. = ( 1r ` R )
3 qqhval.3 
 |-  L = ( ZRHom ` R )
4 eqidd 
 |-  ( f = R -> ZZ = ZZ )
5 fveq2 
 |-  ( f = R -> ( ZRHom ` f ) = ( ZRHom ` R ) )
6 5 3 eqtr4di 
 |-  ( f = R -> ( ZRHom ` f ) = L )
7 6 cnveqd 
 |-  ( f = R -> `' ( ZRHom ` f ) = `' L )
8 fveq2 
 |-  ( f = R -> ( Unit ` f ) = ( Unit ` R ) )
9 7 8 imaeq12d 
 |-  ( f = R -> ( `' ( ZRHom ` f ) " ( Unit ` f ) ) = ( `' L " ( Unit ` R ) ) )
10 fveq2 
 |-  ( f = R -> ( /r ` f ) = ( /r ` R ) )
11 10 1 eqtr4di 
 |-  ( f = R -> ( /r ` f ) = ./ )
12 6 fveq1d 
 |-  ( f = R -> ( ( ZRHom ` f ) ` x ) = ( L ` x ) )
13 6 fveq1d 
 |-  ( f = R -> ( ( ZRHom ` f ) ` y ) = ( L ` y ) )
14 11 12 13 oveq123d 
 |-  ( f = R -> ( ( ( ZRHom ` f ) ` x ) ( /r ` f ) ( ( ZRHom ` f ) ` y ) ) = ( ( L ` x ) ./ ( L ` y ) ) )
15 14 opeq2d 
 |-  ( f = R -> <. ( x / y ) , ( ( ( ZRHom ` f ) ` x ) ( /r ` f ) ( ( ZRHom ` f ) ` y ) ) >. = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. )
16 4 9 15 mpoeq123dv 
 |-  ( f = R -> ( x e. ZZ , y e. ( `' ( ZRHom ` f ) " ( Unit ` f ) ) |-> <. ( x / y ) , ( ( ( ZRHom ` f ) ` x ) ( /r ` f ) ( ( ZRHom ` f ) ` y ) ) >. ) = ( x e. ZZ , y e. ( `' L " ( Unit ` R ) ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) )
17 16 rneqd 
 |-  ( f = R -> ran ( x e. ZZ , y e. ( `' ( ZRHom ` f ) " ( Unit ` f ) ) |-> <. ( x / y ) , ( ( ( ZRHom ` f ) ` x ) ( /r ` f ) ( ( ZRHom ` f ) ` y ) ) >. ) = ran ( x e. ZZ , y e. ( `' L " ( Unit ` R ) ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) )
18 df-qqh 
 |-  QQHom = ( f e. _V |-> ran ( x e. ZZ , y e. ( `' ( ZRHom ` f ) " ( Unit ` f ) ) |-> <. ( x / y ) , ( ( ( ZRHom ` f ) ` x ) ( /r ` f ) ( ( ZRHom ` f ) ` y ) ) >. ) )
19 zex 
 |-  ZZ e. _V
20 3 fvexi 
 |-  L e. _V
21 20 cnvex 
 |-  `' L e. _V
22 imaexg 
 |-  ( `' L e. _V -> ( `' L " ( Unit ` R ) ) e. _V )
23 21 22 ax-mp 
 |-  ( `' L " ( Unit ` R ) ) e. _V
24 19 23 mpoex 
 |-  ( x e. ZZ , y e. ( `' L " ( Unit ` R ) ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) e. _V
25 24 rnex 
 |-  ran ( x e. ZZ , y e. ( `' L " ( Unit ` R ) ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) e. _V
26 17 18 25 fvmpt 
 |-  ( R e. _V -> ( QQHom ` R ) = ran ( x e. ZZ , y e. ( `' L " ( Unit ` R ) ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) )