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

Theorem qqhrhm 30567
Description: The ℚHom 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.)
Hypotheses
Ref Expression
qqhval2.0 𝐵 = (Base‘𝑅)
qqhval2.1 / = (/r𝑅)
qqhval2.2 𝐿 = (ℤRHom‘𝑅)
qqhrhm.1 𝑄 = (ℂflds ℚ)
Assertion
Ref Expression
qqhrhm ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅) ∈ (𝑄 RingHom 𝑅))

Proof of Theorem qqhrhm
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 qqhrhm.1 . . 3 𝑄 = (ℂflds ℚ)
21qrngbas 25721 . 2 ℚ = (Base‘𝑄)
31qrng1 25724 . 2 1 = (1r𝑄)
4 eqid 2825 . 2 (1r𝑅) = (1r𝑅)
5 qex 12083 . . 3 ℚ ∈ V
6 cnfldmul 20112 . . . 4 · = (.r‘ℂfld)
71, 6ressmulr 16365 . . 3 (ℚ ∈ V → · = (.r𝑄))
85, 7ax-mp 5 . 2 · = (.r𝑄)
9 eqid 2825 . 2 (.r𝑅) = (.r𝑅)
101qdrng 25722 . . 3 𝑄 ∈ DivRing
11 drngring 19110 . . 3 (𝑄 ∈ DivRing → 𝑄 ∈ Ring)
1210, 11mp1i 13 . 2 ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → 𝑄 ∈ Ring)
13 isfld 19112 . . . . 5 (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
1413simplbi 493 . . . 4 (𝑅 ∈ Field → 𝑅 ∈ DivRing)
1514adantr 474 . . 3 ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → 𝑅 ∈ DivRing)
16 drngring 19110 . . 3 (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
1715, 16syl 17 . 2 ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → 𝑅 ∈ Ring)
18 qqhval2.0 . . . 4 𝐵 = (Base‘𝑅)
19 qqhval2.1 . . . 4 / = (/r𝑅)
20 qqhval2.2 . . . 4 𝐿 = (ℤRHom‘𝑅)
2118, 19, 20qqh1 30563 . . 3 ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → ((ℚHom‘𝑅)‘1) = (1r𝑅))
2214, 21sylan 575 . 2 ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → ((ℚHom‘𝑅)‘1) = (1r𝑅))
23 eqid 2825 . . . 4 (Unit‘𝑅) = (Unit‘𝑅)
24 eqid 2825 . . . 4 (+g𝑅) = (+g𝑅)
2513simprbi 492 . . . . 5 (𝑅 ∈ Field → 𝑅 ∈ CRing)
2625ad2antrr 717 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑅 ∈ CRing)
2720zrhrhm 20220 . . . . . . 7 (𝑅 ∈ Ring → 𝐿 ∈ (ℤring RingHom 𝑅))
28 zringbas 20184 . . . . . . . 8 ℤ = (Base‘ℤring)
2928, 18rhmf 19082 . . . . . . 7 (𝐿 ∈ (ℤring RingHom 𝑅) → 𝐿:ℤ⟶𝐵)
3017, 27, 293syl 18 . . . . . 6 ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → 𝐿:ℤ⟶𝐵)
3130adantr 474 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝐿:ℤ⟶𝐵)
32 qnumcl 15819 . . . . . 6 (𝑥 ∈ ℚ → (numer‘𝑥) ∈ ℤ)
3332ad2antrl 719 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑥) ∈ ℤ)
3431, 33ffvelrnd 6609 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘(numer‘𝑥)) ∈ 𝐵)
3514ad2antrr 717 . . . . . 6 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑅 ∈ DivRing)
36 simplr 785 . . . . . 6 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (chr‘𝑅) = 0)
3735, 36jca 507 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0))
38 qdencl 15820 . . . . . . 7 (𝑥 ∈ ℚ → (denom‘𝑥) ∈ ℕ)
3938ad2antrl 719 . . . . . 6 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ∈ ℕ)
4039nnzd 11809 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ∈ ℤ)
4139nnne0d 11401 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ≠ 0)
42 eqid 2825 . . . . . 6 (0g𝑅) = (0g𝑅)
4318, 20, 42elzrhunit 30557 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((denom‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ≠ 0)) → (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅))
4437, 40, 41, 43syl12anc 870 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅))
45 qnumcl 15819 . . . . . 6 (𝑦 ∈ ℚ → (numer‘𝑦) ∈ ℤ)
4645ad2antll 720 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑦) ∈ ℤ)
4731, 46ffvelrnd 6609 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘(numer‘𝑦)) ∈ 𝐵)
48 qdencl 15820 . . . . . . 7 (𝑦 ∈ ℚ → (denom‘𝑦) ∈ ℕ)
4948ad2antll 720 . . . . . 6 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ∈ ℕ)
5049nnzd 11809 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ∈ ℤ)
5149nnne0d 11401 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ≠ 0)
5218, 20, 42elzrhunit 30557 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((denom‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ≠ 0)) → (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅))
5337, 50, 51, 52syl12anc 870 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅))
5418, 23, 24, 19, 9, 26, 34, 44, 47, 53rdivmuldivd 30325 . . 3 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥)))(.r𝑅)((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦)))) = (((𝐿‘(numer‘𝑥))(.r𝑅)(𝐿‘(numer‘𝑦))) / ((𝐿‘(denom‘𝑥))(.r𝑅)(𝐿‘(denom‘𝑦)))))
55 qeqnumdivden 15825 . . . . . . 7 (𝑥 ∈ ℚ → 𝑥 = ((numer‘𝑥) / (denom‘𝑥)))
5655fveq2d 6437 . . . . . 6 (𝑥 ∈ ℚ → ((ℚHom‘𝑅)‘𝑥) = ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))))
5756ad2antrl 719 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑥) = ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))))
5818, 19, 20qqhvq 30565 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((numer‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ≠ 0)) → ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))) = ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))))
5937, 33, 40, 41, 58syl13anc 1495 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))) = ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))))
6057, 59eqtrd 2861 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑥) = ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))))
61 qeqnumdivden 15825 . . . . . . 7 (𝑦 ∈ ℚ → 𝑦 = ((numer‘𝑦) / (denom‘𝑦)))
6261fveq2d 6437 . . . . . 6 (𝑦 ∈ ℚ → ((ℚHom‘𝑅)‘𝑦) = ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))))
6362ad2antll 720 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑦) = ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))))
6418, 19, 20qqhvq 30565 . . . . . 6 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((numer‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ≠ 0)) → ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))))
6537, 46, 50, 51, 64syl13anc 1495 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))))
6663, 65eqtrd 2861 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑦) = ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))))
6760, 66oveq12d 6923 . . 3 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((ℚHom‘𝑅)‘𝑥)(.r𝑅)((ℚHom‘𝑅)‘𝑦)) = (((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥)))(.r𝑅)((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦)))))
6855ad2antrl 719 . . . . . . 7 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑥 = ((numer‘𝑥) / (denom‘𝑥)))
6961ad2antll 720 . . . . . . 7 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑦 = ((numer‘𝑦) / (denom‘𝑦)))
7068, 69oveq12d 6923 . . . . . 6 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 · 𝑦) = (((numer‘𝑥) / (denom‘𝑥)) · ((numer‘𝑦) / (denom‘𝑦))))
7133zcnd 11811 . . . . . . 7 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑥) ∈ ℂ)
7240zcnd 11811 . . . . . . 7 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ∈ ℂ)
7346zcnd 11811 . . . . . . 7 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑦) ∈ ℂ)
7450zcnd 11811 . . . . . . 7 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ∈ ℂ)
7571, 72, 73, 74, 41, 51divmuldivd 11168 . . . . . 6 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((numer‘𝑥) / (denom‘𝑥)) · ((numer‘𝑦) / (denom‘𝑦))) = (((numer‘𝑥) · (numer‘𝑦)) / ((denom‘𝑥) · (denom‘𝑦))))
7670, 75eqtrd 2861 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 · 𝑦) = (((numer‘𝑥) · (numer‘𝑦)) / ((denom‘𝑥) · (denom‘𝑦))))
7776fveq2d 6437 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 · 𝑦)) = ((ℚHom‘𝑅)‘(((numer‘𝑥) · (numer‘𝑦)) / ((denom‘𝑥) · (denom‘𝑦)))))
7833, 46zmulcld 11816 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((numer‘𝑥) · (numer‘𝑦)) ∈ ℤ)
7940, 50zmulcld 11816 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((denom‘𝑥) · (denom‘𝑦)) ∈ ℤ)
8072, 74, 41, 51mulne0d 11004 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((denom‘𝑥) · (denom‘𝑦)) ≠ 0)
8118, 19, 20qqhvq 30565 . . . . 5 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (((numer‘𝑥) · (numer‘𝑦)) ∈ ℤ ∧ ((denom‘𝑥) · (denom‘𝑦)) ∈ ℤ ∧ ((denom‘𝑥) · (denom‘𝑦)) ≠ 0)) → ((ℚHom‘𝑅)‘(((numer‘𝑥) · (numer‘𝑦)) / ((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘((numer‘𝑥) · (numer‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
8237, 78, 79, 80, 81syl13anc 1495 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(((numer‘𝑥) · (numer‘𝑦)) / ((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘((numer‘𝑥) · (numer‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
8335, 16syl 17 . . . . . . 7 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑅 ∈ Ring)
8483, 27syl 17 . . . . . 6 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝐿 ∈ (ℤring RingHom 𝑅))
85 zringmulr 20187 . . . . . . 7 · = (.r‘ℤring)
8628, 85, 9rhmmul 19083 . . . . . 6 ((𝐿 ∈ (ℤring RingHom 𝑅) ∧ (numer‘𝑥) ∈ ℤ ∧ (numer‘𝑦) ∈ ℤ) → (𝐿‘((numer‘𝑥) · (numer‘𝑦))) = ((𝐿‘(numer‘𝑥))(.r𝑅)(𝐿‘(numer‘𝑦))))
8784, 33, 46, 86syl3anc 1494 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((numer‘𝑥) · (numer‘𝑦))) = ((𝐿‘(numer‘𝑥))(.r𝑅)(𝐿‘(numer‘𝑦))))
8828, 85, 9rhmmul 19083 . . . . . 6 ((𝐿 ∈ (ℤring RingHom 𝑅) ∧ (denom‘𝑥) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) = ((𝐿‘(denom‘𝑥))(.r𝑅)(𝐿‘(denom‘𝑦))))
8984, 40, 50, 88syl3anc 1494 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) = ((𝐿‘(denom‘𝑥))(.r𝑅)(𝐿‘(denom‘𝑦))))
9087, 89oveq12d 6923 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘((numer‘𝑥) · (numer‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘(numer‘𝑥))(.r𝑅)(𝐿‘(numer‘𝑦))) / ((𝐿‘(denom‘𝑥))(.r𝑅)(𝐿‘(denom‘𝑦)))))
9177, 82, 903eqtrd 2865 . . 3 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 · 𝑦)) = (((𝐿‘(numer‘𝑥))(.r𝑅)(𝐿‘(numer‘𝑦))) / ((𝐿‘(denom‘𝑥))(.r𝑅)(𝐿‘(denom‘𝑦)))))
9254, 67, 913eqtr4rd 2872 . 2 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 · 𝑦)) = (((ℚHom‘𝑅)‘𝑥)(.r𝑅)((ℚHom‘𝑅)‘𝑦)))
93 cnfldadd 20111 . . . 4 + = (+g‘ℂfld)
941, 93ressplusg 16352 . . 3 (ℚ ∈ V → + = (+g𝑄))
955, 94ax-mp 5 . 2 + = (+g𝑄)
9618, 19, 20qqhf 30564 . . 3 ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵)
9714, 96sylan 575 . 2 ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵)
9833, 50zmulcld 11816 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((numer‘𝑥) · (denom‘𝑦)) ∈ ℤ)
9931, 98ffvelrnd 6609 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((numer‘𝑥) · (denom‘𝑦))) ∈ 𝐵)
10046, 40zmulcld 11816 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((numer‘𝑦) · (denom‘𝑥)) ∈ ℤ)
10131, 100ffvelrnd 6609 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((numer‘𝑦) · (denom‘𝑥))) ∈ 𝐵)
10223, 9unitmulcl 19018 . . . . . 6 ((𝑅 ∈ Ring ∧ (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅) ∧ (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅)) → ((𝐿‘(denom‘𝑥))(.r𝑅)(𝐿‘(denom‘𝑦))) ∈ (Unit‘𝑅))
10383, 44, 53, 102syl3anc 1494 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(denom‘𝑥))(.r𝑅)(𝐿‘(denom‘𝑦))) ∈ (Unit‘𝑅))
10489, 103eqeltrd 2906 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) ∈ (Unit‘𝑅))
10518, 23, 24, 19dvrdir 30324 . . . 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‘𝑦))))))
10683, 99, 101, 104, 105syl13anc 1495 . . 3 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))(+g𝑅)((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))))
10768, 69oveq12d 6923 . . . . . 6 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) = (((numer‘𝑥) / (denom‘𝑥)) + ((numer‘𝑦) / (denom‘𝑦))))
10871, 72, 73, 74, 41, 51divadddivd 11171 . . . . . 6 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((numer‘𝑥) / (denom‘𝑥)) + ((numer‘𝑦) / (denom‘𝑦))) = ((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦))))
109107, 108eqtrd 2861 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) = ((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦))))
110109fveq2d 6437 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = ((ℚHom‘𝑅)‘((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦)))))
11198, 100zaddcld 11814 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) ∈ ℤ)
11218, 19, 20qqhvq 30565 . . . . 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‘𝑦)))))
11337, 111, 79, 80, 112syl13anc 1495 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
114 rhmghm 19081 . . . . . 6 (𝐿 ∈ (ℤring RingHom 𝑅) → 𝐿 ∈ (ℤring GrpHom 𝑅))
11584, 114syl 17 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝐿 ∈ (ℤring GrpHom 𝑅))
116 zringplusg 20185 . . . . . . 7 + = (+g‘ℤring)
11728, 116, 24ghmlin 18016 . . . . . 6 ((𝐿 ∈ (ℤring GrpHom 𝑅) ∧ ((numer‘𝑥) · (denom‘𝑦)) ∈ ℤ ∧ ((numer‘𝑦) · (denom‘𝑥)) ∈ ℤ) → (𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))))
118117oveq1d 6920 . . . . 5 ((𝐿 ∈ (ℤring GrpHom 𝑅) ∧ ((numer‘𝑥) · (denom‘𝑦)) ∈ ℤ ∧ ((numer‘𝑦) · (denom‘𝑥)) ∈ ℤ) → ((𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
119115, 98, 100, 118syl3anc 1494 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
120110, 113, 1193eqtrd 2865 . . 3 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
12123, 28, 19, 85rhmdvd 30355 . . . . . 6 ((𝐿 ∈ (ℤring RingHom 𝑅) ∧ ((numer‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ) ∧ ((𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅) ∧ (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅))) → ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
12284, 33, 40, 50, 44, 53, 121syl132anc 1511 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
12357, 59, 1223eqtrd 2865 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑥) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
12423, 28, 19, 85rhmdvd 30355 . . . . . . 7 ((𝐿 ∈ (ℤring RingHom 𝑅) ∧ ((numer‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ ∧ (denom‘𝑥) ∈ ℤ) ∧ ((𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅) ∧ (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅))) → ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑦) · (denom‘𝑥)))))
12584, 46, 50, 40, 53, 44, 124syl132anc 1511 . . . . . 6 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑦) · (denom‘𝑥)))))
12672, 74mulcomd 10378 . . . . . . . 8 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((denom‘𝑥) · (denom‘𝑦)) = ((denom‘𝑦) · (denom‘𝑥)))
127126fveq2d 6437 . . . . . . 7 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) = (𝐿‘((denom‘𝑦) · (denom‘𝑥))))
128127oveq2d 6921 . . . . . 6 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑦) · (denom‘𝑥)))))
129125, 65, 1283eqtr4d 2871 . . . . 5 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
13063, 129eqtrd 2861 . . . 4 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑦) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
131123, 130oveq12d 6923 . . 3 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((ℚHom‘𝑅)‘𝑥)(+g𝑅)((ℚHom‘𝑅)‘𝑦)) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))(+g𝑅)((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))))
132106, 120, 1313eqtr4d 2871 . 2 (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = (((ℚHom‘𝑅)‘𝑥)(+g𝑅)((ℚHom‘𝑅)‘𝑦)))
1332, 3, 4, 8, 9, 12, 17, 22, 92, 18, 95, 24, 97, 132isrhmd 19085 1 ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅) ∈ (𝑄 RingHom 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1111   = wceq 1656  wcel 2164  wne 2999  Vcvv 3414  wf 6119  cfv 6123  (class class class)co 6905  0cc0 10252  1c1 10253   + caddc 10255   · cmul 10257   / cdiv 11009  cn 11350  cz 11704  cq 12071  numercnumer 15812  denomcdenom 15813  Basecbs 16222  s cress 16223  +gcplusg 16305  .rcmulr 16306  0gc0g 16453   GrpHom cghm 18008  1rcur 18855  Ringcrg 18901  CRingccrg 18902  Unitcui 18993  /rcdvr 19036   RingHom crh 19068  DivRingcdr 19103  Fieldcfield 19104  fldccnfld 20106  ringzring 20178  ℤRHomczrh 20208  chrcchr 20210  ℚHomcqqh 30550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-inf2 8815  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329  ax-pre-sup 10330  ax-addf 10331  ax-mulf 10332
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-1st 7428  df-2nd 7429  df-tpos 7617  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-oadd 7830  df-er 8009  df-map 8124  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-sup 8617  df-inf 8618  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-div 11010  df-nn 11351  df-2 11414  df-3 11415  df-4 11416  df-5 11417  df-6 11418  df-7 11419  df-8 11420  df-9 11421  df-n0 11619  df-z 11705  df-dec 11822  df-uz 11969  df-q 12072  df-rp 12113  df-fz 12620  df-fl 12888  df-mod 12964  df-seq 13096  df-exp 13155  df-cj 14216  df-re 14217  df-im 14218  df-sqrt 14352  df-abs 14353  df-dvds 15358  df-gcd 15590  df-numer 15814  df-denom 15815  df-gz 16005  df-struct 16224  df-ndx 16225  df-slot 16226  df-base 16228  df-sets 16229  df-ress 16230  df-plusg 16318  df-mulr 16319  df-starv 16320  df-tset 16324  df-ple 16325  df-ds 16327  df-unif 16328  df-0g 16455  df-mgm 17595  df-sgrp 17637  df-mnd 17648  df-mhm 17688  df-grp 17779  df-minusg 17780  df-sbg 17781  df-mulg 17895  df-subg 17942  df-ghm 18009  df-od 18299  df-cmn 18548  df-mgp 18844  df-ur 18856  df-ring 18903  df-cring 18904  df-oppr 18977  df-dvdsr 18995  df-unit 18996  df-invr 19026  df-dvr 19037  df-rnghom 19071  df-drng 19105  df-field 19106  df-subrg 19134  df-cnfld 20107  df-zring 20179  df-zrh 20212  df-chr 20214  df-qqh 30551
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator