# Metamath Proof Explorer

## Theorem ply1bas

Description: The value of the base set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015)

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