Metamath Proof Explorer

Theorem psrplusgpropd

Description: Property deduction for power series addition. (Contributed by Stefan O'Rear, 27-Mar-2015) (Revised by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypotheses psrplusgpropd.b1 
|- ( ph -> B = ( Base ` R ) )
psrplusgpropd.b2 
|- ( ph -> B = ( Base ` S ) )
psrplusgpropd.p 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )
Assertion psrplusgpropd 
|- ( ph -> ( +g ` ( I mPwSer R ) ) = ( +g ` ( I mPwSer S ) ) )

Proof

Step Hyp Ref Expression
1 psrplusgpropd.b1 
 |-  ( ph -> B = ( Base ` R ) )
2 psrplusgpropd.b2 
 |-  ( ph -> B = ( Base ` S ) )
3 psrplusgpropd.p 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )
4 simpl1 
 |-  ( ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) /\ d e. { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } ) -> ph )
5 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } = { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin }
8 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
9 simp2 
 |-  ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) -> a e. ( Base ` ( I mPwSer R ) ) )
10 5 6 7 8 9 psrelbas 
 |-  ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) -> a : { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } --> ( Base ` R ) )
11 10 ffvelrnda 
 |-  ( ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) /\ d e. { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } ) -> ( a ` d ) e. ( Base ` R ) )
12 4 1 syl 
 |-  ( ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) /\ d e. { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } ) -> B = ( Base ` R ) )
13 11 12 eleqtrrd 
 |-  ( ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) /\ d e. { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } ) -> ( a ` d ) e. B )
14 simp3 
 |-  ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) -> b e. ( Base ` ( I mPwSer R ) ) )
15 5 6 7 8 14 psrelbas 
 |-  ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) -> b : { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } --> ( Base ` R ) )
16 15 ffvelrnda 
 |-  ( ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) /\ d e. { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } ) -> ( b ` d ) e. ( Base ` R ) )
17 16 12 eleqtrrd 
 |-  ( ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) /\ d e. { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } ) -> ( b ` d ) e. B )
18 3 oveqrspc2v 
 |-  ( ( ph /\ ( ( a ` d ) e. B /\ ( b ` d ) e. B ) ) -> ( ( a ` d ) ( +g ` R ) ( b ` d ) ) = ( ( a ` d ) ( +g ` S ) ( b ` d ) ) )
19 4 13 17 18 syl12anc 
 |-  ( ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) /\ d e. { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } ) -> ( ( a ` d ) ( +g ` R ) ( b ` d ) ) = ( ( a ` d ) ( +g ` S ) ( b ` d ) ) )
20 19 mpteq2dva 
 |-  ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) -> ( d e. { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } |-> ( ( a ` d ) ( +g ` R ) ( b ` d ) ) ) = ( d e. { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } |-> ( ( a ` d ) ( +g ` S ) ( b ` d ) ) ) )
21 10 ffnd 
 |-  ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) -> a Fn { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } )
22 15 ffnd 
 |-  ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) -> b Fn { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } )
23 ovex 
 |-  ( NN0 ^m I ) e. _V
24 23 rabex 
 |-  { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } e. _V
25 24 a1i 
 |-  ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) -> { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } e. _V )
26 inidm 
 |-  ( { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } i^i { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } ) = { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin }
27 eqidd 
 |-  ( ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) /\ d e. { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } ) -> ( a ` d ) = ( a ` d ) )
28 eqidd 
 |-  ( ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) /\ d e. { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } ) -> ( b ` d ) = ( b ` d ) )
29 21 22 25 25 26 27 28 offval 
 |-  ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) -> ( a oF ( +g ` R ) b ) = ( d e. { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } |-> ( ( a ` d ) ( +g ` R ) ( b ` d ) ) ) )
30 21 22 25 25 26 27 28 offval 
 |-  ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) -> ( a oF ( +g ` S ) b ) = ( d e. { c e. ( NN0 ^m I ) | ( `' c " NN ) e. Fin } |-> ( ( a ` d ) ( +g ` S ) ( b ` d ) ) ) )
31 20 29 30 3eqtr4d 
 |-  ( ( ph /\ a e. ( Base ` ( I mPwSer R ) ) /\ b e. ( Base ` ( I mPwSer R ) ) ) -> ( a oF ( +g ` R ) b ) = ( a oF ( +g ` S ) b ) )
32 31 mpoeq3dva 
 |-  ( ph -> ( a e. ( Base ` ( I mPwSer R ) ) , b e. ( Base ` ( I mPwSer R ) ) |-> ( a oF ( +g ` R ) b ) ) = ( a e. ( Base ` ( I mPwSer R ) ) , b e. ( Base ` ( I mPwSer R ) ) |-> ( a oF ( +g ` S ) b ) ) )
33 1 2 eqtr3d 
 |-  ( ph -> ( Base ` R ) = ( Base ` S ) )
34 33 psrbaspropd 
 |-  ( ph -> ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer S ) ) )
35 mpoeq12 
 |-  ( ( ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer S ) ) /\ ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer S ) ) ) -> ( a e. ( Base ` ( I mPwSer R ) ) , b e. ( Base ` ( I mPwSer R ) ) |-> ( a oF ( +g ` S ) b ) ) = ( a e. ( Base ` ( I mPwSer S ) ) , b e. ( Base ` ( I mPwSer S ) ) |-> ( a oF ( +g ` S ) b ) ) )
36 34 34 35 syl2anc 
 |-  ( ph -> ( a e. ( Base ` ( I mPwSer R ) ) , b e. ( Base ` ( I mPwSer R ) ) |-> ( a oF ( +g ` S ) b ) ) = ( a e. ( Base ` ( I mPwSer S ) ) , b e. ( Base ` ( I mPwSer S ) ) |-> ( a oF ( +g ` S ) b ) ) )
37 32 36 eqtrd 
 |-  ( ph -> ( a e. ( Base ` ( I mPwSer R ) ) , b e. ( Base ` ( I mPwSer R ) ) |-> ( a oF ( +g ` R ) b ) ) = ( a e. ( Base ` ( I mPwSer S ) ) , b e. ( Base ` ( I mPwSer S ) ) |-> ( a oF ( +g ` S ) b ) ) )
38 ofmres 
 |-  ( oF ( +g ` R ) |` ( ( Base ` ( I mPwSer R ) ) X. ( Base ` ( I mPwSer R ) ) ) ) = ( a e. ( Base ` ( I mPwSer R ) ) , b e. ( Base ` ( I mPwSer R ) ) |-> ( a oF ( +g ` R ) b ) )
39 ofmres 
 |-  ( oF ( +g ` S ) |` ( ( Base ` ( I mPwSer S ) ) X. ( Base ` ( I mPwSer S ) ) ) ) = ( a e. ( Base ` ( I mPwSer S ) ) , b e. ( Base ` ( I mPwSer S ) ) |-> ( a oF ( +g ` S ) b ) )
40 37 38 39 3eqtr4g 
 |-  ( ph -> ( oF ( +g ` R ) |` ( ( Base ` ( I mPwSer R ) ) X. ( Base ` ( I mPwSer R ) ) ) ) = ( oF ( +g ` S ) |` ( ( Base ` ( I mPwSer S ) ) X. ( Base ` ( I mPwSer S ) ) ) ) )
41 eqid 
 |-  ( +g ` R ) = ( +g ` R )
42 eqid 
 |-  ( +g ` ( I mPwSer R ) ) = ( +g ` ( I mPwSer R ) )
43 5 8 41 42 psrplusg 
 |-  ( +g ` ( I mPwSer R ) ) = ( oF ( +g ` R ) |` ( ( Base ` ( I mPwSer R ) ) X. ( Base ` ( I mPwSer R ) ) ) )
44 eqid 
 |-  ( I mPwSer S ) = ( I mPwSer S )
45 eqid 
 |-  ( Base ` ( I mPwSer S ) ) = ( Base ` ( I mPwSer S ) )
46 eqid 
 |-  ( +g ` S ) = ( +g ` S )
47 eqid 
 |-  ( +g ` ( I mPwSer S ) ) = ( +g ` ( I mPwSer S ) )
48 44 45 46 47 psrplusg 
 |-  ( +g ` ( I mPwSer S ) ) = ( oF ( +g ` S ) |` ( ( Base ` ( I mPwSer S ) ) X. ( Base ` ( I mPwSer S ) ) ) )
49 40 43 48 3eqtr4g 
 |-  ( ph -> ( +g ` ( I mPwSer R ) ) = ( +g ` ( I mPwSer S ) ) )