Theorem ply1ascl0

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

	Ref	Expression
Hypotheses	ply1ascl0.w	⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
	ply1ascl0.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	ply1ascl0.o	⊢ 𝑂 = ( 0g ‘ 𝑅 )
	ply1ascl0.1	⊢ 0 = ( 0g ‘ 𝑊 )
	ply1ascl0.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion	ply1ascl0	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑂 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		ply1ascl0.w	⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
2		ply1ascl0.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
3		ply1ascl0.o	⊢ 𝑂 = ( 0g ‘ 𝑅 )
4		ply1ascl0.1	⊢ 0 = ( 0g ‘ 𝑊 )
5		ply1ascl0.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑊 ) )
7	5 6	syl	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑊 ) )
8	7	fveq2d	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
9	3 8	eqtrid	⊢ ( 𝜑 → 𝑂 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
10	9	fveq2d	⊢ ( 𝜑 → ( ( algSc ‘ 𝑊 ) ‘ 𝑂 ) = ( ( algSc ‘ 𝑊 ) ‘ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
11		eqid	⊢ ( algSc ‘ 𝑊 ) = ( algSc ‘ 𝑊 )
12		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
13	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑊 ∈ LMod )
14	5 13	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
15	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑊 ∈ Ring )
16	5 15	syl	⊢ ( 𝜑 → 𝑊 ∈ Ring )
17	11 12 14 16	ascl0	⊢ ( 𝜑 → ( ( algSc ‘ 𝑊 ) ‘ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ 𝑊 ) )
18	10 17	eqtrd	⊢ ( 𝜑 → ( ( algSc ‘ 𝑊 ) ‘ 𝑂 ) = ( 0g ‘ 𝑊 ) )
19	2	fveq1i	⊢ ( 𝐴 ‘ 𝑂 ) = ( ( algSc ‘ 𝑊 ) ‘ 𝑂 )
20	18 19 4	3eqtr4g	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑂 ) = 0 )