Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-idlsrg Structured version   Visualization version   GIF version

Definition df-idlsrg 31115
 Description: Define a structure for the ideals of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.)
Assertion
Ref Expression
df-idlsrg IDLsrg = (𝑟 ∈ V ↦ (LIdeal‘𝑟) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (LSSum‘𝑟)⟩, ⟨(.r‘ndx), (𝑖𝑏, 𝑗𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖𝑏 ↦ {𝑗𝑏 ∣ ¬ 𝑖𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏𝑖𝑗)}⟩}))
Distinct variable group:   𝑟,𝑏,𝑖,𝑗

Detailed syntax breakdown of Definition df-idlsrg
StepHypRef Expression
1 cidlsrg 31114 . 2 class IDLsrg
2 vr . . 3 setvar 𝑟
3 cvv 3442 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1537 . . . . 5 class 𝑟
6 clidl 19956 . . . . 5 class LIdeal
75, 6cfv 6332 . . . 4 class (LIdeal‘𝑟)
8 cnx 16492 . . . . . . . 8 class ndx
9 cbs 16495 . . . . . . . 8 class Base
108, 9cfv 6332 . . . . . . 7 class (Base‘ndx)
114cv 1537 . . . . . . 7 class 𝑏
1210, 11cop 4534 . . . . . 6 class ⟨(Base‘ndx), 𝑏
13 cplusg 16577 . . . . . . . 8 class +g
148, 13cfv 6332 . . . . . . 7 class (+g‘ndx)
15 clsm 18772 . . . . . . . 8 class LSSum
165, 15cfv 6332 . . . . . . 7 class (LSSum‘𝑟)
1714, 16cop 4534 . . . . . 6 class ⟨(+g‘ndx), (LSSum‘𝑟)⟩
18 cmulr 16578 . . . . . . . 8 class .r
198, 18cfv 6332 . . . . . . 7 class (.r‘ndx)
20 vi . . . . . . . 8 setvar 𝑖
21 vj . . . . . . . 8 setvar 𝑗
2220cv 1537 . . . . . . . . . 10 class 𝑖
2321cv 1537 . . . . . . . . . 10 class 𝑗
24 cmgp 19253 . . . . . . . . . . . 12 class mulGrp
255, 24cfv 6332 . . . . . . . . . . 11 class (mulGrp‘𝑟)
2625, 15cfv 6332 . . . . . . . . . 10 class (LSSum‘(mulGrp‘𝑟))
2722, 23, 26co 7145 . . . . . . . . 9 class (𝑖(LSSum‘(mulGrp‘𝑟))𝑗)
28 crsp 19957 . . . . . . . . . 10 class RSpan
295, 28cfv 6332 . . . . . . . . 9 class (RSpan‘𝑟)
3027, 29cfv 6332 . . . . . . . 8 class ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗))
3120, 21, 11, 11, 30cmpo 7147 . . . . . . 7 class (𝑖𝑏, 𝑗𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))
3219, 31cop 4534 . . . . . 6 class ⟨(.r‘ndx), (𝑖𝑏, 𝑗𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩
3312, 17, 32ctp 4532 . . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (LSSum‘𝑟)⟩, ⟨(.r‘ndx), (𝑖𝑏, 𝑗𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩}
34 cts 16583 . . . . . . . 8 class TopSet
358, 34cfv 6332 . . . . . . 7 class (TopSet‘ndx)
3622, 23wss 3883 . . . . . . . . . . 11 wff 𝑖𝑗
3736wn 3 . . . . . . . . . 10 wff ¬ 𝑖𝑗
3837, 21, 11crab 3110 . . . . . . . . 9 class {𝑗𝑏 ∣ ¬ 𝑖𝑗}
3920, 11, 38cmpt 5114 . . . . . . . 8 class (𝑖𝑏 ↦ {𝑗𝑏 ∣ ¬ 𝑖𝑗})
4039crn 5524 . . . . . . 7 class ran (𝑖𝑏 ↦ {𝑗𝑏 ∣ ¬ 𝑖𝑗})
4135, 40cop 4534 . . . . . 6 class ⟨(TopSet‘ndx), ran (𝑖𝑏 ↦ {𝑗𝑏 ∣ ¬ 𝑖𝑗})⟩
42 cple 16584 . . . . . . . 8 class le
438, 42cfv 6332 . . . . . . 7 class (le‘ndx)
4422, 23cpr 4530 . . . . . . . . . 10 class {𝑖, 𝑗}
4544, 11wss 3883 . . . . . . . . 9 wff {𝑖, 𝑗} ⊆ 𝑏
4645, 36wa 399 . . . . . . . 8 wff ({𝑖, 𝑗} ⊆ 𝑏𝑖𝑗)
4746, 20, 21copab 5096 . . . . . . 7 class {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏𝑖𝑗)}
4843, 47cop 4534 . . . . . 6 class ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏𝑖𝑗)}⟩
4941, 48cpr 4530 . . . . 5 class {⟨(TopSet‘ndx), ran (𝑖𝑏 ↦ {𝑗𝑏 ∣ ¬ 𝑖𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏𝑖𝑗)}⟩}
5033, 49cun 3881 . . . 4 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (LSSum‘𝑟)⟩, ⟨(.r‘ndx), (𝑖𝑏, 𝑗𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖𝑏 ↦ {𝑗𝑏 ∣ ¬ 𝑖𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏𝑖𝑗)}⟩})
514, 7, 50csb 3830 . . 3 class (LIdeal‘𝑟) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (LSSum‘𝑟)⟩, ⟨(.r‘ndx), (𝑖𝑏, 𝑗𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖𝑏 ↦ {𝑗𝑏 ∣ ¬ 𝑖𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏𝑖𝑗)}⟩})
522, 3, 51cmpt 5114 . 2 class (𝑟 ∈ V ↦ (LIdeal‘𝑟) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (LSSum‘𝑟)⟩, ⟨(.r‘ndx), (𝑖𝑏, 𝑗𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖𝑏 ↦ {𝑗𝑏 ∣ ¬ 𝑖𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏𝑖𝑗)}⟩}))
531, 52wceq 1538 1 wff IDLsrg = (𝑟 ∈ V ↦ (LIdeal‘𝑟) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (LSSum‘𝑟)⟩, ⟨(.r‘ndx), (𝑖𝑏, 𝑗𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖𝑏 ↦ {𝑗𝑏 ∣ ¬ 𝑖𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏𝑖𝑗)}⟩}))
 Colors of variables: wff setvar class This definition is referenced by:  idlsrgval  31117
 Copyright terms: Public domain W3C validator