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

Metamath Proof Explorer

Theorem psrbaspropd

Description: Property deduction for power series base set. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Hypothesis psrbaspropd.e 
|- ( ph -> ( Base ` R ) = ( Base ` S ) )
Assertion psrbaspropd 
|- ( ph -> ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer S ) ) )

Proof

Step Hyp Ref Expression
1 psrbaspropd.e 
 |-  ( ph -> ( Base ` R ) = ( Base ` S ) )
2 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 eqid 
 |-  { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } = { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin }
5 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
6 simpr 
 |-  ( ( ph /\ I e. _V ) -> I e. _V )
7 2 3 4 5 6 psrbas 
 |-  ( ( ph /\ I e. _V ) -> ( Base ` ( I mPwSer R ) ) = ( ( Base ` R ) ^m { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) )
8 eqid 
 |-  ( I mPwSer S ) = ( I mPwSer S )
9 eqid 
 |-  ( Base ` S ) = ( Base ` S )
10 eqid 
 |-  ( Base ` ( I mPwSer S ) ) = ( Base ` ( I mPwSer S ) )
11 8 9 4 10 6 psrbas 
 |-  ( ( ph /\ I e. _V ) -> ( Base ` ( I mPwSer S ) ) = ( ( Base ` S ) ^m { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) )
12 1 adantr 
 |-  ( ( ph /\ I e. _V ) -> ( Base ` R ) = ( Base ` S ) )
13 12 oveq1d 
 |-  ( ( ph /\ I e. _V ) -> ( ( Base ` R ) ^m { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) = ( ( Base ` S ) ^m { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) )
14 11 13 eqtr4d 
 |-  ( ( ph /\ I e. _V ) -> ( Base ` ( I mPwSer S ) ) = ( ( Base ` R ) ^m { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) )
15 7 14 eqtr4d 
 |-  ( ( ph /\ I e. _V ) -> ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer S ) ) )
16 reldmpsr 
 |-  Rel dom mPwSer
17 16 ovprc1 
 |-  ( -. I e. _V -> ( I mPwSer R ) = (/) )
18 16 ovprc1 
 |-  ( -. I e. _V -> ( I mPwSer S ) = (/) )
19 17 18 eqtr4d 
 |-  ( -. I e. _V -> ( I mPwSer R ) = ( I mPwSer S ) )
20 19 fveq2d 
 |-  ( -. I e. _V -> ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer S ) ) )
21 20 adantl 
 |-  ( ( ph /\ -. I e. _V ) -> ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer S ) ) )
22 15 21 pm2.61dan 
 |-  ( ph -> ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer S ) ) )