Step | Hyp | Ref
| Expression |
1 | | qqhrhm.1 |
. . 3
⊢ 𝑄 = (ℂfld
↾s ℚ) |
2 | 1 | qrngbas 26765 |
. 2
⊢ ℚ =
(Base‘𝑄) |
3 | | qqhval2.0 |
. 2
⊢ 𝐵 = (Base‘𝑅) |
4 | | qex 12700 |
. . 3
⊢ ℚ
∈ V |
5 | | cnfldadd 20600 |
. . . 4
⊢ + =
(+g‘ℂfld) |
6 | 1, 5 | ressplusg 16998 |
. . 3
⊢ (ℚ
∈ V → + = (+g‘𝑄)) |
7 | 4, 6 | ax-mp 5 |
. 2
⊢ + =
(+g‘𝑄) |
8 | | eqid 2740 |
. 2
⊢
(+g‘𝑅) = (+g‘𝑅) |
9 | 1 | qdrng 26766 |
. . 3
⊢ 𝑄 ∈ DivRing |
10 | | drnggrp 19997 |
. . 3
⊢ (𝑄 ∈ DivRing → 𝑄 ∈ Grp) |
11 | 9, 10 | mp1i 13 |
. 2
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
𝑄 ∈
Grp) |
12 | | drnggrp 19997 |
. . 3
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Grp) |
13 | 12 | adantr 481 |
. 2
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
𝑅 ∈
Grp) |
14 | | qqhval2.1 |
. . 3
⊢ / =
(/r‘𝑅) |
15 | | qqhval2.2 |
. . 3
⊢ 𝐿 = (ℤRHom‘𝑅) |
16 | 3, 14, 15 | qqhf 31932 |
. 2
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅):ℚ⟶𝐵) |
17 | | drngring 19996 |
. . . . 5
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
18 | 17 | ad2antrr 723 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
𝑅 ∈
Ring) |
19 | 17 | adantr 481 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
𝑅 ∈
Ring) |
20 | 15 | zrhrhm 20711 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑅)) |
21 | | zringbas 20674 |
. . . . . . . 8
⊢ ℤ =
(Base‘ℤring) |
22 | 21, 3 | rhmf 19968 |
. . . . . . 7
⊢ (𝐿 ∈ (ℤring
RingHom 𝑅) → 𝐿:ℤ⟶𝐵) |
23 | 19, 20, 22 | 3syl 18 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
𝐿:ℤ⟶𝐵) |
24 | 23 | adantr 481 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
𝐿:ℤ⟶𝐵) |
25 | | qnumcl 16442 |
. . . . . . 7
⊢ (𝑥 ∈ ℚ →
(numer‘𝑥) ∈
ℤ) |
26 | 25 | ad2antrl 725 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(numer‘𝑥) ∈
ℤ) |
27 | | qdencl 16443 |
. . . . . . . 8
⊢ (𝑦 ∈ ℚ →
(denom‘𝑦) ∈
ℕ) |
28 | 27 | ad2antll 726 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(denom‘𝑦) ∈
ℕ) |
29 | 28 | nnzd 12424 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(denom‘𝑦) ∈
ℤ) |
30 | 26, 29 | zmulcld 12431 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((numer‘𝑥) ·
(denom‘𝑦)) ∈
ℤ) |
31 | 24, 30 | ffvelrnd 6959 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(𝐿‘((numer‘𝑥) · (denom‘𝑦))) ∈ 𝐵) |
32 | | qnumcl 16442 |
. . . . . . 7
⊢ (𝑦 ∈ ℚ →
(numer‘𝑦) ∈
ℤ) |
33 | 32 | ad2antll 726 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(numer‘𝑦) ∈
ℤ) |
34 | | qdencl 16443 |
. . . . . . . 8
⊢ (𝑥 ∈ ℚ →
(denom‘𝑥) ∈
ℕ) |
35 | 34 | ad2antrl 725 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(denom‘𝑥) ∈
ℕ) |
36 | 35 | nnzd 12424 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(denom‘𝑥) ∈
ℤ) |
37 | 33, 36 | zmulcld 12431 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((numer‘𝑦) ·
(denom‘𝑥)) ∈
ℤ) |
38 | 24, 37 | ffvelrnd 6959 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(𝐿‘((numer‘𝑦) · (denom‘𝑥))) ∈ 𝐵) |
39 | 18, 20 | syl 17 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
𝐿 ∈
(ℤring RingHom 𝑅)) |
40 | | zringmulr 20677 |
. . . . . . 7
⊢ ·
= (.r‘ℤring) |
41 | | eqid 2740 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
42 | 21, 40, 41 | rhmmul 19969 |
. . . . . 6
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑅) ∧
(denom‘𝑥) ∈
ℤ ∧ (denom‘𝑦) ∈ ℤ) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) = ((𝐿‘(denom‘𝑥))(.r‘𝑅)(𝐿‘(denom‘𝑦)))) |
43 | 39, 36, 29, 42 | syl3anc 1370 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(𝐿‘((denom‘𝑥) · (denom‘𝑦))) = ((𝐿‘(denom‘𝑥))(.r‘𝑅)(𝐿‘(denom‘𝑦)))) |
44 | | simpl 483 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(𝑅 ∈ DivRing ∧
(chr‘𝑅) =
0)) |
45 | 35 | nnne0d 12023 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(denom‘𝑥) ≠
0) |
46 | | eqid 2740 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
47 | 3, 15, 46 | elzrhunit 31925 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
((denom‘𝑥) ∈
ℤ ∧ (denom‘𝑥) ≠ 0)) → (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅)) |
48 | 44, 36, 45, 47 | syl12anc 834 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅)) |
49 | 28 | nnne0d 12023 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(denom‘𝑦) ≠
0) |
50 | 3, 15, 46 | elzrhunit 31925 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
((denom‘𝑦) ∈
ℤ ∧ (denom‘𝑦) ≠ 0)) → (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅)) |
51 | 44, 29, 49, 50 | syl12anc 834 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅)) |
52 | | eqid 2740 |
. . . . . . 7
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
53 | 52, 41 | unitmulcl 19904 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅) ∧ (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅)) → ((𝐿‘(denom‘𝑥))(.r‘𝑅)(𝐿‘(denom‘𝑦))) ∈ (Unit‘𝑅)) |
54 | 18, 48, 51, 53 | syl3anc 1370 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((𝐿‘(denom‘𝑥))(.r‘𝑅)(𝐿‘(denom‘𝑦))) ∈ (Unit‘𝑅)) |
55 | 43, 54 | eqeltrd 2841 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(𝐿‘((denom‘𝑥) · (denom‘𝑦))) ∈ (Unit‘𝑅)) |
56 | 3, 52, 8, 14 | dvrdir 31483 |
. . . 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‘𝑦)))))) |
57 | 18, 31, 38, 55, 56 | syl13anc 1371 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g‘𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))(+g‘𝑅)((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))) |
58 | | qeqnumdivden 16448 |
. . . . . . . 8
⊢ (𝑥 ∈ ℚ → 𝑥 = ((numer‘𝑥) / (denom‘𝑥))) |
59 | 58 | ad2antrl 725 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
𝑥 = ((numer‘𝑥) / (denom‘𝑥))) |
60 | | qeqnumdivden 16448 |
. . . . . . . 8
⊢ (𝑦 ∈ ℚ → 𝑦 = ((numer‘𝑦) / (denom‘𝑦))) |
61 | 60 | ad2antll 726 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
𝑦 = ((numer‘𝑦) / (denom‘𝑦))) |
62 | 59, 61 | oveq12d 7289 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(𝑥 + 𝑦) = (((numer‘𝑥) / (denom‘𝑥)) + ((numer‘𝑦) / (denom‘𝑦)))) |
63 | 26 | zcnd 12426 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(numer‘𝑥) ∈
ℂ) |
64 | 36 | zcnd 12426 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(denom‘𝑥) ∈
ℂ) |
65 | 33 | zcnd 12426 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(numer‘𝑦) ∈
ℂ) |
66 | 29 | zcnd 12426 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(denom‘𝑦) ∈
ℂ) |
67 | 63, 64, 65, 66, 45, 49 | divadddivd 11795 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(((numer‘𝑥) /
(denom‘𝑥)) +
((numer‘𝑦) /
(denom‘𝑦))) =
((((numer‘𝑥) ·
(denom‘𝑦)) +
((numer‘𝑦) ·
(denom‘𝑥))) /
((denom‘𝑥) ·
(denom‘𝑦)))) |
68 | 62, 67 | eqtrd 2780 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(𝑥 + 𝑦) = ((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦)))) |
69 | 68 | fveq2d 6775 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = ((ℚHom‘𝑅)‘((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦))))) |
70 | 30, 37 | zaddcld 12429 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(((numer‘𝑥) ·
(denom‘𝑦)) +
((numer‘𝑦) ·
(denom‘𝑥))) ∈
ℤ) |
71 | 36, 29 | zmulcld 12431 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((denom‘𝑥) ·
(denom‘𝑦)) ∈
ℤ) |
72 | 64, 66, 45, 49 | mulne0d 11627 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((denom‘𝑥) ·
(denom‘𝑦)) ≠
0) |
73 | 3, 14, 15 | qqhvq 31933 |
. . . . 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‘𝑦))))) |
74 | 44, 70, 71, 72, 73 | syl13anc 1371 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((ℚHom‘𝑅)‘((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))) |
75 | | rhmghm 19967 |
. . . . . 6
⊢ (𝐿 ∈ (ℤring
RingHom 𝑅) → 𝐿 ∈ (ℤring
GrpHom 𝑅)) |
76 | 39, 75 | syl 17 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
𝐿 ∈
(ℤring GrpHom 𝑅)) |
77 | | zringplusg 20675 |
. . . . . . 7
⊢ + =
(+g‘ℤring) |
78 | 21, 77, 8 | ghmlin 18837 |
. . . . . 6
⊢ ((𝐿 ∈ (ℤring
GrpHom 𝑅) ∧
((numer‘𝑥) ·
(denom‘𝑦)) ∈
ℤ ∧ ((numer‘𝑦) · (denom‘𝑥)) ∈ ℤ) → (𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g‘𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥))))) |
79 | 78 | oveq1d 7286 |
. . . . 5
⊢ ((𝐿 ∈ (ℤ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 1370 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g‘𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))) |
81 | 69, 74, 80 | 3eqtrd 2784 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g‘𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))) |
82 | 58 | fveq2d 6775 |
. . . . . 6
⊢ (𝑥 ∈ ℚ →
((ℚHom‘𝑅)‘𝑥) = ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥)))) |
83 | 82 | ad2antrl 725 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((ℚHom‘𝑅)‘𝑥) = ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥)))) |
84 | 3, 14, 15 | qqhvq 31933 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
((numer‘𝑥) ∈
ℤ ∧ (denom‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ≠ 0)) →
((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))) = ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥)))) |
85 | 44, 26, 36, 45, 84 | syl13anc 1371 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))) = ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥)))) |
86 | 52, 21, 14, 40 | rhmdvd 31516 |
. . . . . 6
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑅) ∧
((numer‘𝑥) ∈
ℤ ∧ (denom‘𝑥) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ) ∧ ((𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅) ∧ (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅))) → ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))) |
87 | 39, 26, 36, 29, 48, 51, 86 | syl132anc 1387 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))) |
88 | 83, 85, 87 | 3eqtrd 2784 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((ℚHom‘𝑅)‘𝑥) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))) |
89 | 60 | fveq2d 6775 |
. . . . . 6
⊢ (𝑦 ∈ ℚ →
((ℚHom‘𝑅)‘𝑦) = ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦)))) |
90 | 89 | ad2antll 726 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((ℚHom‘𝑅)‘𝑦) = ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦)))) |
91 | 52, 21, 14, 40 | rhmdvd 31516 |
. . . . . . 7
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑅) ∧
((numer‘𝑦) ∈
ℤ ∧ (denom‘𝑦) ∈ ℤ ∧ (denom‘𝑥) ∈ ℤ) ∧ ((𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅) ∧ (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅))) → ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑦) · (denom‘𝑥))))) |
92 | 39, 33, 29, 36, 51, 48, 91 | syl132anc 1387 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑦) · (denom‘𝑥))))) |
93 | 3, 14, 15 | qqhvq 31933 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
((numer‘𝑦) ∈
ℤ ∧ (denom‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ≠ 0)) →
((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦)))) |
94 | 44, 33, 29, 49, 93 | syl13anc 1371 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦)))) |
95 | 64, 66 | mulcomd 10997 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((denom‘𝑥) ·
(denom‘𝑦)) =
((denom‘𝑦) ·
(denom‘𝑥))) |
96 | 95 | fveq2d 6775 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(𝐿‘((denom‘𝑥) · (denom‘𝑦))) = (𝐿‘((denom‘𝑦) · (denom‘𝑥)))) |
97 | 96 | oveq2d 7287 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑦) · (denom‘𝑥))))) |
98 | 92, 94, 97 | 3eqtr4d 2790 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))) |
99 | 90, 98 | eqtrd 2780 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((ℚHom‘𝑅)‘𝑦) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))) |
100 | 88, 99 | oveq12d 7289 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
(((ℚHom‘𝑅)‘𝑥)(+g‘𝑅)((ℚHom‘𝑅)‘𝑦)) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))(+g‘𝑅)((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))) |
101 | 57, 81, 100 | 3eqtr4d 2790 |
. 2
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℚ ∧
𝑦 ∈ ℚ)) →
((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = (((ℚHom‘𝑅)‘𝑥)(+g‘𝑅)((ℚHom‘𝑅)‘𝑦))) |
102 | 2, 3, 7, 8, 11, 13, 16, 101 | isghmd 18841 |
1
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) ∈
(𝑄 GrpHom 𝑅)) |