Theorem mplascl1

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

	Ref	Expression
Hypotheses	mplascl1.w	|- W = ( I mPoly R )
	mplascl1.a	|- A = ( algSc ` W )
	mplascl1.o	|- O = ( 1r ` R )
	mplascl1.1	|- .1. = ( 1r ` W )
	mplascl1.i	|- ( ph -> I e. V )
	mplascl1.r	|- ( ph -> R e. Ring )
Assertion	mplascl1	|- ( ph -> ( A ` O ) = .1. )

Proof

Step	Hyp	Ref	Expression
1		mplascl1.w	|- W = ( I mPoly R )
2		mplascl1.a	|- A = ( algSc ` W )
3		mplascl1.o	|- O = ( 1r ` R )
4		mplascl1.1	|- .1. = ( 1r ` W )
5		mplascl1.i	|- ( ph -> I e. V )
6		mplascl1.r	|- ( ph -> R e. Ring )
7	1 5 6	mplsca	|- ( ph -> R = ( Scalar ` W ) )
8	7	fveq2d	|- ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` W ) ) )
9	3 8	eqtrid	|- ( ph -> O = ( 1r ` ( Scalar ` W ) ) )
10	9	fveq2d	|- ( ph -> ( A ` O ) = ( A ` ( 1r ` ( Scalar ` W ) ) ) )
11		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
12	1 5 6	mpllmodd	|- ( ph -> W e. LMod )
13	1 5 6	mplringd	|- ( ph -> W e. Ring )
14	2 11 12 13	ascl1	|- ( ph -> ( A ` ( 1r ` ( Scalar ` W ) ) ) = ( 1r ` W ) )
15	10 14	eqtrd	|- ( ph -> ( A ` O ) = ( 1r ` W ) )
16	15 4	eqtr4di	|- ( ph -> ( A ` O ) = .1. )