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

Metamath Proof Explorer

Theorem ply1bas

Description: The value of the base set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015) Remove hypothesis. (Revised by SN, 20-May-2025)

Ref Expression
Hypotheses ply1val.1 
|- P = ( Poly1 ` R )
ply1bas.u 
|- U = ( Base ` P )
Assertion ply1bas 
|- U = ( Base ` ( 1o mPoly R ) )

Proof

Step Hyp Ref Expression
1 ply1val.1 
 |-  P = ( Poly1 ` R )
2 ply1bas.u 
 |-  U = ( Base ` P )
3 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
4 eqid 
 |-  ( 1o mPwSer R ) = ( 1o mPwSer R )
5 eqid 
 |-  ( Base ` ( 1o mPoly R ) ) = ( Base ` ( 1o mPoly R ) )
6 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
7 eqid 
 |-  ( Base ` ( PwSer1 ` R ) ) = ( Base ` ( PwSer1 ` R ) )
8 6 7 4 psr1bas2 
 |-  ( Base ` ( PwSer1 ` R ) ) = ( Base ` ( 1o mPwSer R ) )
9 3 4 5 8 mplbasss 
 |-  ( Base ` ( 1o mPoly R ) ) C_ ( Base ` ( PwSer1 ` R ) )
10 1 6 ply1val 
 |-  P = ( ( PwSer1 ` R ) |`s ( Base ` ( 1o mPoly R ) ) )
11 10 7 ressbas2 
 |-  ( ( Base ` ( 1o mPoly R ) ) C_ ( Base ` ( PwSer1 ` R ) ) -> ( Base ` ( 1o mPoly R ) ) = ( Base ` P ) )
12 9 11 ax-mp 
 |-  ( Base ` ( 1o mPoly R ) ) = ( Base ` P )
13 2 12 eqtr4i 
 |-  U = ( Base ` ( 1o mPoly R ) )