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	eqtrid	\|- ( -. 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 ) )

Metamath Proof Explorer

Theorem ply1ascl

Proof