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

Metamath Proof Explorer

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	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
		ply1lss.2	⊢ 𝑆 = ( PwSer₁ ‘ 𝑅 )
		ply1lss.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	Assertion	ply1basOLD	⊢ 𝑈 = ( Base ‘ ( 1_o mPoly 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1val.1	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
2		ply1lss.2	⊢ 𝑆 = ( PwSer₁ ‘ 𝑅 )
3		ply1lss.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
4		eqid	⊢ ( 1_o mPoly 𝑅 ) = ( 1_o mPoly 𝑅 )
5		eqid	⊢ ( 1_o mPwSer 𝑅 ) = ( 1_o mPwSer 𝑅 )
6		eqid	⊢ ( Base ‘ ( 1_o mPoly 𝑅 ) ) = ( Base ‘ ( 1_o mPoly 𝑅 ) )
7		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
8	2 7 5	psr1bas2	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ ( 1_o mPwSer 𝑅 ) )
9	4 5 6 8	mplbasss	⊢ ( Base ‘ ( 1_o mPoly 𝑅 ) ) ⊆ ( Base ‘ 𝑆 )
10	1 2	ply1val	⊢ 𝑃 = ( 𝑆 ↾_s ( Base ‘ ( 1_o mPoly 𝑅 ) ) )
11	10 7	ressbas2	⊢ ( ( Base ‘ ( 1_o mPoly 𝑅 ) ) ⊆ ( Base ‘ 𝑆 ) → ( Base ‘ ( 1_o mPoly 𝑅 ) ) = ( Base ‘ 𝑃 ) )
12	9 11	ax-mp	⊢ ( Base ‘ ( 1_o mPoly 𝑅 ) ) = ( Base ‘ 𝑃 )
13	3 12	eqtr4i	⊢ 𝑈 = ( Base ‘ ( 1_o mPoly 𝑅 ) )