Step | Hyp | Ref
| Expression |
1 | | brric 20395 |
. . 3
⊢ (𝑅 ≃𝑟
𝑆 ↔ (𝑅 RingIso 𝑆) ≠ ∅) |
2 | | n0 4338 |
. . 3
⊢ ((𝑅 RingIso 𝑆) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑅 RingIso 𝑆)) |
3 | 1, 2 | bitri 275 |
. 2
⊢ (𝑅 ≃𝑟
𝑆 ↔ ∃𝑓 𝑓 ∈ (𝑅 RingIso 𝑆)) |
4 | | eqid 2724 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
5 | | eqid 2724 |
. . . . . . . . . . 11
⊢
(Base‘𝑆) =
(Base‘𝑆) |
6 | 4, 5 | rimf1o 20385 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (𝑅 RingIso 𝑆) → 𝑓:(Base‘𝑅)–1-1-onto→(Base‘𝑆)) |
7 | | f1ofo 6830 |
. . . . . . . . . 10
⊢ (𝑓:(Base‘𝑅)–1-1-onto→(Base‘𝑆) → 𝑓:(Base‘𝑅)–onto→(Base‘𝑆)) |
8 | | foima 6800 |
. . . . . . . . . 10
⊢ (𝑓:(Base‘𝑅)–onto→(Base‘𝑆) → (𝑓 “ (Base‘𝑅)) = (Base‘𝑆)) |
9 | 6, 7, 8 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝑅 RingIso 𝑆) → (𝑓 “ (Base‘𝑅)) = (Base‘𝑆)) |
10 | 9 | oveq2d 7417 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝑅 RingIso 𝑆) → (𝑆 ↾s (𝑓 “ (Base‘𝑅))) = (𝑆 ↾s (Base‘𝑆))) |
11 | | rimrcl2 41548 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝑅 RingIso 𝑆) → 𝑆 ∈ Ring) |
12 | 5 | ressid 17187 |
. . . . . . . . 9
⊢ (𝑆 ∈ Ring → (𝑆 ↾s
(Base‘𝑆)) = 𝑆) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝑅 RingIso 𝑆) → (𝑆 ↾s (Base‘𝑆)) = 𝑆) |
14 | 10, 13 | eqtr2d 2765 |
. . . . . . 7
⊢ (𝑓 ∈ (𝑅 RingIso 𝑆) → 𝑆 = (𝑆 ↾s (𝑓 “ (Base‘𝑅)))) |
15 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) → 𝑆 = (𝑆 ↾s (𝑓 “ (Base‘𝑅)))) |
16 | | eqid 2724 |
. . . . . . 7
⊢ (𝑆 ↾s (𝑓 “ (Base‘𝑅))) = (𝑆 ↾s (𝑓 “ (Base‘𝑅))) |
17 | | eqid 2724 |
. . . . . . 7
⊢
(0g‘𝑆) = (0g‘𝑆) |
18 | | rimrhm 20387 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝑅 RingIso 𝑆) → 𝑓 ∈ (𝑅 RingHom 𝑆)) |
19 | 18 | adantr 480 |
. . . . . . 7
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) → 𝑓 ∈ (𝑅 RingHom 𝑆)) |
20 | 4 | sdrgid 20632 |
. . . . . . . 8
⊢ (𝑅 ∈ DivRing →
(Base‘𝑅) ∈
(SubDRing‘𝑅)) |
21 | 20 | adantl 481 |
. . . . . . 7
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) → (Base‘𝑅) ∈ (SubDRing‘𝑅)) |
22 | | forn 6798 |
. . . . . . . . . 10
⊢ (𝑓:(Base‘𝑅)–onto→(Base‘𝑆) → ran 𝑓 = (Base‘𝑆)) |
23 | 6, 7, 22 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝑅 RingIso 𝑆) → ran 𝑓 = (Base‘𝑆)) |
24 | 23 | adantr 480 |
. . . . . . . 8
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) → ran 𝑓 = (Base‘𝑆)) |
25 | | rhmrcl2 20368 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (𝑅 RingHom 𝑆) → 𝑆 ∈ Ring) |
26 | | eqid 2724 |
. . . . . . . . . . 11
⊢
(1r‘𝑆) = (1r‘𝑆) |
27 | 5, 26 | ringidcl 20154 |
. . . . . . . . . 10
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ (Base‘𝑆)) |
28 | 18, 25, 27 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝑅 RingIso 𝑆) → (1r‘𝑆) ∈ (Base‘𝑆)) |
29 | | eqid 2724 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝑅) = (0g‘𝑅) |
30 | | eqid 2724 |
. . . . . . . . . . . . . 14
⊢
(1r‘𝑅) = (1r‘𝑅) |
31 | 29, 30 | drngunz 20595 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ DivRing →
(1r‘𝑅)
≠ (0g‘𝑅)) |
32 | 31 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) →
(1r‘𝑅)
≠ (0g‘𝑅)) |
33 | | f1of1 6822 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(Base‘𝑅)–1-1-onto→(Base‘𝑆) → 𝑓:(Base‘𝑅)–1-1→(Base‘𝑆)) |
34 | 6, 33 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (𝑅 RingIso 𝑆) → 𝑓:(Base‘𝑅)–1-1→(Base‘𝑆)) |
35 | | drngring 20583 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
36 | 4, 30 | ringidcl 20154 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ DivRing →
(1r‘𝑅)
∈ (Base‘𝑅)) |
38 | 4, 29 | ring0cl 20155 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ (Base‘𝑅)) |
39 | 35, 38 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ DivRing →
(0g‘𝑅)
∈ (Base‘𝑅)) |
40 | 37, 39 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ DivRing →
((1r‘𝑅)
∈ (Base‘𝑅) ∧
(0g‘𝑅)
∈ (Base‘𝑅))) |
41 | | f1veqaeq 7248 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(Base‘𝑅)–1-1→(Base‘𝑆) ∧ ((1r‘𝑅) ∈ (Base‘𝑅) ∧
(0g‘𝑅)
∈ (Base‘𝑅)))
→ ((𝑓‘(1r‘𝑅)) = (𝑓‘(0g‘𝑅)) → (1r‘𝑅) = (0g‘𝑅))) |
42 | 34, 40, 41 | syl2an 595 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) → ((𝑓‘(1r‘𝑅)) = (𝑓‘(0g‘𝑅)) → (1r‘𝑅) = (0g‘𝑅))) |
43 | 42 | imp 406 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) ∧ (𝑓‘(1r‘𝑅)) = (𝑓‘(0g‘𝑅))) → (1r‘𝑅) = (0g‘𝑅)) |
44 | 32, 43 | mteqand 3025 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) → (𝑓‘(1r‘𝑅)) ≠ (𝑓‘(0g‘𝑅))) |
45 | 30, 26 | rhm1 20380 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (𝑅 RingHom 𝑆) → (𝑓‘(1r‘𝑅)) = (1r‘𝑆)) |
46 | 19, 45 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) → (𝑓‘(1r‘𝑅)) = (1r‘𝑆)) |
47 | | rhmghm 20375 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (𝑅 RingHom 𝑆) → 𝑓 ∈ (𝑅 GrpHom 𝑆)) |
48 | 29, 17 | ghmid 19136 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (𝑅 GrpHom 𝑆) → (𝑓‘(0g‘𝑅)) = (0g‘𝑆)) |
49 | 19, 47, 48 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) → (𝑓‘(0g‘𝑅)) = (0g‘𝑆)) |
50 | 44, 46, 49 | 3netr3d 3009 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) →
(1r‘𝑆)
≠ (0g‘𝑆)) |
51 | | nelsn 4660 |
. . . . . . . . . 10
⊢
((1r‘𝑆) ≠ (0g‘𝑆) → ¬
(1r‘𝑆)
∈ {(0g‘𝑆)}) |
52 | 50, 51 | syl 17 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) → ¬
(1r‘𝑆)
∈ {(0g‘𝑆)}) |
53 | | nelne1 3031 |
. . . . . . . . 9
⊢
(((1r‘𝑆) ∈ (Base‘𝑆) ∧ ¬ (1r‘𝑆) ∈
{(0g‘𝑆)})
→ (Base‘𝑆) ≠
{(0g‘𝑆)}) |
54 | 28, 52, 53 | syl2an2r 682 |
. . . . . . . 8
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) → (Base‘𝑆) ≠
{(0g‘𝑆)}) |
55 | 24, 54 | eqnetrd 3000 |
. . . . . . 7
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) → ran 𝑓 ≠
{(0g‘𝑆)}) |
56 | 16, 17, 19, 21, 55 | imadrhmcl 20637 |
. . . . . 6
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) → (𝑆 ↾s (𝑓 “ (Base‘𝑅))) ∈ DivRing) |
57 | 15, 56 | eqeltrd 2825 |
. . . . 5
⊢ ((𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) → 𝑆 ∈ DivRing) |
58 | 57 | ex 412 |
. . . 4
⊢ (𝑓 ∈ (𝑅 RingIso 𝑆) → (𝑅 ∈ DivRing → 𝑆 ∈ DivRing)) |
59 | 58 | exlimiv 1925 |
. . 3
⊢
(∃𝑓 𝑓 ∈ (𝑅 RingIso 𝑆) → (𝑅 ∈ DivRing → 𝑆 ∈ DivRing)) |
60 | 59 | imp 406 |
. 2
⊢
((∃𝑓 𝑓 ∈ (𝑅 RingIso 𝑆) ∧ 𝑅 ∈ DivRing) → 𝑆 ∈ DivRing) |
61 | 3, 60 | sylanb 580 |
1
⊢ ((𝑅 ≃𝑟
𝑆 ∧ 𝑅 ∈ DivRing) → 𝑆 ∈ DivRing) |