This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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