Metamath Proof Explorer

Theorem idlsrgplusg

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

Ref Expression
Hypotheses idlsrgplusg.1 
|- S = ( IDLsrg ` R )
idlsrgplusg.2 
|- .(+) = ( LSSum ` R )
Assertion idlsrgplusg 
|- ( R e. V -> .(+) = ( +g ` S ) )

Proof

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