Theorem mnringvscad

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

	Ref	Expression
Hypotheses	mnringvscad.1	|- F = ( R MndRing M )
	mnringvscad.2	|- B = ( Base ` M )
	mnringvscad.3	|- V = ( R freeLMod B )
	mnringvscad.4	|- ( ph -> R e. U )
	mnringvscad.5	|- ( ph -> M e. W )
Assertion	mnringvscad	|- ( ph -> ( .s ` V ) = ( .s ` F ) )

Proof

Step	Hyp	Ref	Expression
1		mnringvscad.1	|- F = ( R MndRing M )
2		mnringvscad.2	|- B = ( Base ` M )
3		mnringvscad.3	|- V = ( R freeLMod B )
4		mnringvscad.4	|- ( ph -> R e. U )
5		mnringvscad.5	|- ( ph -> M e. W )
6		df-vsca	|- .s = Slot 6
7		6nn	|- 6 e. NN
8		3re	|- 3 e. RR
9		3lt6	|- 3 < 6
10	8 9	gtneii	|- 6 =/= 3
11		mulrndx	|- ( .r ` ndx ) = 3
12	10 11	neeqtrri	|- 6 =/= ( .r ` ndx )
13	1 6 7 12 2 3 4 5	mnringnmulrd	|- ( ph -> ( .s ` V ) = ( .s ` F ) )