Metamath Proof Explorer


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𝑆 ) ) )