Theorem ply1ascl

Description: The univariate polynomial ring inherits the multivariate ring's scalar function. (Contributed by Stefan O'Rear, 28-Mar-2015) (Proof shortened by Fan Zheng, 26-Jun-2016)

	Ref	Expression
Hypotheses	ply1ascl.p	|- P = ( Poly1 ` R )
	ply1ascl.a	|- A = ( algSc ` P )
Assertion	ply1ascl	|- A = ( algSc ` ( 1o mPoly R ) )

Proof

Step	Hyp	Ref	Expression
1		ply1ascl.p	|- P = ( Poly1 ` R )
2		ply1ascl.a	|- A = ( algSc ` P )
3		eqid	|- ( Scalar ` P ) = ( Scalar ` P )
4		eqid	|- ( Scalar ` ( 1o mPoly R ) ) = ( Scalar ` ( 1o mPoly R ) )
5	1	ply1sca	|- ( R e. _V -> R = ( Scalar ` P ) )
6	5	fveq2d	|- ( R e. _V -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
7		eqid	|- ( 1o mPoly R ) = ( 1o mPoly R )
8		1on	|- 1o e. On
9	8	a1i	|- ( R e. _V -> 1o e. On )
10		id	|- ( R e. _V -> R e. _V )
11	7 9 10	mplsca	|- ( R e. _V -> R = ( Scalar ` ( 1o mPoly R ) ) )
12	11	fveq2d	|- ( R e. _V -> ( Base ` R ) = ( Base ` ( Scalar ` ( 1o mPoly R ) ) ) )
13		eqid	|- ( .s ` P ) = ( .s ` P )
14	1 7 13	ply1vsca	|- ( .s ` P ) = ( .s ` ( 1o mPoly R ) )
15	14	a1i	|- ( R e. _V -> ( .s ` P ) = ( .s ` ( 1o mPoly R ) ) )
16	15	oveqdr	|- ( ( R e. _V /\ ( x e. ( Base ` R ) /\ y e. _V ) ) -> ( x ( .s ` P ) y ) = ( x ( .s ` ( 1o mPoly R ) ) y ) )
17		eqid	|- ( 1r ` P ) = ( 1r ` P )
18	7 1 17	ply1mpl1	|- ( 1r ` P ) = ( 1r ` ( 1o mPoly R ) )
19	18	a1i	|- ( R e. _V -> ( 1r ` P ) = ( 1r ` ( 1o mPoly R ) ) )
20		fvexd	|- ( R e. _V -> ( 1r ` P ) e. _V )
21	3 4 6 12 16 19 20	asclpropd	|- ( R e. _V -> ( algSc ` P ) = ( algSc ` ( 1o mPoly R ) ) )
22		fvprc	|- ( -. R e. _V -> ( Poly1 ` R ) = (/) )
23	1 22	syl5eq	|- ( -. R e. _V -> P = (/) )
24		reldmmpl	|- Rel dom mPoly
25	24	ovprc2	|- ( -. R e. _V -> ( 1o mPoly R ) = (/) )
26	23 25	eqtr4d	|- ( -. R e. _V -> P = ( 1o mPoly R ) )
27	26	fveq2d	|- ( -. R e. _V -> ( algSc ` P ) = ( algSc ` ( 1o mPoly R ) ) )
28	21 27	pm2.61i	|- ( algSc ` P ) = ( algSc ` ( 1o mPoly R ) )
29	2 28	eqtri	|- A = ( algSc ` ( 1o mPoly R ) )