Metamath Proof Explorer

Theorem mnringvald

Description: Value of the monoid ring function. (Contributed by Rohan Ridenour, 14-May-2024)

Ref Expression
Hypotheses mnringvald.1 
|- F = ( R MndRing M )
mnringvald.2 
|- .x. = ( .r ` R )
mnringvald.3 
|- .0. = ( 0g ` R )
mnringvald.4 
|- A = ( Base ` M )
mnringvald.5 
|- .+ = ( +g ` M )
mnringvald.6 
|- V = ( R freeLMod A )
mnringvald.7 
|- B = ( Base ` V )
mnringvald.8 
|- ( ph -> R e. U )
mnringvald.9 
|- ( ph -> M e. W )
Assertion mnringvald 
|- ( ph -> F = ( V sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) )

Proof

Step Hyp Ref Expression
1 mnringvald.1 
 |-  F = ( R MndRing M )
2 mnringvald.2 
 |-  .x. = ( .r ` R )
3 mnringvald.3 
 |-  .0. = ( 0g ` R )
4 mnringvald.4 
 |-  A = ( Base ` M )
5 mnringvald.5 
 |-  .+ = ( +g ` M )
6 mnringvald.6 
 |-  V = ( R freeLMod A )
7 mnringvald.7 
 |-  B = ( Base ` V )
8 mnringvald.8 
 |-  ( ph -> R e. U )
9 mnringvald.9 
 |-  ( ph -> M e. W )
10 8 elexd 
 |-  ( ph -> R e. _V )
11 9 elexd 
 |-  ( ph -> M e. _V )
12 nfv 
 |-  F/ v ( r = R /\ m = M )
13 nfcvd 
 |-  ( ( r = R /\ m = M ) -> F/_ v ( V sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) )
14 ovexd 
 |-  ( ( r = R /\ m = M ) -> ( r freeLMod ( Base ` m ) ) e. _V )
15 simpr 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> v = ( r freeLMod ( Base ` m ) ) )
16 simpll 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> r = R )
17 fveq2 
 |-  ( m = M -> ( Base ` m ) = ( Base ` M ) )
18 17 4 eqtr4di 
 |-  ( m = M -> ( Base ` m ) = A )
19 18 ad2antlr 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> ( Base ` m ) = A )
20 16 19 oveq12d 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> ( r freeLMod ( Base ` m ) ) = ( R freeLMod A ) )
21 15 20 eqtrd 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> v = ( R freeLMod A ) )
22 21 6 eqtr4di 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> v = V )
23 22 fveq2d 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> ( Base ` v ) = ( Base ` V ) )
24 23 7 eqtr4di 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> ( Base ` v ) = B )
25 fveq2 
 |-  ( m = M -> ( +g ` m ) = ( +g ` M ) )
26 25 5 eqtr4di 
 |-  ( m = M -> ( +g ` m ) = .+ )
27 26 oveqd 
 |-  ( m = M -> ( a ( +g ` m ) b ) = ( a .+ b ) )
28 27 ad2antlr 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> ( a ( +g ` m ) b ) = ( a .+ b ) )
29 28 eqeq2d 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> ( i = ( a ( +g ` m ) b ) <-> i = ( a .+ b ) ) )
30 fveq2 
 |-  ( r = R -> ( .r ` r ) = ( .r ` R ) )
31 30 2 eqtr4di 
 |-  ( r = R -> ( .r ` r ) = .x. )
32 31 oveqd 
 |-  ( r = R -> ( ( x ` a ) ( .r ` r ) ( y ` b ) ) = ( ( x ` a ) .x. ( y ` b ) ) )
33 32 ad2antrr 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> ( ( x ` a ) ( .r ` r ) ( y ` b ) ) = ( ( x ` a ) .x. ( y ` b ) ) )
34 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
35 34 3 eqtr4di 
 |-  ( r = R -> ( 0g ` r ) = .0. )
36 35 ad2antrr 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> ( 0g ` r ) = .0. )
37 29 33 36 ifbieq12d 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> if ( i = ( a ( +g ` m ) b ) , ( ( x ` a ) ( .r ` r ) ( y ` b ) ) , ( 0g ` r ) ) = if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) )
38 19 37 mpteq12dv 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> ( i e. ( Base ` m ) |-> if ( i = ( a ( +g ` m ) b ) , ( ( x ` a ) ( .r ` r ) ( y ` b ) ) , ( 0g ` r ) ) ) = ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) )
39 19 19 38 mpoeq123dv 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> ( a e. ( Base ` m ) , b e. ( Base ` m ) |-> ( i e. ( Base ` m ) |-> if ( i = ( a ( +g ` m ) b ) , ( ( x ` a ) ( .r ` r ) ( y ` b ) ) , ( 0g ` r ) ) ) ) = ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) )
40 22 39 oveq12d 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> ( v gsum ( a e. ( Base ` m ) , b e. ( Base ` m ) |-> ( i e. ( Base ` m ) |-> if ( i = ( a ( +g ` m ) b ) , ( ( x ` a ) ( .r ` r ) ( y ` b ) ) , ( 0g ` r ) ) ) ) ) = ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) )
41 24 24 40 mpoeq123dv 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> ( x e. ( Base ` v ) , y e. ( Base ` v ) |-> ( v gsum ( a e. ( Base ` m ) , b e. ( Base ` m ) |-> ( i e. ( Base ` m ) |-> if ( i = ( a ( +g ` m ) b ) , ( ( x ` a ) ( .r ` r ) ( y ` b ) ) , ( 0g ` r ) ) ) ) ) ) = ( x e. B , y e. B |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) )
42 41 opeq2d 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> <. ( .r ` ndx ) , ( x e. ( Base ` v ) , y e. ( Base ` v ) |-> ( v gsum ( a e. ( Base ` m ) , b e. ( Base ` m ) |-> ( i e. ( Base ` m ) |-> if ( i = ( a ( +g ` m ) b ) , ( ( x ` a ) ( .r ` r ) ( y ` b ) ) , ( 0g ` r ) ) ) ) ) ) >. = <. ( .r ` ndx ) , ( x e. B , y e. B |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. )
43 22 42 oveq12d 
 |-  ( ( ( r = R /\ m = M ) /\ v = ( r freeLMod ( Base ` m ) ) ) -> ( v sSet <. ( .r ` ndx ) , ( x e. ( Base ` v ) , y e. ( Base ` v ) |-> ( v gsum ( a e. ( Base ` m ) , b e. ( Base ` m ) |-> ( i e. ( Base ` m ) |-> if ( i = ( a ( +g ` m ) b ) , ( ( x ` a ) ( .r ` r ) ( y ` b ) ) , ( 0g ` r ) ) ) ) ) ) >. ) = ( V sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) )
44 12 13 14 43 csbiedf 
 |-  ( ( r = R /\ m = M ) -> [_ ( r freeLMod ( Base ` m ) ) / v ]_ ( v sSet <. ( .r ` ndx ) , ( x e. ( Base ` v ) , y e. ( Base ` v ) |-> ( v gsum ( a e. ( Base ` m ) , b e. ( Base ` m ) |-> ( i e. ( Base ` m ) |-> if ( i = ( a ( +g ` m ) b ) , ( ( x ` a ) ( .r ` r ) ( y ` b ) ) , ( 0g ` r ) ) ) ) ) ) >. ) = ( V sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) )
45 df-mnring 
 |-  MndRing = ( r e. _V , m e. _V |-> [_ ( r freeLMod ( Base ` m ) ) / v ]_ ( v sSet <. ( .r ` ndx ) , ( x e. ( Base ` v ) , y e. ( Base ` v ) |-> ( v gsum ( a e. ( Base ` m ) , b e. ( Base ` m ) |-> ( i e. ( Base ` m ) |-> if ( i = ( a ( +g ` m ) b ) , ( ( x ` a ) ( .r ` r ) ( y ` b ) ) , ( 0g ` r ) ) ) ) ) ) >. ) )
46 ovex 
 |-  ( V sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) e. _V
47 44 45 46 ovmpoa 
 |-  ( ( R e. _V /\ M e. _V ) -> ( R MndRing M ) = ( V sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) )
48 10 11 47 syl2anc 
 |-  ( ph -> ( R MndRing M ) = ( V sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) )
49 1 48 eqtrid 
 |-  ( ph -> F = ( V sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) )