Definition df-qqh 29345

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	⊢ ℚHom = (𝑟 ∈ V ↦ ran (𝑥 ∈ ℤ, 𝑦 ∈ (◡(ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r‘𝑟)((ℤRHom‘𝑟)‘𝑦))⟩))

Distinct variable group:   𝑥,𝑟,𝑦

Detailed syntax breakdown of Definition df-qqh

Step	Hyp	Ref	Expression
1		cqqh 29344	. 2 class ℚHom
2		vr	. . 3 setvar 𝑟
3		cvv 3173	. . 3 class V
4		vx	. . . . 5 setvar 𝑥
5		vy	. . . . 5 setvar 𝑦
6		cz 11254	. . . . 5 class ℤ
7	2	cv 1474	. . . . . . . 8 class 𝑟
8		czrh 19667	. . . . . . . 8 class ℤRHom
9	7, 8	cfv 5804	. . . . . . 7 class (ℤRHom‘𝑟)
10	9	ccnv 5037	. . . . . 6 class ◡(ℤRHom‘𝑟)
11		cui 18462	. . . . . . 7 class Unit
12	7, 11	cfv 5804	. . . . . 6 class (Unit‘𝑟)
13	10, 12	cima 5041	. . . . 5 class (◡(ℤRHom‘𝑟) “ (Unit‘𝑟))
14	4	cv 1474	. . . . . . 7 class 𝑥
15	5	cv 1474	. . . . . . 7 class 𝑦
16		cdiv 10563	. . . . . . 7 class /
17	14, 15, 16	co 6549	. . . . . 6 class (𝑥 / 𝑦)
18	14, 9	cfv 5804	. . . . . . 7 class ((ℤRHom‘𝑟)‘𝑥)
19	15, 9	cfv 5804	. . . . . . 7 class ((ℤRHom‘𝑟)‘𝑦)
20		cdvr 18505	. . . . . . . 8 class /r
21	7, 20	cfv 5804	. . . . . . 7 class (/r‘𝑟)
22	18, 19, 21	co 6549	. . . . . 6 class (((ℤRHom‘𝑟)‘𝑥)(/r‘𝑟)((ℤRHom‘𝑟)‘𝑦))
23	17, 22	cop 4131	. . . . 5 class ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r‘𝑟)((ℤRHom‘𝑟)‘𝑦))⟩
24	4, 5, 6, 13, 23	cmpt2 6551	. . . 4 class (𝑥 ∈ ℤ, 𝑦 ∈ (◡(ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r‘𝑟)((ℤRHom‘𝑟)‘𝑦))⟩)
25	24	crn 5039	. . 3 class ran (𝑥 ∈ ℤ, 𝑦 ∈ (◡(ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r‘𝑟)((ℤRHom‘𝑟)‘𝑦))⟩)
26	2, 3, 25	cmpt 4643	. 2 class (𝑟 ∈ V ↦ ran (𝑥 ∈ ℤ, 𝑦 ∈ (◡(ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r‘𝑟)((ℤRHom‘𝑟)‘𝑦))⟩))
27	1, 26	wceq 1475	1 wff ℚHom = (𝑟 ∈ V ↦ ran (𝑥 ∈ ℤ, 𝑦 ∈ (◡(ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r‘𝑟)((ℤRHom‘𝑟)‘𝑦))⟩))

This definition is referenced by:  qqhval  29346