Theorem ply1ascl0

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

	Ref	Expression
Hypotheses	ply1ascl0.w	|- W = ( Poly1 ` R )
	ply1ascl0.a	|- A = ( algSc ` W )
	ply1ascl0.o	|- O = ( 0g ` R )
	ply1ascl0.1	|- .0. = ( 0g ` W )
	ply1ascl0.r	|- ( ph -> R e. Ring )
Assertion	ply1ascl0	|- ( ph -> ( A ` O ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		ply1ascl0.w	|- W = ( Poly1 ` R )
2		ply1ascl0.a	|- A = ( algSc ` W )
3		ply1ascl0.o	|- O = ( 0g ` R )
4		ply1ascl0.1	|- .0. = ( 0g ` W )
5		ply1ascl0.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 -> ( 0g ` R ) = ( 0g ` ( Scalar ` W ) ) )
9	3 8	eqtrid	|- ( ph -> O = ( 0g ` ( Scalar ` W ) ) )
10	9	fveq2d	|- ( ph -> ( ( algSc ` W ) ` O ) = ( ( algSc ` W ) ` ( 0g ` ( 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	ascl0	|- ( ph -> ( ( algSc ` W ) ` ( 0g ` ( Scalar ` W ) ) ) = ( 0g ` W ) )
18	10 17	eqtrd	|- ( ph -> ( ( algSc ` W ) ` O ) = ( 0g ` W ) )
19	2	fveq1i	|- ( A ` O ) = ( ( algSc ` W ) ` O )
20	18 19 4	3eqtr4g	|- ( ph -> ( A ` O ) = .0. )