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	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
7		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
8	5 6 7	ply1bas	⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
9		eqid	⊢ ( Poly1 ‘ 𝑆 ) = ( Poly1 ‘ 𝑆 )
10		eqid	⊢ ( PwSer1 ‘ 𝑆 ) = ( PwSer1 ‘ 𝑆 )
11		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) )
12	9 10 11	ply1bas	⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( 1o mPoly 𝑆 ) )
13	4 8 12	3eqtr4g	⊢ ( 𝜑 → ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )