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	Could not format assertion : No typesetting found for |- IDLsrg = ( r e. _V |-> [_ ( LIdeal ` r ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( LSSum ` r ) >. , <. ( .r ` ndx ) , ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) j ) ) ) >. } u. { <. ( TopSet ` ndx ) , ran ( i e. b |-> { j e. b | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ b /\ i C_ j ) } >. } ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cidlsrg	Could not format IDLsrg : No typesetting found for class IDLsrg with typecode class
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		clidl	$$class\mathrm{LIdeal}$$
4	1	cv	$$setvarr$$
5	4 3	cfv	$$class\mathrm{LIdeal}\left(r\right)$$
6		vb	$$setvarb$$
7		cbs	$$class\mathrm{Base}$$
8		cnx	$$class\mathrm{ndx}$$
9	8 7	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
10	6	cv	$$setvarb$$
11	9 10	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩$$
12		cplusg	$$class{+}_{𝑔}$$
13	8 12	cfv	$$class{+}_{\mathrm{ndx}}$$
14		clsm	$$class\mathrm{LSSum}$$
15	4 14	cfv	$$class\mathrm{LSSum}\left(r\right)$$
16	13 15	cop	$$class⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(r\right)⟩$$
17		cmulr	$$class{\cdot }_{𝑟}$$
18	8 17	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
19		vi	$$setvari$$
20		vj	$$setvarj$$
21		crsp	$$class\mathrm{RSpan}$$
22	4 21	cfv	$$class\mathrm{RSpan}\left(r\right)$$
23	19	cv	$$setvari$$
24		cmgp	$$class\mathrm{mulGrp}$$
25	4 24	cfv	$$class{\mathrm{mulGrp}}_r$$
26	25 14	cfv	$$class\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)$$
27	20	cv	$$setvarj$$
28	23 27 26	co	$$class\left(i\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)j\right)$$
29	28 22	cfv	$$class\mathrm{RSpan}\left(r\right)\left(i\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)j\right)$$
30	19 20 10 10 29	cmpo	$$class\left(i\in b,j\in b⟼\mathrm{RSpan}\left(r\right)\left(i\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)j\right)\right)$$
31	18 30	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\left(i\in b,j\in b⟼\mathrm{RSpan}\left(r\right)\left(i\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)j\right)\right)⟩$$
32	11 16 31	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in b,j\in b⟼\mathrm{RSpan}\left(r\right)\left(i\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)j\right)\right)⟩\right\}$$
33		cts	$$class\mathrm{TopSet}$$
34	8 33	cfv	$$class\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
35	23 27	wss	$$wffi\subseteq j$$
36	35	wn	$$wff\neg i\subseteq j$$
37	36 20 10	crab	$$class\left\{j\in b|\neg i\subseteq j\right\}$$
38	19 10 37	cmpt	$$class\left(i\in b⟼\left\{j\in b|\neg i\subseteq j\right\}\right)$$
39	38	crn	$$class\mathrm{ran}\left(i\in b⟼\left\{j\in b|\neg i\subseteq j\right\}\right)$$
40	34 39	cop	$$class⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ran}\left(i\in b⟼\left\{j\in b|\neg i\subseteq j\right\}\right)⟩$$
41		cple	$$class\mathrm{le}$$
42	8 41	cfv	$$class{\le }_{\mathrm{ndx}}$$
43	23 27	cpr	$$class\left\{i,j\right\}$$
44	43 10	wss	$$wff\left\{i,j\right\}\subseteq b$$
45	44 35	wa	$$wff\left(\left\{i,j\right\}\subseteq b\wedge i\subseteq j\right)$$
46	45 19 20	copab	$$class\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq b\wedge i\subseteq j\right)\right\}$$
47	42 46	cop	$$class⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq b\wedge i\subseteq j\right)\right\}⟩$$
48	40 47	cpr	$$class\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ran}\left(i\in b⟼\left\{j\in b|\neg i\subseteq j\right\}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq b\wedge i\subseteq j\right)\right\}⟩\right\}$$
49	32 48	cun	$$class\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in b,j\in b⟼\mathrm{RSpan}\left(r\right)\left(i\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)j\right)\right)⟩\right\}\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ran}\left(i\in b⟼\left\{j\in b|\neg i\subseteq j\right\}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq b\wedge i\subseteq j\right)\right\}⟩\right\}\right)$$
50	6 5 49	csb	$$class⦋\mathrm{LIdeal}\left(r\right)/b⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in b,j\in b⟼\mathrm{RSpan}\left(r\right)\left(i\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)j\right)\right)⟩\right\}\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ran}\left(i\in b⟼\left\{j\in b|\neg i\subseteq j\right\}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq b\wedge i\subseteq j\right)\right\}⟩\right\}\right)$$
51	1 2 50	cmpt	$$class\left(r\in \mathrm{V}⟼⦋\mathrm{LIdeal}\left(r\right)/b⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in b,j\in b⟼\mathrm{RSpan}\left(r\right)\left(i\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)j\right)\right)⟩\right\}\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ran}\left(i\in b⟼\left\{j\in b|\neg i\subseteq j\right\}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq b\wedge i\subseteq j\right)\right\}⟩\right\}\right)\right)$$
52	0 51	wceq	Could not format IDLsrg = ( r e. _V |-> [_ ( LIdeal ` r ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( LSSum ` r ) >. , <. ( .r ` ndx ) , ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) j ) ) ) >. } u. { <. ( TopSet ` ndx ) , ran ( i e. b |-> { j e. b | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ b /\ i C_ j ) } >. } ) ) : No typesetting found for wff IDLsrg = ( r e. _V |-> [_ ( LIdeal ` r ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( LSSum ` r ) >. , <. ( .r ` ndx ) , ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) j ) ) ) >. } u. { <. ( TopSet ` ndx ) , ran ( i e. b |-> { j e. b | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ b /\ i C_ j ) } >. } ) ) with typecode wff