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 ) )