Definition df-idlsrg

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cidlsrg	⊢ IDLsrg
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		clidl	⊢ LIdeal
4	1	cv	⊢ 𝑟
5	4 3	cfv	⊢ ( LIdeal ‘ 𝑟 )
6		vb	⊢ 𝑏
7		cbs	⊢ Base
8		cnx	⊢ ndx
9	8 7	cfv	⊢ ( Base ‘ ndx )
10	6	cv	⊢ 𝑏
11	9 10	cop	⊢ ⟨ ( Base ‘ ndx ) , 𝑏 ⟩
12		cplusg	⊢ +g
13	8 12	cfv	⊢ ( +g ‘ ndx )
14		clsm	⊢ LSSum
15	4 14	cfv	⊢ ( LSSum ‘ 𝑟 )
16	13 15	cop	⊢ ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑟 ) ⟩
17		cmulr	⊢ .r
18	8 17	cfv	⊢ ( .r ‘ ndx )
19		vi	⊢ 𝑖
20		vj	⊢ 𝑗
21		crsp	⊢ RSpan
22	4 21	cfv	⊢ ( RSpan ‘ 𝑟 )
23	19	cv	⊢ 𝑖
24		cmgp	⊢ mulGrp
25	4 24	cfv	⊢ ( mulGrp ‘ 𝑟 )
26	25 14	cfv	⊢ ( LSSum ‘ ( mulGrp ‘ 𝑟 ) )
27	20	cv	⊢ 𝑗
28	23 27 26	co	⊢ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 )
29	28 22	cfv	⊢ ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) )
30	19 20 10 10 29	cmpo	⊢ ( 𝑖 ∈ 𝑏 , 𝑗 ∈ 𝑏 ↦ ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) ) )
31	18 30	cop	⊢ ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝑏 , 𝑗 ∈ 𝑏 ↦ ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) ) ) ⟩
32	11 16 31	ctp	⊢ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑟 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝑏 , 𝑗 ∈ 𝑏 ↦ ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) ) ) ⟩ }
33		cts	⊢ TopSet
34	8 33	cfv	⊢ ( TopSet ‘ ndx )
35	23 27	wss	⊢ 𝑖 ⊆ 𝑗
36	35	wn	⊢ ¬ 𝑖 ⊆ 𝑗
37	36 20 10	crab	⊢ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 }
38	19 10 37	cmpt	⊢ ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } )
39	38	crn	⊢ ran ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } )
40	34 39	cop	⊢ ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩
41		cple	⊢ le
42	8 41	cfv	⊢ ( le ‘ ndx )
43	23 27	cpr	⊢ { 𝑖 , 𝑗 }
44	43 10	wss	⊢ { 𝑖 , 𝑗 } ⊆ 𝑏
45	44 35	wa	⊢ ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 )
46	45 19 20	copab	⊢ { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 ) }
47	42 46	cop	⊢ ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 ) } ⟩
48	40 47	cpr	⊢ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ }
49	32 48	cun	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑟 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝑏 , 𝑗 ∈ 𝑏 ↦ ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } )
50	6 5 49	csb	⊢ ⦋ ( LIdeal ‘ 𝑟 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑟 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝑏 , 𝑗 ∈ 𝑏 ↦ ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } )
51	1 2 50	cmpt	⊢ ( 𝑟 ∈ V ↦ ⦋ ( LIdeal ‘ 𝑟 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑟 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝑏 , 𝑗 ∈ 𝑏 ↦ ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) )
52	0 51	wceq	⊢ IDLsrg = ( 𝑟 ∈ V ↦ ⦋ ( LIdeal ‘ 𝑟 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑟 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝑏 , 𝑗 ∈ 𝑏 ↦ ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) )