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

Metamath Proof Explorer

Theorem ply1basfvi

Description: Protection compatibility of the univariate polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Assertion ply1basfvi ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 fvi ⊢ ( 𝑅 ∈ V → ( I ‘ 𝑅 ) = 𝑅 )
2 1 eqcomd ⊢ ( 𝑅 ∈ V → 𝑅 = ( I ‘ 𝑅 ) )
3 2 fveq2d ⊢ ( 𝑅 ∈ V → ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ ( I ‘ 𝑅 ) ) )
4 3 fveq2d ⊢ ( 𝑅 ∈ V → ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) ) )
5 base0 ⊢ ∅ = ( Base ‘ ∅ )
6 00ply1bas ⊢ ∅ = ( Base ‘ ( Poly1 ‘ ∅ ) )
7 5 6 eqtr3i ⊢ ( Base ‘ ∅ ) = ( Base ‘ ( Poly1 ‘ ∅ ) )
8 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( Poly1 ‘ 𝑅 ) = ∅ )
9 8 fveq2d ⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ∅ ) )
10 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( I ‘ 𝑅 ) = ∅ )
11 10 fveq2d ⊢ ( ¬ 𝑅 ∈ V → ( Poly1 ‘ ( I ‘ 𝑅 ) ) = ( Poly1 ‘ ∅ ) )
12 11 fveq2d ⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) ) = ( Base ‘ ( Poly1 ‘ ∅ ) ) )
13 7 9 12 3eqtr4a ⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) ) )
14 4 13 pm2.61i ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) )