Theorem mnringnmulrd

Description: Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024) (Revised by AV, 1-Nov-2024)

	Ref	Expression
Hypotheses	mnringnmulrd.1	|- F = ( R MndRing M )
	mnringnmulrd.2	|- E = Slot ( E ` ndx )
	mnringnmulrd.4	|- ( E ` ndx ) =/= ( .r ` ndx )
	mnringnmulrd.5	|- A = ( Base ` M )
	mnringnmulrd.6	|- V = ( R freeLMod A )
	mnringnmulrd.7	|- ( ph -> R e. U )
	mnringnmulrd.8	|- ( ph -> M e. W )
Assertion	mnringnmulrd	|- ( ph -> ( E ` V ) = ( E ` F ) )

Proof

Step	Hyp	Ref	Expression
1		mnringnmulrd.1	|- F = ( R MndRing M )
2		mnringnmulrd.2	|- E = Slot ( E ` ndx )
3		mnringnmulrd.4	|- ( E ` ndx ) =/= ( .r ` ndx )
4		mnringnmulrd.5	|- A = ( Base ` M )
5		mnringnmulrd.6	|- V = ( R freeLMod A )
6		mnringnmulrd.7	|- ( ph -> R e. U )
7		mnringnmulrd.8	|- ( ph -> M e. W )
8	2 3	setsnid	|- ( E ` V ) = ( E ` ( V sSet <. ( .r ` ndx ) , ( x e. ( Base ` V ) , y e. ( Base ` V ) |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( x ` a ) ( .r ` R ) ( y ` b ) ) , ( 0g ` R ) ) ) ) ) ) >. ) )
9		eqid	|- ( .r ` R ) = ( .r ` R )
10		eqid	|- ( 0g ` R ) = ( 0g ` R )
11		eqid	|- ( +g ` M ) = ( +g ` M )
12		eqid	|- ( Base ` V ) = ( Base ` V )
13	1 9 10 4 11 5 12 6 7	mnringvald	|- ( ph -> F = ( V sSet <. ( .r ` ndx ) , ( x e. ( Base ` V ) , y e. ( Base ` V ) |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( x ` a ) ( .r ` R ) ( y ` b ) ) , ( 0g ` R ) ) ) ) ) ) >. ) )
14	13	fveq2d	|- ( ph -> ( E ` F ) = ( E ` ( V sSet <. ( .r ` ndx ) , ( x e. ( Base ` V ) , y e. ( Base ` V ) |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( x ` a ) ( .r ` R ) ( y ` b ) ) , ( 0g ` R ) ) ) ) ) ) >. ) ) )
15	8 14	eqtr4id	|- ( ph -> ( E ` V ) = ( E ` F ) )