Metamath Proof Explorer


Theorem coe1fzgsumdlem

Description: Lemma for coe1fzgsumd (induction step). (Contributed by AV, 8-Oct-2019)

Ref Expression
Hypotheses coe1fzgsumd.p
|- P = ( Poly1 ` R )
coe1fzgsumd.b
|- B = ( Base ` P )
coe1fzgsumd.r
|- ( ph -> R e. Ring )
coe1fzgsumd.k
|- ( ph -> K e. NN0 )
Assertion coe1fzgsumdlem
|- ( ( 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 ) ) ) ) ) )

Proof

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