Theorem ply1scl1

Description: The one scalar is the unit polynomial. (Contributed by Stefan O'Rear, 1-Apr-2015) (Proof shortened by SN, 12-Mar-2025)

	Ref	Expression
Hypotheses	ply1scl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1scl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	ply1scl1.o	⊢ 1 = ( 1r ‘ 𝑅 )
	ply1scl1.n	⊢ 𝑁 = ( 1r ‘ 𝑃 )
Assertion	ply1scl1	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 1 ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		ply1scl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1scl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
3		ply1scl1.o	⊢ 1 = ( 1r ‘ 𝑅 )
4		ply1scl1.n	⊢ 𝑁 = ( 1r ‘ 𝑃 )
5	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
6	5	fveq2d	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
7	3 6	eqtrid	⊢ ( 𝑅 ∈ Ring → 1 = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
8	7	fveq2d	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 1 ) = ( 𝐴 ‘ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ) )
9		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
10	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
11	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
12	2 9 10 11	ascl1	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ) = ( 1r ‘ 𝑃 ) )
13	8 12	eqtrd	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 1 ) = ( 1r ‘ 𝑃 ) )
14	13 4	eqtr4di	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 1 ) = 𝑁 )