Metamath Proof Explorer

Theorem psropprmul

Description: Reversing multiplication in a ring reverses multiplication in the power series ring. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Hypotheses psropprmul.y 
|- Y = ( I mPwSer R )
psropprmul.s 
|- S = ( oppR ` R )
psropprmul.z 
|- Z = ( I mPwSer S )
psropprmul.t 
|- .x. = ( .r ` Y )
psropprmul.u 
|- .xb = ( .r ` Z )
psropprmul.b 
|- B = ( Base ` Y )
Assertion psropprmul 
|- ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( F .xb G ) = ( G .x. F ) )

Proof

Step Hyp Ref Expression
1 psropprmul.y 
 |-  Y = ( I mPwSer R )
2 psropprmul.s 
 |-  S = ( oppR ` R )
3 psropprmul.z 
 |-  Z = ( I mPwSer S )
4 psropprmul.t 
 |-  .x. = ( .r ` Y )
5 psropprmul.u 
 |-  .xb = ( .r ` Z )
6 psropprmul.b 
 |-  B = ( Base ` Y )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
9 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
10 9 3ad2ant1 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> R e. CMnd )
11 10 adantr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> R e. CMnd )
12 ovex 
 |-  ( NN0 ^m I ) e. _V
13 12 rabex 
 |-  { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } e. _V
14 13 rabex 
 |-  { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } e. _V
15 14 a1i 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } e. _V )
16 simpll1 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> R e. Ring )
17 eqid 
 |-  { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } = { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin }
18 simp3 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> G e. B )
19 1 7 17 6 18 psrelbas 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> G : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> ( Base ` R ) )
20 19 adantr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> G : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> ( Base ` R ) )
21 elrabi 
 |-  ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } -> e e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } )
22 ffvelrn 
 |-  ( ( G : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> ( Base ` R ) /\ e e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( G ` e ) e. ( Base ` R ) )
23 20 21 22 syl2an 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> ( G ` e ) e. ( Base ` R ) )
24 simp2 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> F e. B )
25 1 7 17 6 24 psrelbas 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> F : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> ( Base ` R ) )
26 25 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> F : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> ( Base ` R ) )
27 ssrab2 
 |-  { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } C_ { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin }
28 eqid 
 |-  { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } = { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b }
29 17 28 psrbagconcl 
 |-  ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> ( b oF - e ) e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } )
30 29 adantll 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> ( b oF - e ) e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } )
31 27 30 sseldi 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> ( b oF - e ) e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } )
32 26 31 ffvelrnd 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> ( F ` ( b oF - e ) ) e. ( Base ` R ) )
33 eqid 
 |-  ( .r ` R ) = ( .r ` R )
34 7 33 ringcl 
 |-  ( ( R e. Ring /\ ( G ` e ) e. ( Base ` R ) /\ ( F ` ( b oF - e ) ) e. ( Base ` R ) ) -> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) e. ( Base ` R ) )
35 16 23 32 34 syl3anc 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) e. ( Base ` R ) )
36 35 fmpttd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) : { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } --> ( Base ` R ) )
37 mptexg 
 |-  ( { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } e. _V -> ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) e. _V )
38 14 37 mp1i 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) e. _V )
39 funmpt 
 |-  Fun ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) )
40 39 a1i 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> Fun ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) )
41 fvexd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( 0g ` R ) e. _V )
42 17 psrbaglefi 
 |-  ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } -> { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } e. Fin )
43 42 adantl 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } e. Fin )
44 suppssdm 
 |-  ( ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) supp ( 0g ` R ) ) C_ dom ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) )
45 eqid 
 |-  ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) = ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) )
46 45 dmmptss 
 |-  dom ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) C_ { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b }
47 44 46 sstri 
 |-  ( ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) supp ( 0g ` R ) ) C_ { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b }
48 47 a1i 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) supp ( 0g ` R ) ) C_ { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } )
49 suppssfifsupp 
 |-  ( ( ( ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) e. _V /\ Fun ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) /\ ( 0g ` R ) e. _V ) /\ ( { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } e. Fin /\ ( ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) supp ( 0g ` R ) ) C_ { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) ) -> ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) finSupp ( 0g ` R ) )
50 38 40 41 43 48 49 syl32anc 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) finSupp ( 0g ` R ) )
51 17 28 psrbagconf1o 
 |-  ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } -> ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( b oF - c ) ) : { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } -1-1-onto-> { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } )
52 51 adantl 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( b oF - c ) ) : { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } -1-1-onto-> { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } )
53 7 8 11 15 36 50 52 gsumf1o 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( R gsum ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) ) = ( R gsum ( ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) o. ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( b oF - c ) ) ) ) )
54 17 28 psrbagconcl 
 |-  ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> ( b oF - c ) e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } )
55 54 adantll 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> ( b oF - c ) e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } )
56 eqidd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( b oF - c ) ) = ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( b oF - c ) ) )
57 eqidd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) = ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) )
58 fveq2 
 |-  ( e = ( b oF - c ) -> ( G ` e ) = ( G ` ( b oF - c ) ) )
59 oveq2 
 |-  ( e = ( b oF - c ) -> ( b oF - e ) = ( b oF - ( b oF - c ) ) )
60 59 fveq2d 
 |-  ( e = ( b oF - c ) -> ( F ` ( b oF - e ) ) = ( F ` ( b oF - ( b oF - c ) ) ) )
61 58 60 oveq12d 
 |-  ( e = ( b oF - c ) -> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) = ( ( G ` ( b oF - c ) ) ( .r ` R ) ( F ` ( b oF - ( b oF - c ) ) ) ) )
62 55 56 57 61 fmptco 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) o. ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( b oF - c ) ) ) = ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` ( b oF - c ) ) ( .r ` R ) ( F ` ( b oF - ( b oF - c ) ) ) ) ) )
63 reldmpsr 
 |-  Rel dom mPwSer
64 1 6 63 strov2rcl 
 |-  ( G e. B -> I e. _V )
65 64 3ad2ant3 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> I e. _V )
66 65 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> I e. _V )
67 17 psrbagf 
 |-  ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } -> b : I --> NN0 )
68 67 adantl 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> b : I --> NN0 )
69 68 adantr 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> b : I --> NN0 )
70 elrabi 
 |-  ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } -> c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } )
71 17 psrbagf 
 |-  ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } -> c : I --> NN0 )
72 70 71 syl 
 |-  ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } -> c : I --> NN0 )
73 72 adantl 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> c : I --> NN0 )
74 nn0cn 
 |-  ( e e. NN0 -> e e. CC )
75 nn0cn 
 |-  ( f e. NN0 -> f e. CC )
76 nncan 
 |-  ( ( e e. CC /\ f e. CC ) -> ( e - ( e - f ) ) = f )
77 74 75 76 syl2an 
 |-  ( ( e e. NN0 /\ f e. NN0 ) -> ( e - ( e - f ) ) = f )
78 77 adantl 
 |-  ( ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) /\ ( e e. NN0 /\ f e. NN0 ) ) -> ( e - ( e - f ) ) = f )
79 66 69 73 78 caonncan 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> ( b oF - ( b oF - c ) ) = c )
80 79 fveq2d 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> ( F ` ( b oF - ( b oF - c ) ) ) = ( F ` c ) )
81 80 oveq2d 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> ( ( G ` ( b oF - c ) ) ( .r ` R ) ( F ` ( b oF - ( b oF - c ) ) ) ) = ( ( G ` ( b oF - c ) ) ( .r ` R ) ( F ` c ) ) )
82 eqid 
 |-  ( .r ` S ) = ( .r ` S )
83 7 33 2 82 opprmul 
 |-  ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) = ( ( G ` ( b oF - c ) ) ( .r ` R ) ( F ` c ) )
84 81 83 eqtr4di 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } ) -> ( ( G ` ( b oF - c ) ) ( .r ` R ) ( F ` ( b oF - ( b oF - c ) ) ) ) = ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) )
85 84 mpteq2dva 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` ( b oF - c ) ) ( .r ` R ) ( F ` ( b oF - ( b oF - c ) ) ) ) ) = ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) ) )
86 62 85 eqtrd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) o. ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( b oF - c ) ) ) = ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) ) )
87 86 oveq2d 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( R gsum ( ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) o. ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( b oF - c ) ) ) ) = ( R gsum ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) ) ) )
88 14 mptex 
 |-  ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) ) e. _V
89 88 a1i 
 |-  ( R e. Ring -> ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) ) e. _V )
90 id 
 |-  ( R e. Ring -> R e. Ring )
91 2 fvexi 
 |-  S e. _V
92 91 a1i 
 |-  ( R e. Ring -> S e. _V )
93 2 7 opprbas 
 |-  ( Base ` R ) = ( Base ` S )
94 93 a1i 
 |-  ( R e. Ring -> ( Base ` R ) = ( Base ` S ) )
95 eqid 
 |-  ( +g ` R ) = ( +g ` R )
96 2 95 oppradd 
 |-  ( +g ` R ) = ( +g ` S )
97 96 a1i 
 |-  ( R e. Ring -> ( +g ` R ) = ( +g ` S ) )
98 89 90 92 94 97 gsumpropd 
 |-  ( R e. Ring -> ( R gsum ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) ) ) = ( S gsum ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) ) ) )
99 98 3ad2ant1 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( R gsum ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) ) ) = ( S gsum ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) ) ) )
100 99 adantr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( R gsum ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) ) ) = ( S gsum ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) ) ) )
101 53 87 100 3eqtrd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( R gsum ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) ) = ( S gsum ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) ) ) )
102 101 mpteq2dva 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( R gsum ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) ) ) = ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( S gsum ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) ) ) ) )
103 1 6 33 4 17 18 24 psrmulfval 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( G .x. F ) = ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( R gsum ( e e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( G ` e ) ( .r ` R ) ( F ` ( b oF - e ) ) ) ) ) ) )
104 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
105 93 a1i 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( Base ` R ) = ( Base ` S ) )
106 105 psrbaspropd 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer S ) ) )
107 1 fveq2i 
 |-  ( Base ` Y ) = ( Base ` ( I mPwSer R ) )
108 6 107 eqtri 
 |-  B = ( Base ` ( I mPwSer R ) )
109 3 fveq2i 
 |-  ( Base ` Z ) = ( Base ` ( I mPwSer S ) )
110 106 108 109 3eqtr4g 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> B = ( Base ` Z ) )
111 24 110 eleqtrd 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> F e. ( Base ` Z ) )
112 18 110 eleqtrd 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> G e. ( Base ` Z ) )
113 3 104 82 5 17 111 112 psrmulfval 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( F .xb G ) = ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( S gsum ( c e. { d e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } | d oR <_ b } |-> ( ( F ` c ) ( .r ` S ) ( G ` ( b oF - c ) ) ) ) ) ) )
114 102 103 113 3eqtr4rd 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( F .xb G ) = ( G .x. F ) )