Theorem idlsrgtset

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

	Ref	Expression
Hypotheses	idlsrgtset.1	No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
	idlsrgtset.2	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
	idlsrgtset.3	$$⊢J=\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)$$
Assertion	idlsrgtset	$$⊢R\in V\to J=\mathrm{TopSet}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		idlsrgtset.1	Could not format S = ( IDLsrg ` R ) : No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
2		idlsrgtset.2	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
3		idlsrgtset.3	$$⊢J=\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)$$
4	2	fvexi	$$⊢I\in \mathrm{V}$$
5	4	mptex	$$⊢\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)\in \mathrm{V}$$
6	5	rnex	$$⊢\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)\in \mathrm{V}$$
7		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\}$$
8	7	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⟩$$
9		tsetid	$$⊢\mathrm{TopSet}=\mathrm{Slot}\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
10		snsspr1	$$⊢\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)⟩\right\}\subseteq \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\}$$
11		ssun2	$$⊢\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\}\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\}$$
12	10 11	sstri	$$⊢\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq 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\}$$
13	8 9 12	strfv	$$⊢\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)\in \mathrm{V}\to \mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)=\mathrm{TopSet}\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)$$
14	6 13	ax-mp	$$⊢\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)=\mathrm{TopSet}\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)$$
15		eqid	$$⊢\mathrm{LSSum}\left(R\right)=\mathrm{LSSum}\left(R\right)$$
16		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
17		eqid	$$⊢\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)=\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)$$
18	2 15 16 17	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 |-
19	1 18	syl5eq	$$⊢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\}$$
20	19	fveq2d	$$⊢R\in V\to \mathrm{TopSet}\left(S\right)=\mathrm{TopSet}\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)$$
21	14 20	eqtr4id	$$⊢R\in V\to \mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)=\mathrm{TopSet}\left(S\right)$$
22	3 21	syl5eq	$$⊢R\in V\to J=\mathrm{TopSet}\left(S\right)$$