Metamath Proof Explorer

Theorem idlsrgtset

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

Ref Expression
Hypotheses idlsrgtset.1 
|- S = ( IDLsrg ` R )
idlsrgtset.2 
|- I = ( LIdeal ` R )
idlsrgtset.3 
|- J = ran ( i e. I |-> { j e. I | -. i C_ j } )
Assertion idlsrgtset 
|- ( R e. V -> J = ( TopSet ` S ) )

Proof

Step Hyp Ref Expression
1 idlsrgtset.1 
 |-  S = ( IDLsrg ` R )
2 idlsrgtset.2 
 |-  I = ( LIdeal ` R )
3 idlsrgtset.3 
 |-  J = ran ( i e. I |-> { j e. I | -. i C_ j } )
4 2 fvexi 
 |-  I e. _V
5 4 mptex 
 |-  ( i e. I |-> { j e. I | -. i C_ j } ) e. _V
6 5 rnex 
 |-  ran ( i e. I |-> { j e. I | -. i C_ j } ) e. _V
7 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 ) } >. } )
8 7 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 >.
9 tsetid 
 |-  TopSet = Slot ( TopSet ` ndx )
10 snsspr1 
 |-  { <. ( TopSet ` ndx ) , ran ( i e. I |-> { j e. I | -. i C_ j } ) >. } C_ { <. ( TopSet ` ndx ) , ran ( i e. I |-> { j e. I | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ I /\ i C_ j ) } >. }
11 ssun2 
 |-  { <. ( TopSet ` ndx ) , ran ( i e. I |-> { j e. I | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ I /\ i C_ 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 ) } >. } )
12 10 11 sstri 
 |-  { <. ( TopSet ` ndx ) , ran ( i e. I |-> { j e. I | -. i C_ 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 ) } >. } )
13 8 9 12 strfv 
 |-  ( ran ( i e. I |-> { j e. I | -. i C_ j } ) e. _V -> ran ( i e. I |-> { j e. I | -. i C_ j } ) = ( TopSet ` ( { <. ( 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 ) } >. } ) ) )
14 6 13 ax-mp 
 |-  ran ( i e. I |-> { j e. I | -. i C_ j } ) = ( TopSet ` ( { <. ( 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 ) } >. } ) )
15 eqid 
 |-  ( LSSum ` R ) = ( LSSum ` R )
16 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
17 eqid 
 |-  ( LSSum ` ( mulGrp ` R ) ) = ( LSSum ` ( mulGrp ` R ) )
18 2 15 16 17 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 ) } >. } ) )
19 1 18 syl5eq 
 |-  ( 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 ) } >. } ) )
20 19 fveq2d 
 |-  ( R e. V -> ( TopSet ` S ) = ( TopSet ` ( { <. ( 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 ) } >. } ) ) )
21 14 20 eqtr4id 
 |-  ( R e. V -> ran ( i e. I |-> { j e. I | -. i C_ j } ) = ( TopSet ` S ) )
22 3 21 syl5eq 
 |-  ( R e. V -> J = ( TopSet ` S ) )