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 sselid
 |-  ( ( ( ( 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 ) )