Theorem ply1scl1

Description: The one scalar is the unit polynomial. (Contributed by Stefan O'Rear, 1-Apr-2015)

	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		eqid	|- ( Base ` R ) = ( Base ` R )
6	5 3	ringidcl	|- ( R e. Ring -> .1. e. ( Base ` R ) )
7	1	ply1sca2	|- ( _I ` R ) = ( Scalar ` P )
8		baseid	|- Base = Slot ( Base ` ndx )
9	8 5	strfvi	|- ( Base ` R ) = ( Base ` ( _I ` R ) )
10		eqid	|- ( .s ` P ) = ( .s ` P )
11	2 7 9 10 4	asclval	|- ( .1. e. ( Base ` R ) -> ( A ` .1. ) = ( .1. ( .s ` P ) N ) )
12	6 11	syl	|- ( R e. Ring -> ( A ` .1. ) = ( .1. ( .s ` P ) N ) )
13		fvi	|- ( R e. Ring -> ( _I ` R ) = R )
14	13	fveq2d	|- ( R e. Ring -> ( 1r ` ( _I ` R ) ) = ( 1r ` R ) )
15	14 3	eqtr4di	|- ( R e. Ring -> ( 1r ` ( _I ` R ) ) = .1. )
16	15	oveq1d	|- ( R e. Ring -> ( ( 1r ` ( _I ` R ) ) ( .s ` P ) N ) = ( .1. ( .s ` P ) N ) )
17	1	ply1lmod	|- ( R e. Ring -> P e. LMod )
18	1	ply1ring	|- ( R e. Ring -> P e. Ring )
19		eqid	|- ( Base ` P ) = ( Base ` P )
20	19 4	ringidcl	|- ( P e. Ring -> N e. ( Base ` P ) )
21	18 20	syl	|- ( R e. Ring -> N e. ( Base ` P ) )
22		eqid	|- ( 1r ` ( _I ` R ) ) = ( 1r ` ( _I ` R ) )
23	19 7 10 22	lmodvs1	|- ( ( P e. LMod /\ N e. ( Base ` P ) ) -> ( ( 1r ` ( _I ` R ) ) ( .s ` P ) N ) = N )
24	17 21 23	syl2anc	|- ( R e. Ring -> ( ( 1r ` ( _I ` R ) ) ( .s ` P ) N ) = N )
25	12 16 24	3eqtr2d	|- ( R e. Ring -> ( A ` .1. ) = N )