Step | Hyp | Ref
| Expression |
1 | | isdrngd.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
2 | | difss 3699 |
. . . . . 6
⊢ (𝐵 ∖ { 0 }) ⊆ 𝐵 |
3 | | isdrngd.b |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
4 | 2, 3 | syl5sseq 3616 |
. . . . 5
⊢ (𝜑 → (𝐵 ∖ { 0 }) ⊆
(Base‘𝑅)) |
5 | | eqid 2610 |
. . . . . 6
⊢
((mulGrp‘𝑅)
↾s (𝐵
∖ { 0 })) = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) |
6 | | eqid 2610 |
. . . . . . 7
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
7 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
8 | 6, 7 | mgpbas 18318 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
9 | 5, 8 | ressbas2 15758 |
. . . . 5
⊢ ((𝐵 ∖ { 0 }) ⊆
(Base‘𝑅) →
(𝐵 ∖ { 0 }) =
(Base‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })))) |
10 | 4, 9 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐵 ∖ { 0 }) =
(Base‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })))) |
11 | | isdrngd.t |
. . . . 5
⊢ (𝜑 → · =
(.r‘𝑅)) |
12 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝑅)
∈ V |
13 | 3, 12 | syl6eqel 2696 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ V) |
14 | | difexg 4735 |
. . . . . 6
⊢ (𝐵 ∈ V → (𝐵 ∖ { 0 }) ∈
V) |
15 | | eqid 2610 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
16 | 6, 15 | mgpplusg 18316 |
. . . . . . 7
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
17 | 5, 16 | ressplusg 15818 |
. . . . . 6
⊢ ((𝐵 ∖ { 0 }) ∈ V →
(.r‘𝑅) =
(+g‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })))) |
18 | 13, 14, 17 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (.r‘𝑅) =
(+g‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })))) |
19 | 11, 18 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → · =
(+g‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })))) |
20 | | eldifsn 4260 |
. . . . 5
⊢ (𝑥 ∈ (𝐵 ∖ { 0 }) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) |
21 | | eldifsn 4260 |
. . . . . 6
⊢ (𝑦 ∈ (𝐵 ∖ { 0 }) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) |
22 | 7, 15 | ringcl 18384 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅)) |
23 | 1, 22 | syl3an1 1351 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅)) |
24 | 23 | 3expib 1260 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅))) |
25 | 3 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝑅))) |
26 | 3 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝑅))) |
27 | 25, 26 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)))) |
28 | 11 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 · 𝑦) = (𝑥(.r‘𝑅)𝑦)) |
29 | 28, 3 | eleq12d 2682 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 · 𝑦) ∈ 𝐵 ↔ (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅))) |
30 | 24, 27, 29 | 3imtr4d 282 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵)) |
31 | 30 | 3impib 1254 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) |
32 | 31 | 3adant2r 1313 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) |
33 | 32 | 3adant3r 1315 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ∈ 𝐵) |
34 | | isdrngd.n |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 ) |
35 | | eldifsn 4260 |
. . . . . . 7
⊢ ((𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 }) ↔ ((𝑥 · 𝑦) ∈ 𝐵 ∧ (𝑥 · 𝑦) ≠ 0 )) |
36 | 33, 34, 35 | sylanbrc 695 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 })) |
37 | 21, 36 | syl3an3b 1356 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 })) |
38 | 20, 37 | syl3an2b 1355 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 })) |
39 | | eldifi 3694 |
. . . . . 6
⊢ (𝑥 ∈ (𝐵 ∖ { 0 }) → 𝑥 ∈ 𝐵) |
40 | | eldifi 3694 |
. . . . . 6
⊢ (𝑦 ∈ (𝐵 ∖ { 0 }) → 𝑦 ∈ 𝐵) |
41 | | eldifi 3694 |
. . . . . 6
⊢ (𝑧 ∈ (𝐵 ∖ { 0 }) → 𝑧 ∈ 𝐵) |
42 | 39, 40, 41 | 3anim123i 1240 |
. . . . 5
⊢ ((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 }) ∧ 𝑧 ∈ (𝐵 ∖ { 0 })) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) |
43 | 7, 15 | ringass 18387 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
44 | 43 | ex 449 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧)))) |
45 | 1, 44 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧)))) |
46 | 3 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ (Base‘𝑅))) |
47 | 25, 26, 46 | 3anbi123d 1391 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅)))) |
48 | | eqidd 2611 |
. . . . . . . . 9
⊢ (𝜑 → 𝑧 = 𝑧) |
49 | 11, 28, 48 | oveq123d 6570 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 · 𝑦) · 𝑧) = ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧)) |
50 | | eqidd 2611 |
. . . . . . . . 9
⊢ (𝜑 → 𝑥 = 𝑥) |
51 | 11 | oveqd 6566 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 · 𝑧) = (𝑦(.r‘𝑅)𝑧)) |
52 | 11, 50, 51 | oveq123d 6570 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 · (𝑦 · 𝑧)) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
53 | 49, 52 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝜑 → (((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)) ↔ ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧)))) |
54 | 45, 47, 53 | 3imtr4d 282 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))) |
55 | 54 | imp 444 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
56 | 42, 55 | sylan2 490 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 }) ∧ 𝑧 ∈ (𝐵 ∖ { 0 }))) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
57 | | eqid 2610 |
. . . . . . . 8
⊢
(1r‘𝑅) = (1r‘𝑅) |
58 | 7, 57 | ringidcl 18391 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
59 | 1, 58 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) |
60 | | isdrngd.u |
. . . . . 6
⊢ (𝜑 → 1 =
(1r‘𝑅)) |
61 | 59, 60, 3 | 3eltr4d 2703 |
. . . . 5
⊢ (𝜑 → 1 ∈ 𝐵) |
62 | | isdrngd.o |
. . . . 5
⊢ (𝜑 → 1 ≠ 0 ) |
63 | | eldifsn 4260 |
. . . . 5
⊢ ( 1 ∈ (𝐵 ∖ { 0 }) ↔ ( 1 ∈ 𝐵 ∧ 1 ≠ 0 )) |
64 | 61, 62, 63 | sylanbrc 695 |
. . . 4
⊢ (𝜑 → 1 ∈ (𝐵 ∖ { 0 })) |
65 | 7, 15, 57 | ringlidm 18394 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥) |
66 | 65 | ex 449 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → (𝑥 ∈ (Base‘𝑅) →
((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥)) |
67 | 1, 66 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) → ((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥)) |
68 | 11, 60, 50 | oveq123d 6570 |
. . . . . . . . 9
⊢ (𝜑 → ( 1 · 𝑥) = ((1r‘𝑅)(.r‘𝑅)𝑥)) |
69 | 68 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝜑 → (( 1 · 𝑥) = 𝑥 ↔ ((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥)) |
70 | 67, 25, 69 | 3imtr4d 282 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐵 → ( 1 · 𝑥) = 𝑥)) |
71 | 70 | imp 444 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥) |
72 | 71 | adantrr 749 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → ( 1 · 𝑥) = 𝑥) |
73 | 20, 72 | sylan2b 491 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → ( 1 · 𝑥) = 𝑥) |
74 | | isdrngd.i |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵) |
75 | | isdrngd.j |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ≠ 0 ) |
76 | | eldifsn 4260 |
. . . . . 6
⊢ (𝐼 ∈ (𝐵 ∖ { 0 }) ↔ (𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 )) |
77 | 74, 75, 76 | sylanbrc 695 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ (𝐵 ∖ { 0 })) |
78 | 20, 77 | sylan2b 491 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝐼 ∈ (𝐵 ∖ { 0 })) |
79 | | isdrngd.k |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝐼 · 𝑥) = 1 ) |
80 | 20, 79 | sylan2b 491 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → (𝐼 · 𝑥) = 1 ) |
81 | 10, 19, 38, 56, 64, 73, 78, 80 | isgrpd 17267 |
. . 3
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ∈
Grp) |
82 | | isdrngd.z |
. . . . . . . 8
⊢ (𝜑 → 0 =
(0g‘𝑅)) |
83 | 82 | sneqd 4137 |
. . . . . . 7
⊢ (𝜑 → { 0 } =
{(0g‘𝑅)}) |
84 | 3, 83 | difeq12d 3691 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∖ { 0 }) = ((Base‘𝑅) ∖
{(0g‘𝑅)})) |
85 | 84 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) = ((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))) |
86 | 85 | eleq1d 2672 |
. . . 4
⊢ (𝜑 → (((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ∈ Grp ↔
((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∈
Grp)) |
87 | 86 | anbi2d 736 |
. . 3
⊢ (𝜑 → ((𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ∈ Grp) ↔
(𝑅 ∈ Ring ∧
((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∈
Grp))) |
88 | 1, 81, 87 | mpbi2and 958 |
. 2
⊢ (𝜑 → (𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))
∈ Grp)) |
89 | | eqid 2610 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
90 | | eqid 2610 |
. . 3
⊢
((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) = ((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)})) |
91 | 7, 89, 90 | isdrng2 18580 |
. 2
⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧
((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∈
Grp)) |
92 | 88, 91 | sylibr 223 |
1
⊢ (𝜑 → 𝑅 ∈ DivRing) |