ply1ascl0

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

Step	Hyp	Ref	Expression
1		ply1ascl0.w	$⊢ W = {Poly}_{1} (R)$
2		ply1ascl0.a	$⊢ A = algSc (W)$
3		ply1ascl0.o	$⊢ O = 0_{R}$
4		ply1ascl0.1	$⊢ \underset{˙}{0} = 0_{W}$
5		ply1ascl0.r	$⊢ φ \to R \in Ring$
6	1	ply1sca	$⊢ R \in Ring \to R = Scalar (W)$
7	5 6	syl	$⊢ φ \to R = Scalar (W)$
8	7	fveq2d	$⊢ φ \to 0_{R} = 0_{Scalar (W)}$
9	3 8	eqtrid	$⊢ φ \to O = 0_{Scalar (W)}$
10	9	fveq2d	$⊢ φ \to algSc (W) (O) = algSc (W) (0_{Scalar (W)})$
11		eqid	$⊢ algSc (W) = algSc (W)$
12		eqid	$⊢ Scalar (W) = Scalar (W)$
13	1	ply1lmod	$⊢ R \in Ring \to W \in LMod$
14	5 13	syl	$⊢ φ \to W \in LMod$
15	1	ply1ring	$⊢ R \in Ring \to W \in Ring$
16	5 15	syl	$⊢ φ \to W \in Ring$
17	11 12 14 16	ascl0	$⊢ φ \to algSc (W) (0_{Scalar (W)}) = 0_{W}$
18	10 17	eqtrd	$⊢ φ \to algSc (W) (O) = 0_{W}$
19	2	fveq1i	$⊢ A (O) = algSc (W) (O)$
20	18 19 4	3eqtr4g	$⊢ φ \to A (O) = \underset{˙}{0}$

Metamath Proof Explorer