Metamath Proof Explorer


Theorem qqhvq

Description: The image of a quotient by the QQHom homomorphism. (Contributed by Thierry Arnoux, 28-Oct-2017)

Ref Expression
Hypotheses qqhval2.0 𝐵 = ( Base ‘ 𝑅 )
qqhval2.1 / = ( /r𝑅 )
qqhval2.2 𝐿 = ( ℤRHom ‘ 𝑅 )
Assertion qqhvq ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑋 / 𝑌 ) ) = ( ( 𝐿𝑋 ) / ( 𝐿𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 qqhval2.0 𝐵 = ( Base ‘ 𝑅 )
2 qqhval2.1 / = ( /r𝑅 )
3 qqhval2.2 𝐿 = ( ℤRHom ‘ 𝑅 )
4 zssq ℤ ⊆ ℚ
5 simpr1 ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → 𝑋 ∈ ℤ )
6 4 5 sselid ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → 𝑋 ∈ ℚ )
7 simpr2 ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → 𝑌 ∈ ℤ )
8 4 7 sselid ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → 𝑌 ∈ ℚ )
9 simpr3 ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → 𝑌 ≠ 0 )
10 qdivcl ( ( 𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0 ) → ( 𝑋 / 𝑌 ) ∈ ℚ )
11 6 8 9 10 syl3anc ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 / 𝑌 ) ∈ ℚ )
12 1 2 3 qqhvval ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 / 𝑌 ) ∈ ℚ ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑋 / 𝑌 ) ) = ( ( 𝐿 ‘ ( numer ‘ ( 𝑋 / 𝑌 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑋 / 𝑌 ) ) ) ) )
13 11 12 syldan ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑋 / 𝑌 ) ) = ( ( 𝐿 ‘ ( numer ‘ ( 𝑋 / 𝑌 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑋 / 𝑌 ) ) ) ) )
14 1 2 3 qqhval2lem ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ( 𝐿 ‘ ( numer ‘ ( 𝑋 / 𝑌 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑋 / 𝑌 ) ) ) ) = ( ( 𝐿𝑋 ) / ( 𝐿𝑌 ) ) )
15 13 14 eqtrd ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑋 / 𝑌 ) ) = ( ( 𝐿𝑋 ) / ( 𝐿𝑌 ) ) )