Definition df-idlsrg 31548

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

Step	Hyp	Ref	Expression
1		cidlsrg 31547	. 2 class IDLsrg
2		vr	. . 3 setvar 𝑟
3		cvv 3422	. . 3 class V
4		vb	. . . 4 setvar 𝑏
5	2	cv 1538	. . . . 5 class 𝑟
6		clidl 20347	. . . . 5 class LIdeal
7	5, 6	cfv 6418	. . . 4 class (LIdeal‘𝑟)
8		cnx 16822	. . . . . . . 8 class ndx
9		cbs 16840	. . . . . . . 8 class Base
10	8, 9	cfv 6418	. . . . . . 7 class (Base‘ndx)
11	4	cv 1538	. . . . . . 7 class 𝑏
12	10, 11	cop 4564	. . . . . 6 class ⟨(Base‘ndx), 𝑏⟩
13		cplusg 16888	. . . . . . . 8 class +g
14	8, 13	cfv 6418	. . . . . . 7 class (+g‘ndx)
15		clsm 19154	. . . . . . . 8 class LSSum
16	5, 15	cfv 6418	. . . . . . 7 class (LSSum‘𝑟)
17	14, 16	cop 4564	. . . . . 6 class ⟨(+g‘ndx), (LSSum‘𝑟)⟩
18		cmulr 16889	. . . . . . . 8 class .r
19	8, 18	cfv 6418	. . . . . . 7 class (.r‘ndx)
20		vi	. . . . . . . 8 setvar 𝑖
21		vj	. . . . . . . 8 setvar 𝑗
22	20	cv 1538	. . . . . . . . . 10 class 𝑖
23	21	cv 1538	. . . . . . . . . 10 class 𝑗
24		cmgp 19635	. . . . . . . . . . . 12 class mulGrp
25	5, 24	cfv 6418	. . . . . . . . . . 11 class (mulGrp‘𝑟)
26	25, 15	cfv 6418	. . . . . . . . . 10 class (LSSum‘(mulGrp‘𝑟))
27	22, 23, 26	co 7255	. . . . . . . . 9 class (𝑖(LSSum‘(mulGrp‘𝑟))𝑗)
28		crsp 20348	. . . . . . . . . 10 class RSpan
29	5, 28	cfv 6418	. . . . . . . . 9 class (RSpan‘𝑟)
30	27, 29	cfv 6418	. . . . . . . 8 class ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗))
31	20, 21, 11, 11, 30	cmpo 7257	. . . . . . 7 class (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))
32	19, 31	cop 4564	. . . . . 6 class ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩
33	12, 17, 32	ctp 4562	. . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (LSSum‘𝑟)⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩}
34		cts 16894	. . . . . . . 8 class TopSet
35	8, 34	cfv 6418	. . . . . . 7 class (TopSet‘ndx)
36	22, 23	wss 3883	. . . . . . . . . . 11 wff 𝑖 ⊆ 𝑗
37	36	wn 3	. . . . . . . . . 10 wff ¬ 𝑖 ⊆ 𝑗
38	37, 21, 11	crab 3067	. . . . . . . . 9 class {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗}
39	20, 11, 38	cmpt 5153	. . . . . . . 8 class (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})
40	39	crn 5581	. . . . . . 7 class ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})
41	35, 40	cop 4564	. . . . . 6 class ⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})⟩
42		cple 16895	. . . . . . . 8 class le
43	8, 42	cfv 6418	. . . . . . 7 class (le‘ndx)
44	22, 23	cpr 4560	. . . . . . . . . 10 class {𝑖, 𝑗}
45	44, 11	wss 3883	. . . . . . . . 9 wff {𝑖, 𝑗} ⊆ 𝑏
46	45, 36	wa 395	. . . . . . . 8 wff ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)
47	46, 20, 21	copab 5132	. . . . . . 7 class {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}
48	43, 47	cop 4564	. . . . . 6 class ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩
49	41, 48	cpr 4560	. . . . 5 class {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩}
50	33, 49	cun 3881	. . . 4 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (LSSum‘𝑟)⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩})
51	4, 7, 50	csb 3828	. . 3 class ⦋(LIdeal‘𝑟) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (LSSum‘𝑟)⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩})
52	2, 3, 51	cmpt 5153	. 2 class (𝑟 ∈ V ↦ ⦋(LIdeal‘𝑟) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (LSSum‘𝑟)⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩}))
53	1, 52	wceq 1539	1 wff IDLsrg = (𝑟 ∈ V ↦ ⦋(LIdeal‘𝑟) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (LSSum‘𝑟)⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩}))

This definition is referenced by:  idlsrgval  31550