Metamath Proof Explorer

Theorem mnringnmulrdOLD

Description: Obsolete version of mnringnmulrd as of 1-Nov-2024. Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 mnringnmulrdOLD.1 
 |-  F = ( R MndRing M )
2 mnringnmulrdOLD.2 
 |-  E = Slot N
3 mnringnmulrdOLD.3 
 |-  N e. NN
4 mnringnmulrdOLD.4 
 |-  N =/= ( .r ` ndx )
5 mnringnmulrdOLD.5 
 |-  A = ( Base ` M )
6 mnringnmulrdOLD.6 
 |-  V = ( R freeLMod A )
7 mnringnmulrdOLD.7 
 |-  ( ph -> R e. U )
8 mnringnmulrdOLD.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 ) )