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 ffvelcdmd ⊒ ( ( ( 𝑅 ∈ 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 ffvelcdmd ⊒ ( ( ( 𝑅 ∈ 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 ffvelcdmd ⊒ ( ( ( 𝑅 ∈ Field ∧ ( chr β€˜ 𝑅 ) = 0 ) ∧ ( π‘₯ ∈ β„š ∧ 𝑦 ∈ β„š ) ) β†’ ( 𝐿 β€˜ ( ( numer β€˜ π‘₯ ) Β· ( denom β€˜ 𝑦 ) ) ) ∈ 𝐡 )
100 46 40 zmulcld ⊒ ( ( ( 𝑅 ∈ Field ∧ ( chr β€˜ 𝑅 ) = 0 ) ∧ ( π‘₯ ∈ β„š ∧ 𝑦 ∈ β„š ) ) β†’ ( ( numer β€˜ 𝑦 ) Β· ( denom β€˜ π‘₯ ) ) ∈ β„€ )
101 31 100 ffvelcdmd ⊒ ( ( ( 𝑅 ∈ 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 𝑅 ) )