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 32953
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 32952 . 2 class β„šHom
2 vr . . 3 setvar π‘Ÿ
3 cvv 3475 . . 3 class V
4 vx . . . . 5 setvar π‘₯
5 vy . . . . 5 setvar 𝑦
6 cz 12558 . . . . 5 class β„€
72cv 1541 . . . . . . . 8 class π‘Ÿ
8 czrh 21049 . . . . . . . 8 class β„€RHom
97, 8cfv 6544 . . . . . . 7 class (β„€RHomβ€˜π‘Ÿ)
109ccnv 5676 . . . . . 6 class β—‘(β„€RHomβ€˜π‘Ÿ)
11 cui 20169 . . . . . . 7 class Unit
127, 11cfv 6544 . . . . . 6 class (Unitβ€˜π‘Ÿ)
1310, 12cima 5680 . . . . 5 class (β—‘(β„€RHomβ€˜π‘Ÿ) β€œ (Unitβ€˜π‘Ÿ))
144cv 1541 . . . . . . 7 class π‘₯
155cv 1541 . . . . . . 7 class 𝑦
16 cdiv 11871 . . . . . . 7 class /
1714, 15, 16co 7409 . . . . . 6 class (π‘₯ / 𝑦)
1814, 9cfv 6544 . . . . . . 7 class ((β„€RHomβ€˜π‘Ÿ)β€˜π‘₯)
1915, 9cfv 6544 . . . . . . 7 class ((β„€RHomβ€˜π‘Ÿ)β€˜π‘¦)
20 cdvr 20214 . . . . . . . 8 class /r
217, 20cfv 6544 . . . . . . 7 class (/rβ€˜π‘Ÿ)
2218, 19, 21co 7409 . . . . . 6 class (((β„€RHomβ€˜π‘Ÿ)β€˜π‘₯)(/rβ€˜π‘Ÿ)((β„€RHomβ€˜π‘Ÿ)β€˜π‘¦))
2317, 22cop 4635 . . . . 5 class ⟨(π‘₯ / 𝑦), (((β„€RHomβ€˜π‘Ÿ)β€˜π‘₯)(/rβ€˜π‘Ÿ)((β„€RHomβ€˜π‘Ÿ)β€˜π‘¦))⟩
244, 5, 6, 13, 23cmpo 7411 . . . 4 class (π‘₯ ∈ β„€, 𝑦 ∈ (β—‘(β„€RHomβ€˜π‘Ÿ) β€œ (Unitβ€˜π‘Ÿ)) ↦ ⟨(π‘₯ / 𝑦), (((β„€RHomβ€˜π‘Ÿ)β€˜π‘₯)(/rβ€˜π‘Ÿ)((β„€RHomβ€˜π‘Ÿ)β€˜π‘¦))⟩)
2524crn 5678 . . 3 class ran (π‘₯ ∈ β„€, 𝑦 ∈ (β—‘(β„€RHomβ€˜π‘Ÿ) β€œ (Unitβ€˜π‘Ÿ)) ↦ ⟨(π‘₯ / 𝑦), (((β„€RHomβ€˜π‘Ÿ)β€˜π‘₯)(/rβ€˜π‘Ÿ)((β„€RHomβ€˜π‘Ÿ)β€˜π‘¦))⟩)
262, 3, 25cmpt 5232 . 2 class (π‘Ÿ ∈ V ↦ ran (π‘₯ ∈ β„€, 𝑦 ∈ (β—‘(β„€RHomβ€˜π‘Ÿ) β€œ (Unitβ€˜π‘Ÿ)) ↦ ⟨(π‘₯ / 𝑦), (((β„€RHomβ€˜π‘Ÿ)β€˜π‘₯)(/rβ€˜π‘Ÿ)((β„€RHomβ€˜π‘Ÿ)β€˜π‘¦))⟩))
271, 26wceq 1542 1 wff β„šHom = (π‘Ÿ ∈ V ↦ ran (π‘₯ ∈ β„€, 𝑦 ∈ (β—‘(β„€RHomβ€˜π‘Ÿ) β€œ (Unitβ€˜π‘Ÿ)) ↦ ⟨(π‘₯ / 𝑦), (((β„€RHomβ€˜π‘Ÿ)β€˜π‘₯)(/rβ€˜π‘Ÿ)((β„€RHomβ€˜π‘Ÿ)β€˜π‘¦))⟩))
Colors of variables: wff setvar class
This definition is referenced by:  qqhval  32954
  Copyright terms: Public domain W3C validator