Theorem idlsrgmulr

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

	Ref	Expression
Hypotheses	idlsrgmulr.1	No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
	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	Could not format S = ( IDLsrg ` R ) : No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
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		mulrid	$$⊢{\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	Could not format ( R e. V -> ( IDLsrg ` R ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) 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 |- ( R e. V -> ( IDLsrg ` R ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) 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 |-
17	1 16	syl5eq	$$⊢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$$