This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ¬ 𝑅 ∈ 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 𝑅 ) )