Theorem ply1ascl1

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

	Ref	Expression
Hypotheses	ply1ascl1.w	⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
	ply1ascl1.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	ply1ascl1.i	⊢ 𝐼 = ( 1r ‘ 𝑅 )
	ply1ascl1.1	⊢ 1 = ( 1r ‘ 𝑊 )
	ply1ascl1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion	ply1ascl1	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐼 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		ply1ascl1.w	⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
2		ply1ascl1.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
3		ply1ascl1.i	⊢ 𝐼 = ( 1r ‘ 𝑅 )
4		ply1ascl1.1	⊢ 1 = ( 1r ‘ 𝑊 )
5		ply1ascl1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑊 ) )
7	5 6	syl	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑊 ) )
8	7	fveq2d	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) )
9	3 8	eqtrid	⊢ ( 𝜑 → 𝐼 = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) )
10	9	fveq2d	⊢ ( 𝜑 → ( ( algSc ‘ 𝑊 ) ‘ 𝐼 ) = ( ( algSc ‘ 𝑊 ) ‘ ( 1r ‘ ( 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	ascl1	⊢ ( 𝜑 → ( ( algSc ‘ 𝑊 ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 1r ‘ 𝑊 ) )
18	10 17	eqtrd	⊢ ( 𝜑 → ( ( algSc ‘ 𝑊 ) ‘ 𝐼 ) = ( 1r ‘ 𝑊 ) )
19	2	fveq1i	⊢ ( 𝐴 ‘ 𝐼 ) = ( ( algSc ‘ 𝑊 ) ‘ 𝐼 )
20	18 19 4	3eqtr4g	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐼 ) = 1 )