Theorem idlsrgmulr

Description: Multiplicative operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024)

	Ref	Expression
Hypotheses	idlsrgmulr.1	$$⊢S=\mathrm{IDLsrg}\left(R\right)$$
	idlsrgmulr.2	$$⊢B=\mathrm{LIdeal}\left(R\right)$$
	idlsrgmulr.3	$$⊢G={\mathrm{mulGrp}}_R$$
	idlsrgmulr.4	$$⊢\underset{\dot{}}{\otimes }=\mathrm{LSSum}\left(G\right)$$
Assertion	idlsrgmulr	$$⊢R\in V\to \left(i\in B,j\in B⟼\mathrm{RSpan}\left(R\right)\left(i\underset{\dot{}}{\otimes }j\right)\right)={\cdot }_S$$

Proof

Step	Hyp	Ref	Expression
1		idlsrgmulr.1	$$⊢S=\mathrm{IDLsrg}\left(R\right)$$
2		idlsrgmulr.2	$$⊢B=\mathrm{LIdeal}\left(R\right)$$
3		idlsrgmulr.3	$$⊢G={\mathrm{mulGrp}}_R$$
4		idlsrgmulr.4	$$⊢\underset{\dot{}}{\otimes }=\mathrm{LSSum}\left(G\right)$$
5	2	fvexi	$$⊢B\in \mathrm{V}$$
6	5 5	mpoex	$$⊢\left(i\in B,j\in B⟼\mathrm{RSpan}\left(R\right)\left(i\underset{\dot{}}{\otimes }j\right)\right)\in \mathrm{V}$$
7		eqid	$$⊢\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\underset{\dot{}}{\otimes }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\}=\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\underset{\dot{}}{\otimes }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\}$$
8	7	idlsrgstr	$$⊢\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\underset{\dot{}}{\otimes }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)\mathrm{Struct}⟨1,10⟩$$
9		mulridx	$$⊢{\cdot }_{𝑟}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
10		snsstp3	$$⊢\left\{⟨{\cdot }_{\mathrm{ndx}},\left(i\in B,j\in B⟼\mathrm{RSpan}\left(R\right)\left(i\underset{\dot{}}{\otimes }j\right)\right)⟩\right\}\subseteq \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\underset{\dot{}}{\otimes }j\right)\right)⟩\right\}$$
11		ssun1	$$⊢\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\underset{\dot{}}{\otimes }j\right)\right)⟩\right\}\subseteq \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\underset{\dot{}}{\otimes }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\}$$
12	10 11	sstri	$$⊢\left\{⟨{\cdot }_{\mathrm{ndx}},\left(i\in B,j\in B⟼\mathrm{RSpan}\left(R\right)\left(i\underset{\dot{}}{\otimes }j\right)\right)⟩\right\}\subseteq \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\underset{\dot{}}{\otimes }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\}$$
13	8 9 12	strfv	$$⊢\left(i\in B,j\in B⟼\mathrm{RSpan}\left(R\right)\left(i\underset{\dot{}}{\otimes }j\right)\right)\in \mathrm{V}\to \left(i\in B,j\in B⟼\mathrm{RSpan}\left(R\right)\left(i\underset{\dot{}}{\otimes }j\right)\right)={\cdot }_{\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\underset{\dot{}}{\otimes }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)}$$
14	6 13	ax-mp	$$⊢\left(i\in B,j\in B⟼\mathrm{RSpan}\left(R\right)\left(i\underset{\dot{}}{\otimes }j\right)\right)={\cdot }_{\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\underset{\dot{}}{\otimes }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)}$$
15		eqid	$$⊢\mathrm{LSSum}\left(R\right)=\mathrm{LSSum}\left(R\right)$$
16	2 15 3 4	idlsrgval	$$⊢R\in V\to \mathrm{IDLsrg}\left(R\right)=\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\underset{\dot{}}{\otimes }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\}$$
17	1 16	eqtrid	$$⊢R\in V\to S=\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\underset{\dot{}}{\otimes }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\}$$
18	17	fveq2d	$$⊢R\in V\to {\cdot }_S={\cdot }_{\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\underset{\dot{}}{\otimes }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)}$$
19	14 18	eqtr4id	$$⊢R\in V\to \left(i\in B,j\in B⟼\mathrm{RSpan}\left(R\right)\left(i\underset{\dot{}}{\otimes }j\right)\right)={\cdot }_S$$