Definition df-qqh 30017

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.)

Assertion

Ref	Expression
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 ) ) >. ) )

Distinct variable group:   x, r, y

Detailed syntax breakdown of Definition df-qqh

Step	Hyp	Ref	Expression
1		cqqh 30016	. 2 class QQHom
2		vr	. . 3 setvar r
3		cvv 3200	. . 3 class _V
4		vx	. . . . 5 setvar x
5		vy	. . . . 5 setvar y
6		cz 11377	. . . . 5 class ZZ
7	2	cv 1482	. . . . . . . 8 class r
8		czrh 19848	. . . . . . . 8 class ZRHom
9	7, 8	cfv 5888	. . . . . . 7 class ( ZRHom ` r )
10	9	ccnv 5113	. . . . . 6 class `' ( ZRHom ` r )
11		cui 18639	. . . . . . 7 class Unit
12	7, 11	cfv 5888	. . . . . 6 class (Unit ` r )
13	10, 12	cima 5117	. . . . 5 class ( `' ( ZRHom ` r ) " (Unit ` r ) )
14	4	cv 1482	. . . . . . 7 class x
15	5	cv 1482	. . . . . . 7 class y
16		cdiv 10684	. . . . . . 7 class /
17	14, 15, 16	co 6650	. . . . . 6 class ( x / y )
18	14, 9	cfv 5888	. . . . . . 7 class ( ( ZRHom ` r ) ` x )
19	15, 9	cfv 5888	. . . . . . 7 class ( ( ZRHom ` r ) ` y )
20		cdvr 18682	. . . . . . . 8 class /r
21	7, 20	cfv 5888	. . . . . . 7 class (/r ` r )
22	18, 19, 21	co 6650	. . . . . 6 class ( ( ( ZRHom ` r ) ` x ) (/r ` r ) ( ( ZRHom ` r ) ` y ) )
23	17, 22	cop 4183	. . . . 5 class <. ( x / y ) , ( ( ( ZRHom ` r ) ` x ) (/r ` r ) ( ( ZRHom ` r ) ` y ) ) >.
24	4, 5, 6, 13, 23	cmpt2 6652	. . . 4 class ( x e. ZZ , y e. ( `' ( ZRHom ` r ) " (Unit ` r ) ) |-> <. ( x / y ) , ( ( ( ZRHom ` r ) ` x ) (/r ` r ) ( ( ZRHom ` r ) ` y ) ) >. )
25	24	crn 5115	. . 3 class ran ( x e. ZZ , y e. ( `' ( ZRHom ` r ) " (Unit ` r ) ) |-> <. ( x / y ) , ( ( ( ZRHom ` r ) ` x ) (/r ` r ) ( ( ZRHom ` r ) ` y ) ) >. )
26	2, 3, 25	cmpt 4729	. 2 class ( r e. _V |-> ran ( x e. ZZ , y e. ( `' ( ZRHom ` r ) " (Unit ` r ) ) |-> <. ( x / y ) , ( ( ( ZRHom ` r ) ` x ) (/r ` r ) ( ( ZRHom ` r ) ` y ) ) >. ) )
27	1, 26	wceq 1483	1 wff QQHom = ( r e. _V |-> ran ( x e. ZZ , y e. ( `' ( ZRHom ` r ) " (Unit ` r ) ) |-> <. ( x / y ) , ( ( ( ZRHom ` r ) ` x ) (/r ` r ) ( ( ZRHom ` r ) ` y ) ) >. ) )

This definition is referenced by:  qqhval  30018