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
|- ( ph -> B = ( Base ` R ) )
ply1baspropd.b2
|- ( ph -> B = ( Base ` S ) )
ply1baspropd.p
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )
Assertion ply1baspropd
|- ( ph -> ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` S ) ) )

Proof

Step Hyp Ref Expression
1 ply1baspropd.b1
 |-  ( ph -> B = ( Base ` R ) )
2 ply1baspropd.b2
 |-  ( ph -> B = ( Base ` S ) )
3 ply1baspropd.p
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )
4 1 2 3 mplbaspropd
 |-  ( ph -> ( Base ` ( 1o mPoly R ) ) = ( Base ` ( 1o mPoly S ) ) )
5 eqid
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
6 eqid
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
7 5 6 ply1bas
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( 1o mPoly R ) )
8 eqid
 |-  ( Poly1 ` S ) = ( Poly1 ` S )
9 eqid
 |-  ( Base ` ( Poly1 ` S ) ) = ( Base ` ( Poly1 ` S ) )
10 8 9 ply1bas
 |-  ( Base ` ( Poly1 ` S ) ) = ( Base ` ( 1o mPoly S ) )
11 4 7 10 3eqtr4g
 |-  ( ph -> ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` S ) ) )