Metamath Proof Explorer

Theorem idlsrgval

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

Ref Expression
Hypotheses idlsrgval.1 
|- I = ( LIdeal ` R )
idlsrgval.2 
|- .(+) = ( LSSum ` R )
idlsrgval.3 
|- G = ( mulGrp ` R )
idlsrgval.4 
|- .(x) = ( LSSum ` G )
Assertion idlsrgval 
|- ( 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 ) } >. } ) )

Proof

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