Theorem mnringmulrvald

Description: Value of multiplication in a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		mnringmulrvald.1	|- F = ( R MndRing M )
2		mnringmulrvald.2	|- B = ( Base ` F )
3		mnringmulrvald.3	|- .xb = ( .r ` R )
4		mnringmulrvald.4	|- .0b = ( 0g ` R )
5		mnringmulrvald.5	|- A = ( Base ` M )
6		mnringmulrvald.6	|- .+ = ( +g ` M )
7		mnringmulrvald.7	|- .x. = ( .r ` F )
8		mnringmulrvald.8	|- ( ph -> R e. U )
9		mnringmulrvald.9	|- ( ph -> M e. W )
10		mnringmulrvald.10	|- ( ph -> X e. B )
11		mnringmulrvald.11	|- ( ph -> Y e. B )
12	1 2 3 4 5 6 8 9	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 ) .xb ( y ` b ) ) , .0b ) ) ) ) ) = ( .r ` F ) )
13	12 7	eqtr4di	|- ( ph -> ( x e. B , y e. B |-> ( F gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .xb ( y ` b ) ) , .0b ) ) ) ) ) = .x. )
14	13	eqcomd	|- ( ph -> .x. = ( x e. B , y e. B |-> ( F gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .xb ( y ` b ) ) , .0b ) ) ) ) ) )
15		fveq1	|- ( x = X -> ( x ` a ) = ( X ` a ) )
16		fveq1	|- ( y = Y -> ( y ` b ) = ( Y ` b ) )
17	15 16	oveqan12d	|- ( ( x = X /\ y = Y ) -> ( ( x ` a ) .xb ( y ` b ) ) = ( ( X ` a ) .xb ( Y ` b ) ) )
18	17	ifeq1d	|- ( ( x = X /\ y = Y ) -> if ( i = ( a .+ b ) , ( ( x ` a ) .xb ( y ` b ) ) , .0b ) = if ( i = ( a .+ b ) , ( ( X ` a ) .xb ( Y ` b ) ) , .0b ) )
19	18	mpteq2dv	|- ( ( x = X /\ y = Y ) -> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .xb ( y ` b ) ) , .0b ) ) = ( i e. A |-> if ( i = ( a .+ b ) , ( ( X ` a ) .xb ( Y ` b ) ) , .0b ) ) )
20	19	mpoeq3dv	|- ( ( x = X /\ y = Y ) -> ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .xb ( y ` b ) ) , .0b ) ) ) = ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( X ` a ) .xb ( Y ` b ) ) , .0b ) ) ) )
21	20	oveq2d	|- ( ( x = X /\ y = Y ) -> ( F gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .xb ( y ` b ) ) , .0b ) ) ) ) = ( F gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( X ` a ) .xb ( Y ` b ) ) , .0b ) ) ) ) )
22	21	adantl	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( F gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .xb ( y ` b ) ) , .0b ) ) ) ) = ( F gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( X ` a ) .xb ( Y ` b ) ) , .0b ) ) ) ) )
23		ovexd	|- ( ph -> ( F gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( X ` a ) .xb ( Y ` b ) ) , .0b ) ) ) ) e. _V )
24	14 22 10 11 23	ovmpod	|- ( ph -> ( X .x. Y ) = ( F gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( X ` a ) .xb ( Y ` b ) ) , .0b ) ) ) ) )