Theorem idlsrgplusg

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

	Ref	Expression
Hypotheses	idlsrgplusg.1	No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
	idlsrgplusg.2	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(R\right)$$
Assertion	idlsrgplusg	$$⊢R\in V\to \underset{\dot{}}{\oplus }={+}_S$$

Proof

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