Metamath Proof Explorer


Theorem mnringaddgd

Description: The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024) (Proof shortened by AV, 1-Nov-2024)

Ref Expression
Hypotheses mnringaddgd.1 𝐹 = ( 𝑅 MndRing 𝑀 )
mnringaddgd.2 𝐴 = ( Base ‘ 𝑀 )
mnringaddgd.3 𝑉 = ( 𝑅 freeLMod 𝐴 )
mnringaddgd.4 ( 𝜑𝑅𝑈 )
mnringaddgd.5 ( 𝜑𝑀𝑊 )
Assertion mnringaddgd ( 𝜑 → ( +g𝑉 ) = ( +g𝐹 ) )

Proof

Step Hyp Ref Expression
1 mnringaddgd.1 𝐹 = ( 𝑅 MndRing 𝑀 )
2 mnringaddgd.2 𝐴 = ( Base ‘ 𝑀 )
3 mnringaddgd.3 𝑉 = ( 𝑅 freeLMod 𝐴 )
4 mnringaddgd.4 ( 𝜑𝑅𝑈 )
5 mnringaddgd.5 ( 𝜑𝑀𝑊 )
6 plusgid +g = Slot ( +g ‘ ndx )
7 plusgndxnmulrndx ( +g ‘ ndx ) ≠ ( .r ‘ ndx )
8 1 6 7 2 3 4 5 mnringnmulrd ( 𝜑 → ( +g𝑉 ) = ( +g𝐹 ) )