Metamath Proof Explorer

Theorem qqhf

Description: QQHom as a function. (Contributed by Thierry Arnoux, 28-Oct-2017)

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

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 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
6 5 adantr ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → 𝑅 ∈ Ring )
7 6 adantr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → 𝑅 ∈ Ring )
8 3 zrhrhm ⊢ ( 𝑅 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
9 zringbas ⊢ ℤ = ( Base ‘ ℤring )
10 9 1 rhmf ⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) → 𝐿 : ℤ ⟶ 𝐵 )
11 7 8 10 3syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → 𝐿 : ℤ ⟶ 𝐵 )
12 qnumcl ⊢ ( 𝑞 ∈ ℚ → ( numer ‘ 𝑞 ) ∈ ℤ )
13 12 adantl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ( numer ‘ 𝑞 ) ∈ ℤ )
14 11 13 ffvelcdmd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) ∈ 𝐵 )
15 simpll ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → 𝑅 ∈ DivRing )
16 qdencl ⊢ ( 𝑞 ∈ ℚ → ( denom ‘ 𝑞 ) ∈ ℕ )
17 16 adantl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ( denom ‘ 𝑞 ) ∈ ℕ )
18 17 nnzd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ( denom ‘ 𝑞 ) ∈ ℤ )
19 11 18 ffvelcdmd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ 𝐵 )
20 17 nnne0d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ( denom ‘ 𝑞 ) ≠ 0 )
21 20 neneqd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ¬ ( denom ‘ 𝑞 ) = 0 )
22 fvex ⊢ ( denom ‘ 𝑞 ) ∈ V
23 22 elsn ⊢ ( ( denom ‘ 𝑞 ) ∈ { 0 } ↔ ( denom ‘ 𝑞 ) = 0 )
24 21 23 sylnibr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ¬ ( denom ‘ 𝑞 ) ∈ { 0 } )
25 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
26 1 3 25 zrhker ⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) = 0 ↔ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) = { 0 } ) )
27 26 biimpa ⊢ ( ( 𝑅 ∈ Ring ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) = { 0 } )
28 5 27 sylan ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) = { 0 } )
29 28 adantr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) = { 0 } )
30 24 29 neleqtrrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ¬ ( denom ‘ 𝑞 ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) )
31 ffn ⊢ ( 𝐿 : ℤ ⟶ 𝐵 → 𝐿 Fn ℤ )
32 8 10 31 3syl ⊢ ( 𝑅 ∈ Ring → 𝐿 Fn ℤ )
33 elpreima ⊢ ( 𝐿 Fn ℤ → ( ( denom ‘ 𝑞 ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) ↔ ( ( denom ‘ 𝑞 ) ∈ ℤ ∧ ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ { ( 0g ‘ 𝑅 ) } ) ) )
34 5 32 33 3syl ⊢ ( 𝑅 ∈ DivRing → ( ( denom ‘ 𝑞 ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) ↔ ( ( denom ‘ 𝑞 ) ∈ ℤ ∧ ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ { ( 0g ‘ 𝑅 ) } ) ) )
35 34 biimpar ⊢ ( ( 𝑅 ∈ DivRing ∧ ( ( denom ‘ 𝑞 ) ∈ ℤ ∧ ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ { ( 0g ‘ 𝑅 ) } ) ) → ( denom ‘ 𝑞 ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) )
36 35 expr ⊢ ( ( 𝑅 ∈ DivRing ∧ ( denom ‘ 𝑞 ) ∈ ℤ ) → ( ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ { ( 0g ‘ 𝑅 ) } → ( denom ‘ 𝑞 ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) ) )
37 36 con3dimp ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( denom ‘ 𝑞 ) ∈ ℤ ) ∧ ¬ ( denom ‘ 𝑞 ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) ) → ¬ ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ { ( 0g ‘ 𝑅 ) } )
38 15 18 30 37 syl21anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ¬ ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ { ( 0g ‘ 𝑅 ) } )
39 fvex ⊢ ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ V
40 39 elsn ⊢ ( ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ { ( 0g ‘ 𝑅 ) } ↔ ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) = ( 0g ‘ 𝑅 ) )
41 38 40 sylnib ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ¬ ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) = ( 0g ‘ 𝑅 ) )
42 41 neqned ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ≠ ( 0g ‘ 𝑅 ) )
43 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
44 1 43 25 drngunit ⊢ ( 𝑅 ∈ DivRing → ( ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ 𝐵 ∧ ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ≠ ( 0g ‘ 𝑅 ) ) ) )
45 44 biimpar ⊢ ( ( 𝑅 ∈ DivRing ∧ ( ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ 𝐵 ∧ ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ ( Unit ‘ 𝑅 ) )
46 15 19 42 45 syl12anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ ( Unit ‘ 𝑅 ) )
47 1 43 2 dvrcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) ∈ 𝐵 ∧ ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ∈ 𝐵 )
48 7 14 46 47 syl3anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑞 ∈ ℚ ) → ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ∈ 𝐵 )
49 4 48 fmpt3d ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) : ℚ ⟶ 𝐵 )