Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  qqhghm Structured version   Visualization version   GIF version

Theorem qqhghm 29832
 Description: The ℚHom homomorphism is a group homomorphism if the target structure is a division ring. (Contributed by Thierry Arnoux, 9-Nov-2017.)
Hypotheses
Ref Expression
qqhval2.0 𝐵 = (Base‘𝑅)
qqhval2.1 / = (/r𝑅)
qqhval2.2 𝐿 = (ℤRHom‘𝑅)
qqhrhm.1 𝑄 = (ℂflds ℚ)
Assertion
Ref Expression
qqhghm ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅) ∈ (𝑄 GrpHom 𝑅))

Proof of Theorem qqhghm
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 qqhrhm.1 . . 3 𝑄 = (ℂflds ℚ)
21qrngbas 25221 . 2 ℚ = (Base‘𝑄)
3 qqhval2.0 . 2 𝐵 = (Base‘𝑅)
4 qex 11751 . . 3 ℚ ∈ V
5 cnfldadd 19679 . . . 4 + = (+g‘ℂfld)
61, 5ressplusg 15921 . . 3 (ℚ ∈ V → + = (+g𝑄))
74, 6ax-mp 5 . 2 + = (+g𝑄)
8 eqid 2621 . 2 (+g𝑅) = (+g𝑅)
91qdrng 25222 . . 3 𝑄 ∈ DivRing
10 drnggrp 18683 . . 3 (𝑄 ∈ DivRing → 𝑄 ∈ Grp)
119, 10mp1i 13 . 2 ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → 𝑄 ∈ Grp)
12 drnggrp 18683 . . 3 (𝑅 ∈ DivRing → 𝑅 ∈ Grp)
1312adantr 481 . 2 ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → 𝑅 ∈ Grp)
14 qqhval2.1 . . 3 / = (/r𝑅)
15 qqhval2.2 . . 3 𝐿 = (ℤRHom‘𝑅)
163, 14, 15qqhf 29830 . 2 ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵)
17 drngring 18682 . . . . 5 (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
1817ad2antrr 761 . . . 4 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑅 ∈ Ring)
1917adantr 481 . . . . . . 7 ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → 𝑅 ∈ Ring)
2015zrhrhm 19788 . . . . . . 7 (𝑅 ∈ Ring → 𝐿 ∈ (ℤring RingHom 𝑅))
21 zringbas 19752 . . . . . . . 8 ℤ = (Base‘ℤring)
2221, 3rhmf 18654 . . . . . . 7 (𝐿 ∈ (ℤring RingHom 𝑅) → 𝐿:ℤ⟶𝐵)
2319, 20, 223syl 18 . . . . . 6 ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → 𝐿:ℤ⟶𝐵)
2423adantr 481 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝐿:ℤ⟶𝐵)
25 qnumcl 15379 . . . . . . 7 (𝑥 ∈ ℚ → (numer‘𝑥) ∈ ℤ)
2625ad2antrl 763 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑥) ∈ ℤ)
27 qdencl 15380 . . . . . . . 8 (𝑦 ∈ ℚ → (denom‘𝑦) ∈ ℕ)
2827ad2antll 764 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ∈ ℕ)
2928nnzd 11432 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ∈ ℤ)
3026, 29zmulcld 11439 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((numer‘𝑥) · (denom‘𝑦)) ∈ ℤ)
3124, 30ffvelrnd 6321 . . . 4 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((numer‘𝑥) · (denom‘𝑦))) ∈ 𝐵)
32 qnumcl 15379 . . . . . . 7 (𝑦 ∈ ℚ → (numer‘𝑦) ∈ ℤ)
3332ad2antll 764 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑦) ∈ ℤ)
34 qdencl 15380 . . . . . . . 8 (𝑥 ∈ ℚ → (denom‘𝑥) ∈ ℕ)
3534ad2antrl 763 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ∈ ℕ)
3635nnzd 11432 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ∈ ℤ)
3733, 36zmulcld 11439 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((numer‘𝑦) · (denom‘𝑥)) ∈ ℤ)
3824, 37ffvelrnd 6321 . . . 4 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((numer‘𝑦) · (denom‘𝑥))) ∈ 𝐵)
3918, 20syl 17 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝐿 ∈ (ℤring RingHom 𝑅))
40 zringmulr 19755 . . . . . . 7 · = (.r‘ℤring)
41 eqid 2621 . . . . . . 7 (.r𝑅) = (.r𝑅)
4221, 40, 41rhmmul 18655 . . . . . 6 ((𝐿 ∈ (ℤring RingHom 𝑅) ∧ (denom‘𝑥) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) = ((𝐿‘(denom‘𝑥))(.r𝑅)(𝐿‘(denom‘𝑦))))
4339, 36, 29, 42syl3anc 1323 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) = ((𝐿‘(denom‘𝑥))(.r𝑅)(𝐿‘(denom‘𝑦))))
44 simpl 473 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0))
4535nnne0d 11016 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ≠ 0)
46 eqid 2621 . . . . . . . 8 (0g𝑅) = (0g𝑅)
473, 15, 46elzrhunit 29823 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((denom‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ≠ 0)) → (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅))
4844, 36, 45, 47syl12anc 1321 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅))
4928nnne0d 11016 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ≠ 0)
503, 15, 46elzrhunit 29823 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((denom‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ≠ 0)) → (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅))
5144, 29, 49, 50syl12anc 1321 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅))
52 eqid 2621 . . . . . . 7 (Unit‘𝑅) = (Unit‘𝑅)
5352, 41unitmulcl 18592 . . . . . 6 ((𝑅 ∈ Ring ∧ (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅) ∧ (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅)) → ((𝐿‘(denom‘𝑥))(.r𝑅)(𝐿‘(denom‘𝑦))) ∈ (Unit‘𝑅))
5418, 48, 51, 53syl3anc 1323 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(denom‘𝑥))(.r𝑅)(𝐿‘(denom‘𝑦))) ∈ (Unit‘𝑅))
5543, 54eqeltrd 2698 . . . 4 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) ∈ (Unit‘𝑅))
563, 52, 8, 14dvrdir 29593 . . . 4 ((𝑅 ∈ Ring ∧ ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) ∈ 𝐵 ∧ (𝐿‘((numer‘𝑦) · (denom‘𝑥))) ∈ 𝐵 ∧ (𝐿‘((denom‘𝑥) · (denom‘𝑦))) ∈ (Unit‘𝑅))) → (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))(+g𝑅)((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))))
5718, 31, 38, 55, 56syl13anc 1325 . . 3 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))(+g𝑅)((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))))
58 qeqnumdivden 15385 . . . . . . . 8 (𝑥 ∈ ℚ → 𝑥 = ((numer‘𝑥) / (denom‘𝑥)))
5958ad2antrl 763 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑥 = ((numer‘𝑥) / (denom‘𝑥)))
60 qeqnumdivden 15385 . . . . . . . 8 (𝑦 ∈ ℚ → 𝑦 = ((numer‘𝑦) / (denom‘𝑦)))
6160ad2antll 764 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑦 = ((numer‘𝑦) / (denom‘𝑦)))
6259, 61oveq12d 6628 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) = (((numer‘𝑥) / (denom‘𝑥)) + ((numer‘𝑦) / (denom‘𝑦))))
6326zcnd 11434 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑥) ∈ ℂ)
6436zcnd 11434 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ∈ ℂ)
6533zcnd 11434 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑦) ∈ ℂ)
6629zcnd 11434 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ∈ ℂ)
6763, 64, 65, 66, 45, 49divadddivd 10796 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((numer‘𝑥) / (denom‘𝑥)) + ((numer‘𝑦) / (denom‘𝑦))) = ((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦))))
6862, 67eqtrd 2655 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) = ((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦))))
6968fveq2d 6157 . . . 4 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = ((ℚHom‘𝑅)‘((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦)))))
7030, 37zaddcld 11437 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) ∈ ℤ)
7136, 29zmulcld 11439 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((denom‘𝑥) · (denom‘𝑦)) ∈ ℤ)
7264, 66, 45, 49mulne0d 10630 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((denom‘𝑥) · (denom‘𝑦)) ≠ 0)
733, 14, 15qqhvq 29831 . . . . 5 (((𝑅 ∈ 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‘𝑦)))))
7444, 70, 71, 72, 73syl13anc 1325 . . . 4 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
75 rhmghm 18653 . . . . . 6 (𝐿 ∈ (ℤring RingHom 𝑅) → 𝐿 ∈ (ℤring GrpHom 𝑅))
7639, 75syl 17 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝐿 ∈ (ℤring GrpHom 𝑅))
77 zringplusg 19753 . . . . . . 7 + = (+g‘ℤring)
7821, 77, 8ghmlin 17593 . . . . . 6 ((𝐿 ∈ (ℤring GrpHom 𝑅) ∧ ((numer‘𝑥) · (denom‘𝑦)) ∈ ℤ ∧ ((numer‘𝑦) · (denom‘𝑥)) ∈ ℤ) → (𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))))
7978oveq1d 6625 . . . . 5 ((𝐿 ∈ (ℤring GrpHom 𝑅) ∧ ((numer‘𝑥) · (denom‘𝑦)) ∈ ℤ ∧ ((numer‘𝑦) · (denom‘𝑥)) ∈ ℤ) → ((𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
8076, 30, 37, 79syl3anc 1323 . . . 4 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
8169, 74, 803eqtrd 2659 . . 3 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
8258fveq2d 6157 . . . . . 6 (𝑥 ∈ ℚ → ((ℚHom‘𝑅)‘𝑥) = ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))))
8382ad2antrl 763 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑥) = ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))))
843, 14, 15qqhvq 29831 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((numer‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ≠ 0)) → ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))) = ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))))
8544, 26, 36, 45, 84syl13anc 1325 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))) = ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))))
8652, 21, 14, 40rhmdvd 29624 . . . . . 6 ((𝐿 ∈ (ℤring RingHom 𝑅) ∧ ((numer‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ) ∧ ((𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅) ∧ (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅))) → ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
8739, 26, 36, 29, 48, 51, 86syl132anc 1341 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
8883, 85, 873eqtrd 2659 . . . 4 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑥) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
8960fveq2d 6157 . . . . . 6 (𝑦 ∈ ℚ → ((ℚHom‘𝑅)‘𝑦) = ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))))
9089ad2antll 764 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑦) = ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))))
9152, 21, 14, 40rhmdvd 29624 . . . . . . 7 ((𝐿 ∈ (ℤring RingHom 𝑅) ∧ ((numer‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ ∧ (denom‘𝑥) ∈ ℤ) ∧ ((𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅) ∧ (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅))) → ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑦) · (denom‘𝑥)))))
9239, 33, 29, 36, 51, 48, 91syl132anc 1341 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑦) · (denom‘𝑥)))))
933, 14, 15qqhvq 29831 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((numer‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ≠ 0)) → ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))))
9444, 33, 29, 49, 93syl13anc 1325 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))))
9564, 66mulcomd 10012 . . . . . . . 8 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((denom‘𝑥) · (denom‘𝑦)) = ((denom‘𝑦) · (denom‘𝑥)))
9695fveq2d 6157 . . . . . . 7 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) = (𝐿‘((denom‘𝑦) · (denom‘𝑥))))
9796oveq2d 6626 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑦) · (denom‘𝑥)))))
9892, 94, 973eqtr4d 2665 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
9990, 98eqtrd 2655 . . . 4 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑦) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
10088, 99oveq12d 6628 . . 3 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((ℚHom‘𝑅)‘𝑥)(+g𝑅)((ℚHom‘𝑅)‘𝑦)) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))(+g𝑅)((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))))
10157, 81, 1003eqtr4d 2665 . 2 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = (((ℚHom‘𝑅)‘𝑥)(+g𝑅)((ℚHom‘𝑅)‘𝑦)))
1022, 3, 7, 8, 11, 13, 16, 101isghmd 17597 1 ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅) ∈ (𝑄 GrpHom 𝑅))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  Vcvv 3189  ⟶wf 5848  ‘cfv 5852  (class class class)co 6610  0cc0 9887   + caddc 9890   · cmul 9892   / cdiv 10635  ℕcn 10971  ℤcz 11328  ℚcq 11739  numercnumer 15372  denomcdenom 15373  Basecbs 15788   ↾s cress 15789  +gcplusg 15869  .rcmulr 15870  0gc0g 16028  Grpcgrp 17350   GrpHom cghm 17585  Ringcrg 18475  Unitcui 18567  /rcdvr 18610   RingHom crh 18640  DivRingcdr 18675  ℂfldccnfld 19674  ℤringzring 19746  ℤRHomczrh 19776  chrcchr 19778  ℚHomcqqh 29816 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965  ax-addf 9966  ax-mulf 9967 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-tpos 7304  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-map 7811  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-sup 8299  df-inf 8300  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-4 11032  df-5 11033  df-6 11034  df-7 11035  df-8 11036  df-9 11037  df-n0 11244  df-z 11329  df-dec 11445  df-uz 11639  df-q 11740  df-rp 11784  df-fz 12276  df-fl 12540  df-mod 12616  df-seq 12749  df-exp 12808  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-dvds 14915  df-gcd 15148  df-numer 15374  df-denom 15375  df-gz 15565  df-struct 15790  df-ndx 15791  df-slot 15792  df-base 15793  df-sets 15794  df-ress 15795  df-plusg 15882  df-mulr 15883  df-starv 15884  df-tset 15888  df-ple 15889  df-ds 15892  df-unif 15893  df-0g 16030  df-mgm 17170  df-sgrp 17212  df-mnd 17223  df-mhm 17263  df-grp 17353  df-minusg 17354  df-sbg 17355  df-mulg 17469  df-subg 17519  df-ghm 17586  df-od 17876  df-cmn 18123  df-mgp 18418  df-ur 18430  df-ring 18477  df-cring 18478  df-oppr 18551  df-dvdsr 18569  df-unit 18570  df-invr 18600  df-dvr 18611  df-rnghom 18643  df-drng 18677  df-subrg 18706  df-cnfld 19675  df-zring 19747  df-zrh 19780  df-chr 19782  df-qqh 29817 This theorem is referenced by:  qqhcn  29835  qqhucn  29836
 Copyright terms: Public domain W3C validator