Metamath Proof Explorer


Theorem idlsrgval

Description: Lemma for idlsrgbas through idlsrgtset . (Contributed by Thierry Arnoux, 1-Jun-2024)

Ref Expression
Hypotheses idlsrgval.1 I = LIdeal R
idlsrgval.2 ˙ = LSSum R
idlsrgval.3 G = mulGrp R
idlsrgval.4 ˙ = LSSum G
Assertion idlsrgval Could not format assertion : No typesetting found for |- ( R e. V -> ( IDLsrg ` R ) = ( { <. ( Base ` ndx ) , I >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , ( i e. I , j e. I |-> ( ( RSpan ` R ) ` ( i .(x) 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 |-

Proof

Step Hyp Ref Expression
1 idlsrgval.1 I = LIdeal R
2 idlsrgval.2 ˙ = LSSum R
3 idlsrgval.3 G = mulGrp R
4 idlsrgval.4 ˙ = LSSum G
5 elex R V R V
6 fvexd r = R LIdeal r V
7 simpr r = R b = LIdeal r b = LIdeal r
8 simpl r = R b = LIdeal r r = R
9 8 fveq2d r = R b = LIdeal r LIdeal r = LIdeal R
10 7 9 eqtrd r = R b = LIdeal r b = LIdeal R
11 10 1 eqtr4di r = R b = LIdeal r b = I
12 11 opeq2d r = R b = LIdeal r Base ndx b = Base ndx I
13 8 fveq2d r = R b = LIdeal r LSSum r = LSSum R
14 13 2 eqtr4di r = R b = LIdeal r LSSum r = ˙
15 14 opeq2d r = R b = LIdeal r + ndx LSSum r = + ndx ˙
16 8 fveq2d r = R b = LIdeal r RSpan r = RSpan R
17 8 fveq2d r = R b = LIdeal r mulGrp r = mulGrp R
18 17 3 eqtr4di r = R b = LIdeal r mulGrp r = G
19 18 fveq2d r = R b = LIdeal r LSSum mulGrp r = LSSum G
20 19 4 eqtr4di r = R b = LIdeal r LSSum mulGrp r = ˙
21 20 oveqd r = R b = LIdeal r i LSSum mulGrp r j = i ˙ j
22 16 21 fveq12d r = R b = LIdeal r RSpan r i LSSum mulGrp r j = RSpan R i ˙ j
23 11 11 22 mpoeq123dv r = R b = LIdeal r i b , j b RSpan r i LSSum mulGrp r j = i I , j I RSpan R i ˙ j
24 23 opeq2d r = R b = LIdeal r ndx i b , j b RSpan r i LSSum mulGrp r j = ndx i I , j I RSpan R i ˙ j
25 12 15 24 tpeq123d r = R b = LIdeal r Base ndx b + ndx LSSum r ndx i b , j b RSpan r i LSSum mulGrp r j = Base ndx I + ndx ˙ ndx i I , j I RSpan R i ˙ j
26 11 rabeqdv r = R b = LIdeal r j b | ¬ i j = j I | ¬ i j
27 11 26 mpteq12dv r = R b = LIdeal r i b j b | ¬ i j = i I j I | ¬ i j
28 27 rneqd r = R b = LIdeal r ran i b j b | ¬ i j = ran i I j I | ¬ i j
29 28 opeq2d r = R b = LIdeal r TopSet ndx ran i b j b | ¬ i j = TopSet ndx ran i I j I | ¬ i j
30 11 sseq2d r = R b = LIdeal r i j b i j I
31 30 anbi1d r = R b = LIdeal r i j b i j i j I i j
32 31 opabbidv r = R b = LIdeal r i j | i j b i j = i j | i j I i j
33 32 opeq2d r = R b = LIdeal r ndx i j | i j b i j = ndx i j | i j I i j
34 29 33 preq12d r = R b = LIdeal r TopSet ndx ran i b j b | ¬ i j ndx i j | i j b i j = TopSet ndx ran i I j I | ¬ i j ndx i j | i j I i j
35 25 34 uneq12d r = R b = LIdeal r Base ndx b + ndx LSSum r ndx i b , j b RSpan r i LSSum mulGrp r j TopSet ndx ran i b j b | ¬ i j ndx i j | i j b i j = Base ndx I + ndx ˙ ndx i I , j I RSpan R i ˙ j TopSet ndx ran i I j I | ¬ i j ndx i j | i j I i j
36 6 35 csbied r = R LIdeal r / b Base ndx b + ndx LSSum r ndx i b , j b RSpan r i LSSum mulGrp r j TopSet ndx ran i b j b | ¬ i j ndx i j | i j b i j = Base ndx I + ndx ˙ ndx i I , j I RSpan R i ˙ j TopSet ndx ran i I j I | ¬ i j ndx i j | i j I i j
37 df-idlsrg Could not format IDLsrg = ( r e. _V |-> [_ ( LIdeal ` r ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( LSSum ` r ) >. , <. ( .r ` ndx ) , ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) 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 ) } >. } ) ) : No typesetting found for |- IDLsrg = ( r e. _V |-> [_ ( LIdeal ` r ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( LSSum ` r ) >. , <. ( .r ` ndx ) , ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) 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 ) } >. } ) ) with typecode |-
38 tpex Base ndx I + ndx ˙ ndx i I , j I RSpan R i ˙ j V
39 prex TopSet ndx ran i I j I | ¬ i j ndx i j | i j I i j V
40 38 39 unex Base ndx I + ndx ˙ ndx i I , j I RSpan R i ˙ j TopSet ndx ran i I j I | ¬ i j ndx i j | i j I i j V
41 36 37 40 fvmpt Could not format ( R e. _V -> ( IDLsrg ` R ) = ( { <. ( Base ` ndx ) , I >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , ( i e. I , j e. I |-> ( ( RSpan ` R ) ` ( i .(x) 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 ) , .(+) >. , <. ( .r ` ndx ) , ( i e. I , j e. I |-> ( ( RSpan ` R ) ` ( i .(x) 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 |-
42 5 41 syl Could not format ( R e. V -> ( IDLsrg ` R ) = ( { <. ( Base ` ndx ) , I >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , ( i e. I , j e. I |-> ( ( RSpan ` R ) ` ( i .(x) 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 ) , .(+) >. , <. ( .r ` ndx ) , ( i e. I , j e. I |-> ( ( RSpan ` R ) ` ( i .(x) 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 |-