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 ` R ) ) = ( Base ` ( Poly1 ` ( _I ` R ) ) )

Proof

Step Hyp Ref Expression
1 fvi 
 |-  ( R e. _V -> ( _I ` R ) = R )
2 1 eqcomd 
 |-  ( R e. _V -> R = ( _I ` R ) )
3 2 fveq2d 
 |-  ( R e. _V -> ( Poly1 ` R ) = ( Poly1 ` ( _I ` R ) ) )
4 3 fveq2d 
 |-  ( R e. _V -> ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` ( _I ` R ) ) ) )
5 base0 
 |-  (/) = ( Base ` (/) )
6 00ply1bas 
 |-  (/) = ( Base ` ( Poly1 ` (/) ) )
7 5 6 eqtr3i 
 |-  ( Base ` (/) ) = ( Base ` ( Poly1 ` (/) ) )
8 fvprc 
 |-  ( -. R e. _V -> ( Poly1 ` R ) = (/) )
9 8 fveq2d 
 |-  ( -. R e. _V -> ( Base ` ( Poly1 ` R ) ) = ( Base ` (/) ) )
10 fvprc 
 |-  ( -. R e. _V -> ( _I ` R ) = (/) )
11 10 fveq2d 
 |-  ( -. R e. _V -> ( Poly1 ` ( _I ` R ) ) = ( Poly1 ` (/) ) )
12 11 fveq2d 
 |-  ( -. R e. _V -> ( Base ` ( Poly1 ` ( _I ` R ) ) ) = ( Base ` ( Poly1 ` (/) ) ) )
13 7 9 12 3eqtr4a 
 |-  ( -. R e. _V -> ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` ( _I ` R ) ) ) )
14 4 13 pm2.61i 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` ( _I ` R ) ) )