Theorem rlmlsm

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

	Ref	Expression
Assertion	rlmlsm	⊢ ( 𝑅 ∈ 𝑉 → ( LSSum ‘ 𝑅 ) = ( LSSum ‘ ( ringLMod ‘ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
2		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
3		eqid	⊢ ( LSSum ‘ 𝑅 ) = ( LSSum ‘ 𝑅 )
4	1 2 3	lsmfval	⊢ ( 𝑅 ∈ 𝑉 → ( LSSum ‘ 𝑅 ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑅 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑅 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) ) )
5		fvex	⊢ ( ringLMod ‘ 𝑅 ) ∈ V
6		rlmbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
7		rlmplusg	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) )
8		eqid	⊢ ( LSSum ‘ ( ringLMod ‘ 𝑅 ) ) = ( LSSum ‘ ( ringLMod ‘ 𝑅 ) )
9	6 7 8	lsmfval	⊢ ( ( ringLMod ‘ 𝑅 ) ∈ V → ( LSSum ‘ ( ringLMod ‘ 𝑅 ) ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑅 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑅 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) ) )
10	5 9	mp1i	⊢ ( 𝑅 ∈ 𝑉 → ( LSSum ‘ ( ringLMod ‘ 𝑅 ) ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑅 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑅 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) ) )
11	4 10	eqtr4d	⊢ ( 𝑅 ∈ 𝑉 → ( LSSum ‘ 𝑅 ) = ( LSSum ‘ ( ringLMod ‘ 𝑅 ) ) )