This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 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 ‘ 𝑆 ) ) )