Metamath Proof Explorer

Theorem evl1gsumdlem

Description: Lemma for evl1gsumd (induction step). (Contributed by AV, 17-Sep-2019)

Ref Expression
Hypotheses evl1gsumd.q 
|- O = ( eval1 ` R )
evl1gsumd.p 
|- P = ( Poly1 ` R )
evl1gsumd.b 
|- B = ( Base ` R )
evl1gsumd.u 
|- U = ( Base ` P )
evl1gsumd.r 
|- ( ph -> R e. CRing )
evl1gsumd.y 
|- ( ph -> Y e. B )
Assertion evl1gsumdlem 
|- ( ( m e. Fin /\ -. a e. m /\ ph ) -> ( ( A. x e. m M e. U -> ( ( O ` ( P gsum ( x e. m |-> M ) ) ) ` Y ) = ( R gsum ( x e. m |-> ( ( O ` M ) ` Y ) ) ) ) -> ( A. x e. ( m u. { a } ) M e. U -> ( ( O ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` Y ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( O ` M ) ` Y ) ) ) ) ) )

Proof

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