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 ) ) )