Definition df-idlsrg 31005

Description: Define a structure for the ideals of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.)

Assertion

Ref	Expression
df-idlsrg	⊢ IDLsrg = (𝑟 ∈ Ring ↦ ⦋(LIdeal‘𝑟) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩}))

Distinct variable group:   𝑟,𝑏,𝑖,𝑗

Detailed syntax breakdown of Definition df-idlsrg

Step	Hyp	Ref	Expression
1		cidlsrg 31004	. 2 class IDLsrg
2		vr	. . 3 setvar 𝑟
3		crg 19290	. . 3 class Ring
4		vb	. . . 4 setvar 𝑏
5	2	cv 1535	. . . . 5 class 𝑟
6		clidl 19935	. . . . 5 class LIdeal
7	5, 6	cfv 6348	. . . 4 class (LIdeal‘𝑟)
8		cnx 16473	. . . . . . . 8 class ndx
9		cbs 16476	. . . . . . . 8 class Base
10	8, 9	cfv 6348	. . . . . . 7 class (Base‘ndx)
11	4	cv 1535	. . . . . . 7 class 𝑏
12	10, 11	cop 4566	. . . . . 6 class ⟨(Base‘ndx), 𝑏⟩
13		cplusg 16558	. . . . . . . 8 class +g
14	8, 13	cfv 6348	. . . . . . 7 class (+g‘ndx)
15		vi	. . . . . . . 8 setvar 𝑖
16		vj	. . . . . . . 8 setvar 𝑗
17		cplusf 17842	. . . . . . . . . 10 class +𝑓
18	5, 17	cfv 6348	. . . . . . . . 9 class (+𝑓‘𝑟)
19	15	cv 1535	. . . . . . . . . 10 class 𝑖
20	16	cv 1535	. . . . . . . . . 10 class 𝑗
21	19, 20	cxp 5546	. . . . . . . . 9 class (𝑖 × 𝑗)
22	18, 21	cima 5551	. . . . . . . 8 class ((+𝑓‘𝑟) “ (𝑖 × 𝑗))
23	15, 16, 11, 11, 22	cmpo 7151	. . . . . . 7 class (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))
24	14, 23	cop 4566	. . . . . 6 class ⟨(+g‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))⟩
25		cmulr 16559	. . . . . . . 8 class .r
26	8, 25	cfv 6348	. . . . . . 7 class (.r‘ndx)
27		cmgp 19232	. . . . . . . . . . . 12 class mulGrp
28	5, 27	cfv 6348	. . . . . . . . . . 11 class (mulGrp‘𝑟)
29	28, 17	cfv 6348	. . . . . . . . . 10 class (+𝑓‘(mulGrp‘𝑟))
30	29, 21	cima 5551	. . . . . . . . 9 class ((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))
31		crsp 19936	. . . . . . . . . 10 class RSpan
32	5, 31	cfv 6348	. . . . . . . . 9 class (RSpan‘𝑟)
33	30, 32	cfv 6348	. . . . . . . 8 class ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗)))
34	15, 16, 11, 11, 33	cmpo 7151	. . . . . . 7 class (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))
35	26, 34	cop 4566	. . . . . 6 class ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))⟩
36	12, 24, 35	ctp 4564	. . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))⟩}
37		cts 16564	. . . . . . . 8 class TopSet
38	8, 37	cfv 6348	. . . . . . 7 class (TopSet‘ndx)
39	20, 19	wss 3929	. . . . . . . . . . 11 wff 𝑗 ⊆ 𝑖
40		cprmidl 30973	. . . . . . . . . . . 12 class PrmIdeal
41	5, 40	cfv 6348	. . . . . . . . . . 11 class (PrmIdeal‘𝑟)
42	39, 16, 41	crab 3141	. . . . . . . . . 10 class {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}
43	11, 42	cdif 3926	. . . . . . . . 9 class (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖})
44	15, 11, 43	cmpt 5139	. . . . . . . 8 class (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))
45	44	crn 5549	. . . . . . 7 class ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))
46	38, 45	cop 4566	. . . . . 6 class ⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))⟩
47		cple 16565	. . . . . . . 8 class le
48	8, 47	cfv 6348	. . . . . . 7 class (le‘ndx)
49	19, 20	cpr 4562	. . . . . . . . . 10 class {𝑖, 𝑗}
50	49, 11	wss 3929	. . . . . . . . 9 wff {𝑖, 𝑗} ⊆ 𝑏
51	19, 20	wss 3929	. . . . . . . . 9 wff 𝑖 ⊆ 𝑗
52	50, 51	wa 398	. . . . . . . 8 wff ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)
53	52, 15, 16	copab 5121	. . . . . . 7 class {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}
54	48, 53	cop 4566	. . . . . 6 class ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩
55	46, 54	cpr 4562	. . . . 5 class {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩}
56	36, 55	cun 3927	. . . 4 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩})
57	4, 7, 56	csb 3876	. . 3 class ⦋(LIdeal‘𝑟) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩})
58	2, 3, 57	cmpt 5139	. 2 class (𝑟 ∈ Ring ↦ ⦋(LIdeal‘𝑟) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩}))
59	1, 58	wceq 1536	1 wff IDLsrg = (𝑟 ∈ Ring ↦ ⦋(LIdeal‘𝑟) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩}))

This definition is referenced by: (None)