Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → 𝑅 ∈ DivRing) |
2 | | drngring 18577 |
. . 3
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
3 | | cntzsdrg.b |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
4 | | cntzsdrg.m |
. . . 4
⊢ 𝑀 = (mulGrp‘𝑅) |
5 | | cntzsdrg.z |
. . . 4
⊢ 𝑍 = (Cntz‘𝑀) |
6 | 3, 4, 5 | cntzsubr 18635 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubRing‘𝑅)) |
7 | 2, 6 | sylan 487 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubRing‘𝑅)) |
8 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑦 = (0g‘𝑅) →
(((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅))) |
9 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑦 = (0g‘𝑅) → (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥)) = ((0g‘𝑅)(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
10 | 8, 9 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑦 = (0g‘𝑅) →
((((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥)) ↔ (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(.r‘𝑅)((invr‘𝑅)‘𝑥)))) |
11 | | eldifsn 4260 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝑆 ∖ {(0g‘𝑅)}) ↔ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ (0g‘𝑅))) |
12 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
13 | 4 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ↾s
(Unit‘𝑅)) =
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) |
14 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(invr‘𝑅) = (invr‘𝑅) |
15 | 12, 13, 14 | invrfval 18496 |
. . . . . . . . . . . . 13
⊢
(invr‘𝑅) = (invg‘(𝑀 ↾s
(Unit‘𝑅))) |
16 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(0g‘𝑅) = (0g‘𝑅) |
17 | 3, 12, 16 | isdrng 18574 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖
{(0g‘𝑅)}))) |
18 | 17 | simprbi 479 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ DivRing →
(Unit‘𝑅) = (𝐵 ∖
{(0g‘𝑅)})) |
19 | 18 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ DivRing → (𝑀 ↾s
(Unit‘𝑅)) = (𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))) |
20 | 19 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ DivRing →
(invg‘(𝑀
↾s (Unit‘𝑅))) = (invg‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))) |
21 | 15, 20 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ DivRing →
(invr‘𝑅) =
(invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))) |
22 | 21 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
(invr‘𝑅) =
(invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))) |
23 | 22 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invr‘𝑅)‘𝑥) = ((invg‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))‘𝑥)) |
24 | 4 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))
= ((mulGrp‘𝑅)
↾s (𝐵
∖ {(0g‘𝑅)})) |
25 | 3, 16, 24 | drngmgp 18582 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ DivRing → (𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))
∈ Grp) |
26 | 25 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → (𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})) ∈
Grp) |
27 | | ssdif 3707 |
. . . . . . . . . . . . 13
⊢ (𝑆 ⊆ 𝐵 → (𝑆 ∖ {(0g‘𝑅)}) ⊆ (𝐵 ∖ {(0g‘𝑅)})) |
28 | 27 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → (𝑆 ∖ {(0g‘𝑅)}) ⊆ (𝐵 ∖ {(0g‘𝑅)})) |
29 | | difss 3699 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∖
{(0g‘𝑅)})
⊆ 𝐵 |
30 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))
= (𝑀 ↾s
(𝐵 ∖
{(0g‘𝑅)})) |
31 | 4, 3 | mgpbas 18318 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝑀) |
32 | 30, 31 | ressbas2 15758 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∖
{(0g‘𝑅)})
⊆ 𝐵 → (𝐵 ∖
{(0g‘𝑅)})
= (Base‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))) |
33 | 29, 32 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∖
{(0g‘𝑅)})
= (Base‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)}))) |
34 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Cntz‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)}))) = (Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)}))) |
35 | 33, 34 | cntzsubg 17592 |
. . . . . . . . . . . 12
⊢ (((𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))
∈ Grp ∧ (𝑆 ∖
{(0g‘𝑅)})
⊆ (𝐵 ∖
{(0g‘𝑅)}))
→ ((Cntz‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) ∈ (SubGrp‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))) |
36 | 26, 28, 35 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → ((Cntz‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) ∈ (SubGrp‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))) |
37 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → 𝑆 ⊆ 𝐵) |
38 | | difss 3699 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∖
{(0g‘𝑅)})
⊆ 𝑆 |
39 | 31, 5 | cntz2ss 17588 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ⊆ 𝐵 ∧ (𝑆 ∖ {(0g‘𝑅)}) ⊆ 𝑆) → (𝑍‘𝑆) ⊆ (𝑍‘(𝑆 ∖ {(0g‘𝑅)}))) |
40 | 37, 38, 39 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ⊆ (𝑍‘(𝑆 ∖ {(0g‘𝑅)}))) |
41 | 40 | ssdifssd 3710 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) ⊆ (𝑍‘(𝑆 ∖ {(0g‘𝑅)}))) |
42 | 41 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ (𝑍‘(𝑆 ∖ {(0g‘𝑅)}))) |
43 | 31, 5 | cntzssv 17584 |
. . . . . . . . . . . . . . 15
⊢ (𝑍‘𝑆) ⊆ 𝐵 |
44 | | ssdif 3707 |
. . . . . . . . . . . . . . 15
⊢ ((𝑍‘𝑆) ⊆ 𝐵 → ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) ⊆ (𝐵 ∖ {(0g‘𝑅)})) |
45 | 43, 44 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) ⊆ (𝐵 ∖ {(0g‘𝑅)})) |
46 | 45 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ (𝐵 ∖ {(0g‘𝑅)})) |
47 | 42, 46 | elind 3760 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ ((𝑍‘(𝑆 ∖ {(0g‘𝑅)})) ∩ (𝐵 ∖ {(0g‘𝑅)}))) |
48 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑅)
∈ V |
49 | 3, 48 | eqeltri 2684 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ∈ V |
50 | | difexg 4735 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ V → (𝐵 ∖
{(0g‘𝑅)})
∈ V) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∖
{(0g‘𝑅)})
∈ V |
52 | 30, 5, 34 | resscntz 17587 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∖
{(0g‘𝑅)})
∈ V ∧ (𝑆 ∖
{(0g‘𝑅)})
⊆ (𝐵 ∖
{(0g‘𝑅)}))
→ ((Cntz‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) = ((𝑍‘(𝑆 ∖ {(0g‘𝑅)})) ∩ (𝐵 ∖ {(0g‘𝑅)}))) |
53 | 51, 28, 52 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → ((Cntz‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) = ((𝑍‘(𝑆 ∖ {(0g‘𝑅)})) ∩ (𝐵 ∖ {(0g‘𝑅)}))) |
54 | 47, 53 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) |
55 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(invg‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)}))) =
(invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)}))) |
56 | 55 | subginvcl 17426 |
. . . . . . . . . . 11
⊢
((((Cntz‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) ∈ (SubGrp‘(𝑀 ↾s (𝐵 ∖
{(0g‘𝑅)}))) ∧ 𝑥 ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) →
((invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘𝑥) ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) |
57 | 36, 54, 56 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invg‘(𝑀
↾s (𝐵
∖ {(0g‘𝑅)})))‘𝑥) ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) |
58 | 23, 57 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invr‘𝑅)‘𝑥) ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)}))) |
59 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(.r‘𝑅) = (.r‘𝑅) |
60 | 4, 59 | mgpplusg 18316 |
. . . . . . . . . . . 12
⊢
(.r‘𝑅) = (+g‘𝑀) |
61 | 30, 60 | ressplusg 15818 |
. . . . . . . . . . 11
⊢ ((𝐵 ∖
{(0g‘𝑅)})
∈ V → (.r‘𝑅) = (+g‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))) |
62 | 51, 61 | ax-mp 5 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (+g‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)}))) |
63 | 62, 34 | cntzi 17585 |
. . . . . . . . 9
⊢
((((invr‘𝑅)‘𝑥) ∈ ((Cntz‘(𝑀 ↾s (𝐵 ∖ {(0g‘𝑅)})))‘(𝑆 ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ (𝑆 ∖ {(0g‘𝑅)})) →
(((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
64 | 58, 63 | sylan 487 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ (𝑆 ∖ {(0g‘𝑅)})) →
(((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
65 | 11, 64 | sylan2br 492 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ (0g‘𝑅))) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
66 | 65 | anassrs 678 |
. . . . . 6
⊢
(((((𝑅 ∈
DivRing ∧ 𝑆 ⊆
𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 ≠ (0g‘𝑅)) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
67 | 2 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → 𝑅 ∈ Ring) |
68 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑅 ∈ DivRing) |
69 | | eldifi 3694 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) → 𝑥 ∈ (𝑍‘𝑆)) |
70 | 69 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ (𝑍‘𝑆)) |
71 | 43, 70 | sseldi 3566 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ∈ 𝐵) |
72 | | eldifsni 4261 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)}) → 𝑥 ≠ (0g‘𝑅)) |
73 | 72 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑥 ≠ (0g‘𝑅)) |
74 | 3, 16, 14 | drnginvrcl 18587 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
75 | 68, 71, 73, 74 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invr‘𝑅)‘𝑥) ∈ 𝐵) |
76 | 75 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
77 | 3, 59, 16 | ringrz 18411 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
((invr‘𝑅)‘𝑥) ∈ 𝐵) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
78 | 67, 76, 77 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
79 | 3, 59, 16 | ringlz 18410 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
((invr‘𝑅)‘𝑥) ∈ 𝐵) → ((0g‘𝑅)(.r‘𝑅)((invr‘𝑅)‘𝑥)) = (0g‘𝑅)) |
80 | 67, 76, 79 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → ((0g‘𝑅)(.r‘𝑅)((invr‘𝑅)‘𝑥)) = (0g‘𝑅)) |
81 | 78, 80 | eqtr4d 2647 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
82 | 10, 66, 81 | pm2.61ne 2867 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) ∧ 𝑦 ∈ 𝑆) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
83 | 82 | ralrimiva 2949 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → ∀𝑦 ∈ 𝑆 (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥))) |
84 | | simplr 788 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) → 𝑆 ⊆ 𝐵) |
85 | 31, 60, 5 | cntzel 17579 |
. . . . 5
⊢ ((𝑆 ⊆ 𝐵 ∧ ((invr‘𝑅)‘𝑥) ∈ 𝐵) → (((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆) ↔ ∀𝑦 ∈ 𝑆 (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥)))) |
86 | 84, 75, 85 | syl2anc 691 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
(((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆) ↔ ∀𝑦 ∈ 𝑆 (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)((invr‘𝑅)‘𝑥)))) |
87 | 83, 86 | mpbird 246 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})) →
((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆)) |
88 | 87 | ralrimiva 2949 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → ∀𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆)) |
89 | 14, 16 | issdrg2 36787 |
. 2
⊢ ((𝑍‘𝑆) ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ (𝑍‘𝑆) ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ ((𝑍‘𝑆) ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ (𝑍‘𝑆))) |
90 | 1, 7, 88, 89 | syl3anbrc 1239 |
1
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubDRing‘𝑅)) |