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 = ( 𝑟 ∈ V ↦ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ◡ ( ℤRHom ‘ 𝑟 ) “ ( Unit ‘ 𝑟 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑥 ) ( /r ‘ 𝑟 ) ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑦 ) ) ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cqqh	⊢ ℚHom
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cz	⊢ ℤ
5		vy	⊢ 𝑦
6		czrh	⊢ ℤRHom
7	1	cv	⊢ 𝑟
8	7 6	cfv	⊢ ( ℤRHom ‘ 𝑟 )
9	8	ccnv	⊢ ◡ ( ℤRHom ‘ 𝑟 )
10		cui	⊢ Unit
11	7 10	cfv	⊢ ( Unit ‘ 𝑟 )
12	9 11	cima	⊢ ( ◡ ( ℤRHom ‘ 𝑟 ) “ ( Unit ‘ 𝑟 ) )
13	3	cv	⊢ 𝑥
14		cdiv	⊢ /
15	5	cv	⊢ 𝑦
16	13 15 14	co	⊢ ( 𝑥 / 𝑦 )
17	13 8	cfv	⊢ ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑥 )
18		cdvr	⊢ /r
19	7 18	cfv	⊢ ( /r ‘ 𝑟 )
20	15 8	cfv	⊢ ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑦 )
21	17 20 19	co	⊢ ( ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑥 ) ( /r ‘ 𝑟 ) ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑦 ) )
22	16 21	cop	⊢ ⟨ ( 𝑥 / 𝑦 ) , ( ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑥 ) ( /r ‘ 𝑟 ) ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑦 ) ) ⟩
23	3 5 4 12 22	cmpo	⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ◡ ( ℤRHom ‘ 𝑟 ) “ ( Unit ‘ 𝑟 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑥 ) ( /r ‘ 𝑟 ) ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑦 ) ) ⟩ )
24	23	crn	⊢ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ◡ ( ℤRHom ‘ 𝑟 ) “ ( Unit ‘ 𝑟 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑥 ) ( /r ‘ 𝑟 ) ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑦 ) ) ⟩ )
25	1 2 24	cmpt	⊢ ( 𝑟 ∈ V ↦ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ◡ ( ℤRHom ‘ 𝑟 ) “ ( Unit ‘ 𝑟 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑥 ) ( /r ‘ 𝑟 ) ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑦 ) ) ⟩ ) )
26	0 25	wceq	⊢ ℚHom = ( 𝑟 ∈ V ↦ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ◡ ( ℤRHom ‘ 𝑟 ) “ ( Unit ‘ 𝑟 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑥 ) ( /r ‘ 𝑟 ) ( ( ℤRHom ‘ 𝑟 ) ‘ 𝑦 ) ) ⟩ ) )