Theorem idlsrgbas

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

	Ref	Expression
Hypotheses	idlsrgbas.1	No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
	idlsrgbas.2	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
Assertion	idlsrgbas	$$⊢R\in V\to I={\mathrm{Base}}_S$$

Proof

Step	Hyp	Ref	Expression
1		idlsrgbas.1	Could not format S = ( IDLsrg ` R ) : No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
2		idlsrgbas.2	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
3	2	fvexi	$$⊢I\in \mathrm{V}$$
4		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\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 I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq I\wedge i\subseteq j\right)\right\}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\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 I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq I\wedge i\subseteq j\right)\right\}⟩\right\}$$
5	4	idlsrgstr	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\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 I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq I\wedge i\subseteq j\right)\right\}⟩\right\}\right)\mathrm{Struct}⟨1,10⟩$$
6		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
7		snsstp1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\mathrm{RSpan}\left(R\right)\left(i\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)j\right)\right)⟩\right\}$$
8		ssun1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\mathrm{RSpan}\left(R\right)\left(i\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)j\right)\right)⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\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 I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq I\wedge i\subseteq j\right)\right\}⟩\right\}$$
9	7 8	sstri	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\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 I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq I\wedge i\subseteq j\right)\right\}⟩\right\}$$
10	5 6 9	strfv	$$⊢I\in \mathrm{V}\to I={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\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 I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq I\wedge i\subseteq j\right)\right\}⟩\right\}\right)}$$
11	3 10	ax-mp	$$⊢I={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\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 I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq I\wedge i\subseteq j\right)\right\}⟩\right\}\right)}$$
12		eqid	$$⊢\mathrm{LSSum}\left(R\right)=\mathrm{LSSum}\left(R\right)$$
13		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
14		eqid	$$⊢\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)=\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)$$
15	2 12 13 14	idlsrgval	Could not format ( R e. V -> ( IDLsrg ` R ) = ( { <. ( Base ` ndx ) , I >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. I , j e. I |-> ( ( RSpan ` R ) ` ( i ( LSSum ` ( mulGrp ` R ) ) j ) ) ) >. } u. { <. ( TopSet ` ndx ) , ran ( i e. I |-> { j e. I | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ I /\ i C_ j ) } >. } ) ) : No typesetting found for |- ( R e. V -> ( IDLsrg ` R ) = ( { <. ( Base ` ndx ) , I >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. I , j e. I |-> ( ( RSpan ` R ) ` ( i ( LSSum ` ( mulGrp ` R ) ) j ) ) ) >. } u. { <. ( TopSet ` ndx ) , ran ( i e. I |-> { j e. I | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ I /\ i C_ j ) } >. } ) ) with typecode |-
16	1 15	eqtrid	$$⊢R\in V\to S=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\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 I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq I\wedge i\subseteq j\right)\right\}⟩\right\}$$
17	16	fveq2d	$$⊢R\in V\to {\mathrm{Base}}_S={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\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 I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq I\wedge i\subseteq j\right)\right\}⟩\right\}\right)}$$
18	11 17	eqtr4id	$$⊢R\in V\to I={\mathrm{Base}}_S$$