Step | Hyp | Ref
| Expression |
1 | | isdrng2.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
2 | | eqid 2610 |
. . 3
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
3 | | isdrng2.z |
. . 3
⊢ 0 =
(0g‘𝑅) |
4 | 1, 2, 3 | isdrng 18574 |
. 2
⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖ { 0 }))) |
5 | | oveq2 6557 |
. . . . . . 7
⊢
((Unit‘𝑅) =
(𝐵 ∖ { 0 }) →
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))) |
6 | 5 | adantl 481 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖ { 0 })) →
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))) |
7 | | isdrng2.g |
. . . . . 6
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) |
8 | 6, 7 | syl6eqr 2662 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖ { 0 })) →
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) = 𝐺) |
9 | | eqid 2610 |
. . . . . . 7
⊢
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) |
10 | 2, 9 | unitgrp 18490 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) ∈ Grp) |
11 | 10 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖ { 0 })) →
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) ∈ Grp) |
12 | 8, 11 | eqeltrrd 2689 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖ { 0 })) → 𝐺 ∈ Grp) |
13 | 1, 2 | unitcl 18482 |
. . . . . . . . 9
⊢ (𝑥 ∈ (Unit‘𝑅) → 𝑥 ∈ 𝐵) |
14 | 13 | adantl 481 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) → 𝑥 ∈ 𝐵) |
15 | | difss 3699 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∖ { 0 }) ⊆ 𝐵 |
16 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
17 | 16, 1 | mgpbas 18318 |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 =
(Base‘(mulGrp‘𝑅)) |
18 | 7, 17 | ressbas2 15758 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∖ { 0 }) ⊆ 𝐵 → (𝐵 ∖ { 0 }) = (Base‘𝐺)) |
19 | 15, 18 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∖ { 0 }) = (Base‘𝐺) |
20 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝐺) = (0g‘𝐺) |
21 | 19, 20 | grpidcl 17273 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ (𝐵 ∖ { 0
})) |
22 | 21 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
(0g‘𝐺)
∈ (𝐵 ∖ { 0
})) |
23 | | eldifsn 4260 |
. . . . . . . . . . . 12
⊢
((0g‘𝐺) ∈ (𝐵 ∖ { 0 }) ↔
((0g‘𝐺)
∈ 𝐵 ∧
(0g‘𝐺)
≠ 0
)) |
24 | 22, 23 | sylib 207 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
((0g‘𝐺)
∈ 𝐵 ∧
(0g‘𝐺)
≠ 0
)) |
25 | 24 | simprd 478 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
(0g‘𝐺)
≠ 0
) |
26 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) → 𝑅 ∈ Ring) |
27 | 22 | eldifad 3552 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
(0g‘𝐺)
∈ 𝐵) |
28 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) → 𝑥 ∈ (Unit‘𝑅)) |
29 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(/r‘𝑅) = (/r‘𝑅) |
30 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(.r‘𝑅) = (.r‘𝑅) |
31 | 1, 2, 29, 30 | dvrcan1 18514 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧
(0g‘𝐺)
∈ 𝐵 ∧ 𝑥 ∈ (Unit‘𝑅)) →
(((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅)𝑥) = (0g‘𝐺)) |
32 | 26, 27, 28, 31 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
(((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅)𝑥) = (0g‘𝐺)) |
33 | 1, 2, 29 | dvrcl 18509 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧
(0g‘𝐺)
∈ 𝐵 ∧ 𝑥 ∈ (Unit‘𝑅)) →
((0g‘𝐺)(/r‘𝑅)𝑥) ∈ 𝐵) |
34 | 26, 27, 28, 33 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
((0g‘𝐺)(/r‘𝑅)𝑥) ∈ 𝐵) |
35 | 1, 30, 3 | ringrz 18411 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧
((0g‘𝐺)(/r‘𝑅)𝑥) ∈ 𝐵) → (((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅) 0 ) = 0 ) |
36 | 26, 34, 35 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
(((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅) 0 ) = 0 ) |
37 | 25, 32, 36 | 3netr4d 2859 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
(((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅)𝑥) ≠ (((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅) 0 )) |
38 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑥 = 0 →
(((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅)𝑥) = (((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅) 0 )) |
39 | 38 | necon3i 2814 |
. . . . . . . . 9
⊢
((((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅)𝑥) ≠ (((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅) 0 ) → 𝑥 ≠ 0 ) |
40 | 37, 39 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) → 𝑥 ≠ 0 ) |
41 | | eldifsn 4260 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ∖ { 0 }) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) |
42 | 14, 40, 41 | sylanbrc 695 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) → 𝑥 ∈ (𝐵 ∖ { 0 })) |
43 | 42 | ex 449 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) → (𝑥 ∈ (Unit‘𝑅) → 𝑥 ∈ (𝐵 ∖ { 0 }))) |
44 | 43 | ssrdv 3574 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) →
(Unit‘𝑅) ⊆
(𝐵 ∖ { 0
})) |
45 | | eldifi 3694 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐵 ∖ { 0 }) → 𝑥 ∈ 𝐵) |
46 | 45 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝑥 ∈ 𝐵) |
47 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(invg‘𝐺) = (invg‘𝐺) |
48 | 19, 47 | grpinvcl 17290 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
((invg‘𝐺)‘𝑥) ∈ (𝐵 ∖ { 0 })) |
49 | 48 | adantll 746 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
((invg‘𝐺)‘𝑥) ∈ (𝐵 ∖ { 0 })) |
50 | 49 | eldifad 3552 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
((invg‘𝐺)‘𝑥) ∈ 𝐵) |
51 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(∥r‘𝑅) = (∥r‘𝑅) |
52 | 1, 51, 30 | dvdsrmul 18471 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑥) ∈ 𝐵) → 𝑥(∥r‘𝑅)(((invg‘𝐺)‘𝑥)(.r‘𝑅)𝑥)) |
53 | 46, 50, 52 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝑥(∥r‘𝑅)(((invg‘𝐺)‘𝑥)(.r‘𝑅)𝑥)) |
54 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑅)
∈ V |
55 | 1, 54 | eqeltri 2684 |
. . . . . . . . . . . . 13
⊢ 𝐵 ∈ V |
56 | | difexg 4735 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ V → (𝐵 ∖ { 0 }) ∈
V) |
57 | 16, 30 | mgpplusg 18316 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
58 | 7, 57 | ressplusg 15818 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∖ { 0 }) ∈ V →
(.r‘𝑅) =
(+g‘𝐺)) |
59 | 55, 56, 58 | mp2b 10 |
. . . . . . . . . . . 12
⊢
(.r‘𝑅) = (+g‘𝐺) |
60 | 19, 59, 20, 47 | grplinv 17291 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
(((invg‘𝐺)‘𝑥)(.r‘𝑅)𝑥) = (0g‘𝐺)) |
61 | 60 | adantll 746 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
(((invg‘𝐺)‘𝑥)(.r‘𝑅)𝑥) = (0g‘𝐺)) |
62 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(1r‘𝑅) = (1r‘𝑅) |
63 | 1, 62 | ringidcl 18391 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) |
64 | 1, 30, 62 | ringlidm 18394 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
∈ 𝐵) →
((1r‘𝑅)(.r‘𝑅)(1r‘𝑅)) = (1r‘𝑅)) |
65 | 63, 64 | mpdan 699 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring →
((1r‘𝑅)(.r‘𝑅)(1r‘𝑅)) = (1r‘𝑅)) |
66 | 65 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) →
((1r‘𝑅)(.r‘𝑅)(1r‘𝑅)) = (1r‘𝑅)) |
67 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) → 𝐺 ∈ Grp) |
68 | 2, 62 | 1unit 18481 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Unit‘𝑅)) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) →
(1r‘𝑅)
∈ (Unit‘𝑅)) |
70 | 44, 69 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) →
(1r‘𝑅)
∈ (𝐵 ∖ { 0
})) |
71 | 19, 59, 20 | grpid 17280 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧
(1r‘𝑅)
∈ (𝐵 ∖ { 0 })) →
(((1r‘𝑅)(.r‘𝑅)(1r‘𝑅)) = (1r‘𝑅) ↔ (0g‘𝐺) = (1r‘𝑅))) |
72 | 67, 70, 71 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) →
(((1r‘𝑅)(.r‘𝑅)(1r‘𝑅)) = (1r‘𝑅) ↔ (0g‘𝐺) = (1r‘𝑅))) |
73 | 66, 72 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) →
(0g‘𝐺) =
(1r‘𝑅)) |
74 | 73 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
(0g‘𝐺) =
(1r‘𝑅)) |
75 | 61, 74 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
(((invg‘𝐺)‘𝑥)(.r‘𝑅)𝑥) = (1r‘𝑅)) |
76 | 53, 75 | breqtrd 4609 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝑥(∥r‘𝑅)(1r‘𝑅)) |
77 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
78 | 77, 1 | opprbas 18452 |
. . . . . . . . . . 11
⊢ 𝐵 =
(Base‘(oppr‘𝑅)) |
79 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅)) |
80 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
81 | 78, 79, 80 | dvdsrmul 18471 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑥) ∈ 𝐵) → 𝑥(∥r‘(oppr‘𝑅))(((invg‘𝐺)‘𝑥)(.r‘(oppr‘𝑅))𝑥)) |
82 | 46, 50, 81 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝑥(∥r‘(oppr‘𝑅))(((invg‘𝐺)‘𝑥)(.r‘(oppr‘𝑅))𝑥)) |
83 | 1, 30, 77, 80 | opprmul 18449 |
. . . . . . . . . 10
⊢
(((invg‘𝐺)‘𝑥)(.r‘(oppr‘𝑅))𝑥) = (𝑥(.r‘𝑅)((invg‘𝐺)‘𝑥)) |
84 | 19, 59, 20, 47 | grprinv 17292 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)((invg‘𝐺)‘𝑥)) = (0g‘𝐺)) |
85 | 84 | adantll 746 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)((invg‘𝐺)‘𝑥)) = (0g‘𝐺)) |
86 | 85, 74 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)((invg‘𝐺)‘𝑥)) = (1r‘𝑅)) |
87 | 83, 86 | syl5eq 2656 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
(((invg‘𝐺)‘𝑥)(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) |
88 | 82, 87 | breqtrd 4609 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
89 | 2, 62, 51, 77, 79 | isunit 18480 |
. . . . . . . 8
⊢ (𝑥 ∈ (Unit‘𝑅) ↔ (𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
90 | 76, 88, 89 | sylanbrc 695 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝑥 ∈ (Unit‘𝑅)) |
91 | 90 | ex 449 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) → (𝑥 ∈ (𝐵 ∖ { 0 }) → 𝑥 ∈ (Unit‘𝑅))) |
92 | 91 | ssrdv 3574 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) → (𝐵 ∖ { 0 }) ⊆
(Unit‘𝑅)) |
93 | 44, 92 | eqssd 3585 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) →
(Unit‘𝑅) = (𝐵 ∖ { 0 })) |
94 | 12, 93 | impbida 873 |
. . 3
⊢ (𝑅 ∈ Ring →
((Unit‘𝑅) = (𝐵 ∖ { 0 }) ↔ 𝐺 ∈ Grp)) |
95 | 94 | pm5.32i 667 |
. 2
⊢ ((𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖ { 0 })) ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ Grp)) |
96 | 4, 95 | bitri 263 |
1
⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ Grp)) |