Step | Hyp | Ref
| Expression |
1 | | zringbas 20622 |
. . . . . . . . . 10
⊢ ℤ =
(Base‘ℤring) |
2 | | eqid 2821 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | 1, 2 | rhmf 19477 |
. . . . . . . . 9
⊢ (𝑓 ∈ (ℤring
RingHom 𝑅) → 𝑓:ℤ⟶(Base‘𝑅)) |
4 | 3 | adantl 484 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) → 𝑓:ℤ⟶(Base‘𝑅)) |
5 | 4 | feqmptd 6732 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) → 𝑓 = (𝑛 ∈ ℤ ↦ (𝑓‘𝑛))) |
6 | | rhmghm 19476 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (ℤring
RingHom 𝑅) → 𝑓 ∈ (ℤring
GrpHom 𝑅)) |
7 | 6 | ad2antlr 725 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) ∧ 𝑛 ∈ ℤ) → 𝑓 ∈ (ℤring
GrpHom 𝑅)) |
8 | | simpr 487 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈
ℤ) |
9 | | 1zzd 12012 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) ∧ 𝑛 ∈ ℤ) → 1 ∈
ℤ) |
10 | | eqid 2821 |
. . . . . . . . . . 11
⊢
(.g‘ℤring) =
(.g‘ℤring) |
11 | | mulgghm2.m |
. . . . . . . . . . 11
⊢ · =
(.g‘𝑅) |
12 | 1, 10, 11 | ghmmulg 18369 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (ℤring
GrpHom 𝑅) ∧ 𝑛 ∈ ℤ ∧ 1 ∈
ℤ) → (𝑓‘(𝑛(.g‘ℤring)1))
= (𝑛 · (𝑓‘1))) |
13 | 7, 8, 9, 12 | syl3anc 1367 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) ∧ 𝑛 ∈ ℤ) → (𝑓‘(𝑛(.g‘ℤring)1))
= (𝑛 · (𝑓‘1))) |
14 | | ax-1cn 10594 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
15 | | cnfldmulg 20576 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 1 ∈
ℂ) → (𝑛(.g‘ℂfld)1)
= (𝑛 ·
1)) |
16 | 14, 15 | mpan2 689 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → (𝑛(.g‘ℂfld)1)
= (𝑛 ·
1)) |
17 | | 1z 12011 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
18 | 16 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℤ ∧ 1 ∈
ℤ) → (𝑛(.g‘ℂfld)1)
= (𝑛 ·
1)) |
19 | | zringmulg 20624 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℤ ∧ 1 ∈
ℤ) → (𝑛(.g‘ℤring)1)
= (𝑛 ·
1)) |
20 | 18, 19 | eqtr4d 2859 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 1 ∈
ℤ) → (𝑛(.g‘ℂfld)1)
= (𝑛(.g‘ℤring)1)) |
21 | 17, 20 | mpan2 689 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → (𝑛(.g‘ℂfld)1)
= (𝑛(.g‘ℤring)1)) |
22 | | zcn 11985 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
23 | 22 | mulid1d 10657 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → (𝑛 · 1) = 𝑛) |
24 | 16, 21, 23 | 3eqtr3d 2864 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → (𝑛(.g‘ℤring)1)
= 𝑛) |
25 | 24 | adantl 484 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) ∧ 𝑛 ∈ ℤ) → (𝑛(.g‘ℤring)1)
= 𝑛) |
26 | 25 | fveq2d 6673 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) ∧ 𝑛 ∈ ℤ) → (𝑓‘(𝑛(.g‘ℤring)1))
= (𝑓‘𝑛)) |
27 | | zring1 20627 |
. . . . . . . . . . . 12
⊢ 1 =
(1r‘ℤring) |
28 | | mulgrhm.1 |
. . . . . . . . . . . 12
⊢ 1 =
(1r‘𝑅) |
29 | 27, 28 | rhm1 19481 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (ℤring
RingHom 𝑅) → (𝑓‘1) = 1 ) |
30 | 29 | ad2antlr 725 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) ∧ 𝑛 ∈ ℤ) → (𝑓‘1) = 1 ) |
31 | 30 | oveq2d 7171 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) ∧ 𝑛 ∈ ℤ) → (𝑛 · (𝑓‘1)) = (𝑛 · 1 )) |
32 | 13, 26, 31 | 3eqtr3d 2864 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) ∧ 𝑛 ∈ ℤ) → (𝑓‘𝑛) = (𝑛 · 1 )) |
33 | 32 | mpteq2dva 5160 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) → (𝑛 ∈ ℤ ↦ (𝑓‘𝑛)) = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))) |
34 | 5, 33 | eqtrd 2856 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) → 𝑓 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))) |
35 | | mulgghm2.f |
. . . . . 6
⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )) |
36 | 34, 35 | syl6eqr 2874 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) → 𝑓 = 𝐹) |
37 | | velsn 4582 |
. . . . 5
⊢ (𝑓 ∈ {𝐹} ↔ 𝑓 = 𝐹) |
38 | 36, 37 | sylibr 236 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑓 ∈ (ℤring
RingHom 𝑅)) → 𝑓 ∈ {𝐹}) |
39 | 38 | ex 415 |
. . 3
⊢ (𝑅 ∈ Ring → (𝑓 ∈ (ℤring
RingHom 𝑅) → 𝑓 ∈ {𝐹})) |
40 | 39 | ssrdv 3972 |
. 2
⊢ (𝑅 ∈ Ring →
(ℤring RingHom 𝑅) ⊆ {𝐹}) |
41 | 11, 35, 28 | mulgrhm 20644 |
. . 3
⊢ (𝑅 ∈ Ring → 𝐹 ∈ (ℤring
RingHom 𝑅)) |
42 | 41 | snssd 4741 |
. 2
⊢ (𝑅 ∈ Ring → {𝐹} ⊆
(ℤring RingHom 𝑅)) |
43 | 40, 42 | eqssd 3983 |
1
⊢ (𝑅 ∈ Ring →
(ℤring RingHom 𝑅) = {𝐹}) |