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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1ascl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
Assertion	ply1ascl	⊢ 𝐴 = ( algSc ‘ ( 1o mPoly 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1ascl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1ascl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
3		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
4		eqid	⊢ ( Scalar ‘ ( 1o mPoly 𝑅 ) ) = ( Scalar ‘ ( 1o mPoly 𝑅 ) )
5	1	ply1sca	⊢ ( 𝑅 ∈ V → 𝑅 = ( Scalar ‘ 𝑃 ) )
6	5	fveq2d	⊢ ( 𝑅 ∈ V → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
7		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
8		1on	⊢ 1o ∈ On
9	8	a1i	⊢ ( 𝑅 ∈ V → 1o ∈ On )
10		id	⊢ ( 𝑅 ∈ V → 𝑅 ∈ V )
11	7 9 10	mplsca	⊢ ( 𝑅 ∈ V → 𝑅 = ( Scalar ‘ ( 1o mPoly 𝑅 ) ) )
12	11	fveq2d	⊢ ( 𝑅 ∈ V → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ ( 1o mPoly 𝑅 ) ) ) )
13		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
14	1 7 13	ply1vsca	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
15	14	a1i	⊢ ( 𝑅 ∈ V → ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) )
16	15	oveqdr	⊢ ( ( 𝑅 ∈ V ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ V ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) 𝑦 ) )
17		eqid	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
18	7 1 17	ply1mpl1	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ ( 1o mPoly 𝑅 ) )
19	18	a1i	⊢ ( 𝑅 ∈ V → ( 1r ‘ 𝑃 ) = ( 1r ‘ ( 1o mPoly 𝑅 ) ) )
20		fvexd	⊢ ( 𝑅 ∈ V → ( 1r ‘ 𝑃 ) ∈ V )
21	3 4 6 12 16 19 20	asclpropd	⊢ ( 𝑅 ∈ V → ( algSc ‘ 𝑃 ) = ( algSc ‘ ( 1o mPoly 𝑅 ) ) )
22		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( Poly1 ‘ 𝑅 ) = ∅ )
23	1 22	syl5eq	⊢ ( ¬ 𝑅 ∈ V → 𝑃 = ∅ )
24		reldmmpl	⊢ Rel dom mPoly
25	24	ovprc2	⊢ ( ¬ 𝑅 ∈ V → ( 1o mPoly 𝑅 ) = ∅ )
26	23 25	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → 𝑃 = ( 1o mPoly 𝑅 ) )
27	26	fveq2d	⊢ ( ¬ 𝑅 ∈ V → ( algSc ‘ 𝑃 ) = ( algSc ‘ ( 1o mPoly 𝑅 ) ) )
28	21 27	pm2.61i	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ ( 1o mPoly 𝑅 ) )
29	2 28	eqtri	⊢ 𝐴 = ( algSc ‘ ( 1o mPoly 𝑅 ) )