Metamath Proof Explorer

Definition df-qqh

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)

Ref Expression
Assertion df-qqh ⊢ ℚHom = r ∈ V ⟼ ran ⁡ x ∈ ℤ , y ∈ ℤRHom ⁡ r -1 Unit ⁡ r ⟼ x y ℤRHom ⁡ r ⁡ x / r ⁡ r ℤRHom ⁡ r ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cqqh class ℚHom
1 vr setvar r
2 cvv class V
3 vx setvar x
4 cz class ℤ
5 vy setvar y
6 czrh class ℤRHom
7 1 cv setvar r
8 7 6 cfv class ℤRHom ⁡ r
9 8 ccnv class ℤRHom ⁡ r -1
10 cui class Unit
11 7 10 cfv class Unit ⁡ r
12 9 11 cima class ℤRHom ⁡ r -1 Unit ⁡ r
13 3 cv setvar x
14 cdiv class ÷
15 5 cv setvar y
16 13 15 14 co class x y
17 13 8 cfv class ℤRHom ⁡ r ⁡ x
18 cdvr class / r
19 7 18 cfv class / r ⁡ r
20 15 8 cfv class ℤRHom ⁡ r ⁡ y
21 17 20 19 co class ℤRHom ⁡ r ⁡ x / r ⁡ r ℤRHom ⁡ r ⁡ y
22 16 21 cop class x y ℤRHom ⁡ r ⁡ x / r ⁡ r ℤRHom ⁡ r ⁡ y
23 3 5 4 12 22 cmpo class x ∈ ℤ , y ∈ ℤRHom ⁡ r -1 Unit ⁡ r ⟼ x y ℤRHom ⁡ r ⁡ x / r ⁡ r ℤRHom ⁡ r ⁡ y
24 23 crn class ran ⁡ x ∈ ℤ , y ∈ ℤRHom ⁡ r -1 Unit ⁡ r ⟼ x y ℤRHom ⁡ r ⁡ x / r ⁡ r ℤRHom ⁡ r ⁡ y
25 1 2 24 cmpt class r ∈ V ⟼ ran ⁡ x ∈ ℤ , y ∈ ℤRHom ⁡ r -1 Unit ⁡ r ⟼ x y ℤRHom ⁡ r ⁡ x / r ⁡ r ℤRHom ⁡ r ⁡ y
26 0 25 wceq wff ℚHom = r ∈ V ⟼ ran ⁡ x ∈ ℤ , y ∈ ℤRHom ⁡ r -1 Unit ⁡ r ⟼ x y ℤRHom ⁡ r ⁡ x / r ⁡ r ℤRHom ⁡ r ⁡ y