qqhval

Description: Value of the canonical homormorphism from the rational number to a field. (Contributed by Thierry Arnoux, 22-Oct-2017)

	Ref	Expression
Hypotheses	qqhval.1	⊢ / = ( /_r ‘ 𝑅 )
	qqhval.2	⊢ 1 = ( 1_r ‘ 𝑅 )
	qqhval.3	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
Assertion	qqhval	⊢ ( 𝑅 ∈ V → ( ℚHom ‘ 𝑅 ) = ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ^◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		qqhval.1	⊢ / = ( /_r ‘ 𝑅 )
2		qqhval.2	⊢ 1 = ( 1_r ‘ 𝑅 )
3		qqhval.3	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
4		eqidd	⊢ ( 𝑓 = 𝑅 → ℤ = ℤ )
5		fveq2	⊢ ( 𝑓 = 𝑅 → ( ℤRHom ‘ 𝑓 ) = ( ℤRHom ‘ 𝑅 ) )
6	5 3	eqtr4di	⊢ ( 𝑓 = 𝑅 → ( ℤRHom ‘ 𝑓 ) = 𝐿 )
7	6	cnveqd	⊢ ( 𝑓 = 𝑅 → ^◡ ( ℤRHom ‘ 𝑓 ) = ^◡ 𝐿 )
8		fveq2	⊢ ( 𝑓 = 𝑅 → ( Unit ‘ 𝑓 ) = ( Unit ‘ 𝑅 ) )
9	7 8	imaeq12d	⊢ ( 𝑓 = 𝑅 → ( ^◡ ( ℤRHom ‘ 𝑓 ) “ ( Unit ‘ 𝑓 ) ) = ( ^◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) )
10		fveq2	⊢ ( 𝑓 = 𝑅 → ( /_r ‘ 𝑓 ) = ( /_r ‘ 𝑅 ) )
11	10 1	eqtr4di	⊢ ( 𝑓 = 𝑅 → ( /_r ‘ 𝑓 ) = / )
12	6	fveq1d	⊢ ( 𝑓 = 𝑅 → ( ( ℤRHom ‘ 𝑓 ) ‘ 𝑥 ) = ( 𝐿 ‘ 𝑥 ) )
13	6	fveq1d	⊢ ( 𝑓 = 𝑅 → ( ( ℤRHom ‘ 𝑓 ) ‘ 𝑦 ) = ( 𝐿 ‘ 𝑦 ) )
14	11 12 13	oveq123d	⊢ ( 𝑓 = 𝑅 → ( ( ( ℤRHom ‘ 𝑓 ) ‘ 𝑥 ) ( /_r ‘ 𝑓 ) ( ( ℤRHom ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) )
15	14	opeq2d	⊢ ( 𝑓 = 𝑅 → ⟨ ( 𝑥 / 𝑦 ) , ( ( ( ℤRHom ‘ 𝑓 ) ‘ 𝑥 ) ( /_r ‘ 𝑓 ) ( ( ℤRHom ‘ 𝑓 ) ‘ 𝑦 ) ) ⟩ = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ )
16	4 9 15	mpoeq123dv	⊢ ( 𝑓 = 𝑅 → ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ^◡ ( ℤRHom ‘ 𝑓 ) “ ( Unit ‘ 𝑓 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( ( ℤRHom ‘ 𝑓 ) ‘ 𝑥 ) ( /_r ‘ 𝑓 ) ( ( ℤRHom ‘ 𝑓 ) ‘ 𝑦 ) ) ⟩ ) = ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ^◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) )
17	16	rneqd	⊢ ( 𝑓 = 𝑅 → ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ^◡ ( ℤRHom ‘ 𝑓 ) “ ( Unit ‘ 𝑓 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( ( ℤRHom ‘ 𝑓 ) ‘ 𝑥 ) ( /_r ‘ 𝑓 ) ( ( ℤRHom ‘ 𝑓 ) ‘ 𝑦 ) ) ⟩ ) = ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ^◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) )
18		df-qqh	⊢ ℚHom = ( 𝑓 ∈ V ↦ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ^◡ ( ℤRHom ‘ 𝑓 ) “ ( Unit ‘ 𝑓 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( ( ℤRHom ‘ 𝑓 ) ‘ 𝑥 ) ( /_r ‘ 𝑓 ) ( ( ℤRHom ‘ 𝑓 ) ‘ 𝑦 ) ) ⟩ ) )
19		zex	⊢ ℤ ∈ V
20	3	fvexi	⊢ 𝐿 ∈ V
21	20	cnvex	⊢ ^◡ 𝐿 ∈ V
22		imaexg	⊢ ( ^◡ 𝐿 ∈ V → ( ^◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ∈ V )
23	21 22	ax-mp	⊢ ( ^◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ∈ V
24	19 23	mpoex	⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ^◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) ∈ V
25	24	rnex	⊢ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ^◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) ∈ V
26	17 18 25	fvmpt	⊢ ( 𝑅 ∈ V → ( ℚHom ‘ 𝑅 ) = ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ^◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) )

Metamath Proof Explorer

Theorem qqhval

Proof