Metamath Proof Explorer

Theorem rlmlsm

Description: Subgroup sum of the ring module. (Contributed by Thierry Arnoux, 9-Apr-2024)

Ref Expression
Assertion rlmlsm 
|- ( R e. V -> ( LSSum ` R ) = ( LSSum ` ( ringLMod ` R ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` R ) = ( Base ` R )
2 eqid 
 |-  ( +g ` R ) = ( +g ` R )
3 eqid 
 |-  ( LSSum ` R ) = ( LSSum ` R )
4 1 2 3 lsmfval 
 |-  ( R e. V -> ( LSSum ` R ) = ( t e. ~P ( Base ` R ) , u e. ~P ( Base ` R ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` R ) y ) ) ) )
5 fvex 
 |-  ( ringLMod ` R ) e. _V
6 rlmbas 
 |-  ( Base ` R ) = ( Base ` ( ringLMod ` R ) )
7 rlmplusg 
 |-  ( +g ` R ) = ( +g ` ( ringLMod ` R ) )
8 eqid 
 |-  ( LSSum ` ( ringLMod ` R ) ) = ( LSSum ` ( ringLMod ` R ) )
9 6 7 8 lsmfval 
 |-  ( ( ringLMod ` R ) e. _V -> ( LSSum ` ( ringLMod ` R ) ) = ( t e. ~P ( Base ` R ) , u e. ~P ( Base ` R ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` R ) y ) ) ) )
10 5 9 mp1i 
 |-  ( R e. V -> ( LSSum ` ( ringLMod ` R ) ) = ( t e. ~P ( Base ` R ) , u e. ~P ( Base ` R ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` R ) y ) ) ) )
11 4 10 eqtr4d 
 |-  ( R e. V -> ( LSSum ` R ) = ( LSSum ` ( ringLMod ` R ) ) )