Theorem ply1baspropd

Description: Property deduction for univariate polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	ply1baspropd.b1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
	ply1baspropd.b2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑆 ) )
	ply1baspropd.p	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
Assertion	ply1baspropd	⊢ ( 𝜑 → ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1baspropd.b1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
2		ply1baspropd.b2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑆 ) )
3		ply1baspropd.p	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
4	1 2 3	mplbaspropd	⊢ ( 𝜑 → ( Base ‘ ( 1o mPoly 𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑆 ) ) )
5		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
6		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
7	5 6	ply1bas	⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
8		eqid	⊢ ( Poly1 ‘ 𝑆 ) = ( Poly1 ‘ 𝑆 )
9		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) )
10	8 9	ply1bas	⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( 1o mPoly 𝑆 ) )
11	4 7 10	3eqtr4g	⊢ ( 𝜑 → ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )