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 \in V ⟼ ran (x \in ℤ, y \in {ℤRHom (r)}^{-1} [Unit (r)] ⟼ ⟨\frac{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 \div$
15	5	cv	$setvar y$
16	13 15 14	co	$class (\frac{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 ⟨\frac{x}{y}, ℤRHom (r) (x) /_{r} (r) ℤRHom (r) (y)⟩$
23	3 5 4 12 22	cmpo	$class (x \in ℤ, y \in {ℤRHom (r)}^{-1} [Unit (r)] ⟼ ⟨\frac{x}{y}, ℤRHom (r) (x) /_{r} (r) ℤRHom (r) (y)⟩)$
24	23	crn	$class ran (x \in ℤ, y \in {ℤRHom (r)}^{-1} [Unit (r)] ⟼ ⟨\frac{x}{y}, ℤRHom (r) (x) /_{r} (r) ℤRHom (r) (y)⟩)$
25	1 2 24	cmpt	$class (r \in V ⟼ ran (x \in ℤ, y \in {ℤRHom (r)}^{-1} [Unit (r)] ⟼ ⟨\frac{x}{y}, ℤRHom (r) (x) /_{r} (r) ℤRHom (r) (y)⟩))$
26	0 25	wceq	$wff ℚHom = (r \in V ⟼ ran (x \in ℤ, y \in {ℤRHom (r)}^{-1} [Unit (r)] ⟼ ⟨\frac{x}{y}, ℤRHom (r) (x) /_{r} (r) ℤRHom (r) (y)⟩))$

Metamath Proof Explorer

Definition df-qqh

Detailed syntax breakdown