Metamath Proof Explorer

Theorem qqh1

Description: The image of 1 by the QQHom homomorphism is the ring's unit. (Contributed by Thierry Arnoux, 22-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 qqhval2.0 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 qqhval2.1 ⊢ / = ( /r ‘ 𝑅 )
3 qqhval2.2 ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
4 zssq ⊢ ℤ ⊆ ℚ
5 1z ⊢ 1 ∈ ℤ
6 4 5 sselii ⊢ 1 ∈ ℚ
7 1 2 3 qqhvval ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 1 ∈ ℚ ) → ( ( ℚHom ‘ 𝑅 ) ‘ 1 ) = ( ( 𝐿 ‘ ( numer ‘ 1 ) ) / ( 𝐿 ‘ ( denom ‘ 1 ) ) ) )
8 6 7 mpan2 ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ( ℚHom ‘ 𝑅 ) ‘ 1 ) = ( ( 𝐿 ‘ ( numer ‘ 1 ) ) / ( 𝐿 ‘ ( denom ‘ 1 ) ) ) )
9 gcd1 ⊢ ( 1 ∈ ℤ → ( 1 gcd 1 ) = 1 )
10 5 9 ax-mp ⊢ ( 1 gcd 1 ) = 1
11 1div1e1 ⊢ ( 1 / 1 ) = 1
12 11 eqcomi ⊢ 1 = ( 1 / 1 )
13 10 12 pm3.2i ⊢ ( ( 1 gcd 1 ) = 1 ∧ 1 = ( 1 / 1 ) )
14 1nn ⊢ 1 ∈ ℕ
15 qnumdenbi ⊢ ( ( 1 ∈ ℚ ∧ 1 ∈ ℤ ∧ 1 ∈ ℕ ) → ( ( ( 1 gcd 1 ) = 1 ∧ 1 = ( 1 / 1 ) ) ↔ ( ( numer ‘ 1 ) = 1 ∧ ( denom ‘ 1 ) = 1 ) ) )
16 6 5 14 15 mp3an ⊢ ( ( ( 1 gcd 1 ) = 1 ∧ 1 = ( 1 / 1 ) ) ↔ ( ( numer ‘ 1 ) = 1 ∧ ( denom ‘ 1 ) = 1 ) )
17 13 16 mpbi ⊢ ( ( numer ‘ 1 ) = 1 ∧ ( denom ‘ 1 ) = 1 )
18 17 simpli ⊢ ( numer ‘ 1 ) = 1
19 18 fveq2i ⊢ ( 𝐿 ‘ ( numer ‘ 1 ) ) = ( 𝐿 ‘ 1 )
20 17 simpri ⊢ ( denom ‘ 1 ) = 1
21 20 fveq2i ⊢ ( 𝐿 ‘ ( denom ‘ 1 ) ) = ( 𝐿 ‘ 1 )
22 19 21 oveq12i ⊢ ( ( 𝐿 ‘ ( numer ‘ 1 ) ) / ( 𝐿 ‘ ( denom ‘ 1 ) ) ) = ( ( 𝐿 ‘ 1 ) / ( 𝐿 ‘ 1 ) )
23 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
24 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
25 3 24 zrh1 ⊢ ( 𝑅 ∈ Ring → ( 𝐿 ‘ 1 ) = ( 1r ‘ 𝑅 ) )
26 25 25 oveq12d ⊢ ( 𝑅 ∈ Ring → ( ( 𝐿 ‘ 1 ) / ( 𝐿 ‘ 1 ) ) = ( ( 1r ‘ 𝑅 ) / ( 1r ‘ 𝑅 ) ) )
27 23 26 syl ⊢ ( 𝑅 ∈ DivRing → ( ( 𝐿 ‘ 1 ) / ( 𝐿 ‘ 1 ) ) = ( ( 1r ‘ 𝑅 ) / ( 1r ‘ 𝑅 ) ) )
28 1 24 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
29 1 2 24 dvr1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) / ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
30 23 28 29 syl2anc2 ⊢ ( 𝑅 ∈ DivRing → ( ( 1r ‘ 𝑅 ) / ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
31 27 30 eqtrd ⊢ ( 𝑅 ∈ DivRing → ( ( 𝐿 ‘ 1 ) / ( 𝐿 ‘ 1 ) ) = ( 1r ‘ 𝑅 ) )
32 22 31 syl5eq ⊢ ( 𝑅 ∈ DivRing → ( ( 𝐿 ‘ ( numer ‘ 1 ) ) / ( 𝐿 ‘ ( denom ‘ 1 ) ) ) = ( 1r ‘ 𝑅 ) )
33 32 adantr ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ( 𝐿 ‘ ( numer ‘ 1 ) ) / ( 𝐿 ‘ ( denom ‘ 1 ) ) ) = ( 1r ‘ 𝑅 ) )
34 8 33 eqtrd ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ( ℚHom ‘ 𝑅 ) ‘ 1 ) = ( 1r ‘ 𝑅 ) )