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	|- P = ( Poly1 ` R )
	ply1scl.a	|- A = ( algSc ` P )
	ply1scl1.o	|- .1. = ( 1r ` R )
	ply1scl1.n	|- N = ( 1r ` P )
Assertion	ply1scl1	|- ( R e. Ring -> ( A ` .1. ) = N )

Proof

Step	Hyp	Ref	Expression
1		ply1scl.p	|- P = ( Poly1 ` R )
2		ply1scl.a	|- A = ( algSc ` P )
3		ply1scl1.o	|- .1. = ( 1r ` R )
4		ply1scl1.n	|- N = ( 1r ` P )
5	1	ply1sca	|- ( R e. Ring -> R = ( Scalar ` P ) )
6	5	fveq2d	|- ( R e. Ring -> ( 1r ` R ) = ( 1r ` ( Scalar ` P ) ) )
7	3 6	eqtrid	|- ( R e. Ring -> .1. = ( 1r ` ( Scalar ` P ) ) )
8	7	fveq2d	|- ( R e. Ring -> ( A ` .1. ) = ( A ` ( 1r ` ( Scalar ` P ) ) ) )
9		eqid	|- ( Scalar ` P ) = ( Scalar ` P )
10	1	ply1lmod	|- ( R e. Ring -> P e. LMod )
11	1	ply1ring	|- ( R e. Ring -> P e. Ring )
12	2 9 10 11	ascl1	|- ( R e. Ring -> ( A ` ( 1r ` ( Scalar ` P ) ) ) = ( 1r ` P ) )
13	8 12	eqtrd	|- ( R e. Ring -> ( A ` .1. ) = ( 1r ` P ) )
14	13 4	eqtr4di	|- ( R e. Ring -> ( A ` .1. ) = N )