Metamath Proof Explorer

Definition df-qqh

Description: Define the canonical homomorphism from the rationals into any field. (Contributed by Mario Carneiro, 22-Oct-2017) (Revised by Thierry Arnoux, 23-Oct-2017)

Ref Expression
Assertion df-qqh 
|- QQHom = ( r e. _V |-> ran ( x e. ZZ , y e. ( `' ( ZRHom ` r ) " ( Unit ` r ) ) |-> <. ( x / y ) , ( ( ( ZRHom ` r ) ` x ) ( /r ` r ) ( ( ZRHom ` r ) ` y ) ) >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cqqh 
 |-  QQHom
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vx 
 |-  x
4 cz 
 |-  ZZ
5 vy 
 |-  y
6 czrh 
 |-  ZRHom
7 1 cv 
 |-  r
8 7 6 cfv 
 |-  ( ZRHom ` r )
9 8 ccnv 
 |-  `' ( ZRHom ` r )
10 cui 
 |-  Unit
11 7 10 cfv 
 |-  ( Unit ` r )
12 9 11 cima 
 |-  ( `' ( ZRHom ` r ) " ( Unit ` r ) )
13 3 cv 
 |-  x
14 cdiv 
 |-  /
15 5 cv 
 |-  y
16 13 15 14 co 
 |-  ( x / y )
17 13 8 cfv 
 |-  ( ( ZRHom ` r ) ` x )
18 cdvr 
 |-  /r
19 7 18 cfv 
 |-  ( /r ` r )
20 15 8 cfv 
 |-  ( ( ZRHom ` r ) ` y )
21 17 20 19 co 
 |-  ( ( ( ZRHom ` r ) ` x ) ( /r ` r ) ( ( ZRHom ` r ) ` y ) )
22 16 21 cop 
 |-  <. ( x / y ) , ( ( ( ZRHom ` r ) ` x ) ( /r ` r ) ( ( ZRHom ` r ) ` y ) ) >.
23 3 5 4 12 22 cmpo 
 |-  ( x e. ZZ , y e. ( `' ( ZRHom ` r ) " ( Unit ` r ) ) |-> <. ( x / y ) , ( ( ( ZRHom ` r ) ` x ) ( /r ` r ) ( ( ZRHom ` r ) ` y ) ) >. )
24 23 crn 
 |-  ran ( x e. ZZ , y e. ( `' ( ZRHom ` r ) " ( Unit ` r ) ) |-> <. ( x / y ) , ( ( ( ZRHom ` r ) ` x ) ( /r ` r ) ( ( ZRHom ` r ) ` y ) ) >. )
25 1 2 24 cmpt 
 |-  ( r e. _V |-> ran ( x e. ZZ , y e. ( `' ( ZRHom ` r ) " ( Unit ` r ) ) |-> <. ( x / y ) , ( ( ( ZRHom ` r ) ` x ) ( /r ` r ) ( ( ZRHom ` r ) ` y ) ) >. ) )
26 0 25 wceq 
 |-  QQHom = ( r e. _V |-> ran ( x e. ZZ , y e. ( `' ( ZRHom ` r ) " ( Unit ` r ) ) |-> <. ( x / y ) , ( ( ( ZRHom ` r ) ` x ) ( /r ` r ) ( ( ZRHom ` r ) ` y ) ) >. ) )