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	$⊢ P = {Poly}_{1} (R)$
		ply1lss.2	$⊢ S = {PwSer}_{1} (R)$
		ply1lss.u	$⊢ U = {Base}_{P}$
	Assertion	ply1basOLD	$⊢ U = {Base}_{(1_{𝑜} mPoly R)}$

Proof

Step	Hyp	Ref	Expression
1		ply1val.1	$⊢ P = {Poly}_{1} (R)$
2		ply1lss.2	$⊢ S = {PwSer}_{1} (R)$
3		ply1lss.u	$⊢ U = {Base}_{P}$
4		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
5		eqid	$⊢ 1_{𝑜} mPwSer R = 1_{𝑜} mPwSer R$
6		eqid	$⊢ {Base}_{(1_{𝑜} mPoly R)} = {Base}_{(1_{𝑜} mPoly R)}$
7		eqid	$⊢ {Base}_{S} = {Base}_{S}$
8	2 7 5	psr1bas2	$⊢ {Base}_{S} = {Base}_{(1_{𝑜} mPwSer R)}$
9	4 5 6 8	mplbasss	$⊢ {Base}_{(1_{𝑜} mPoly R)} \subseteq {Base}_{S}$
10	1 2	ply1val	$⊢ P = S ↾_{𝑠} {Base}_{(1_{𝑜} mPoly R)}$
11	10 7	ressbas2	$⊢ {Base}_{(1_{𝑜} mPoly R)} \subseteq {Base}_{S} \to {Base}_{(1_{𝑜} mPoly R)} = {Base}_{P}$
12	9 11	ax-mp	$⊢ {Base}_{(1_{𝑜} mPoly R)} = {Base}_{P}$
13	3 12	eqtr4i	$⊢ U = {Base}_{(1_{𝑜} mPoly R)}$