Theorem mnringscad

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

	Ref	Expression
Hypotheses	mnringscad.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
	mnringscad.2	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
	mnringscad.3	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
Assertion	mnringscad	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		mnringscad.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
2		mnringscad.2	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
3		mnringscad.3	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
4		fvex	⊢ ( Base ‘ 𝑀 ) ∈ V
5		eqid	⊢ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) = ( 𝑅 freeLMod ( Base ‘ 𝑀 ) )
6	5	frlmsca	⊢ ( ( 𝑅 ∈ 𝑈 ∧ ( Base ‘ 𝑀 ) ∈ V ) → 𝑅 = ( Scalar ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) )
7	2 4 6	sylancl	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) )
8		scaid	⊢ Scalar = Slot ( Scalar ‘ ndx )
9		scandxnmulrndx	⊢ ( Scalar ‘ ndx ) ≠ ( .r ‘ ndx )
10		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
11	1 8 9 10 5 2 3	mnringnmulrd	⊢ ( 𝜑 → ( Scalar ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) = ( Scalar ‘ 𝐹 ) )
12	7 11	eqtrd	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝐹 ) )