Metamath Proof Explorer

Theorem idlsrgmulr

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

Ref Expression
Hypotheses idlsrgmulr.1 
|- S = ( IDLsrg ` R )
idlsrgmulr.2 
|- B = ( LIdeal ` R )
idlsrgmulr.3 
|- G = ( mulGrp ` R )
idlsrgmulr.4 
|- .(x) = ( LSSum ` G )
Assertion idlsrgmulr 
|- ( R e. V -> ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) j ) ) ) = ( .r ` S ) )

Proof

Step Hyp Ref Expression
1 idlsrgmulr.1 
 |-  S = ( IDLsrg ` R )
2 idlsrgmulr.2 
 |-  B = ( LIdeal ` R )
3 idlsrgmulr.3 
 |-  G = ( mulGrp ` R )
4 idlsrgmulr.4 
 |-  .(x) = ( LSSum ` G )
5 2 fvexi 
 |-  B e. _V
6 5 5 mpoex 
 |-  ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) j ) ) ) e. _V
7 eqid 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) 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 ) , B >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) 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 ) } >. } )
8 7 idlsrgstr 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) 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 ) } >. } ) Struct <. 1 , ; 1 0 >.
9 mulrid 
 |-  .r = Slot ( .r ` ndx )
10 snsstp3 
 |-  { <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) j ) ) ) >. } C_ { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) j ) ) ) >. }
11 ssun1 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) j ) ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) 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 ) } >. } )
12 10 11 sstri 
 |-  { <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) j ) ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) 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 ) } >. } )
13 8 9 12 strfv 
 |-  ( ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) j ) ) ) e. _V -> ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) j ) ) ) = ( .r ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) 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 ) } >. } ) ) )
14 6 13 ax-mp 
 |-  ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) j ) ) ) = ( .r ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) 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 ) } >. } ) )
15 eqid 
 |-  ( LSSum ` R ) = ( LSSum ` R )
16 2 15 3 4 idlsrgval 
 |-  ( R e. V -> ( IDLsrg ` R ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) 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 ) } >. } ) )
17 1 16 syl5eq 
 |-  ( R e. V -> S = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) 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 ) } >. } ) )
18 17 fveq2d 
 |-  ( R e. V -> ( .r ` S ) = ( .r ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) 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 ) } >. } ) ) )
19 14 18 eqtr4id 
 |-  ( R e. V -> ( i e. B , j e. B |-> ( ( RSpan ` R ) ` ( i .(x) j ) ) ) = ( .r ` S ) )