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 32298
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 32297 . 2 class IDLsrg
2 vr . . 3 setvar π‘Ÿ
3 cvv 3447 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1541 . . . . 5 class π‘Ÿ
6 clidl 20676 . . . . 5 class LIdeal
75, 6cfv 6500 . . . 4 class (LIdealβ€˜π‘Ÿ)
8 cnx 17073 . . . . . . . 8 class ndx
9 cbs 17091 . . . . . . . 8 class Base
108, 9cfv 6500 . . . . . . 7 class (Baseβ€˜ndx)
114cv 1541 . . . . . . 7 class 𝑏
1210, 11cop 4596 . . . . . 6 class ⟨(Baseβ€˜ndx), π‘βŸ©
13 cplusg 17141 . . . . . . . 8 class +g
148, 13cfv 6500 . . . . . . 7 class (+gβ€˜ndx)
15 clsm 19424 . . . . . . . 8 class LSSum
165, 15cfv 6500 . . . . . . 7 class (LSSumβ€˜π‘Ÿ)
1714, 16cop 4596 . . . . . 6 class ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩
18 cmulr 17142 . . . . . . . 8 class .r
198, 18cfv 6500 . . . . . . 7 class (.rβ€˜ndx)
20 vi . . . . . . . 8 setvar 𝑖
21 vj . . . . . . . 8 setvar 𝑗
2220cv 1541 . . . . . . . . . 10 class 𝑖
2321cv 1541 . . . . . . . . . 10 class 𝑗
24 cmgp 19904 . . . . . . . . . . . 12 class mulGrp
255, 24cfv 6500 . . . . . . . . . . 11 class (mulGrpβ€˜π‘Ÿ)
2625, 15cfv 6500 . . . . . . . . . 10 class (LSSumβ€˜(mulGrpβ€˜π‘Ÿ))
2722, 23, 26co 7361 . . . . . . . . 9 class (𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)
28 crsp 20677 . . . . . . . . . 10 class RSpan
295, 28cfv 6500 . . . . . . . . 9 class (RSpanβ€˜π‘Ÿ)
3027, 29cfv 6500 . . . . . . . 8 class ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗))
3120, 21, 11, 11, 30cmpo 7363 . . . . . . 7 class (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))
3219, 31cop 4596 . . . . . 6 class ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩
3312, 17, 32ctp 4594 . . . . 5 class {⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩, ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩}
34 cts 17147 . . . . . . . 8 class TopSet
358, 34cfv 6500 . . . . . . 7 class (TopSetβ€˜ndx)
3622, 23wss 3914 . . . . . . . . . . 11 wff 𝑖 βŠ† 𝑗
3736wn 3 . . . . . . . . . 10 wff Β¬ 𝑖 βŠ† 𝑗
3837, 21, 11crab 3406 . . . . . . . . 9 class {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗}
3920, 11, 38cmpt 5192 . . . . . . . 8 class (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})
4039crn 5638 . . . . . . 7 class ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})
4135, 40cop 4596 . . . . . 6 class ⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩
42 cple 17148 . . . . . . . 8 class le
438, 42cfv 6500 . . . . . . 7 class (leβ€˜ndx)
4422, 23cpr 4592 . . . . . . . . . 10 class {𝑖, 𝑗}
4544, 11wss 3914 . . . . . . . . 9 wff {𝑖, 𝑗} βŠ† 𝑏
4645, 36wa 397 . . . . . . . 8 wff ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)
4746, 20, 21copab 5171 . . . . . . 7 class {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}
4843, 47cop 4596 . . . . . 6 class ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩
4941, 48cpr 4592 . . . . 5 class {⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩, ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩}
5033, 49cun 3912 . . . 4 class ({⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩, ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩} βˆͺ {⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩, ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩})
514, 7, 50csb 3859 . . 3 class ⦋(LIdealβ€˜π‘Ÿ) / π‘β¦Œ({⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩, ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩} βˆͺ {⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩, ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩})
522, 3, 51cmpt 5192 . 2 class (π‘Ÿ ∈ V ↦ ⦋(LIdealβ€˜π‘Ÿ) / π‘β¦Œ({⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩, ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩} βˆͺ {⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩, ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩}))
531, 52wceq 1542 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  32300
  Copyright terms: Public domain W3C validator