Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-qqh Structured version   Visualization version   GIF version

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
StepHypRef 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
72cv 1474 . . . . . . . 8 class 𝑟
8 czrh 19667 . . . . . . . 8 class ℤRHom
97, 8cfv 5804 . . . . . . 7 class (ℤRHom‘𝑟)
109ccnv 5037 . . . . . 6 class (ℤRHom‘𝑟)
11 cui 18462 . . . . . . 7 class Unit
127, 11cfv 5804 . . . . . 6 class (Unit‘𝑟)
1310, 12cima 5041 . . . . 5 class ((ℤRHom‘𝑟) “ (Unit‘𝑟))
144cv 1474 . . . . . . 7 class 𝑥
155cv 1474 . . . . . . 7 class 𝑦
16 cdiv 10563 . . . . . . 7 class /
1714, 15, 16co 6549 . . . . . 6 class (𝑥 / 𝑦)
1814, 9cfv 5804 . . . . . . 7 class ((ℤRHom‘𝑟)‘𝑥)
1915, 9cfv 5804 . . . . . . 7 class ((ℤRHom‘𝑟)‘𝑦)
20 cdvr 18505 . . . . . . . 8 class /r
217, 20cfv 5804 . . . . . . 7 class (/r𝑟)
2218, 19, 21co 6549 . . . . . 6 class (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))
2317, 22cop 4131 . . . . 5 class ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩
244, 5, 6, 13, 23cmpt2 6551 . . . 4 class (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩)
2524crn 5039 . . 3 class ran (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩)
262, 3, 25cmpt 4643 . 2 class (𝑟 ∈ V ↦ ran (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩))
271, 26wceq 1475 1 wff ℚHom = (𝑟 ∈ V ↦ ran (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩))
 Colors of variables: wff setvar class This definition is referenced by:  qqhval  29346
 Copyright terms: Public domain W3C validator