Step | Hyp | Ref
| Expression |
1 | | domnring 20567 |
. . . . 5
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring) |
2 | 1 | adantl 482 |
. . . 4
⊢ ((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) → 𝑅 ∈ Ring) |
3 | | domnnzr 20566 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
4 | 3 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) → 𝑅 ∈ NzRing) |
5 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(1r‘𝑅) = (1r‘𝑅) |
6 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
7 | 5, 6 | nzrnz 20531 |
. . . . . . . . . 10
⊢ (𝑅 ∈ NzRing →
(1r‘𝑅)
≠ (0g‘𝑅)) |
8 | 4, 7 | syl 17 |
. . . . . . . . 9
⊢ ((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) →
(1r‘𝑅)
≠ (0g‘𝑅)) |
9 | 8 | neneqd 2948 |
. . . . . . . 8
⊢ ((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) → ¬
(1r‘𝑅) =
(0g‘𝑅)) |
10 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
11 | 10, 6, 5 | 0unit 19922 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
((0g‘𝑅)
∈ (Unit‘𝑅)
↔ (1r‘𝑅) = (0g‘𝑅))) |
12 | 2, 11 | syl 17 |
. . . . . . . 8
⊢ ((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) →
((0g‘𝑅)
∈ (Unit‘𝑅)
↔ (1r‘𝑅) = (0g‘𝑅))) |
13 | 9, 12 | mtbird 325 |
. . . . . . 7
⊢ ((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) → ¬
(0g‘𝑅)
∈ (Unit‘𝑅)) |
14 | | disjsn 4647 |
. . . . . . 7
⊢
(((Unit‘𝑅)
∩ {(0g‘𝑅)}) = ∅ ↔ ¬
(0g‘𝑅)
∈ (Unit‘𝑅)) |
15 | 13, 14 | sylibr 233 |
. . . . . 6
⊢ ((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) →
((Unit‘𝑅) ∩
{(0g‘𝑅)})
= ∅) |
16 | | fidomndrng.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) |
17 | 16, 10 | unitss 19902 |
. . . . . . 7
⊢
(Unit‘𝑅)
⊆ 𝐵 |
18 | | reldisj 4385 |
. . . . . . 7
⊢
((Unit‘𝑅)
⊆ 𝐵 →
(((Unit‘𝑅) ∩
{(0g‘𝑅)})
= ∅ ↔ (Unit‘𝑅) ⊆ (𝐵 ∖ {(0g‘𝑅)}))) |
19 | 17, 18 | ax-mp 5 |
. . . . . 6
⊢
(((Unit‘𝑅)
∩ {(0g‘𝑅)}) = ∅ ↔ (Unit‘𝑅) ⊆ (𝐵 ∖ {(0g‘𝑅)})) |
20 | 15, 19 | sylib 217 |
. . . . 5
⊢ ((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) →
(Unit‘𝑅) ⊆
(𝐵 ∖
{(0g‘𝑅)})) |
21 | | eqid 2738 |
. . . . . . 7
⊢
(∥r‘𝑅) = (∥r‘𝑅) |
22 | | eqid 2738 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
23 | | simplr 766 |
. . . . . . 7
⊢ (((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) ∧ 𝑥 ∈ (𝐵 ∖ {(0g‘𝑅)})) → 𝑅 ∈ Domn) |
24 | | simpll 764 |
. . . . . . 7
⊢ (((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) ∧ 𝑥 ∈ (𝐵 ∖ {(0g‘𝑅)})) → 𝐵 ∈ Fin) |
25 | | simpr 485 |
. . . . . . 7
⊢ (((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) ∧ 𝑥 ∈ (𝐵 ∖ {(0g‘𝑅)})) → 𝑥 ∈ (𝐵 ∖ {(0g‘𝑅)})) |
26 | | eqid 2738 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 ↦ (𝑦(.r‘𝑅)𝑥)) = (𝑦 ∈ 𝐵 ↦ (𝑦(.r‘𝑅)𝑥)) |
27 | 16, 6, 5, 21, 22, 23, 24, 25, 26 | fidomndrnglem 20578 |
. . . . . 6
⊢ (((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) ∧ 𝑥 ∈ (𝐵 ∖ {(0g‘𝑅)})) → 𝑥(∥r‘𝑅)(1r‘𝑅)) |
28 | | eqid 2738 |
. . . . . . . 8
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
29 | 28, 16 | opprbas 19869 |
. . . . . . 7
⊢ 𝐵 =
(Base‘(oppr‘𝑅)) |
30 | 28, 6 | oppr0 19875 |
. . . . . . 7
⊢
(0g‘𝑅) =
(0g‘(oppr‘𝑅)) |
31 | 28, 5 | oppr1 19876 |
. . . . . . 7
⊢
(1r‘𝑅) =
(1r‘(oppr‘𝑅)) |
32 | | eqid 2738 |
. . . . . . 7
⊢
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅)) |
33 | | eqid 2738 |
. . . . . . 7
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
34 | 28 | opprdomn 20572 |
. . . . . . . 8
⊢ (𝑅 ∈ Domn →
(oppr‘𝑅) ∈ Domn) |
35 | 23, 34 | syl 17 |
. . . . . . 7
⊢ (((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) ∧ 𝑥 ∈ (𝐵 ∖ {(0g‘𝑅)})) →
(oppr‘𝑅) ∈ Domn) |
36 | | eqid 2738 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 ↦ (𝑦(.r‘(oppr‘𝑅))𝑥)) = (𝑦 ∈ 𝐵 ↦ (𝑦(.r‘(oppr‘𝑅))𝑥)) |
37 | 29, 30, 31, 32, 33, 35, 24, 25, 36 | fidomndrnglem 20578 |
. . . . . 6
⊢ (((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) ∧ 𝑥 ∈ (𝐵 ∖ {(0g‘𝑅)})) → 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
38 | 10, 5, 21, 28, 32 | isunit 19899 |
. . . . . 6
⊢ (𝑥 ∈ (Unit‘𝑅) ↔ (𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
39 | 27, 37, 38 | sylanbrc 583 |
. . . . 5
⊢ (((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) ∧ 𝑥 ∈ (𝐵 ∖ {(0g‘𝑅)})) → 𝑥 ∈ (Unit‘𝑅)) |
40 | 20, 39 | eqelssd 3942 |
. . . 4
⊢ ((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) →
(Unit‘𝑅) = (𝐵 ∖
{(0g‘𝑅)})) |
41 | 16, 10, 6 | isdrng 19995 |
. . . 4
⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖
{(0g‘𝑅)}))) |
42 | 2, 40, 41 | sylanbrc 583 |
. . 3
⊢ ((𝐵 ∈ Fin ∧ 𝑅 ∈ Domn) → 𝑅 ∈
DivRing) |
43 | 42 | ex 413 |
. 2
⊢ (𝐵 ∈ Fin → (𝑅 ∈ Domn → 𝑅 ∈
DivRing)) |
44 | | drngdomn 20574 |
. 2
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Domn) |
45 | 43, 44 | impbid1 224 |
1
⊢ (𝐵 ∈ Fin → (𝑅 ∈ Domn ↔ 𝑅 ∈
DivRing)) |