Theorem mplascl1

Description: The one scalar as a polynomial. (Contributed by SN, 12-Mar-2025)

	Ref	Expression
Hypotheses	mplascl1.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
	mplascl1.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	mplascl1.o	⊢ 𝑂 = ( 1r ‘ 𝑅 )
	mplascl1.1	⊢ 1 = ( 1r ‘ 𝑊 )
	mplascl1.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mplascl1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion	mplascl1	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑂 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		mplascl1.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
2		mplascl1.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
3		mplascl1.o	⊢ 𝑂 = ( 1r ‘ 𝑅 )
4		mplascl1.1	⊢ 1 = ( 1r ‘ 𝑊 )
5		mplascl1.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		mplascl1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7	1 5 6	mplsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑊 ) )
8	7	fveq2d	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) )
9	3 8	eqtrid	⊢ ( 𝜑 → 𝑂 = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) )
10	9	fveq2d	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑂 ) = ( 𝐴 ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) )
11		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
12	1 5 6	mpllmodd	⊢ ( 𝜑 → 𝑊 ∈ LMod )
13	1 5 6	mplringd	⊢ ( 𝜑 → 𝑊 ∈ Ring )
14	2 11 12 13	ascl1	⊢ ( 𝜑 → ( 𝐴 ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 1r ‘ 𝑊 ) )
15	10 14	eqtrd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑂 ) = ( 1r ‘ 𝑊 ) )
16	15 4	eqtr4di	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑂 ) = 1 )