Metamath Proof Explorer

Theorem mnringmulrd

Description: The ring product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024)

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

Proof

Step Hyp Ref Expression
1 mnringmulrd.1 
 |-  F = ( R MndRing M )
2 mnringmulrd.2 
 |-  B = ( Base ` F )
3 mnringmulrd.3 
 |-  .x. = ( .r ` R )
4 mnringmulrd.4 
 |-  .0. = ( 0g ` R )
5 mnringmulrd.5 
 |-  A = ( Base ` M )
6 mnringmulrd.6 
 |-  .+ = ( +g ` M )
7 mnringmulrd.7 
 |-  ( ph -> R e. U )
8 mnringmulrd.8 
 |-  ( ph -> M e. W )
9 eqid 
 |-  ( R freeLMod A ) = ( R freeLMod A )
10 1 2 5 9 7 8 mnringbaserd 
 |-  ( ph -> B = ( Base ` ( R freeLMod A ) ) )
11 5 fvexi 
 |-  A e. _V
12 11 11 mpoex 
 |-  ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) e. _V
13 12 a1i 
 |-  ( ph -> ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) e. _V )
14 1 ovexi 
 |-  F e. _V
15 14 a1i 
 |-  ( ph -> F e. _V )
16 ovex 
 |-  ( R freeLMod A ) e. _V
17 16 a1i 
 |-  ( ph -> ( R freeLMod A ) e. _V )
18 2 10 eqtr3id 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( R freeLMod A ) ) )
19 1 5 9 7 8 mnringaddgd 
 |-  ( ph -> ( +g ` ( R freeLMod A ) ) = ( +g ` F ) )
20 19 eqcomd 
 |-  ( ph -> ( +g ` F ) = ( +g ` ( R freeLMod A ) ) )
21 13 15 17 18 20 gsumpropd 
 |-  ( ph -> ( F gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) = ( ( R freeLMod A ) gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) )
22 10 10 21 mpoeq123dv 
 |-  ( ph -> ( x e. B , y e. B |-> ( F gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) = ( x e. ( Base ` ( R freeLMod A ) ) , y e. ( Base ` ( R freeLMod A ) ) |-> ( ( R freeLMod A ) gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) )
23 fvex 
 |-  ( Base ` ( R freeLMod A ) ) e. _V
24 23 23 mpoex 
 |-  ( x e. ( Base ` ( R freeLMod A ) ) , y e. ( Base ` ( R freeLMod A ) ) |-> ( ( R freeLMod A ) gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) e. _V
25 mulrid 
 |-  .r = Slot ( .r ` ndx )
26 25 setsid 
 |-  ( ( ( R freeLMod A ) e. _V /\ ( x e. ( Base ` ( R freeLMod A ) ) , y e. ( Base ` ( R freeLMod A ) ) |-> ( ( R freeLMod A ) gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) e. _V ) -> ( x e. ( Base ` ( R freeLMod A ) ) , y e. ( Base ` ( R freeLMod A ) ) |-> ( ( R freeLMod A ) gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) = ( .r ` ( ( R freeLMod A ) sSet <. ( .r ` ndx ) , ( x e. ( Base ` ( R freeLMod A ) ) , y e. ( Base ` ( R freeLMod A ) ) |-> ( ( R freeLMod A ) gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) ) )
27 16 24 26 mp2an 
 |-  ( x e. ( Base ` ( R freeLMod A ) ) , y e. ( Base ` ( R freeLMod A ) ) |-> ( ( R freeLMod A ) gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) = ( .r ` ( ( R freeLMod A ) sSet <. ( .r ` ndx ) , ( x e. ( Base ` ( R freeLMod A ) ) , y e. ( Base ` ( R freeLMod A ) ) |-> ( ( R freeLMod A ) gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) )
28 eqid 
 |-  ( Base ` ( R freeLMod A ) ) = ( Base ` ( R freeLMod A ) )
29 1 3 4 5 6 9 28 7 8 mnringvald 
 |-  ( ph -> F = ( ( R freeLMod A ) sSet <. ( .r ` ndx ) , ( x e. ( Base ` ( R freeLMod A ) ) , y e. ( Base ` ( R freeLMod A ) ) |-> ( ( R freeLMod A ) gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) )
30 29 fveq2d 
 |-  ( ph -> ( .r ` F ) = ( .r ` ( ( R freeLMod A ) sSet <. ( .r ` ndx ) , ( x e. ( Base ` ( R freeLMod A ) ) , y e. ( Base ` ( R freeLMod A ) ) |-> ( ( R freeLMod A ) gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) ) )
31 27 30 eqtr4id 
 |-  ( ph -> ( x e. ( Base ` ( R freeLMod A ) ) , y e. ( Base ` ( R freeLMod A ) ) |-> ( ( R freeLMod A ) gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) = ( .r ` F ) )
32 22 31 eqtrd 
 |-  ( ph -> ( x e. B , y e. B |-> ( F gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) = ( .r ` F ) )