Theorem rlmlsm

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

	Ref	Expression
Assertion	rlmlsm	$$⊢R\in V\to \mathrm{LSSum}\left(R\right)=\mathrm{LSSum}\left(\mathrm{ringLMod}\left(R\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
2		eqid	$$⊢{+}_R={+}_R$$
3		eqid	$$⊢\mathrm{LSSum}\left(R\right)=\mathrm{LSSum}\left(R\right)$$
4	1 2 3	lsmfval	$$⊢R\in V\to \mathrm{LSSum}\left(R\right)=\left(t\in 𝒫{\mathrm{Base}}_R,u\in 𝒫{\mathrm{Base}}_R⟼\mathrm{ran}\left(x\in t,y\in u⟼x{+}_{R}y\right)\right)$$
5		fvex	$$⊢\mathrm{ringLMod}\left(R\right)\in \mathrm{V}$$
6		rlmbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
7		rlmplusg	$$⊢{+}_R={+}_{\mathrm{ringLMod}\left(R\right)}$$
8		eqid	$$⊢\mathrm{LSSum}\left(\mathrm{ringLMod}\left(R\right)\right)=\mathrm{LSSum}\left(\mathrm{ringLMod}\left(R\right)\right)$$
9	6 7 8	lsmfval	$$⊢\mathrm{ringLMod}\left(R\right)\in \mathrm{V}\to \mathrm{LSSum}\left(\mathrm{ringLMod}\left(R\right)\right)=\left(t\in 𝒫{\mathrm{Base}}_R,u\in 𝒫{\mathrm{Base}}_R⟼\mathrm{ran}\left(x\in t,y\in u⟼x{+}_{R}y\right)\right)$$
10	5 9	mp1i	$$⊢R\in V\to \mathrm{LSSum}\left(\mathrm{ringLMod}\left(R\right)\right)=\left(t\in 𝒫{\mathrm{Base}}_R,u\in 𝒫{\mathrm{Base}}_R⟼\mathrm{ran}\left(x\in t,y\in u⟼x{+}_{R}y\right)\right)$$
11	4 10	eqtr4d	$$⊢R\in V\to \mathrm{LSSum}\left(R\right)=\mathrm{LSSum}\left(\mathrm{ringLMod}\left(R\right)\right)$$