Metamath Proof Explorer


Theorem mnringaddgd

Description: The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-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 df-plusg +g = Slot 2
7 2nn 2 ∈ ℕ
8 2re 2 ∈ ℝ
9 2lt3 2 < 3
10 8 9 ltneii 2 ≠ 3
11 mulrndx ( .r ‘ ndx ) = 3
12 10 11 neeqtrri 2 ≠ ( .r ‘ ndx )
13 1 6 7 12 2 3 4 5 mnringnmulrd ( 𝜑 → ( +g𝑉 ) = ( +g𝐹 ) )