Metamath Proof Explorer

Theorem qqhghm

Description: The QQHom homomorphism is a group homomorphism if the target structure is a division ring. (Contributed by Thierry Arnoux, 9-Nov-2017)

Ref Expression
Hypotheses qqhval2.0 ⊢ 𝐵 = ( Base ‘ 𝑅 )
qqhval2.1 ⊢ / = ( /r ‘ 𝑅 )
qqhval2.2 ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
qqhrhm.1 ⊢ 𝑄 = ( ℂfld ↾s ℚ )
Assertion qqhghm ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) ∈ ( 𝑄 GrpHom 𝑅 ) )

Proof

Step Hyp Ref Expression
1 qqhval2.0 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 qqhval2.1 ⊢ / = ( /r ‘ 𝑅 )
3 qqhval2.2 ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
4 qqhrhm.1 ⊢ 𝑄 = ( ℂfld ↾s ℚ )
5 4 qrngbas ⊢ ℚ = ( Base ‘ 𝑄 )
6 qex ⊢ ℚ ∈ V
7 cnfldadd ⊢ + = ( +g ‘ ℂfld )
8 4 7 ressplusg ⊢ ( ℚ ∈ V → + = ( +g ‘ 𝑄 ) )
9 6 8 ax-mp ⊢ + = ( +g ‘ 𝑄 )
10 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
11 4 qdrng ⊢ 𝑄 ∈ DivRing
12 drnggrp ⊢ ( 𝑄 ∈ DivRing → 𝑄 ∈ Grp )
13 11 12 mp1i ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → 𝑄 ∈ Grp )
14 drnggrp ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Grp )
15 14 adantr ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → 𝑅 ∈ Grp )
16 1 2 3 qqhf ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) : ℚ ⟶ 𝐵 )
17 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
18 17 ad2antrr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → 𝑅 ∈ Ring )
19 17 adantr ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → 𝑅 ∈ Ring )
20 3 zrhrhm ⊢ ( 𝑅 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
21 zringbas ⊢ ℤ = ( Base ‘ ℤring )
22 21 1 rhmf ⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) → 𝐿 : ℤ ⟶ 𝐵 )
23 19 20 22 3syl ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → 𝐿 : ℤ ⟶ 𝐵 )
24 23 adantr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → 𝐿 : ℤ ⟶ 𝐵 )
25 qnumcl ⊢ ( 𝑥 ∈ ℚ → ( numer ‘ 𝑥 ) ∈ ℤ )
26 25 ad2antrl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( numer ‘ 𝑥 ) ∈ ℤ )
27 qdencl ⊢ ( 𝑦 ∈ ℚ → ( denom ‘ 𝑦 ) ∈ ℕ )
28 27 ad2antll ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑦 ) ∈ ℕ )
29 28 nnzd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑦 ) ∈ ℤ )
30 26 29 zmulcld ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ∈ ℤ )
31 24 30 ffvelrnd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ∈ 𝐵 )
32 qnumcl ⊢ ( 𝑦 ∈ ℚ → ( numer ‘ 𝑦 ) ∈ ℤ )
33 32 ad2antll ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( numer ‘ 𝑦 ) ∈ ℤ )
34 qdencl ⊢ ( 𝑥 ∈ ℚ → ( denom ‘ 𝑥 ) ∈ ℕ )
35 34 ad2antrl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑥 ) ∈ ℕ )
36 35 nnzd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑥 ) ∈ ℤ )
37 33 36 zmulcld ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ∈ ℤ )
38 24 37 ffvelrnd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ∈ 𝐵 )
39 18 20 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
40 zringmulr ⊢ · = ( .r ‘ ℤring )
41 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
42 21 40 41 rhmmul ⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) ∧ ( denom ‘ 𝑥 ) ∈ ℤ ∧ ( denom ‘ 𝑦 ) ∈ ℤ ) → ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) )
43 39 36 29 42 syl3anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) )
44 simpl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) )
45 35 nnne0d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑥 ) ≠ 0 )
46 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
47 1 3 46 elzrhunit ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( ( denom ‘ 𝑥 ) ∈ ℤ ∧ ( denom ‘ 𝑥 ) ≠ 0 ) ) → ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ∈ ( Unit ‘ 𝑅 ) )
48 44 36 45 47 syl12anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ∈ ( Unit ‘ 𝑅 ) )
49 28 nnne0d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑦 ) ≠ 0 )
50 1 3 46 elzrhunit ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( ( denom ‘ 𝑦 ) ∈ ℤ ∧ ( denom ‘ 𝑦 ) ≠ 0 ) ) → ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ∈ ( Unit ‘ 𝑅 ) )
51 44 29 49 50 syl12anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ∈ ( Unit ‘ 𝑅 ) )
52 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
53 52 41 unitmulcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) ∈ ( Unit ‘ 𝑅 ) )
54 18 48 51 53 syl3anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) ∈ ( Unit ‘ 𝑅 ) )
55 43 54 eqeltrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ∈ ( Unit ‘ 𝑅 ) )
56 1 52 10 2 dvrdir ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ∈ 𝐵 ∧ ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ∈ 𝐵 ∧ ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) ( +g ‘ 𝑅 ) ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) ) )
57 18 31 38 55 56 syl13anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) ( +g ‘ 𝑅 ) ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) ) )
58 qeqnumdivden ⊢ ( 𝑥 ∈ ℚ → 𝑥 = ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) )
59 58 ad2antrl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → 𝑥 = ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) )
60 qeqnumdivden ⊢ ( 𝑦 ∈ ℚ → 𝑦 = ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) )
61 60 ad2antll ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → 𝑦 = ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) )
62 59 61 oveq12d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝑥 + 𝑦 ) = ( ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) + ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) )
63 26 zcnd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( numer ‘ 𝑥 ) ∈ ℂ )
64 36 zcnd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑥 ) ∈ ℂ )
65 33 zcnd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( numer ‘ 𝑦 ) ∈ ℂ )
66 29 zcnd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑦 ) ∈ ℂ )
67 63 64 65 66 45 49 divadddivd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) + ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) = ( ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) )
68 62 67 eqtrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝑥 + 𝑦 ) = ( ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) )
69 68 fveq2d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( ℚHom ‘ 𝑅 ) ‘ ( ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
70 30 37 zaddcld ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ∈ ℤ )
71 36 29 zmulcld ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ∈ ℤ )
72 64 66 45 49 mulne0d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ≠ 0 )
73 1 2 3 qqhvq ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ∈ ℤ ∧ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ∈ ℤ ∧ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ≠ 0 ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( 𝐿 ‘ ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
74 44 70 71 72 73 syl13anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( 𝐿 ‘ ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
75 rhmghm ⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) → 𝐿 ∈ ( ℤring GrpHom 𝑅 ) )
76 39 75 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → 𝐿 ∈ ( ℤring GrpHom 𝑅 ) )
77 zringplusg ⊢ + = ( +g ‘ ℤring )
78 21 77 10 ghmlin ⊢ ( ( 𝐿 ∈ ( ℤring GrpHom 𝑅 ) ∧ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ∈ ℤ ∧ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ∈ ℤ ) → ( 𝐿 ‘ ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) )
79 78 oveq1d ⊢ ( ( 𝐿 ∈ ( ℤring GrpHom 𝑅 ) ∧ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ∈ ℤ ∧ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ∈ ℤ ) → ( ( 𝐿 ‘ ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
80 76 30 37 79 syl3anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( 𝐿 ‘ ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
81 69 74 80 3eqtrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
82 58 fveq2d ⊢ ( 𝑥 ∈ ℚ → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑥 ) = ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) ) )
83 82 ad2antrl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑥 ) = ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) ) )
84 1 2 3 qqhvq ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( ( numer ‘ 𝑥 ) ∈ ℤ ∧ ( denom ‘ 𝑥 ) ∈ ℤ ∧ ( denom ‘ 𝑥 ) ≠ 0 ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) ) = ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ) )
85 44 26 36 45 84 syl13anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) ) = ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ) )
86 52 21 2 40 rhmdvd ⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) ∧ ( ( numer ‘ 𝑥 ) ∈ ℤ ∧ ( denom ‘ 𝑥 ) ∈ ℤ ∧ ( denom ‘ 𝑦 ) ∈ ℤ ) ∧ ( ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
87 39 26 36 29 48 51 86 syl132anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
88 83 85 87 3eqtrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑥 ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
89 60 fveq2d ⊢ ( 𝑦 ∈ ℚ → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑦 ) = ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) )
90 89 ad2antll ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑦 ) = ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) )
91 52 21 2 40 rhmdvd ⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) ∧ ( ( numer ‘ 𝑦 ) ∈ ℤ ∧ ( denom ‘ 𝑦 ) ∈ ℤ ∧ ( denom ‘ 𝑥 ) ∈ ℤ ) ∧ ( ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) )
92 39 33 29 36 51 48 91 syl132anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) )
93 1 2 3 qqhvq ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( ( numer ‘ 𝑦 ) ∈ ℤ ∧ ( denom ‘ 𝑦 ) ∈ ℤ ∧ ( denom ‘ 𝑦 ) ≠ 0 ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) )
94 44 33 29 49 93 syl13anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) )
95 64 66 mulcomd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) = ( ( denom ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) )
96 95 fveq2d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) = ( 𝐿 ‘ ( ( denom ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) )
97 96 oveq2d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) )
98 92 94 97 3eqtr4d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
99 90 98 eqtrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑦 ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
100 88 99 oveq12d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑦 ) ) = ( ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) ( +g ‘ 𝑅 ) ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) ) )
101 57 81 100 3eqtr4d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑦 ) ) )
102 5 1 9 10 13 15 16 101 isghmd ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) ∈ ( 𝑄 GrpHom 𝑅 ) )