Theorem ply1ascl1

Description: The multiplicative identity scalar as a univariate polynomial. (Contributed by Thierry Arnoux, 20-Jan-2025)

	Ref	Expression
Hypotheses	ply1ascl1.w	|- W = ( Poly1 ` R )
	ply1ascl1.a	|- A = ( algSc ` W )
	ply1ascl1.i	|- I = ( 1r ` R )
	ply1ascl1.1	|- .1. = ( 1r ` W )
	ply1ascl1.r	|- ( ph -> R e. Ring )
Assertion	ply1ascl1	|- ( ph -> ( A ` I ) = .1. )

Proof

Step	Hyp	Ref	Expression
1		ply1ascl1.w	|- W = ( Poly1 ` R )
2		ply1ascl1.a	|- A = ( algSc ` W )
3		ply1ascl1.i	|- I = ( 1r ` R )
4		ply1ascl1.1	|- .1. = ( 1r ` W )
5		ply1ascl1.r	|- ( ph -> R e. Ring )
6	1	ply1sca	|- ( R e. Ring -> R = ( Scalar ` W ) )
7	5 6	syl	|- ( ph -> R = ( Scalar ` W ) )
8	7	fveq2d	|- ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` W ) ) )
9	3 8	eqtrid	|- ( ph -> I = ( 1r ` ( Scalar ` W ) ) )
10	9	fveq2d	|- ( ph -> ( ( algSc ` W ) ` I ) = ( ( algSc ` W ) ` ( 1r ` ( Scalar ` W ) ) ) )
11		eqid	|- ( algSc ` W ) = ( algSc ` W )
12		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
13	1	ply1lmod	|- ( R e. Ring -> W e. LMod )
14	5 13	syl	|- ( ph -> W e. LMod )
15	1	ply1ring	|- ( R e. Ring -> W e. Ring )
16	5 15	syl	|- ( ph -> W e. Ring )
17	11 12 14 16	ascl1	|- ( ph -> ( ( algSc ` W ) ` ( 1r ` ( Scalar ` W ) ) ) = ( 1r ` W ) )
18	10 17	eqtrd	|- ( ph -> ( ( algSc ` W ) ` I ) = ( 1r ` W ) )
19	2	fveq1i	|- ( A ` I ) = ( ( algSc ` W ) ` I )
20	18 19 4	3eqtr4g	|- ( ph -> ( A ` I ) = .1. )