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 31299
 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 31298 . 2 class ℚHom
2 vr . . 3 setvar 𝑟
3 cvv 3480 . . 3 class V
4 vx . . . . 5 setvar 𝑥
5 vy . . . . 5 setvar 𝑦
6 cz 11980 . . . . 5 class
72cv 1537 . . . . . . . 8 class 𝑟
8 czrh 20202 . . . . . . . 8 class ℤRHom
97, 8cfv 6345 . . . . . . 7 class (ℤRHom‘𝑟)
109ccnv 5542 . . . . . 6 class (ℤRHom‘𝑟)
11 cui 19394 . . . . . . 7 class Unit
127, 11cfv 6345 . . . . . 6 class (Unit‘𝑟)
1310, 12cima 5546 . . . . 5 class ((ℤRHom‘𝑟) “ (Unit‘𝑟))
144cv 1537 . . . . . . 7 class 𝑥
155cv 1537 . . . . . . 7 class 𝑦
16 cdiv 11297 . . . . . . 7 class /
1714, 15, 16co 7151 . . . . . 6 class (𝑥 / 𝑦)
1814, 9cfv 6345 . . . . . . 7 class ((ℤRHom‘𝑟)‘𝑥)
1915, 9cfv 6345 . . . . . . 7 class ((ℤRHom‘𝑟)‘𝑦)
20 cdvr 19437 . . . . . . . 8 class /r
217, 20cfv 6345 . . . . . . 7 class (/r𝑟)
2218, 19, 21co 7151 . . . . . 6 class (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))
2317, 22cop 4556 . . . . 5 class ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩
244, 5, 6, 13, 23cmpo 7153 . . . 4 class (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩)
2524crn 5544 . . 3 class ran (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩)
262, 3, 25cmpt 5133 . 2 class (𝑟 ∈ V ↦ ran (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩))
271, 26wceq 1538 1 wff ℚHom = (𝑟 ∈ V ↦ ran (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩))
 Colors of variables: wff setvar class This definition is referenced by:  qqhval  31300
 Copyright terms: Public domain W3C validator