Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → 𝑅 ∈ DivRing) |
2 | | drngring 19998 |
. . 3
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
3 | | cntzsdrg.b |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
4 | | cntzsdrg.m |
. . . 4
⊢ 𝑀 = (mulGrp‘𝑅) |
5 | | cntzsdrg.z |
. . . 4
⊢ 𝑍 = (Cntz‘𝑀) |
6 | 3, 4, 5 | cntzsubr 20057 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubRing‘𝑅)) |
7 | 2, 6 | sylan 580 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubRing‘𝑅)) |
8 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑦 = (0g‘𝑅) →
(((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅))) |
9 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑦 = (0g‘𝑅) → (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥)) = ((0g‘𝑅)(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
10 | 8, 9 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑦 = (0g‘𝑅) →
((((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥)) ↔ (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(.r‘𝑅)((invr‘𝑅)‘𝑥)))) |
11 | | eldifsn 4720 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝑆 ∖ {(0g‘𝑅)}) ↔ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ (0g‘𝑅))) |
12 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
13 | 4 | oveq1i 7285 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ↾s
(Unit‘𝑅)) =
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) |
14 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(invr‘𝑅) = (invr‘𝑅) |
15 | 12, 13, 14 | invrfval 19915 |
. . . . . . . . . . . . 13
⊢
(invr‘𝑅) = (invg‘(𝑀 ↾s
(Unit‘𝑅))) |
16 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(0g‘𝑅) = (0g‘𝑅) |
17 | 3, 12, 16 | isdrng 19995 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖
{(0g‘𝑅)}))) |
18 | 17 | simprbi 497 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ DivRing →
(Unit‘𝑅) = (𝐵 ∖
{(0g‘𝑅)})) |
19 | 18 | oveq2d 7291 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ DivRing → (𝑀 ↾s
(Unit‘𝑅)) = (𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))) |
20 | 19 | fveq2d 6778 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ DivRing →
(invg‘(𝑀
↾s (Unit‘𝑅))) = (invg‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))) |
21 | 15, 20 | eqtrid 2790 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ DivRing →
(invr‘𝑅) =
(invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))) |
22 | 21 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
(invr‘𝑅) =
(invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))) |
23 | 22 | fveq1d 6776 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invr‘𝑅)‘𝑥) = ((invg‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))‘𝑥)) |
24 | 4 | oveq1i 7285 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))
= ((mulGrp‘𝑅)
↾s (𝐵
∖ {(0g‘𝑅)})) |
25 | 3, 16, 24 | drngmgp 20003 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ DivRing → (𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))
∈ Grp) |
26 | 25 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → (𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})) ∈
Grp) |
27 | | ssdif 4074 |
. . . . . . . . . . . . 13
⊢ (𝑆 ⊆ 𝐵 → (𝑆 ∖ {(0g‘𝑅)}) ⊆ (𝐵 ∖ {(0g‘𝑅)})) |
28 | 27 | ad2antlr 724 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → (𝑆 ∖ {(0g‘𝑅)}) ⊆ (𝐵 ∖ {(0g‘𝑅)})) |
29 | | difss 4066 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∖
{(0g‘𝑅)})
⊆ 𝐵 |
30 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))
= (𝑀 ↾s
(𝐵 ∖
{(0g‘𝑅)})) |
31 | 4, 3 | mgpbas 19726 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝑀) |
32 | 30, 31 | ressbas2 16949 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∖
{(0g‘𝑅)})
⊆ 𝐵 → (𝐵 ∖
{(0g‘𝑅)})
= (Base‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))) |
33 | 29, 32 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∖
{(0g‘𝑅)})
= (Base‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)}))) |
34 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(Cntz‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)}))) = (Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)}))) |
35 | 33, 34 | cntzsubg 18943 |
. . . . . . . . . . . 12
⊢ (((𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))
∈ Grp ∧ (𝑆 ∖
{(0g‘𝑅)})
⊆ (𝐵 ∖
{(0g‘𝑅)}))
→ ((Cntz‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) ∈ (SubGrp‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))) |
36 | 26, 28, 35 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → ((Cntz‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) ∈ (SubGrp‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))) |
37 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → 𝑆 ⊆ 𝐵) |
38 | | difss 4066 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∖
{(0g‘𝑅)})
⊆ 𝑆 |
39 | 31, 5 | cntz2ss 18939 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ⊆ 𝐵 ∧ (𝑆 ∖ {(0g‘𝑅)}) ⊆ 𝑆) → (𝑍‘𝑆) ⊆ (𝑍‘(𝑆 ∖ {(0g‘𝑅)}))) |
40 | 37, 38, 39 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ⊆ (𝑍‘(𝑆 ∖ {(0g‘𝑅)}))) |
41 | 40 | ssdifssd 4077 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) ⊆ (𝑍‘(𝑆 ∖ {(0g‘𝑅)}))) |
42 | 41 | sselda 3921 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ (𝑍‘(𝑆 ∖ {(0g‘𝑅)}))) |
43 | 31, 5 | cntzssv 18934 |
. . . . . . . . . . . . . . 15
⊢ (𝑍‘𝑆) ⊆ 𝐵 |
44 | | ssdif 4074 |
. . . . . . . . . . . . . . 15
⊢ ((𝑍‘𝑆) ⊆ 𝐵 → ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) ⊆ (𝐵 ∖ {(0g‘𝑅)})) |
45 | 43, 44 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) ⊆ (𝐵 ∖ {(0g‘𝑅)})) |
46 | 45 | sselda 3921 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ (𝐵 ∖ {(0g‘𝑅)})) |
47 | 42, 46 | elind 4128 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ ((𝑍‘(𝑆 ∖ {(0g‘𝑅)})) ∩ (𝐵 ∖ {(0g‘𝑅)}))) |
48 | 3 | fvexi 6788 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ∈ V |
49 | 48 | difexi 5252 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∖
{(0g‘𝑅)})
∈ V |
50 | 30, 5, 34 | resscntz 18938 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∖
{(0g‘𝑅)})
∈ V ∧ (𝑆 ∖
{(0g‘𝑅)})
⊆ (𝐵 ∖
{(0g‘𝑅)}))
→ ((Cntz‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) = ((𝑍‘(𝑆 ∖ {(0g‘𝑅)})) ∩ (𝐵 ∖ {(0g‘𝑅)}))) |
51 | 49, 28, 50 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → ((Cntz‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) = ((𝑍‘(𝑆 ∖ {(0g‘𝑅)})) ∩ (𝐵 ∖ {(0g‘𝑅)}))) |
52 | 47, 51 | eleqtrrd 2842 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) |
53 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(invg‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)}))) =
(invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)}))) |
54 | 53 | subginvcl 18764 |
. . . . . . . . . . 11
⊢
((((Cntz‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) ∈ (SubGrp‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))) ∧ 𝑥 ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) →
((invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘𝑥) ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) |
55 | 36, 52, 54 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘𝑥) ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) |
56 | 23, 55 | eqeltrd 2839 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invr‘𝑅)‘𝑥) ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) |
57 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(.r‘𝑅) = (.r‘𝑅) |
58 | 4, 57 | mgpplusg 19724 |
. . . . . . . . . . . 12
⊢
(.r‘𝑅) = (+g‘𝑀) |
59 | 30, 58 | ressplusg 17000 |
. . . . . . . . . . 11
⊢ ((𝐵 ∖
{(0g‘𝑅)})
∈ V → (.r‘𝑅) = (+g‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))) |
60 | 49, 59 | ax-mp 5 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (+g‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)}))) |
61 | 60, 34 | cntzi 18935 |
. . . . . . . . 9
⊢
((((invr‘𝑅)‘𝑥) ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ (𝑆 ∖ {(0g‘𝑅)})) →
(((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
62 | 56, 61 | sylan 580 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ (𝑆 ∖ {(0g‘𝑅)})) →
(((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
63 | 11, 62 | sylan2br 595 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ (0g‘𝑅))) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
64 | 63 | anassrs 468 |
. . . . . 6
⊢
(((((𝑅 ∈
DivRing ∧ 𝑆 ⊆
𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 ≠ (0g‘𝑅)) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
65 | 2 | ad3antrrr 727 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → 𝑅 ∈ Ring) |
66 | 1 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑅 ∈ DivRing) |
67 | | eldifi 4061 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) → 𝑥 ∈ (𝑍‘𝑆)) |
68 | 67 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ (𝑍‘𝑆)) |
69 | 43, 68 | sselid 3919 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ 𝐵) |
70 | | eldifsni 4723 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) → 𝑥 ≠ (0g‘𝑅)) |
71 | 70 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ≠ (0g‘𝑅)) |
72 | 3, 16, 14 | drnginvrcl 20008 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
73 | 66, 69, 71, 72 | syl3anc 1370 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invr‘𝑅)‘𝑥) ∈ 𝐵) |
74 | 73 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
75 | 3, 57, 16 | ringrz 19827 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
((invr‘𝑅)‘𝑥) ∈ 𝐵) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
76 | 65, 74, 75 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
77 | 3, 57, 16 | ringlz 19826 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
((invr‘𝑅)‘𝑥) ∈ 𝐵) → ((0g‘𝑅)(.r‘𝑅)((invr‘𝑅)‘𝑥)) = (0g‘𝑅)) |
78 | 65, 74, 77 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → ((0g‘𝑅)(.r‘𝑅)((invr‘𝑅)‘𝑥)) = (0g‘𝑅)) |
79 | 76, 78 | eqtr4d 2781 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
80 | 10, 64, 79 | pm2.61ne 3030 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
81 | 80 | ralrimiva 3103 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → ∀𝑦 ∈ 𝑆 (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
82 | | simplr 766 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑆 ⊆ 𝐵) |
83 | 31, 58, 5 | cntzel 18929 |
. . . . 5
⊢ ((𝑆 ⊆ 𝐵 ∧ ((invr‘𝑅)‘𝑥) ∈ 𝐵) → (((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆) ↔ ∀𝑦 ∈ 𝑆 (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥)))) |
84 | 82, 73, 83 | syl2anc 584 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
(((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆) ↔ ∀𝑦 ∈ 𝑆 (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥)))) |
85 | 81, 84 | mpbird 256 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆)) |
86 | 85 | ralrimiva 3103 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → ∀𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆)) |
87 | 14, 16 | issdrg2 20066 |
. 2
⊢ ((𝑍‘𝑆) ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ (𝑍‘𝑆) ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆))) |
88 | 1, 7, 86, 87 | syl3anbrc 1342 |
1
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubDRing‘𝑅)) |