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 29799
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 29798 . 2 class ℚHom
2 vr . . 3 setvar 𝑟
3 cvv 3186 . . 3 class V
4 vx . . . . 5 setvar 𝑥
5 vy . . . . 5 setvar 𝑦
6 cz 11321 . . . . 5 class
72cv 1479 . . . . . . . 8 class 𝑟
8 czrh 19767 . . . . . . . 8 class ℤRHom
97, 8cfv 5847 . . . . . . 7 class (ℤRHom‘𝑟)
109ccnv 5073 . . . . . 6 class (ℤRHom‘𝑟)
11 cui 18560 . . . . . . 7 class Unit
127, 11cfv 5847 . . . . . 6 class (Unit‘𝑟)
1310, 12cima 5077 . . . . 5 class ((ℤRHom‘𝑟) “ (Unit‘𝑟))
144cv 1479 . . . . . . 7 class 𝑥
155cv 1479 . . . . . . 7 class 𝑦
16 cdiv 10628 . . . . . . 7 class /
1714, 15, 16co 6604 . . . . . 6 class (𝑥 / 𝑦)
1814, 9cfv 5847 . . . . . . 7 class ((ℤRHom‘𝑟)‘𝑥)
1915, 9cfv 5847 . . . . . . 7 class ((ℤRHom‘𝑟)‘𝑦)
20 cdvr 18603 . . . . . . . 8 class /r
217, 20cfv 5847 . . . . . . 7 class (/r𝑟)
2218, 19, 21co 6604 . . . . . 6 class (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))
2317, 22cop 4154 . . . . 5 class ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩
244, 5, 6, 13, 23cmpt2 6606 . . . 4 class (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩)
2524crn 5075 . . 3 class ran (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩)
262, 3, 25cmpt 4673 . 2 class (𝑟 ∈ V ↦ ran (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩))
271, 26wceq 1480 1 wff ℚHom = (𝑟 ∈ V ↦ ran (𝑥 ∈ ℤ, 𝑦 ∈ ((ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r𝑟)((ℤRHom‘𝑟)‘𝑦))⟩))
Colors of variables: wff setvar class
This definition is referenced by:  qqhval  29800
  Copyright terms: Public domain W3C validator