Theorem ply1basOLD

Description: Obsolete version of ply1bas as of 20-May-2025. (Contributed by Mario Carneiro, 9-Feb-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ply1val.1	|- P = ( Poly1 ` R )
	ply1lss.2	|- S = ( PwSer1 ` R )
	ply1lss.u	|- U = ( Base ` P )
Assertion	ply1basOLD	|- U = ( Base ` ( 1o mPoly R ) )

Proof

Step	Hyp	Ref	Expression
1		ply1val.1	|- P = ( Poly1 ` R )
2		ply1lss.2	|- S = ( PwSer1 ` R )
3		ply1lss.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 ) )