Users' Mathboxes 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 31113
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 31112 . 2 class ℚHom
2 vr . . 3 setvar 𝑟
3 cvv 3492 . . 3 class V
4 vx . . . . 5 setvar 𝑥
5 vy . . . . 5 setvar 𝑦
6 cz 11969 . . . . 5 class
72cv 1527 . . . . . . . 8 class 𝑟
8 czrh 20575 . . . . . . . 8 class ℤRHom
97, 8cfv 6348 . . . . . . 7 class (ℤRHom‘𝑟)
109ccnv 5547 . . . . . 6 class (ℤRHom‘𝑟)
11 cui 19318 . . . . . . 7 class Unit
127, 11cfv 6348 . . . . . 6 class (Unit‘𝑟)
1310, 12cima 5551 . . . . 5 class ((ℤRHom‘𝑟) “ (Unit‘𝑟))
144cv 1527 . . . . . . 7 class 𝑥
155cv 1527 . . . . . . 7 class 𝑦
16 cdiv 11285 . . . . . . 7 class /
1714, 15, 16co 7145 . . . . . 6 class (𝑥 / 𝑦)
1814, 9cfv 6348 . . . . . . 7 class ((ℤRHom‘𝑟)‘𝑥)
1915, 9cfv 6348 . . . . . . 7 class ((ℤRHom‘𝑟)‘𝑦)
20 cdvr 19361 . . . . . . . 8 class /r
217, 20cfv 6348 . . . . . . 7 class (/r𝑟)
2218, 19, 21co 7145 . . . . . 6 class (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))
2317, 22cop 4563 . . . . 5 class ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩
244, 5, 6, 13, 23cmpo 7147 . . . 4 class (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩)
2524crn 5549 . . 3 class ran (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩)
262, 3, 25cmpt 5137 . 2 class (𝑟 ∈ V ↦ ran (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩))
271, 26wceq 1528 1 wff ℚHom = (𝑟 ∈ V ↦ ran (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩))
Colors of variables: wff setvar class
This definition is referenced by:  qqhval  31114
  Copyright terms: Public domain W3C validator