This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid 
 |-  ( ( ( ( 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 ffvelcdmd 
 |-  ( ( ( ( ( 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 ffvelcdmd 
 |-  ( ( ( ( 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 eqtrid 
 |-  ( ( ( ( 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 biimtrid 
 |-  ( ( ( 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 ) ) ) ) ) )