Step |
Hyp |
Ref |
Expression |
1 |
|
psrmulcl.s |
|- S = ( I mPwSer R ) |
2 |
|
psrmulcl.b |
|- B = ( Base ` S ) |
3 |
|
psrmulcl.t |
|- .x. = ( .r ` S ) |
4 |
|
psrmulcl.r |
|- ( ph -> R e. Ring ) |
5 |
|
psrmulcl.x |
|- ( ph -> X e. B ) |
6 |
|
psrmulcl.y |
|- ( ph -> Y e. B ) |
7 |
|
psrmulcl.d |
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
8 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
9 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
10 |
4
|
adantr |
|- ( ( ph /\ k e. D ) -> R e. Ring ) |
11 |
|
ringcmn |
|- ( R e. Ring -> R e. CMnd ) |
12 |
10 11
|
syl |
|- ( ( ph /\ k e. D ) -> R e. CMnd ) |
13 |
7
|
psrbaglefi |
|- ( k e. D -> { y e. D | y oR <_ k } e. Fin ) |
14 |
13
|
adantl |
|- ( ( ph /\ k e. D ) -> { y e. D | y oR <_ k } e. Fin ) |
15 |
4
|
ad2antrr |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> R e. Ring ) |
16 |
1 8 7 2 5
|
psrelbas |
|- ( ph -> X : D --> ( Base ` R ) ) |
17 |
16
|
ad2antrr |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> X : D --> ( Base ` R ) ) |
18 |
|
simpr |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. { y e. D | y oR <_ k } ) |
19 |
|
breq1 |
|- ( y = x -> ( y oR <_ k <-> x oR <_ k ) ) |
20 |
19
|
elrab |
|- ( x e. { y e. D | y oR <_ k } <-> ( x e. D /\ x oR <_ k ) ) |
21 |
18 20
|
sylib |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( x e. D /\ x oR <_ k ) ) |
22 |
21
|
simpld |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. D ) |
23 |
17 22
|
ffvelrnd |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( X ` x ) e. ( Base ` R ) ) |
24 |
1 8 7 2 6
|
psrelbas |
|- ( ph -> Y : D --> ( Base ` R ) ) |
25 |
24
|
ad2antrr |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Y : D --> ( Base ` R ) ) |
26 |
|
simplr |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> k e. D ) |
27 |
7
|
psrbagf |
|- ( x e. D -> x : I --> NN0 ) |
28 |
22 27
|
syl |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x : I --> NN0 ) |
29 |
21
|
simprd |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x oR <_ k ) |
30 |
7
|
psrbagcon |
|- ( ( k e. D /\ x : I --> NN0 /\ x oR <_ k ) -> ( ( k oF - x ) e. D /\ ( k oF - x ) oR <_ k ) ) |
31 |
26 28 29 30
|
syl3anc |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( k oF - x ) e. D /\ ( k oF - x ) oR <_ k ) ) |
32 |
31
|
simpld |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. D ) |
33 |
25 32
|
ffvelrnd |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( Y ` ( k oF - x ) ) e. ( Base ` R ) ) |
34 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
35 |
8 34
|
ringcl |
|- ( ( R e. Ring /\ ( X ` x ) e. ( Base ` R ) /\ ( Y ` ( k oF - x ) ) e. ( Base ` R ) ) -> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) e. ( Base ` R ) ) |
36 |
15 23 33 35
|
syl3anc |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) e. ( Base ` R ) ) |
37 |
36
|
fmpttd |
|- ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) : { y e. D | y oR <_ k } --> ( Base ` R ) ) |
38 |
|
fvexd |
|- ( ( ph /\ k e. D ) -> ( 0g ` R ) e. _V ) |
39 |
37 14 38
|
fdmfifsupp |
|- ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) finSupp ( 0g ` R ) ) |
40 |
8 9 12 14 37 39
|
gsumcl |
|- ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) e. ( Base ` R ) ) |
41 |
40
|
fmpttd |
|- ( ph -> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) : D --> ( Base ` R ) ) |
42 |
|
fvex |
|- ( Base ` R ) e. _V |
43 |
|
ovex |
|- ( NN0 ^m I ) e. _V |
44 |
7 43
|
rabex2 |
|- D e. _V |
45 |
42 44
|
elmap |
|- ( ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) e. ( ( Base ` R ) ^m D ) <-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) : D --> ( Base ` R ) ) |
46 |
41 45
|
sylibr |
|- ( ph -> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) e. ( ( Base ` R ) ^m D ) ) |
47 |
1 2 34 3 7 5 6
|
psrmulfval |
|- ( ph -> ( X .x. Y ) = ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) ) |
48 |
|
reldmpsr |
|- Rel dom mPwSer |
49 |
48 1 2
|
elbasov |
|- ( X e. B -> ( I e. _V /\ R e. _V ) ) |
50 |
5 49
|
syl |
|- ( ph -> ( I e. _V /\ R e. _V ) ) |
51 |
50
|
simpld |
|- ( ph -> I e. _V ) |
52 |
1 8 7 2 51
|
psrbas |
|- ( ph -> B = ( ( Base ` R ) ^m D ) ) |
53 |
46 47 52
|
3eltr4d |
|- ( ph -> ( X .x. Y ) e. B ) |