Step |
Hyp |
Ref |
Expression |
1 |
|
psrring.s |
|- S = ( I mPwSer R ) |
2 |
|
psrring.i |
|- ( ph -> I e. V ) |
3 |
|
psrring.r |
|- ( ph -> R e. Ring ) |
4 |
|
psrass.d |
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
5 |
|
psrass.t |
|- .X. = ( .r ` S ) |
6 |
|
psrass.b |
|- B = ( Base ` S ) |
7 |
|
psrass.x |
|- ( ph -> X e. B ) |
8 |
|
psrass.y |
|- ( ph -> Y e. B ) |
9 |
|
psrass.z |
|- ( ph -> Z e. B ) |
10 |
|
psrdi.a |
|- .+ = ( +g ` S ) |
11 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
12 |
1 6 11 10 8 9
|
psradd |
|- ( ph -> ( Y .+ Z ) = ( Y oF ( +g ` R ) Z ) ) |
13 |
12
|
fveq1d |
|- ( ph -> ( ( Y .+ Z ) ` ( k oF - x ) ) = ( ( Y oF ( +g ` R ) Z ) ` ( k oF - x ) ) ) |
14 |
13
|
ad2antrr |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( Y .+ Z ) ` ( k oF - x ) ) = ( ( Y oF ( +g ` R ) Z ) ` ( k oF - x ) ) ) |
15 |
|
ssrab2 |
|- { y e. D | y oR <_ k } C_ D |
16 |
|
eqid |
|- { y e. D | y oR <_ k } = { y e. D | y oR <_ k } |
17 |
4 16
|
psrbagconcl |
|- ( ( k e. D /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. { y e. D | y oR <_ k } ) |
18 |
17
|
adantll |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. { y e. D | y oR <_ k } ) |
19 |
15 18
|
sselid |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. D ) |
20 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
21 |
1 20 4 6 8
|
psrelbas |
|- ( ph -> Y : D --> ( Base ` R ) ) |
22 |
21
|
ad2antrr |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Y : D --> ( Base ` R ) ) |
23 |
22
|
ffnd |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Y Fn D ) |
24 |
1 20 4 6 9
|
psrelbas |
|- ( ph -> Z : D --> ( Base ` R ) ) |
25 |
24
|
ad2antrr |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Z : D --> ( Base ` R ) ) |
26 |
25
|
ffnd |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Z Fn D ) |
27 |
|
ovex |
|- ( NN0 ^m I ) e. _V |
28 |
4 27
|
rabex2 |
|- D e. _V |
29 |
28
|
a1i |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> D e. _V ) |
30 |
|
inidm |
|- ( D i^i D ) = D |
31 |
|
eqidd |
|- ( ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) /\ ( k oF - x ) e. D ) -> ( Y ` ( k oF - x ) ) = ( Y ` ( k oF - x ) ) ) |
32 |
|
eqidd |
|- ( ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) /\ ( k oF - x ) e. D ) -> ( Z ` ( k oF - x ) ) = ( Z ` ( k oF - x ) ) ) |
33 |
23 26 29 29 30 31 32
|
ofval |
|- ( ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) /\ ( k oF - x ) e. D ) -> ( ( Y oF ( +g ` R ) Z ) ` ( k oF - x ) ) = ( ( Y ` ( k oF - x ) ) ( +g ` R ) ( Z ` ( k oF - x ) ) ) ) |
34 |
19 33
|
mpdan |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( Y oF ( +g ` R ) Z ) ` ( k oF - x ) ) = ( ( Y ` ( k oF - x ) ) ( +g ` R ) ( Z ` ( k oF - x ) ) ) ) |
35 |
14 34
|
eqtrd |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( Y .+ Z ) ` ( k oF - x ) ) = ( ( Y ` ( k oF - x ) ) ( +g ` R ) ( Z ` ( k oF - x ) ) ) ) |
36 |
35
|
oveq2d |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) = ( ( X ` x ) ( .r ` R ) ( ( Y ` ( k oF - x ) ) ( +g ` R ) ( Z ` ( k oF - x ) ) ) ) ) |
37 |
3
|
ad2antrr |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> R e. Ring ) |
38 |
1 20 4 6 7
|
psrelbas |
|- ( ph -> X : D --> ( Base ` R ) ) |
39 |
38
|
ad2antrr |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> X : D --> ( Base ` R ) ) |
40 |
|
simpr |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. { y e. D | y oR <_ k } ) |
41 |
15 40
|
sselid |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. D ) |
42 |
39 41
|
ffvelcdmd |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( X ` x ) e. ( Base ` R ) ) |
43 |
22 19
|
ffvelcdmd |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( Y ` ( k oF - x ) ) e. ( Base ` R ) ) |
44 |
25 19
|
ffvelcdmd |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( Z ` ( k oF - x ) ) e. ( Base ` R ) ) |
45 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
46 |
20 11 45
|
ringdi |
|- ( ( R e. Ring /\ ( ( X ` x ) e. ( Base ` R ) /\ ( Y ` ( k oF - x ) ) e. ( Base ` R ) /\ ( Z ` ( k oF - x ) ) e. ( Base ` R ) ) ) -> ( ( X ` x ) ( .r ` R ) ( ( Y ` ( k oF - x ) ) ( +g ` R ) ( Z ` ( k oF - x ) ) ) ) = ( ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ( +g ` R ) ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) |
47 |
37 42 43 44 46
|
syl13anc |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( ( Y ` ( k oF - x ) ) ( +g ` R ) ( Z ` ( k oF - x ) ) ) ) = ( ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ( +g ` R ) ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) |
48 |
36 47
|
eqtrd |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) = ( ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ( +g ` R ) ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) |
49 |
48
|
mpteq2dva |
|- ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ( +g ` R ) ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) |
50 |
4
|
psrbaglefi |
|- ( k e. D -> { y e. D | y oR <_ k } e. Fin ) |
51 |
50
|
adantl |
|- ( ( ph /\ k e. D ) -> { y e. D | y oR <_ k } e. Fin ) |
52 |
20 45 37 42 43
|
ringcld |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) e. ( Base ` R ) ) |
53 |
20 45 37 42 44
|
ringcld |
|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) e. ( Base ` R ) ) |
54 |
|
eqidd |
|- ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) |
55 |
|
eqidd |
|- ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) |
56 |
51 52 53 54 55
|
offval2 |
|- ( ( ph /\ k e. D ) -> ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) oF ( +g ` R ) ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ( +g ` R ) ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) |
57 |
49 56
|
eqtr4d |
|- ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) ) = ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) oF ( +g ` R ) ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) |
58 |
57
|
oveq2d |
|- ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) ) ) = ( R gsum ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) oF ( +g ` R ) ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) ) |
59 |
3
|
adantr |
|- ( ( ph /\ k e. D ) -> R e. Ring ) |
60 |
59
|
ringcmnd |
|- ( ( ph /\ k e. D ) -> R e. CMnd ) |
61 |
|
eqid |
|- ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) |
62 |
|
eqid |
|- ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) |
63 |
20 11 60 51 52 53 61 62
|
gsummptfidmadd2 |
|- ( ( ph /\ k e. D ) -> ( R gsum ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) oF ( +g ` R ) ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) = ( ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ( +g ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) ) |
64 |
58 63
|
eqtrd |
|- ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) ) ) = ( ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ( +g ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) ) |
65 |
64
|
mpteq2dva |
|- ( ph -> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) ) ) ) = ( k e. D |-> ( ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ( +g ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) ) ) |
66 |
3
|
ringgrpd |
|- ( ph -> R e. Grp ) |
67 |
66
|
grpmgmd |
|- ( ph -> R e. Mgm ) |
68 |
1 6 10 67 8 9
|
psraddcl |
|- ( ph -> ( Y .+ Z ) e. B ) |
69 |
1 6 45 5 4 7 68
|
psrmulfval |
|- ( ph -> ( X .X. ( Y .+ Z ) ) = ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) ) ) ) ) |
70 |
1 6 5 3 7 8
|
psrmulcl |
|- ( ph -> ( X .X. Y ) e. B ) |
71 |
1 6 5 3 7 9
|
psrmulcl |
|- ( ph -> ( X .X. Z ) e. B ) |
72 |
1 6 11 10 70 71
|
psradd |
|- ( ph -> ( ( X .X. Y ) .+ ( X .X. Z ) ) = ( ( X .X. Y ) oF ( +g ` R ) ( X .X. Z ) ) ) |
73 |
28
|
a1i |
|- ( ph -> D e. _V ) |
74 |
|
ovexd |
|- ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) e. _V ) |
75 |
|
ovexd |
|- ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) e. _V ) |
76 |
1 6 45 5 4 7 8
|
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 ) ) ) ) ) ) ) |
77 |
1 6 45 5 4 7 9
|
psrmulfval |
|- ( ph -> ( X .X. Z ) = ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) ) |
78 |
73 74 75 76 77
|
offval2 |
|- ( ph -> ( ( X .X. Y ) oF ( +g ` R ) ( X .X. Z ) ) = ( k e. D |-> ( ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ( +g ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) ) ) |
79 |
72 78
|
eqtrd |
|- ( ph -> ( ( X .X. Y ) .+ ( X .X. Z ) ) = ( k e. D |-> ( ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ( +g ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) ) ) |
80 |
65 69 79
|
3eqtr4d |
|- ( ph -> ( X .X. ( Y .+ Z ) ) = ( ( X .X. Y ) .+ ( X .X. Z ) ) ) |