Metamath Proof Explorer

Theorem idlsrgbas

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

Ref Expression
Hypotheses idlsrgbas.1 
|- S = ( IDLsrg ` R )
idlsrgbas.2 
|- I = ( LIdeal ` R )
Assertion idlsrgbas 
|- ( R e. V -> I = ( Base ` S ) )

Proof

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