Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → 𝑅 ∈ DivRing) |
2 | | drngring 19621 |
. . 3
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
3 | | cntzsdrg.b |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
4 | | cntzsdrg.m |
. . . 4
⊢ 𝑀 = (mulGrp‘𝑅) |
5 | | cntzsdrg.z |
. . . 4
⊢ 𝑍 = (Cntz‘𝑀) |
6 | 3, 4, 5 | cntzsubr 19680 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubRing‘𝑅)) |
7 | 2, 6 | sylan 583 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubRing‘𝑅)) |
8 | | oveq2 7172 |
. . . . . . 7
⊢ (𝑦 = (0g‘𝑅) →
(((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅))) |
9 | | oveq1 7171 |
. . . . . . 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 4672 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝑆 ∖ {(0g‘𝑅)}) ↔ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ (0g‘𝑅))) |
12 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
13 | 4 | oveq1i 7174 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ↾s
(Unit‘𝑅)) =
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) |
14 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(invr‘𝑅) = (invr‘𝑅) |
15 | 12, 13, 14 | invrfval 19538 |
. . . . . . . . . . . . 13
⊢
(invr‘𝑅) = (invg‘(𝑀 ↾s
(Unit‘𝑅))) |
16 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(0g‘𝑅) = (0g‘𝑅) |
17 | 3, 12, 16 | isdrng 19618 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖
{(0g‘𝑅)}))) |
18 | 17 | simprbi 500 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ DivRing →
(Unit‘𝑅) = (𝐵 ∖
{(0g‘𝑅)})) |
19 | 18 | oveq2d 7180 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ DivRing → (𝑀 ↾s
(Unit‘𝑅)) = (𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))) |
20 | 19 | fveq2d 6672 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ DivRing →
(invg‘(𝑀
↾s (Unit‘𝑅))) = (invg‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))) |
21 | 15, 20 | syl5eq 2785 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ DivRing →
(invr‘𝑅) =
(invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))) |
22 | 21 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
(invr‘𝑅) =
(invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))) |
23 | 22 | fveq1d 6670 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invr‘𝑅)‘𝑥) = ((invg‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))‘𝑥)) |
24 | 4 | oveq1i 7174 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))
= ((mulGrp‘𝑅)
↾s (𝐵
∖ {(0g‘𝑅)})) |
25 | 3, 16, 24 | drngmgp 19626 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ DivRing → (𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))
∈ Grp) |
26 | 25 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → (𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})) ∈
Grp) |
27 | | ssdif 4028 |
. . . . . . . . . . . . 13
⊢ (𝑆 ⊆ 𝐵 → (𝑆 ∖ {(0g‘𝑅)}) ⊆ (𝐵 ∖ {(0g‘𝑅)})) |
28 | 27 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → (𝑆 ∖ {(0g‘𝑅)}) ⊆ (𝐵 ∖ {(0g‘𝑅)})) |
29 | | difss 4020 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∖
{(0g‘𝑅)})
⊆ 𝐵 |
30 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))
= (𝑀 ↾s
(𝐵 ∖
{(0g‘𝑅)})) |
31 | 4, 3 | mgpbas 19357 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝑀) |
32 | 30, 31 | ressbas2 16651 |
. . . . . . . . . . . . . 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 18578 |
. . . . . . . . . . . 12
⊢ (((𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))
∈ Grp ∧ (𝑆 ∖
{(0g‘𝑅)})
⊆ (𝐵 ∖
{(0g‘𝑅)}))
→ ((Cntz‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) ∈ (SubGrp‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))) |
36 | 26, 28, 35 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → ((Cntz‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) ∈ (SubGrp‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))) |
37 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → 𝑆 ⊆ 𝐵) |
38 | | difss 4020 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∖
{(0g‘𝑅)})
⊆ 𝑆 |
39 | 31, 5 | cntz2ss 18574 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ⊆ 𝐵 ∧ (𝑆 ∖ {(0g‘𝑅)}) ⊆ 𝑆) → (𝑍‘𝑆) ⊆ (𝑍‘(𝑆 ∖ {(0g‘𝑅)}))) |
40 | 37, 38, 39 | sylancl 589 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ⊆ (𝑍‘(𝑆 ∖ {(0g‘𝑅)}))) |
41 | 40 | ssdifssd 4031 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) ⊆ (𝑍‘(𝑆 ∖ {(0g‘𝑅)}))) |
42 | 41 | sselda 3875 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ (𝑍‘(𝑆 ∖ {(0g‘𝑅)}))) |
43 | 31, 5 | cntzssv 18569 |
. . . . . . . . . . . . . . 15
⊢ (𝑍‘𝑆) ⊆ 𝐵 |
44 | | ssdif 4028 |
. . . . . . . . . . . . . . 15
⊢ ((𝑍‘𝑆) ⊆ 𝐵 → ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) ⊆ (𝐵 ∖ {(0g‘𝑅)})) |
45 | 43, 44 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) ⊆ (𝐵 ∖ {(0g‘𝑅)})) |
46 | 45 | sselda 3875 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ (𝐵 ∖ {(0g‘𝑅)})) |
47 | 42, 46 | elind 4082 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ ((𝑍‘(𝑆 ∖ {(0g‘𝑅)})) ∩ (𝐵 ∖ {(0g‘𝑅)}))) |
48 | 3 | fvexi 6682 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ∈ V |
49 | 48 | difexi 5193 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∖
{(0g‘𝑅)})
∈ V |
50 | 30, 5, 34 | resscntz 18573 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∖
{(0g‘𝑅)})
∈ V ∧ (𝑆 ∖
{(0g‘𝑅)})
⊆ (𝐵 ∖
{(0g‘𝑅)}))
→ ((Cntz‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) = ((𝑍‘(𝑆 ∖ {(0g‘𝑅)})) ∩ (𝐵 ∖ {(0g‘𝑅)}))) |
51 | 49, 28, 50 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → ((Cntz‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) = ((𝑍‘(𝑆 ∖ {(0g‘𝑅)})) ∩ (𝐵 ∖ {(0g‘𝑅)}))) |
52 | 47, 51 | eleqtrrd 2836 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) |
53 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(invg‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)}))) =
(invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)}))) |
54 | 53 | subginvcl 18399 |
. . . . . . . . . . 11
⊢
((((Cntz‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) ∈ (SubGrp‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))) ∧ 𝑥 ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) →
((invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘𝑥) ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) |
55 | 36, 52, 54 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘𝑥) ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) |
56 | 23, 55 | eqeltrd 2833 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invr‘𝑅)‘𝑥) ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) |
57 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(.r‘𝑅) = (.r‘𝑅) |
58 | 4, 57 | mgpplusg 19355 |
. . . . . . . . . . . 12
⊢
(.r‘𝑅) = (+g‘𝑀) |
59 | 30, 58 | ressplusg 16708 |
. . . . . . . . . . 11
⊢ ((𝐵 ∖
{(0g‘𝑅)})
∈ V → (.r‘𝑅) = (+g‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))) |
60 | 49, 59 | ax-mp 5 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (+g‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)}))) |
61 | 60, 34 | cntzi 18570 |
. . . . . . . . 9
⊢
((((invr‘𝑅)‘𝑥) ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ (𝑆 ∖ {(0g‘𝑅)})) →
(((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
62 | 56, 61 | sylan 583 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ (𝑆 ∖ {(0g‘𝑅)})) →
(((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
63 | 11, 62 | sylan2br 598 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ (0g‘𝑅))) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
64 | 63 | anassrs 471 |
. . . . . 6
⊢
(((((𝑅 ∈
DivRing ∧ 𝑆 ⊆
𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 ≠ (0g‘𝑅)) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
65 | 2 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → 𝑅 ∈ Ring) |
66 | 1 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑅 ∈ DivRing) |
67 | | eldifi 4015 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) → 𝑥 ∈ (𝑍‘𝑆)) |
68 | 67 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ (𝑍‘𝑆)) |
69 | 43, 68 | sseldi 3873 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ 𝐵) |
70 | | eldifsni 4675 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) → 𝑥 ≠ (0g‘𝑅)) |
71 | 70 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ≠ (0g‘𝑅)) |
72 | 3, 16, 14 | drnginvrcl 19631 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
73 | 66, 69, 71, 72 | syl3anc 1372 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invr‘𝑅)‘𝑥) ∈ 𝐵) |
74 | 73 | adantr 484 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
75 | 3, 57, 16 | ringrz 19453 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
((invr‘𝑅)‘𝑥) ∈ 𝐵) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
76 | 65, 74, 75 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
77 | 3, 57, 16 | ringlz 19452 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
((invr‘𝑅)‘𝑥) ∈ 𝐵) → ((0g‘𝑅)(.r‘𝑅)((invr‘𝑅)‘𝑥)) = (0g‘𝑅)) |
78 | 65, 74, 77 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → ((0g‘𝑅)(.r‘𝑅)((invr‘𝑅)‘𝑥)) = (0g‘𝑅)) |
79 | 76, 78 | eqtr4d 2776 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
80 | 10, 64, 79 | pm2.61ne 3019 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
81 | 80 | ralrimiva 3096 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → ∀𝑦 ∈ 𝑆 (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
82 | | simplr 769 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑆 ⊆ 𝐵) |
83 | 31, 58, 5 | cntzel 18564 |
. . . . 5
⊢ ((𝑆 ⊆ 𝐵 ∧ ((invr‘𝑅)‘𝑥) ∈ 𝐵) → (((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆) ↔ ∀𝑦 ∈ 𝑆 (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥)))) |
84 | 82, 73, 83 | syl2anc 587 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
(((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆) ↔ ∀𝑦 ∈ 𝑆 (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥)))) |
85 | 81, 84 | mpbird 260 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆)) |
86 | 85 | ralrimiva 3096 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → ∀𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆)) |
87 | 14, 16 | issdrg2 19689 |
. 2
⊢ ((𝑍‘𝑆) ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ (𝑍‘𝑆) ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆))) |
88 | 1, 7, 86, 87 | syl3anbrc 1344 |
1
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubDRing‘𝑅)) |