Step |
Hyp |
Ref |
Expression |
1 |
|
coe1fzgsumd.p |
|- P = ( Poly1 ` R ) |
2 |
|
coe1fzgsumd.b |
|- B = ( Base ` P ) |
3 |
|
coe1fzgsumd.r |
|- ( ph -> R e. Ring ) |
4 |
|
coe1fzgsumd.k |
|- ( ph -> K e. NN0 ) |
5 |
|
ralunb |
|- ( A. x e. ( m u. { a } ) M e. B <-> ( A. x e. m M e. B /\ A. x e. { a } M e. B ) ) |
6 |
|
nfcv |
|- F/_ y M |
7 |
|
nfcsb1v |
|- F/_ x [_ y / x ]_ M |
8 |
|
csbeq1a |
|- ( x = y -> M = [_ y / x ]_ M ) |
9 |
6 7 8
|
cbvmpt |
|- ( x e. ( m u. { a } ) |-> M ) = ( y e. ( m u. { a } ) |-> [_ y / x ]_ M ) |
10 |
9
|
oveq2i |
|- ( P gsum ( x e. ( m u. { a } ) |-> M ) ) = ( P gsum ( y e. ( m u. { a } ) |-> [_ y / x ]_ M ) ) |
11 |
|
eqid |
|- ( +g ` P ) = ( +g ` P ) |
12 |
1
|
ply1ring |
|- ( R e. Ring -> P e. Ring ) |
13 |
3 12
|
syl |
|- ( ph -> P e. Ring ) |
14 |
|
ringcmn |
|- ( P e. Ring -> P e. CMnd ) |
15 |
13 14
|
syl |
|- ( ph -> P e. CMnd ) |
16 |
15
|
3ad2ant3 |
|- ( ( m e. Fin /\ -. a e. m /\ ph ) -> P e. CMnd ) |
17 |
16
|
ad2antrr |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> P e. CMnd ) |
18 |
|
simpll1 |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> m e. Fin ) |
19 |
|
rspcsbela |
|- ( ( y e. m /\ A. x e. m M e. B ) -> [_ y / x ]_ M e. B ) |
20 |
19
|
expcom |
|- ( A. x e. m M e. B -> ( y e. m -> [_ y / x ]_ M e. B ) ) |
21 |
20
|
adantl |
|- ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) -> ( y e. m -> [_ y / x ]_ M e. B ) ) |
22 |
21
|
adantr |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> ( y e. m -> [_ y / x ]_ M e. B ) ) |
23 |
22
|
imp |
|- ( ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) /\ y e. m ) -> [_ y / x ]_ M e. B ) |
24 |
|
vex |
|- a e. _V |
25 |
24
|
a1i |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> a e. _V ) |
26 |
|
simpll2 |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> -. a e. m ) |
27 |
|
vsnid |
|- a e. { a } |
28 |
|
rspcsbela |
|- ( ( a e. { a } /\ A. x e. { a } M e. B ) -> [_ a / x ]_ M e. B ) |
29 |
27 28
|
mpan |
|- ( A. x e. { a } M e. B -> [_ a / x ]_ M e. B ) |
30 |
29
|
adantl |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> [_ a / x ]_ M e. B ) |
31 |
|
csbeq1 |
|- ( y = a -> [_ y / x ]_ M = [_ a / x ]_ M ) |
32 |
2 11 17 18 23 25 26 30 31
|
gsumunsn |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> ( P gsum ( y e. ( m u. { a } ) |-> [_ y / x ]_ M ) ) = ( ( P gsum ( y e. m |-> [_ y / x ]_ M ) ) ( +g ` P ) [_ a / x ]_ M ) ) |
33 |
10 32
|
syl5eq |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> ( P gsum ( x e. ( m u. { a } ) |-> M ) ) = ( ( P gsum ( y e. m |-> [_ y / x ]_ M ) ) ( +g ` P ) [_ a / x ]_ M ) ) |
34 |
6 7 8
|
cbvmpt |
|- ( x e. m |-> M ) = ( y e. m |-> [_ y / x ]_ M ) |
35 |
34
|
eqcomi |
|- ( y e. m |-> [_ y / x ]_ M ) = ( x e. m |-> M ) |
36 |
35
|
oveq2i |
|- ( P gsum ( y e. m |-> [_ y / x ]_ M ) ) = ( P gsum ( x e. m |-> M ) ) |
37 |
36
|
oveq1i |
|- ( ( P gsum ( y e. m |-> [_ y / x ]_ M ) ) ( +g ` P ) [_ a / x ]_ M ) = ( ( P gsum ( x e. m |-> M ) ) ( +g ` P ) [_ a / x ]_ M ) |
38 |
33 37
|
eqtrdi |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> ( P gsum ( x e. ( m u. { a } ) |-> M ) ) = ( ( P gsum ( x e. m |-> M ) ) ( +g ` P ) [_ a / x ]_ M ) ) |
39 |
38
|
fveq2d |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) = ( coe1 ` ( ( P gsum ( x e. m |-> M ) ) ( +g ` P ) [_ a / x ]_ M ) ) ) |
40 |
39
|
fveq1d |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( ( coe1 ` ( ( P gsum ( x e. m |-> M ) ) ( +g ` P ) [_ a / x ]_ M ) ) ` K ) ) |
41 |
3
|
3ad2ant3 |
|- ( ( m e. Fin /\ -. a e. m /\ ph ) -> R e. Ring ) |
42 |
41
|
ad2antrr |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> R e. Ring ) |
43 |
|
simplr |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> A. x e. m M e. B ) |
44 |
2 17 18 43
|
gsummptcl |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> ( P gsum ( x e. m |-> M ) ) e. B ) |
45 |
4
|
3ad2ant3 |
|- ( ( m e. Fin /\ -. a e. m /\ ph ) -> K e. NN0 ) |
46 |
45
|
ad2antrr |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> K e. NN0 ) |
47 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
48 |
1 2 11 47
|
coe1addfv |
|- ( ( ( R e. Ring /\ ( P gsum ( x e. m |-> M ) ) e. B /\ [_ a / x ]_ M e. B ) /\ K e. NN0 ) -> ( ( coe1 ` ( ( P gsum ( x e. m |-> M ) ) ( +g ` P ) [_ a / x ]_ M ) ) ` K ) = ( ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) ( +g ` R ) ( ( coe1 ` [_ a / x ]_ M ) ` K ) ) ) |
49 |
42 44 30 46 48
|
syl31anc |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> ( ( coe1 ` ( ( P gsum ( x e. m |-> M ) ) ( +g ` P ) [_ a / x ]_ M ) ) ` K ) = ( ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) ( +g ` R ) ( ( coe1 ` [_ a / x ]_ M ) ` K ) ) ) |
50 |
40 49
|
eqtrd |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) ( +g ` R ) ( ( coe1 ` [_ a / x ]_ M ) ` K ) ) ) |
51 |
|
oveq1 |
|- ( ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) -> ( ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) ( +g ` R ) ( ( coe1 ` [_ a / x ]_ M ) ` K ) ) = ( ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ( +g ` R ) ( ( coe1 ` [_ a / x ]_ M ) ` K ) ) ) |
52 |
50 51
|
sylan9eq |
|- ( ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) /\ ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ( +g ` R ) ( ( coe1 ` [_ a / x ]_ M ) ` K ) ) ) |
53 |
|
nfcv |
|- F/_ y ( ( coe1 ` M ) ` K ) |
54 |
|
nfcsb1v |
|- F/_ x [_ y / x ]_ ( ( coe1 ` M ) ` K ) |
55 |
|
csbeq1a |
|- ( x = y -> ( ( coe1 ` M ) ` K ) = [_ y / x ]_ ( ( coe1 ` M ) ` K ) ) |
56 |
53 54 55
|
cbvmpt |
|- ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) = ( y e. ( m u. { a } ) |-> [_ y / x ]_ ( ( coe1 ` M ) ` K ) ) |
57 |
56
|
oveq2i |
|- ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) = ( R gsum ( y e. ( m u. { a } ) |-> [_ y / x ]_ ( ( coe1 ` M ) ` K ) ) ) |
58 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
59 |
|
ringcmn |
|- ( R e. Ring -> R e. CMnd ) |
60 |
3 59
|
syl |
|- ( ph -> R e. CMnd ) |
61 |
60
|
3ad2ant3 |
|- ( ( m e. Fin /\ -. a e. m /\ ph ) -> R e. CMnd ) |
62 |
61
|
ad2antrr |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> R e. CMnd ) |
63 |
|
csbfv12 |
|- [_ y / x ]_ ( ( coe1 ` M ) ` K ) = ( [_ y / x ]_ ( coe1 ` M ) ` [_ y / x ]_ K ) |
64 |
|
csbfv2g |
|- ( y e. _V -> [_ y / x ]_ ( coe1 ` M ) = ( coe1 ` [_ y / x ]_ M ) ) |
65 |
64
|
elv |
|- [_ y / x ]_ ( coe1 ` M ) = ( coe1 ` [_ y / x ]_ M ) |
66 |
|
csbconstg |
|- ( y e. _V -> [_ y / x ]_ K = K ) |
67 |
66
|
elv |
|- [_ y / x ]_ K = K |
68 |
65 67
|
fveq12i |
|- ( [_ y / x ]_ ( coe1 ` M ) ` [_ y / x ]_ K ) = ( ( coe1 ` [_ y / x ]_ M ) ` K ) |
69 |
63 68
|
eqtri |
|- [_ y / x ]_ ( ( coe1 ` M ) ` K ) = ( ( coe1 ` [_ y / x ]_ M ) ` K ) |
70 |
|
eqid |
|- ( coe1 ` [_ y / x ]_ M ) = ( coe1 ` [_ y / x ]_ M ) |
71 |
70 2 1 58
|
coe1f |
|- ( [_ y / x ]_ M e. B -> ( coe1 ` [_ y / x ]_ M ) : NN0 --> ( Base ` R ) ) |
72 |
23 71
|
syl |
|- ( ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) /\ y e. m ) -> ( coe1 ` [_ y / x ]_ M ) : NN0 --> ( Base ` R ) ) |
73 |
45
|
adantr |
|- ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) -> K e. NN0 ) |
74 |
73
|
ad2antrr |
|- ( ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) /\ y e. m ) -> K e. NN0 ) |
75 |
72 74
|
ffvelrnd |
|- ( ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) /\ y e. m ) -> ( ( coe1 ` [_ y / x ]_ M ) ` K ) e. ( Base ` R ) ) |
76 |
69 75
|
eqeltrid |
|- ( ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) /\ y e. m ) -> [_ y / x ]_ ( ( coe1 ` M ) ` K ) e. ( Base ` R ) ) |
77 |
|
eqid |
|- ( coe1 ` [_ a / x ]_ M ) = ( coe1 ` [_ a / x ]_ M ) |
78 |
77 2 1 58
|
coe1f |
|- ( [_ a / x ]_ M e. B -> ( coe1 ` [_ a / x ]_ M ) : NN0 --> ( Base ` R ) ) |
79 |
30 78
|
syl |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> ( coe1 ` [_ a / x ]_ M ) : NN0 --> ( Base ` R ) ) |
80 |
79 46
|
ffvelrnd |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> ( ( coe1 ` [_ a / x ]_ M ) ` K ) e. ( Base ` R ) ) |
81 |
|
nfcv |
|- F/_ x a |
82 |
|
nfcv |
|- F/_ x coe1 |
83 |
|
nfcsb1v |
|- F/_ x [_ a / x ]_ M |
84 |
82 83
|
nffv |
|- F/_ x ( coe1 ` [_ a / x ]_ M ) |
85 |
|
nfcv |
|- F/_ x K |
86 |
84 85
|
nffv |
|- F/_ x ( ( coe1 ` [_ a / x ]_ M ) ` K ) |
87 |
|
csbeq1a |
|- ( x = a -> M = [_ a / x ]_ M ) |
88 |
87
|
fveq2d |
|- ( x = a -> ( coe1 ` M ) = ( coe1 ` [_ a / x ]_ M ) ) |
89 |
88
|
fveq1d |
|- ( x = a -> ( ( coe1 ` M ) ` K ) = ( ( coe1 ` [_ a / x ]_ M ) ` K ) ) |
90 |
81 86 89
|
csbhypf |
|- ( y = a -> [_ y / x ]_ ( ( coe1 ` M ) ` K ) = ( ( coe1 ` [_ a / x ]_ M ) ` K ) ) |
91 |
58 47 62 18 76 25 26 80 90
|
gsumunsn |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> ( R gsum ( y e. ( m u. { a } ) |-> [_ y / x ]_ ( ( coe1 ` M ) ` K ) ) ) = ( ( R gsum ( y e. m |-> [_ y / x ]_ ( ( coe1 ` M ) ` K ) ) ) ( +g ` R ) ( ( coe1 ` [_ a / x ]_ M ) ` K ) ) ) |
92 |
57 91
|
syl5eq |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) = ( ( R gsum ( y e. m |-> [_ y / x ]_ ( ( coe1 ` M ) ` K ) ) ) ( +g ` R ) ( ( coe1 ` [_ a / x ]_ M ) ` K ) ) ) |
93 |
53 54 55
|
cbvmpt |
|- ( x e. m |-> ( ( coe1 ` M ) ` K ) ) = ( y e. m |-> [_ y / x ]_ ( ( coe1 ` M ) ` K ) ) |
94 |
93
|
eqcomi |
|- ( y e. m |-> [_ y / x ]_ ( ( coe1 ` M ) ` K ) ) = ( x e. m |-> ( ( coe1 ` M ) ` K ) ) |
95 |
94
|
oveq2i |
|- ( R gsum ( y e. m |-> [_ y / x ]_ ( ( coe1 ` M ) ` K ) ) ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) |
96 |
95
|
oveq1i |
|- ( ( R gsum ( y e. m |-> [_ y / x ]_ ( ( coe1 ` M ) ` K ) ) ) ( +g ` R ) ( ( coe1 ` [_ a / x ]_ M ) ` K ) ) = ( ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ( +g ` R ) ( ( coe1 ` [_ a / x ]_ M ) ` K ) ) |
97 |
92 96
|
eqtr2di |
|- ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) -> ( ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ( +g ` R ) ( ( coe1 ` [_ a / x ]_ M ) ` K ) ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) |
98 |
97
|
adantr |
|- ( ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) /\ ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) -> ( ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ( +g ` R ) ( ( coe1 ` [_ a / x ]_ M ) ` K ) ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) |
99 |
52 98
|
eqtrd |
|- ( ( ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) /\ A. x e. { a } M e. B ) /\ ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) |
100 |
99
|
exp31 |
|- ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) -> ( A. x e. { a } M e. B -> ( ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) ) ) |
101 |
100
|
com23 |
|- ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ A. x e. m M e. B ) -> ( ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) -> ( A. x e. { a } M e. B -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) ) ) |
102 |
101
|
ex |
|- ( ( m e. Fin /\ -. a e. m /\ ph ) -> ( A. x e. m M e. B -> ( ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) -> ( A. x e. { a } M e. B -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) ) ) ) |
103 |
102
|
a2d |
|- ( ( m e. Fin /\ -. a e. m /\ ph ) -> ( ( A. x e. m M e. B -> ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) -> ( A. x e. m M e. B -> ( A. x e. { a } M e. B -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) ) ) ) |
104 |
103
|
imp4b |
|- ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ ( A. x e. m M e. B -> ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) ) -> ( ( A. x e. m M e. B /\ A. x e. { a } M e. B ) -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) ) |
105 |
5 104
|
syl5bi |
|- ( ( ( m e. Fin /\ -. a e. m /\ ph ) /\ ( A. x e. m M e. B -> ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) ) -> ( A. x e. ( m u. { a } ) M e. B -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) ) |
106 |
105
|
ex |
|- ( ( m e. Fin /\ -. a e. m /\ ph ) -> ( ( A. x e. m M e. B -> ( ( coe1 ` ( P gsum ( x e. m |-> M ) ) ) ` K ) = ( R gsum ( x e. m |-> ( ( coe1 ` M ) ` K ) ) ) ) -> ( A. x e. ( m u. { a } ) M e. B -> ( ( coe1 ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` K ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( coe1 ` M ) ` K ) ) ) ) ) ) |