Metamath Proof Explorer


Theorem idlsrgbas

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

Ref Expression
Hypotheses idlsrgbas.1 No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
idlsrgbas.2 I = LIdeal R
Assertion idlsrgbas R V I = Base S

Proof

Step Hyp Ref Expression
1 idlsrgbas.1 Could not format S = ( IDLsrg ` R ) : No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
2 idlsrgbas.2 I = LIdeal R
3 2 fvexi I V
4 eqid Base ndx I + ndx LSSum R ndx i I , j I RSpan R i LSSum mulGrp R j TopSet ndx ran i I j I | ¬ i j ndx i j | i j I i j = Base ndx I + ndx LSSum R ndx i I , j I RSpan R i LSSum mulGrp R j TopSet ndx ran i I j I | ¬ i j ndx i j | i j I i j
5 4 idlsrgstr Base ndx I + ndx LSSum R ndx i I , j I RSpan R i LSSum mulGrp R j TopSet ndx ran i I j I | ¬ i j ndx i j | i j I i j Struct 1 10
6 baseid Base = Slot Base ndx
7 snsstp1 Base ndx I Base ndx I + ndx LSSum R ndx i I , j I RSpan R i LSSum mulGrp R j
8 ssun1 Base ndx I + ndx LSSum R ndx i I , j I RSpan R i LSSum mulGrp R j Base ndx I + ndx LSSum R ndx i I , j I RSpan R i LSSum mulGrp R j TopSet ndx ran i I j I | ¬ i j ndx i j | i j I i j
9 7 8 sstri Base ndx I Base ndx I + ndx LSSum R ndx i I , j I RSpan R i LSSum mulGrp R j TopSet ndx ran i I j I | ¬ i j ndx i j | i j I i j
10 5 6 9 strfv I V I = Base Base ndx I + ndx LSSum R ndx i I , j I RSpan R i LSSum mulGrp R j TopSet ndx ran i I j I | ¬ i j ndx i j | i j I i j
11 3 10 ax-mp I = Base Base ndx I + ndx LSSum R ndx i I , j I RSpan R i LSSum mulGrp R j TopSet ndx ran i I j I | ¬ i j ndx i j | i j I i 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 Could not format ( 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 ) } >. } ) ) : No typesetting found for |- ( 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 ) } >. } ) ) with typecode |-
16 1 15 syl5eq R V S = Base ndx I + ndx LSSum R ndx i I , j I RSpan R i LSSum mulGrp R j TopSet ndx ran i I j I | ¬ i j ndx i j | i j I i j
17 16 fveq2d R V Base S = Base Base ndx I + ndx LSSum R ndx i I , j I RSpan R i LSSum mulGrp R j TopSet ndx ran i I j I | ¬ i j ndx i j | i j I i j
18 11 17 eqtr4id R V I = Base S