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 32610
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 32609 . 2 class IDLsrg
2 vr . . 3 setvar π‘Ÿ
3 cvv 3474 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1540 . . . . 5 class π‘Ÿ
6 clidl 20782 . . . . 5 class LIdeal
75, 6cfv 6543 . . . 4 class (LIdealβ€˜π‘Ÿ)
8 cnx 17125 . . . . . . . 8 class ndx
9 cbs 17143 . . . . . . . 8 class Base
108, 9cfv 6543 . . . . . . 7 class (Baseβ€˜ndx)
114cv 1540 . . . . . . 7 class 𝑏
1210, 11cop 4634 . . . . . 6 class ⟨(Baseβ€˜ndx), π‘βŸ©
13 cplusg 17196 . . . . . . . 8 class +g
148, 13cfv 6543 . . . . . . 7 class (+gβ€˜ndx)
15 clsm 19501 . . . . . . . 8 class LSSum
165, 15cfv 6543 . . . . . . 7 class (LSSumβ€˜π‘Ÿ)
1714, 16cop 4634 . . . . . 6 class ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩
18 cmulr 17197 . . . . . . . 8 class .r
198, 18cfv 6543 . . . . . . 7 class (.rβ€˜ndx)
20 vi . . . . . . . 8 setvar 𝑖
21 vj . . . . . . . 8 setvar 𝑗
2220cv 1540 . . . . . . . . . 10 class 𝑖
2321cv 1540 . . . . . . . . . 10 class 𝑗
24 cmgp 19986 . . . . . . . . . . . 12 class mulGrp
255, 24cfv 6543 . . . . . . . . . . 11 class (mulGrpβ€˜π‘Ÿ)
2625, 15cfv 6543 . . . . . . . . . 10 class (LSSumβ€˜(mulGrpβ€˜π‘Ÿ))
2722, 23, 26co 7408 . . . . . . . . 9 class (𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)
28 crsp 20783 . . . . . . . . . 10 class RSpan
295, 28cfv 6543 . . . . . . . . 9 class (RSpanβ€˜π‘Ÿ)
3027, 29cfv 6543 . . . . . . . 8 class ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗))
3120, 21, 11, 11, 30cmpo 7410 . . . . . . 7 class (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))
3219, 31cop 4634 . . . . . 6 class ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩
3312, 17, 32ctp 4632 . . . . 5 class {⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩, ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩}
34 cts 17202 . . . . . . . 8 class TopSet
358, 34cfv 6543 . . . . . . 7 class (TopSetβ€˜ndx)
3622, 23wss 3948 . . . . . . . . . . 11 wff 𝑖 βŠ† 𝑗
3736wn 3 . . . . . . . . . 10 wff Β¬ 𝑖 βŠ† 𝑗
3837, 21, 11crab 3432 . . . . . . . . 9 class {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗}
3920, 11, 38cmpt 5231 . . . . . . . 8 class (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})
4039crn 5677 . . . . . . 7 class ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})
4135, 40cop 4634 . . . . . 6 class ⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩
42 cple 17203 . . . . . . . 8 class le
438, 42cfv 6543 . . . . . . 7 class (leβ€˜ndx)
4422, 23cpr 4630 . . . . . . . . . 10 class {𝑖, 𝑗}
4544, 11wss 3948 . . . . . . . . 9 wff {𝑖, 𝑗} βŠ† 𝑏
4645, 36wa 396 . . . . . . . 8 wff ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)
4746, 20, 21copab 5210 . . . . . . 7 class {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}
4843, 47cop 4634 . . . . . 6 class ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩
4941, 48cpr 4630 . . . . 5 class {⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩, ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩}
5033, 49cun 3946 . . . 4 class ({⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩, ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩} βˆͺ {⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩, ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩})
514, 7, 50csb 3893 . . 3 class ⦋(LIdealβ€˜π‘Ÿ) / π‘β¦Œ({⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩, ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩} βˆͺ {⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩, ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩})
522, 3, 51cmpt 5231 . 2 class (π‘Ÿ ∈ V ↦ ⦋(LIdealβ€˜π‘Ÿ) / π‘β¦Œ({⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (LSSumβ€˜π‘Ÿ)⟩, ⟨(.rβ€˜ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpanβ€˜π‘Ÿ)β€˜(𝑖(LSSumβ€˜(mulGrpβ€˜π‘Ÿ))𝑗)))⟩} βˆͺ {⟨(TopSetβ€˜ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ Β¬ 𝑖 βŠ† 𝑗})⟩, ⟨(leβ€˜ndx), {βŸ¨π‘–, π‘—βŸ© ∣ ({𝑖, 𝑗} βŠ† 𝑏 ∧ 𝑖 βŠ† 𝑗)}⟩}))
531, 52wceq 1541 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  32612
  Copyright terms: Public domain W3C validator