Theorem qqhvval

Description: Value of the canonical homormorphism from the rational number when the target ring is a division ring. (Contributed by Thierry Arnoux, 30-Oct-2017)

	Ref	Expression
Hypotheses	qqhval2.0	⊢ 𝐵 = ( Base ‘ 𝑅 )
	qqhval2.1	⊢ / = ( /r ‘ 𝑅 )
	qqhval2.2	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
Assertion	qqhvval	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑄 ) = ( ( 𝐿 ‘ ( numer ‘ 𝑄 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑄 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		qqhval2.0	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		qqhval2.1	⊢ / = ( /r ‘ 𝑅 )
3		qqhval2.2	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
4	1 2 3	qqhval2	⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) = ( 𝑞 ∈ ℚ ↦ ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) )
5	4	adantr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( ℚHom ‘ 𝑅 ) = ( 𝑞 ∈ ℚ ↦ ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) )
6		simpr	⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) ∧ 𝑞 = 𝑄 ) → 𝑞 = 𝑄 )
7	6	fveq2d	⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) ∧ 𝑞 = 𝑄 ) → ( numer ‘ 𝑞 ) = ( numer ‘ 𝑄 ) )
8	7	fveq2d	⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) ∧ 𝑞 = 𝑄 ) → ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) = ( 𝐿 ‘ ( numer ‘ 𝑄 ) ) )
9	6	fveq2d	⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) ∧ 𝑞 = 𝑄 ) → ( denom ‘ 𝑞 ) = ( denom ‘ 𝑄 ) )
10	9	fveq2d	⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) ∧ 𝑞 = 𝑄 ) → ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) = ( 𝐿 ‘ ( denom ‘ 𝑄 ) ) )
11	8 10	oveq12d	⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) ∧ 𝑞 = 𝑄 ) → ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) = ( ( 𝐿 ‘ ( numer ‘ 𝑄 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑄 ) ) ) )
12		simpr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → 𝑄 ∈ ℚ )
13		ovexd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( ( 𝐿 ‘ ( numer ‘ 𝑄 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑄 ) ) ) ∈ V )
14	5 11 12 13	fvmptd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑄 ) = ( ( 𝐿 ‘ ( numer ‘ 𝑄 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑄 ) ) ) )