Proof of Theorem subdrgint
| Step | Hyp | Ref
| Expression |
| 1 | | subdrgint.3 |
. . . 4
⊢ (𝜑 → 𝑆 ⊆ (SubRing‘𝑅)) |
| 2 | | subdrgint.4 |
. . . 4
⊢ (𝜑 → 𝑆 ≠ ∅) |
| 3 | | subrgint 20595 |
. . . 4
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆
∈ (SubRing‘𝑅)) |
| 4 | 1, 2, 3 | syl2anc 584 |
. . 3
⊢ (𝜑 → ∩ 𝑆
∈ (SubRing‘𝑅)) |
| 5 | | subdrgint.1 |
. . . 4
⊢ 𝐿 = (𝑅 ↾s ∩ 𝑆) |
| 6 | 5 | subrgring 20574 |
. . 3
⊢ (∩ 𝑆
∈ (SubRing‘𝑅)
→ 𝐿 ∈
Ring) |
| 7 | 4, 6 | syl 17 |
. 2
⊢ (𝜑 → 𝐿 ∈ Ring) |
| 8 | 5 | fveq2i 6909 |
. . . 4
⊢
(mulGrp‘𝐿) =
(mulGrp‘(𝑅
↾s ∩ 𝑆)) |
| 9 | 8 | oveq1i 7441 |
. . 3
⊢
((mulGrp‘𝐿)
↾s ((Base‘𝐿) ∖ {(0g‘𝐿)})) = ((mulGrp‘(𝑅 ↾s ∩ 𝑆))
↾s ((Base‘𝐿) ∖ {(0g‘𝐿)})) |
| 10 | | subdrgint.2 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ DivRing) |
| 11 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑅 ↾s ∩ 𝑆) =
(𝑅 ↾s
∩ 𝑆) |
| 12 | | eqid 2737 |
. . . . . . . 8
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 13 | 11, 12 | mgpress 20147 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ ∩ 𝑆
∈ (SubRing‘𝑅))
→ ((mulGrp‘𝑅)
↾s ∩ 𝑆) = (mulGrp‘(𝑅 ↾s ∩ 𝑆))) |
| 14 | 10, 4, 13 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s ∩ 𝑆) =
(mulGrp‘(𝑅
↾s ∩ 𝑆))) |
| 15 | 14 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → (((mulGrp‘𝑅) ↾s ∩ 𝑆)
↾s ((Base‘𝐿) ∖ {(0g‘𝐿)})) = ((mulGrp‘(𝑅 ↾s ∩ 𝑆))
↾s ((Base‘𝐿) ∖ {(0g‘𝐿)}))) |
| 16 | | difssd 4137 |
. . . . . . 7
⊢ (𝜑 → ((Base‘𝐿) ∖
{(0g‘𝐿)})
⊆ (Base‘𝐿)) |
| 17 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 18 | 17 | subrgss 20572 |
. . . . . . . 8
⊢ (∩ 𝑆
∈ (SubRing‘𝑅)
→ ∩ 𝑆 ⊆ (Base‘𝑅)) |
| 19 | 5, 17 | ressbas2 17283 |
. . . . . . . 8
⊢ (∩ 𝑆
⊆ (Base‘𝑅)
→ ∩ 𝑆 = (Base‘𝐿)) |
| 20 | 4, 18, 19 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ∩ 𝑆 =
(Base‘𝐿)) |
| 21 | 16, 20 | sseqtrrd 4021 |
. . . . . 6
⊢ (𝜑 → ((Base‘𝐿) ∖
{(0g‘𝐿)})
⊆ ∩ 𝑆) |
| 22 | | ressabs 17294 |
. . . . . 6
⊢ ((∩ 𝑆
∈ (SubRing‘𝑅)
∧ ((Base‘𝐿)
∖ {(0g‘𝐿)}) ⊆ ∩
𝑆) →
(((mulGrp‘𝑅)
↾s ∩ 𝑆) ↾s ((Base‘𝐿) ∖
{(0g‘𝐿)}))
= ((mulGrp‘𝑅)
↾s ((Base‘𝐿) ∖ {(0g‘𝐿)}))) |
| 23 | 4, 21, 22 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (((mulGrp‘𝑅) ↾s ∩ 𝑆)
↾s ((Base‘𝐿) ∖ {(0g‘𝐿)})) = ((mulGrp‘𝑅) ↾s
((Base‘𝐿) ∖
{(0g‘𝐿)}))) |
| 24 | 15, 23 | eqtr3d 2779 |
. . . 4
⊢ (𝜑 → ((mulGrp‘(𝑅 ↾s ∩ 𝑆))
↾s ((Base‘𝐿) ∖ {(0g‘𝐿)})) = ((mulGrp‘𝑅) ↾s
((Base‘𝐿) ∖
{(0g‘𝐿)}))) |
| 25 | | intiin 5059 |
. . . . . . . 8
⊢ ∩ 𝑆 =
∩ 𝑠 ∈ 𝑆 𝑠 |
| 26 | 20, 25 | eqtr3di 2792 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝐿) = ∩ 𝑠 ∈ 𝑆 𝑠) |
| 27 | 26 | difeq1d 4125 |
. . . . . 6
⊢ (𝜑 → ((Base‘𝐿) ∖
{(0g‘𝐿)})
= (∩ 𝑠 ∈ 𝑆 𝑠 ∖ {(0g‘𝐿)})) |
| 28 | 27 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s
((Base‘𝐿) ∖
{(0g‘𝐿)}))
= ((mulGrp‘𝑅)
↾s (∩ 𝑠 ∈ 𝑆 𝑠 ∖ {(0g‘𝐿)}))) |
| 29 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑠 ∈ V |
| 30 | 29 | difexi 5330 |
. . . . . . . . 9
⊢ (𝑠 ∖
{(0g‘𝐿)})
∈ V |
| 31 | 30 | dfiin3 5981 |
. . . . . . . 8
⊢ ∩ 𝑠 ∈ 𝑆 (𝑠 ∖ {(0g‘𝐿)}) = ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) |
| 32 | | iindif1 5075 |
. . . . . . . . 9
⊢ (𝑆 ≠ ∅ → ∩ 𝑠 ∈ 𝑆 (𝑠 ∖ {(0g‘𝐿)}) = (∩ 𝑠 ∈ 𝑆 𝑠 ∖ {(0g‘𝐿)})) |
| 33 | 2, 32 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ∩ 𝑠 ∈ 𝑆 (𝑠 ∖ {(0g‘𝐿)}) = (∩ 𝑠 ∈ 𝑆 𝑠 ∖ {(0g‘𝐿)})) |
| 34 | 31, 33 | eqtr3id 2791 |
. . . . . . 7
⊢ (𝜑 → ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) = (∩ 𝑠 ∈ 𝑆 𝑠 ∖ {(0g‘𝐿)})) |
| 35 | 34 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)}))) = ((mulGrp‘𝑅) ↾s (∩ 𝑠 ∈ 𝑆 𝑠 ∖ {(0g‘𝐿)}))) |
| 36 | | difss 4136 |
. . . . . . . . . 10
⊢
((Base‘𝑅)
∖ {(0g‘𝑅)}) ⊆ (Base‘𝑅) |
| 37 | | eqid 2737 |
. . . . . . . . . . 11
⊢
((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) = ((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)})) |
| 38 | 12, 17 | mgpbas 20142 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
| 39 | 37, 38 | ressbas2 17283 |
. . . . . . . . . 10
⊢
(((Base‘𝑅)
∖ {(0g‘𝑅)}) ⊆ (Base‘𝑅) → ((Base‘𝑅) ∖ {(0g‘𝑅)}) =
(Base‘((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)})))) |
| 40 | 36, 39 | ax-mp 5 |
. . . . . . . . 9
⊢
((Base‘𝑅)
∖ {(0g‘𝑅)}) = (Base‘((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))) |
| 41 | 40 | fvexi 6920 |
. . . . . . . 8
⊢
((Base‘𝑅)
∖ {(0g‘𝑅)}) ∈ V |
| 42 | | iinssiun 5005 |
. . . . . . . . . . 11
⊢ (𝑆 ≠ ∅ → ∩ 𝑠 ∈ 𝑆 (𝑠 ∖ {(0g‘𝐿)}) ⊆ ∪ 𝑠 ∈ 𝑆 (𝑠 ∖ {(0g‘𝐿)})) |
| 43 | 2, 42 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ∩ 𝑠 ∈ 𝑆 (𝑠 ∖ {(0g‘𝐿)}) ⊆ ∪ 𝑠 ∈ 𝑆 (𝑠 ∖ {(0g‘𝐿)})) |
| 44 | | subrgsubg 20577 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ (SubRing‘𝑅) → 𝑠 ∈ (SubGrp‘𝑅)) |
| 45 | 44 | ssriv 3987 |
. . . . . . . . . . . . . . . . . 18
⊢
(SubRing‘𝑅)
⊆ (SubGrp‘𝑅) |
| 46 | 1, 45 | sstrdi 3996 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑆 ⊆ (SubGrp‘𝑅)) |
| 47 | | subgint 19168 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ⊆ (SubGrp‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆
∈ (SubGrp‘𝑅)) |
| 48 | 46, 2, 47 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∩ 𝑆
∈ (SubGrp‘𝑅)) |
| 49 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 50 | 5, 49 | subg0 19150 |
. . . . . . . . . . . . . . . 16
⊢ (∩ 𝑆
∈ (SubGrp‘𝑅)
→ (0g‘𝑅) = (0g‘𝐿)) |
| 51 | 48, 50 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0g‘𝑅) = (0g‘𝐿)) |
| 52 | 51 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (0g‘𝑅) = (0g‘𝐿)) |
| 53 | 52 | sneqd 4638 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → {(0g‘𝑅)} = {(0g‘𝐿)}) |
| 54 | 53 | difeq2d 4126 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑠 ∖ {(0g‘𝑅)}) = (𝑠 ∖ {(0g‘𝐿)})) |
| 55 | 1 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ (SubRing‘𝑅)) |
| 56 | 17 | subrgss 20572 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ (SubRing‘𝑅) → 𝑠 ⊆ (Base‘𝑅)) |
| 57 | 55, 56 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ⊆ (Base‘𝑅)) |
| 58 | 57 | ssdifd 4145 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑠 ∖ {(0g‘𝑅)}) ⊆ ((Base‘𝑅) ∖
{(0g‘𝑅)})) |
| 59 | 54, 58 | eqsstrrd 4019 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑠 ∖ {(0g‘𝐿)}) ⊆ ((Base‘𝑅) ∖
{(0g‘𝑅)})) |
| 60 | 59 | iunssd 5050 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑠 ∈ 𝑆 (𝑠 ∖ {(0g‘𝐿)}) ⊆ ((Base‘𝑅) ∖
{(0g‘𝑅)})) |
| 61 | 43, 60 | sstrd 3994 |
. . . . . . . . 9
⊢ (𝜑 → ∩ 𝑠 ∈ 𝑆 (𝑠 ∖ {(0g‘𝐿)}) ⊆ ((Base‘𝑅) ∖
{(0g‘𝑅)})) |
| 62 | 31, 61 | eqsstrrid 4023 |
. . . . . . . 8
⊢ (𝜑 → ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) ⊆ ((Base‘𝑅) ∖
{(0g‘𝑅)})) |
| 63 | | ressabs 17294 |
. . . . . . . 8
⊢
((((Base‘𝑅)
∖ {(0g‘𝑅)}) ∈ V ∧ ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) ⊆ ((Base‘𝑅) ∖
{(0g‘𝑅)}))
→ (((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) ↾s ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)}))) = ((mulGrp‘𝑅) ↾s ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})))) |
| 64 | 41, 62, 63 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))
↾s ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)}))) = ((mulGrp‘𝑅) ↾s ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})))) |
| 65 | 17, 49, 37 | drngmgp 20745 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ DivRing →
((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∈
Grp) |
| 66 | 10, 65 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))
∈ Grp) |
| 67 | 66 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → ((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)}))
∈ Grp) |
| 68 | 59, 40 | sseqtrdi 4024 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑠 ∖ {(0g‘𝐿)}) ⊆
(Base‘((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)})))) |
| 69 | | ressabs 17294 |
. . . . . . . . . . . . . 14
⊢
((((Base‘𝑅)
∖ {(0g‘𝑅)}) ∈ V ∧ (𝑠 ∖ {(0g‘𝐿)}) ⊆ ((Base‘𝑅) ∖
{(0g‘𝑅)}))
→ (((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) ↾s (𝑠 ∖
{(0g‘𝐿)}))
= ((mulGrp‘𝑅)
↾s (𝑠
∖ {(0g‘𝐿)}))) |
| 70 | 41, 59, 69 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)}))
↾s (𝑠
∖ {(0g‘𝐿)})) = ((mulGrp‘𝑅) ↾s (𝑠 ∖ {(0g‘𝐿)}))) |
| 71 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ↾s 𝑠) = (𝑅 ↾s 𝑠) |
| 72 | 71, 12 | mgpress 20147 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ DivRing ∧ 𝑠 ∈ 𝑆) → ((mulGrp‘𝑅) ↾s 𝑠) = (mulGrp‘(𝑅 ↾s 𝑠))) |
| 73 | 10, 72 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → ((mulGrp‘𝑅) ↾s 𝑠) = (mulGrp‘(𝑅 ↾s 𝑠))) |
| 74 | 54 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑠 ∖ {(0g‘𝐿)}) = (𝑠 ∖ {(0g‘𝑅)})) |
| 75 | 73, 74 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (((mulGrp‘𝑅) ↾s 𝑠) ↾s (𝑠 ∖ {(0g‘𝐿)})) = ((mulGrp‘(𝑅 ↾s 𝑠)) ↾s (𝑠 ∖
{(0g‘𝑅)}))) |
| 76 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆) |
| 77 | | difssd 4137 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑠 ∖ {(0g‘𝐿)}) ⊆ 𝑠) |
| 78 | | ressabs 17294 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠 ∈ 𝑆 ∧ (𝑠 ∖ {(0g‘𝐿)}) ⊆ 𝑠) → (((mulGrp‘𝑅) ↾s 𝑠) ↾s (𝑠 ∖ {(0g‘𝐿)})) = ((mulGrp‘𝑅) ↾s (𝑠 ∖
{(0g‘𝐿)}))) |
| 79 | 76, 77, 78 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (((mulGrp‘𝑅) ↾s 𝑠) ↾s (𝑠 ∖ {(0g‘𝐿)})) = ((mulGrp‘𝑅) ↾s (𝑠 ∖
{(0g‘𝐿)}))) |
| 80 | 75, 79 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → ((mulGrp‘(𝑅 ↾s 𝑠)) ↾s (𝑠 ∖ {(0g‘𝑅)})) = ((mulGrp‘𝑅) ↾s (𝑠 ∖
{(0g‘𝐿)}))) |
| 81 | 71, 17 | ressbas2 17283 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ⊆ (Base‘𝑅) → 𝑠 = (Base‘(𝑅 ↾s 𝑠))) |
| 82 | 55, 56, 81 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 = (Base‘(𝑅 ↾s 𝑠))) |
| 83 | 71, 49 | subrg0 20579 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ (SubRing‘𝑅) →
(0g‘𝑅) =
(0g‘(𝑅
↾s 𝑠))) |
| 84 | 55, 83 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑠))) |
| 85 | 84 | sneqd 4638 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → {(0g‘𝑅)} =
{(0g‘(𝑅
↾s 𝑠))}) |
| 86 | 82, 85 | difeq12d 4127 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑠 ∖ {(0g‘𝑅)}) = ((Base‘(𝑅 ↾s 𝑠)) ∖
{(0g‘(𝑅
↾s 𝑠))})) |
| 87 | 86 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → ((mulGrp‘(𝑅 ↾s 𝑠)) ↾s (𝑠 ∖ {(0g‘𝑅)})) = ((mulGrp‘(𝑅 ↾s 𝑠)) ↾s
((Base‘(𝑅
↾s 𝑠))
∖ {(0g‘(𝑅 ↾s 𝑠))}))) |
| 88 | | subdrgint.5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑅 ↾s 𝑠) ∈ DivRing) |
| 89 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(𝑅
↾s 𝑠)) =
(Base‘(𝑅
↾s 𝑠)) |
| 90 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(0g‘(𝑅 ↾s 𝑠)) = (0g‘(𝑅 ↾s 𝑠)) |
| 91 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
((mulGrp‘(𝑅
↾s 𝑠))
↾s ((Base‘(𝑅 ↾s 𝑠)) ∖ {(0g‘(𝑅 ↾s 𝑠))})) = ((mulGrp‘(𝑅 ↾s 𝑠)) ↾s
((Base‘(𝑅
↾s 𝑠))
∖ {(0g‘(𝑅 ↾s 𝑠))})) |
| 92 | 89, 90, 91 | drngmgp 20745 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ↾s 𝑠) ∈ DivRing →
((mulGrp‘(𝑅
↾s 𝑠))
↾s ((Base‘(𝑅 ↾s 𝑠)) ∖ {(0g‘(𝑅 ↾s 𝑠))})) ∈
Grp) |
| 93 | 88, 92 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → ((mulGrp‘(𝑅 ↾s 𝑠)) ↾s ((Base‘(𝑅 ↾s 𝑠)) ∖
{(0g‘(𝑅
↾s 𝑠))}))
∈ Grp) |
| 94 | 87, 93 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → ((mulGrp‘(𝑅 ↾s 𝑠)) ↾s (𝑠 ∖ {(0g‘𝑅)})) ∈
Grp) |
| 95 | 80, 94 | eqeltrrd 2842 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → ((mulGrp‘𝑅) ↾s (𝑠 ∖ {(0g‘𝐿)})) ∈
Grp) |
| 96 | 70, 95 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)}))
↾s (𝑠
∖ {(0g‘𝐿)})) ∈ Grp) |
| 97 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)}))) = (Base‘((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))) |
| 98 | 97 | issubg 19144 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∖
{(0g‘𝐿)})
∈ (SubGrp‘((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)}))) ↔ (((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))
∈ Grp ∧ (𝑠 ∖
{(0g‘𝐿)})
⊆ (Base‘((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)}))) ∧ (((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))
↾s (𝑠
∖ {(0g‘𝐿)})) ∈ Grp)) |
| 99 | 67, 68, 96, 98 | syl3anbrc 1344 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑠 ∖ {(0g‘𝐿)}) ∈
(SubGrp‘((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)})))) |
| 100 | 99 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑠 ∈ 𝑆 (𝑠 ∖ {(0g‘𝐿)}) ∈
(SubGrp‘((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)})))) |
| 101 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) = (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) |
| 102 | 101 | rnmptss 7143 |
. . . . . . . . . 10
⊢
(∀𝑠 ∈
𝑆 (𝑠 ∖ {(0g‘𝐿)}) ∈
(SubGrp‘((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)}))) → ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) ⊆
(SubGrp‘((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)})))) |
| 103 | 100, 102 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) ⊆
(SubGrp‘((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)})))) |
| 104 | | dmmptg 6262 |
. . . . . . . . . . . . 13
⊢
(∀𝑠 ∈
𝑆 (𝑠 ∖ {(0g‘𝐿)}) ∈ V → dom (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) = 𝑆) |
| 105 | | difexg 5329 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ 𝑆 → (𝑠 ∖ {(0g‘𝐿)}) ∈ V) |
| 106 | 104, 105 | mprg 3067 |
. . . . . . . . . . . 12
⊢ dom
(𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) = 𝑆 |
| 107 | 106 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) = 𝑆) |
| 108 | 107, 2 | eqnetrd 3008 |
. . . . . . . . . 10
⊢ (𝜑 → dom (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) ≠
∅) |
| 109 | | dm0rn0 5935 |
. . . . . . . . . . 11
⊢ (dom
(𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) = ∅ ↔ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) = ∅) |
| 110 | 109 | necon3bii 2993 |
. . . . . . . . . 10
⊢ (dom
(𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) ≠ ∅ ↔ ran
(𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) ≠
∅) |
| 111 | 108, 110 | sylib 218 |
. . . . . . . . 9
⊢ (𝜑 → ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) ≠
∅) |
| 112 | | subgint 19168 |
. . . . . . . . 9
⊢ ((ran
(𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) ⊆
(SubGrp‘((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)}))) ∧ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) ≠ ∅) → ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) ∈
(SubGrp‘((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)})))) |
| 113 | 103, 111,
112 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) ∈
(SubGrp‘((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)})))) |
| 114 | | eqid 2737 |
. . . . . . . . 9
⊢
(((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) ↾s ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)}))) = (((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))
↾s ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)}))) |
| 115 | 114 | subggrp 19147 |
. . . . . . . 8
⊢ (∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)})) ∈
(SubGrp‘((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖
{(0g‘𝑅)}))) → (((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))
↾s ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)}))) ∈
Grp) |
| 116 | 113, 115 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))
↾s ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)}))) ∈
Grp) |
| 117 | 64, 116 | eqeltrrd 2842 |
. . . . . 6
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s ∩ ran (𝑠 ∈ 𝑆 ↦ (𝑠 ∖ {(0g‘𝐿)}))) ∈
Grp) |
| 118 | 35, 117 | eqeltrrd 2842 |
. . . . 5
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s (∩ 𝑠 ∈ 𝑆 𝑠 ∖ {(0g‘𝐿)})) ∈
Grp) |
| 119 | 28, 118 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s
((Base‘𝐿) ∖
{(0g‘𝐿)}))
∈ Grp) |
| 120 | 24, 119 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → ((mulGrp‘(𝑅 ↾s ∩ 𝑆))
↾s ((Base‘𝐿) ∖ {(0g‘𝐿)})) ∈
Grp) |
| 121 | 9, 120 | eqeltrid 2845 |
. 2
⊢ (𝜑 → ((mulGrp‘𝐿) ↾s
((Base‘𝐿) ∖
{(0g‘𝐿)}))
∈ Grp) |
| 122 | | eqid 2737 |
. . 3
⊢
(Base‘𝐿) =
(Base‘𝐿) |
| 123 | | eqid 2737 |
. . 3
⊢
(0g‘𝐿) = (0g‘𝐿) |
| 124 | | eqid 2737 |
. . 3
⊢
((mulGrp‘𝐿)
↾s ((Base‘𝐿) ∖ {(0g‘𝐿)})) = ((mulGrp‘𝐿) ↾s
((Base‘𝐿) ∖
{(0g‘𝐿)})) |
| 125 | 122, 123,
124 | isdrng2 20743 |
. 2
⊢ (𝐿 ∈ DivRing ↔ (𝐿 ∈ Ring ∧
((mulGrp‘𝐿)
↾s ((Base‘𝐿) ∖ {(0g‘𝐿)})) ∈
Grp)) |
| 126 | 7, 121, 125 | sylanbrc 583 |
1
⊢ (𝜑 → 𝐿 ∈ DivRing) |