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