Theorem mnringvscad

Description: The scalar product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024)

	Ref	Expression
Hypotheses	mnringvscad.1	No typesetting found for |- F = ( R MndRing M ) with typecode |-
	mnringvscad.2	$$⊢B={\mathrm{Base}}_M$$
	mnringvscad.3	$$⊢V=R\mathrm{freeLMod}B$$
	mnringvscad.4	$$⊢\phi \to R\in U$$
	mnringvscad.5	$$⊢\phi \to M\in W$$
Assertion	mnringvscad	$$⊢\phi \to {\cdot }_V={\cdot }_F$$

Proof

Step	Hyp	Ref	Expression
1		mnringvscad.1	Could not format F = ( R MndRing M ) : No typesetting found for |- F = ( R MndRing M ) with typecode |-
2		mnringvscad.2	$$⊢B={\mathrm{Base}}_M$$
3		mnringvscad.3	$$⊢V=R\mathrm{freeLMod}B$$
4		mnringvscad.4	$$⊢\phi \to R\in U$$
5		mnringvscad.5	$$⊢\phi \to M\in W$$
6		df-vsca	$$⊢{\cdot }_{𝑠}=\mathrm{Slot}6$$
7		6nn	$$⊢6\in \mathbb{N}$$
8		3re	$$⊢3\in ℝ$$
9		3lt6	$$⊢3<6$$
10	8 9	gtneii	$$⊢6\ne 3$$
11		mulrndx	$$⊢{\cdot }_{\mathrm{ndx}}=3$$
12	10 11	neeqtrri	$$⊢6\ne {\cdot }_{\mathrm{ndx}}$$
13	1 6 7 12 2 3 4 5	mnringnmulrd	$$⊢\phi \to {\cdot }_V={\cdot }_F$$