Users' Mathboxes 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 32886
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 32885 . 2 class IDLsrg
2 vr . . 3 setvar π‘Ÿ
3 cvv 3473 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1539 . . . . 5 class π‘Ÿ
6 clidl 20929 . . . . 5 class LIdeal
75, 6cfv 6544 . . . 4 class (LIdealβ€˜π‘Ÿ)
8 cnx 17131 . . . . . . . 8 class ndx
9 cbs 17149 . . . . . . . 8 class Base
108, 9cfv 6544 . . . . . . 7 class (Baseβ€˜ndx)
114cv 1539 . . . . . . 7 class 𝑏
1210, 11cop 4635 . . . . . 6 class ⟨(Baseβ€˜ndx), π‘βŸ©
13 cplusg 17202 . . . . . . . 8 class +g
148, 13cfv 6544 . . . . . . 7 class (+gβ€˜ndx)
15 clsm 19544 . . . . . . . 8 class LSSum
165, 15cfv 6544 . . . . . . 7 class (LSSumβ€˜π‘Ÿ)
1714, 16cop 4635 . . . . . 6 class ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩
18 cmulr 17203 . . . . . . . 8 class .r
198, 18cfv 6544 . . . . . . 7 class (.rβ€˜ndx)
20 vi . . . . . . . 8 setvar 𝑖
21 vj . . . . . . . 8 setvar 𝑗
2220cv 1539 . . . . . . . . . 10 class 𝑖
2321cv 1539 . . . . . . . . . 10 class 𝑗
24 cmgp 20029 . . . . . . . . . . . 12 class mulGrp
255, 24cfv 6544 . . . . . . . . . . 11 class (mulGrpβ€˜π‘Ÿ)
2625, 15cfv 6544 . . . . . . . . . 10 class (LSSumβ€˜(mulGrpβ€˜π‘Ÿ))
2722, 23, 26co 7412 . . . . . . . . 9 class (𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)
28 crsp 20930 . . . . . . . . . 10 class RSpan
295, 28cfv 6544 . . . . . . . . 9 class (RSpanβ€˜π‘Ÿ)
3027, 29cfv 6544 . . . . . . . 8 class ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗))
3120, 21, 11, 11, 30cmpo 7414 . . . . . . 7 class (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))
3219, 31cop 4635 . . . . . 6 class ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩
3312, 17, 32ctp 4633 . . . . 5 class {⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩, ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩}
34 cts 17208 . . . . . . . 8 class TopSet
358, 34cfv 6544 . . . . . . 7 class (TopSetβ€˜ndx)
3622, 23wss 3949 . . . . . . . . . . 11 wff 𝑖 βŠ† 𝑗
3736wn 3 . . . . . . . . . 10 wff Β¬ 𝑖 βŠ† 𝑗
3837, 21, 11crab 3431 . . . . . . . . 9 class {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗}
3920, 11, 38cmpt 5232 . . . . . . . 8 class (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})
4039crn 5678 . . . . . . 7 class ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})
4135, 40cop 4635 . . . . . 6 class ⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩
42 cple 17209 . . . . . . . 8 class le
438, 42cfv 6544 . . . . . . 7 class (leβ€˜ndx)
4422, 23cpr 4631 . . . . . . . . . 10 class {𝑖, 𝑗}
4544, 11wss 3949 . . . . . . . . 9 wff {𝑖, 𝑗} βŠ† 𝑏
4645, 36wa 395 . . . . . . . 8 wff ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)
4746, 20, 21copab 5211 . . . . . . 7 class {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}
4843, 47cop 4635 . . . . . 6 class ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩
4941, 48cpr 4631 . . . . 5 class {⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩, ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩}
5033, 49cun 3947 . . . 4 class ({⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩, ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩} βˆͺ {⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩, ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩})
514, 7, 50csb 3894 . . 3 class ⦋(LIdealβ€˜π‘Ÿ) / π‘β¦Œ({⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩, ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩} βˆͺ {⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩, ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩})
522, 3, 51cmpt 5232 . 2 class (π‘Ÿ ∈ V ↦ ⦋(LIdealβ€˜π‘Ÿ) / π‘β¦Œ({⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩, ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩} βˆͺ {⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩, ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩}))
531, 52wceq 1540 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  32888
  Copyright terms: Public domain W3C validator