Metamath Proof Explorer

Theorem qqhrhm

Description: The QQHom homomorphism is a ring homomorphism if the target structure is a field. If the target structure is a division ring, it is a group homomorphism, but not a ring homomorphism, because it does not preserve the ring multiplication operation. (Contributed by Thierry Arnoux, 29-Oct-2017)

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

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 4 qrng1 ⊢ 1 = ( 1r ‘ 𝑄 )
7 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8 qex ⊢ ℚ ∈ V
9 cnfldmul ⊢ · = ( .r ‘ ℂfld )
10 4 9 ressmulr ⊢ ( ℚ ∈ V → · = ( .r ‘ 𝑄 ) )
11 8 10 ax-mp ⊢ · = ( .r ‘ 𝑄 )
12 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
13 4 qdrng ⊢ 𝑄 ∈ DivRing
14 drngring ⊢ ( 𝑄 ∈ DivRing → 𝑄 ∈ Ring )
15 13 14 mp1i ⊢ ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) → 𝑄 ∈ Ring )
16 isfld ⊢ ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing ) )
17 16 simplbi ⊢ ( 𝑅 ∈ Field → 𝑅 ∈ DivRing )
18 17 adantr ⊢ ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) → 𝑅 ∈ DivRing )
19 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
20 18 19 syl ⊢ ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) → 𝑅 ∈ Ring )
21 1 2 3 qqh1 ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ( ℚHom ‘ 𝑅 ) ‘ 1 ) = ( 1r ‘ 𝑅 ) )
22 17 21 sylan ⊢ ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ( ℚHom ‘ 𝑅 ) ‘ 1 ) = ( 1r ‘ 𝑅 ) )
23 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
24 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
25 16 simprbi ⊢ ( 𝑅 ∈ Field → 𝑅 ∈ CRing )
26 25 ad2antrr ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → 𝑅 ∈ CRing )
27 3 zrhrhm ⊢ ( 𝑅 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
28 zringbas ⊢ ℤ = ( Base ‘ ℤring )
29 28 1 rhmf ⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) → 𝐿 : ℤ ⟶ 𝐵 )
30 20 27 29 3syl ⊢ ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) → 𝐿 : ℤ ⟶ 𝐵 )
31 30 adantr ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → 𝐿 : ℤ ⟶ 𝐵 )
32 qnumcl ⊢ ( 𝑥 ∈ ℚ → ( numer ‘ 𝑥 ) ∈ ℤ )
33 32 ad2antrl ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( numer ‘ 𝑥 ) ∈ ℤ )
34 31 33 ffvelrnd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) ∈ 𝐵 )
35 17 ad2antrr ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → 𝑅 ∈ DivRing )
36 simplr ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( chr ‘ 𝑅 ) = 0 )
37 35 36 jca ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) )
38 qdencl ⊢ ( 𝑥 ∈ ℚ → ( denom ‘ 𝑥 ) ∈ ℕ )
39 38 ad2antrl ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑥 ) ∈ ℕ )
40 39 nnzd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑥 ) ∈ ℤ )
41 39 nnne0d ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑥 ) ≠ 0 )
42 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
43 1 3 42 elzrhunit ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( ( denom ‘ 𝑥 ) ∈ ℤ ∧ ( denom ‘ 𝑥 ) ≠ 0 ) ) → ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ∈ ( Unit ‘ 𝑅 ) )
44 37 40 41 43 syl12anc ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ∈ ( Unit ‘ 𝑅 ) )
45 qnumcl ⊢ ( 𝑦 ∈ ℚ → ( numer ‘ 𝑦 ) ∈ ℤ )
46 45 ad2antll ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( numer ‘ 𝑦 ) ∈ ℤ )
47 31 46 ffvelrnd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) ∈ 𝐵 )
48 qdencl ⊢ ( 𝑦 ∈ ℚ → ( denom ‘ 𝑦 ) ∈ ℕ )
49 48 ad2antll ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑦 ) ∈ ℕ )
50 49 nnzd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑦 ) ∈ ℤ )
51 49 nnne0d ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑦 ) ≠ 0 )
52 1 3 42 elzrhunit ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( ( denom ‘ 𝑦 ) ∈ ℤ ∧ ( denom ‘ 𝑦 ) ≠ 0 ) ) → ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ∈ ( Unit ‘ 𝑅 ) )
53 37 50 51 52 syl12anc ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ∈ ( Unit ‘ 𝑅 ) )
54 1 23 24 2 12 26 34 44 47 53 rdivmuldivd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ) ( .r ‘ 𝑅 ) ( ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) ) = ( ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) ) / ( ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) ) )
55 qeqnumdivden ⊢ ( 𝑥 ∈ ℚ → 𝑥 = ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) )
56 55 fveq2d ⊢ ( 𝑥 ∈ ℚ → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑥 ) = ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) ) )
57 56 ad2antrl ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑥 ) = ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) ) )
58 1 2 3 qqhvq ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( ( numer ‘ 𝑥 ) ∈ ℤ ∧ ( denom ‘ 𝑥 ) ∈ ℤ ∧ ( denom ‘ 𝑥 ) ≠ 0 ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) ) = ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ) )
59 37 33 40 41 58 syl13anc ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) ) = ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ) )
60 57 59 eqtrd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑥 ) = ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ) )
61 qeqnumdivden ⊢ ( 𝑦 ∈ ℚ → 𝑦 = ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) )
62 61 fveq2d ⊢ ( 𝑦 ∈ ℚ → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑦 ) = ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) )
63 62 ad2antll ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑦 ) = ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) )
64 1 2 3 qqhvq ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( ( numer ‘ 𝑦 ) ∈ ℤ ∧ ( denom ‘ 𝑦 ) ∈ ℤ ∧ ( denom ‘ 𝑦 ) ≠ 0 ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) )
65 37 46 50 51 64 syl13anc ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) )
66 63 65 eqtrd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑦 ) = ( ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) )
67 60 66 oveq12d ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑦 ) ) = ( ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ) ( .r ‘ 𝑅 ) ( ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) ) )
68 55 ad2antrl ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → 𝑥 = ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) )
69 61 ad2antll ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → 𝑦 = ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) )
70 68 69 oveq12d ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝑥 · 𝑦 ) = ( ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) · ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) )
71 33 zcnd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( numer ‘ 𝑥 ) ∈ ℂ )
72 40 zcnd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑥 ) ∈ ℂ )
73 46 zcnd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( numer ‘ 𝑦 ) ∈ ℂ )
74 50 zcnd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( denom ‘ 𝑦 ) ∈ ℂ )
75 71 72 73 74 41 51 divmuldivd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) · ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) = ( ( ( numer ‘ 𝑥 ) · ( numer ‘ 𝑦 ) ) / ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) )
76 70 75 eqtrd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝑥 · 𝑦 ) = ( ( ( numer ‘ 𝑥 ) · ( numer ‘ 𝑦 ) ) / ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) )
77 76 fveq2d ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑥 · 𝑦 ) ) = ( ( ℚHom ‘ 𝑅 ) ‘ ( ( ( numer ‘ 𝑥 ) · ( numer ‘ 𝑦 ) ) / ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
78 33 46 zmulcld ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( numer ‘ 𝑥 ) · ( numer ‘ 𝑦 ) ) ∈ ℤ )
79 40 50 zmulcld ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ∈ ℤ )
80 72 74 41 51 mulne0d ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ≠ 0 )
81 1 2 3 qqhvq ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( ( ( numer ‘ 𝑥 ) · ( numer ‘ 𝑦 ) ) ∈ ℤ ∧ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ∈ ℤ ∧ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ≠ 0 ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( ( numer ‘ 𝑥 ) · ( numer ‘ 𝑦 ) ) / ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( numer ‘ 𝑦 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
82 37 78 79 80 81 syl13anc ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( ( numer ‘ 𝑥 ) · ( numer ‘ 𝑦 ) ) / ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( numer ‘ 𝑦 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
83 35 19 syl ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → 𝑅 ∈ Ring )
84 83 27 syl ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
85 zringmulr ⊢ · = ( .r ‘ ℤring )
86 28 85 12 rhmmul ⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) ∧ ( numer ‘ 𝑥 ) ∈ ℤ ∧ ( numer ‘ 𝑦 ) ∈ ℤ ) → ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( numer ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) ) )
87 84 33 46 86 syl3anc ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( numer ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) ) )
88 28 85 12 rhmmul ⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) ∧ ( denom ‘ 𝑥 ) ∈ ℤ ∧ ( denom ‘ 𝑦 ) ∈ ℤ ) → ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) )
89 84 40 50 88 syl3anc ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) )
90 87 89 oveq12d ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( numer ‘ 𝑦 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) ) / ( ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) ) )
91 77 82 90 3eqtrd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑥 · 𝑦 ) ) = ( ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) ) / ( ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) ) )
92 54 67 91 3eqtr4rd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑥 · 𝑦 ) ) = ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑦 ) ) )
93 cnfldadd ⊢ + = ( +g ‘ ℂfld )
94 4 93 ressplusg ⊢ ( ℚ ∈ V → + = ( +g ‘ 𝑄 ) )
95 8 94 ax-mp ⊢ + = ( +g ‘ 𝑄 )
96 1 2 3 qqhf ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) : ℚ ⟶ 𝐵 )
97 17 96 sylan ⊢ ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) : ℚ ⟶ 𝐵 )
98 33 50 zmulcld ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ∈ ℤ )
99 31 98 ffvelrnd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ∈ 𝐵 )
100 46 40 zmulcld ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ∈ ℤ )
101 31 100 ffvelrnd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ∈ 𝐵 )
102 23 12 unitmulcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) ∈ ( Unit ‘ 𝑅 ) )
103 83 44 53 102 syl3anc ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) ∈ ( Unit ‘ 𝑅 ) )
104 89 103 eqeltrd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ∈ ( Unit ‘ 𝑅 ) )
105 1 23 24 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 ‘ 𝑦 ) ) ) ) ) )
106 83 99 101 104 105 syl13anc ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) ( +g ‘ 𝑅 ) ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) ) )
107 68 69 oveq12d ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝑥 + 𝑦 ) = ( ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) + ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) )
108 71 72 73 74 41 51 divadddivd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ( numer ‘ 𝑥 ) / ( denom ‘ 𝑥 ) ) + ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) = ( ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) )
109 107 108 eqtrd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝑥 + 𝑦 ) = ( ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) )
110 109 fveq2d ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( ℚHom ‘ 𝑅 ) ‘ ( ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
111 98 100 zaddcld ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ∈ ℤ )
112 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 ‘ 𝑦 ) ) ) ) )
113 37 111 79 80 112 syl13anc ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( 𝐿 ‘ ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
114 rhmghm ⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) → 𝐿 ∈ ( ℤring GrpHom 𝑅 ) )
115 84 114 syl ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → 𝐿 ∈ ( ℤring GrpHom 𝑅 ) )
116 zringplusg ⊢ + = ( +g ‘ ℤring )
117 28 116 24 ghmlin ⊢ ( ( 𝐿 ∈ ( ℤring GrpHom 𝑅 ) ∧ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ∈ ℤ ∧ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ∈ ℤ ) → ( 𝐿 ‘ ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) )
118 117 oveq1d ⊢ ( ( 𝐿 ∈ ( ℤring GrpHom 𝑅 ) ∧ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ∈ ℤ ∧ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ∈ ℤ ) → ( ( 𝐿 ‘ ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
119 115 98 100 118 syl3anc ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( 𝐿 ‘ ( ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) + ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
120 110 113 119 3eqtrd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
121 23 28 2 85 rhmdvd ⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) ∧ ( ( numer ‘ 𝑥 ) ∈ ℤ ∧ ( denom ‘ 𝑥 ) ∈ ℤ ∧ ( denom ‘ 𝑦 ) ∈ ℤ ) ∧ ( ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
122 84 33 40 50 44 53 121 syl132anc ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( 𝐿 ‘ ( numer ‘ 𝑥 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
123 57 59 122 3eqtrd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑥 ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
124 23 28 2 85 rhmdvd ⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) ∧ ( ( numer ‘ 𝑦 ) ∈ ℤ ∧ ( denom ‘ 𝑦 ) ∈ ℤ ∧ ( denom ‘ 𝑥 ) ∈ ℤ ) ∧ ( ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝐿 ‘ ( denom ‘ 𝑥 ) ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) )
125 84 46 50 40 53 44 124 syl132anc ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( 𝐿 ‘ ( numer ‘ 𝑦 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) )
126 72 74 mulcomd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) = ( ( denom ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) )
127 126 fveq2d ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) = ( 𝐿 ‘ ( ( denom ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) )
128 127 oveq2d ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) ) )
129 125 65 128 3eqtr4d ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( ( numer ‘ 𝑦 ) / ( denom ‘ 𝑦 ) ) ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
130 63 129 eqtrd ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑦 ) = ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) )
131 123 130 oveq12d ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑦 ) ) = ( ( ( 𝐿 ‘ ( ( numer ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) ( +g ‘ 𝑅 ) ( ( 𝐿 ‘ ( ( numer ‘ 𝑦 ) · ( denom ‘ 𝑥 ) ) ) / ( 𝐿 ‘ ( ( denom ‘ 𝑥 ) · ( denom ‘ 𝑦 ) ) ) ) ) )
132 106 120 131 3eqtr4d ⊢ ( ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑦 ) ) )
133 5 6 7 11 12 15 20 22 92 1 95 24 97 132 isrhmd ⊢ ( ( 𝑅 ∈ Field ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) ∈ ( 𝑄 RingHom 𝑅 ) )