Theorem idlsrgval

Description: Lemma for idlsrgbas through idlsrgtset . (Contributed by Thierry Arnoux, 1-Jun-2024)

	Ref	Expression
Hypotheses	idlsrgval.1	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
	idlsrgval.2	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(R\right)$$
	idlsrgval.3	$$⊢G={\mathrm{mulGrp}}_R$$
	idlsrgval.4	$$⊢\underset{\dot{}}{\otimes }=\mathrm{LSSum}\left(G\right)$$
Assertion	idlsrgval	Could not format assertion : No typesetting found for |- ( R e. V -> ( IDLsrg ` R ) = ( { <. ( Base ` ndx ) , I >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , ( i e. I , j e. I |-> ( ( RSpan ` R ) ` ( i .(x) 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 |-

Proof

Step	Hyp	Ref	Expression
1		idlsrgval.1	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
2		idlsrgval.2	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(R\right)$$
3		idlsrgval.3	$$⊢G={\mathrm{mulGrp}}_R$$
4		idlsrgval.4	$$⊢\underset{\dot{}}{\otimes }=\mathrm{LSSum}\left(G\right)$$
5		elex	$$⊢R\in V\to R\in \mathrm{V}$$
6		fvexd	$$⊢r=R\to \mathrm{LIdeal}\left(r\right)\in \mathrm{V}$$
7		simpr	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to b=\mathrm{LIdeal}\left(r\right)$$
8		simpl	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to r=R$$
9	8	fveq2d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \mathrm{LIdeal}\left(r\right)=\mathrm{LIdeal}\left(R\right)$$
10	7 9	eqtrd	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to b=\mathrm{LIdeal}\left(R\right)$$
11	10 1	eqtr4di	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to b=I$$
12	11	opeq2d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩$$
13	8	fveq2d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \mathrm{LSSum}\left(r\right)=\mathrm{LSSum}\left(R\right)$$
14	13 2	eqtr4di	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \mathrm{LSSum}\left(r\right)=\underset{\dot{}}{\oplus }$$
15	14	opeq2d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to ⟨{+}_{\mathrm{ndx}},\mathrm{LSSum}\left(r\right)⟩=⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{\oplus }⟩$$
16	8	fveq2d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \mathrm{RSpan}\left(r\right)=\mathrm{RSpan}\left(R\right)$$
17	8	fveq2d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to {\mathrm{mulGrp}}_r={\mathrm{mulGrp}}_R$$
18	17 3	eqtr4di	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to {\mathrm{mulGrp}}_r=G$$
19	18	fveq2d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)=\mathrm{LSSum}\left(G\right)$$
20	19 4	eqtr4di	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)=\underset{\dot{}}{\otimes }$$
21	20	oveqd	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to i\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)j=i\underset{\dot{}}{\otimes }j$$
22	16 21	fveq12d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \mathrm{RSpan}\left(r\right)\left(i\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)j\right)=\mathrm{RSpan}\left(R\right)\left(i\underset{\dot{}}{\otimes }j\right)$$
23	11 11 22	mpoeq123dv	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \left(i\in b,j\in b⟼\mathrm{RSpan}\left(r\right)\left(i\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)j\right)\right)=\left(i\in I,j\in I⟼\mathrm{RSpan}\left(R\right)\left(i\underset{\dot{}}{\otimes }j\right)\right)$$
24	23	opeq2d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to ⟨{\cdot }_{\mathrm{ndx}},\left(i\in b,j\in b⟼\mathrm{RSpan}\left(r\right)\left(i\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)j\right)\right)⟩=⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\mathrm{RSpan}\left(R\right)\left(i\underset{\dot{}}{\otimes }j\right)\right)⟩$$
25	12 15 24	tpeq123d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \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\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)j\right)\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{\oplus }⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\mathrm{RSpan}\left(R\right)\left(i\underset{\dot{}}{\otimes }j\right)\right)⟩\right\}$$
26	11	rabeqdv	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \left\{j\in b|\neg i\subseteq j\right\}=\left\{j\in I|\neg i\subseteq j\right\}$$
27	11 26	mpteq12dv	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \left(i\in b⟼\left\{j\in b|\neg i\subseteq j\right\}\right)=\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)$$
28	27	rneqd	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \mathrm{ran}\left(i\in b⟼\left\{j\in b|\neg i\subseteq j\right\}\right)=\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)$$
29	28	opeq2d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to ⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ran}\left(i\in b⟼\left\{j\in b|\neg i\subseteq j\right\}\right)⟩=⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)⟩$$
30	11	sseq2d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \left(\left\{i,j\right\}\subseteq b\leftrightarrow \left\{i,j\right\}\subseteq I\right)$$
31	30	anbi1d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \left(\left(\left\{i,j\right\}\subseteq b\wedge i\subseteq j\right)\leftrightarrow \left(\left\{i,j\right\}\subseteq I\wedge i\subseteq j\right)\right)$$
32	31	opabbidv	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq b\wedge i\subseteq j\right)\right\}=\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq I\wedge i\subseteq j\right)\right\}$$
33	32	opeq2d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to ⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq b\wedge i\subseteq j\right)\right\}⟩=⟨{\le }_{\mathrm{ndx}},\left\{⟨i,j⟩|\left(\left\{i,j\right\}\subseteq I\wedge i\subseteq j\right)\right\}⟩$$
34	29 33	preq12d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \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{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\}$$
35	25 34	uneq12d	$$⊢\left(r=R\wedge b=\mathrm{LIdeal}\left(r\right)\right)\to \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\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)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}},I⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{\oplus }⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\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 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\}$$
36	6 35	csbied	$$⊢r=R\to ⦋\mathrm{LIdeal}\left(r\right)/b⦌\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\mathrm{LSSum}\left({\mathrm{mulGrp}}_r\right)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)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{\oplus }⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\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 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\}$$
37		df-idlsrg	Could not format IDLsrg = ( r e. _V |-> [_ ( LIdeal ` r ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( LSSum ` r ) >. , <. ( .r ` ndx ) , ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) 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 |- IDLsrg = ( r e. _V |-> [_ ( LIdeal ` r ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( LSSum ` r ) >. , <. ( .r ` ndx ) , ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) 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 |-
38		tpex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{\oplus }⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\mathrm{RSpan}\left(R\right)\left(i\underset{\dot{}}{\otimes }j\right)\right)⟩\right\}\in \mathrm{V}$$
39		prex	$$⊢\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\}\in \mathrm{V}$$
40	38 39	unex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},I⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{\oplus }⟩,⟨{\cdot }_{\mathrm{ndx}},\left(i\in I,j\in I⟼\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 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\}\in \mathrm{V}$$
41	36 37 40	fvmpt	Could not format ( R e. _V -> ( IDLsrg ` R ) = ( { <. ( Base ` ndx ) , I >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , ( i e. I , j e. I |-> ( ( RSpan ` R ) ` ( i .(x) 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 ) , .(+) >. , <. ( .r ` ndx ) , ( i e. I , j e. I |-> ( ( RSpan ` R ) ` ( i .(x) 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 |-
42	5 41	syl	Could not format ( R e. V -> ( IDLsrg ` R ) = ( { <. ( Base ` ndx ) , I >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , ( i e. I , j e. I |-> ( ( RSpan ` R ) ` ( i .(x) 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 ) , .(+) >. , <. ( .r ` ndx ) , ( i e. I , j e. I |-> ( ( RSpan ` R ) ` ( i .(x) 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 |-