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)

	Ref	Expression
Hypotheses	mnringnmulrd.1	|- F = ( R MndRing M )
	mnringnmulrd.2	|- E = Slot N
	mnringnmulrd.3	|- N e. NN
	mnringnmulrd.4	|- N =/= ( .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 N
3		mnringnmulrd.3	|- N e. NN
4		mnringnmulrd.4	|- N =/= ( .r ` ndx )
5		mnringnmulrd.5	|- A = ( Base ` M )
6		mnringnmulrd.6	|- V = ( R freeLMod A )
7		mnringnmulrd.7	|- ( ph -> R e. U )
8		mnringnmulrd.8	|- ( ph -> M e. W )
9	2 3	ndxid	|- E = Slot ( E ` ndx )
10	2 3	ndxarg	|- ( E ` ndx ) = N
11	10 4	eqnetri	|- ( E ` ndx ) =/= ( .r ` ndx )
12	9 11	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 ) ) ) ) ) ) >. ) )
13		eqid	|- ( .r ` R ) = ( .r ` R )
14		eqid	|- ( 0g ` R ) = ( 0g ` R )
15		eqid	|- ( +g ` M ) = ( +g ` M )
16		eqid	|- ( Base ` V ) = ( Base ` V )
17	1 13 14 5 15 6 16 7 8	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 ) ) ) ) ) ) >. ) )
18	17	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 ) ) ) ) ) ) >. ) ) )
19	12 18	eqtr4id	|- ( ph -> ( E ` V ) = ( E ` F ) )