Metamath Proof Explorer

Theorem evl1gsumd

Description: Polynomial evaluation builder for a finite group sum of polynomials. (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 )
evl1gsumd.m 
|- ( ph -> A. x e. N M e. U )
evl1gsumd.n 
|- ( ph -> N e. Fin )
Assertion evl1gsumd 
|- ( ph -> ( ( O ` ( P gsum ( x e. N |-> M ) ) ) ` Y ) = ( R gsum ( x e. N |-> ( ( 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 evl1gsumd.m 
 |-  ( ph -> A. x e. N M e. U )
8 evl1gsumd.n 
 |-  ( ph -> N e. Fin )
9 raleq 
 |-  ( n = (/) -> ( A. x e. n M e. U <-> A. x e. (/) M e. U ) )
10 9 anbi2d 
 |-  ( n = (/) -> ( ( ph /\ A. x e. n M e. U ) <-> ( ph /\ A. x e. (/) M e. U ) ) )
11 mpteq1 
 |-  ( n = (/) -> ( x e. n |-> M ) = ( x e. (/) |-> M ) )
12 11 oveq2d 
 |-  ( n = (/) -> ( P gsum ( x e. n |-> M ) ) = ( P gsum ( x e. (/) |-> M ) ) )
13 12 fveq2d 
 |-  ( n = (/) -> ( O ` ( P gsum ( x e. n |-> M ) ) ) = ( O ` ( P gsum ( x e. (/) |-> M ) ) ) )
14 13 fveq1d 
 |-  ( n = (/) -> ( ( O ` ( P gsum ( x e. n |-> M ) ) ) ` Y ) = ( ( O ` ( P gsum ( x e. (/) |-> M ) ) ) ` Y ) )
15 mpteq1 
 |-  ( n = (/) -> ( x e. n |-> ( ( O ` M ) ` Y ) ) = ( x e. (/) |-> ( ( O ` M ) ` Y ) ) )
16 15 oveq2d 
 |-  ( n = (/) -> ( R gsum ( x e. n |-> ( ( O ` M ) ` Y ) ) ) = ( R gsum ( x e. (/) |-> ( ( O ` M ) ` Y ) ) ) )
17 14 16 eqeq12d 
 |-  ( n = (/) -> ( ( ( O ` ( P gsum ( x e. n |-> M ) ) ) ` Y ) = ( R gsum ( x e. n |-> ( ( O ` M ) ` Y ) ) ) <-> ( ( O ` ( P gsum ( x e. (/) |-> M ) ) ) ` Y ) = ( R gsum ( x e. (/) |-> ( ( O ` M ) ` Y ) ) ) ) )
18 10 17 imbi12d 
 |-  ( n = (/) -> ( ( ( ph /\ A. x e. n M e. U ) -> ( ( O ` ( P gsum ( x e. n |-> M ) ) ) ` Y ) = ( R gsum ( x e. n |-> ( ( O ` M ) ` Y ) ) ) ) <-> ( ( ph /\ A. x e. (/) M e. U ) -> ( ( O ` ( P gsum ( x e. (/) |-> M ) ) ) ` Y ) = ( R gsum ( x e. (/) |-> ( ( O ` M ) ` Y ) ) ) ) ) )
19 raleq 
 |-  ( n = m -> ( A. x e. n M e. U <-> A. x e. m M e. U ) )
20 19 anbi2d 
 |-  ( n = m -> ( ( ph /\ A. x e. n M e. U ) <-> ( ph /\ A. x e. m M e. U ) ) )
21 mpteq1 
 |-  ( n = m -> ( x e. n |-> M ) = ( x e. m |-> M ) )
22 21 oveq2d 
 |-  ( n = m -> ( P gsum ( x e. n |-> M ) ) = ( P gsum ( x e. m |-> M ) ) )
23 22 fveq2d 
 |-  ( n = m -> ( O ` ( P gsum ( x e. n |-> M ) ) ) = ( O ` ( P gsum ( x e. m |-> M ) ) ) )
24 23 fveq1d 
 |-  ( n = m -> ( ( O ` ( P gsum ( x e. n |-> M ) ) ) ` Y ) = ( ( O ` ( P gsum ( x e. m |-> M ) ) ) ` Y ) )
25 mpteq1 
 |-  ( n = m -> ( x e. n |-> ( ( O ` M ) ` Y ) ) = ( x e. m |-> ( ( O ` M ) ` Y ) ) )
26 25 oveq2d 
 |-  ( n = m -> ( R gsum ( x e. n |-> ( ( O ` M ) ` Y ) ) ) = ( R gsum ( x e. m |-> ( ( O ` M ) ` Y ) ) ) )
27 24 26 eqeq12d 
 |-  ( n = m -> ( ( ( O ` ( P gsum ( x e. n |-> M ) ) ) ` Y ) = ( R gsum ( x e. n |-> ( ( O ` M ) ` Y ) ) ) <-> ( ( O ` ( P gsum ( x e. m |-> M ) ) ) ` Y ) = ( R gsum ( x e. m |-> ( ( O ` M ) ` Y ) ) ) ) )
28 20 27 imbi12d 
 |-  ( n = m -> ( ( ( ph /\ A. x e. n M e. U ) -> ( ( O ` ( P gsum ( x e. n |-> M ) ) ) ` Y ) = ( R gsum ( x e. n |-> ( ( O ` M ) ` Y ) ) ) ) <-> ( ( ph /\ A. x e. m M e. U ) -> ( ( O ` ( P gsum ( x e. m |-> M ) ) ) ` Y ) = ( R gsum ( x e. m |-> ( ( O ` M ) ` Y ) ) ) ) ) )
29 raleq 
 |-  ( n = ( m u. { a } ) -> ( A. x e. n M e. U <-> A. x e. ( m u. { a } ) M e. U ) )
30 29 anbi2d 
 |-  ( n = ( m u. { a } ) -> ( ( ph /\ A. x e. n M e. U ) <-> ( ph /\ A. x e. ( m u. { a } ) M e. U ) ) )
31 mpteq1 
 |-  ( n = ( m u. { a } ) -> ( x e. n |-> M ) = ( x e. ( m u. { a } ) |-> M ) )
32 31 oveq2d 
 |-  ( n = ( m u. { a } ) -> ( P gsum ( x e. n |-> M ) ) = ( P gsum ( x e. ( m u. { a } ) |-> M ) ) )
33 32 fveq2d 
 |-  ( n = ( m u. { a } ) -> ( O ` ( P gsum ( x e. n |-> M ) ) ) = ( O ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) )
34 33 fveq1d 
 |-  ( n = ( m u. { a } ) -> ( ( O ` ( P gsum ( x e. n |-> M ) ) ) ` Y ) = ( ( O ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` Y ) )
35 mpteq1 
 |-  ( n = ( m u. { a } ) -> ( x e. n |-> ( ( O ` M ) ` Y ) ) = ( x e. ( m u. { a } ) |-> ( ( O ` M ) ` Y ) ) )
36 35 oveq2d 
 |-  ( n = ( m u. { a } ) -> ( R gsum ( x e. n |-> ( ( O ` M ) ` Y ) ) ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( O ` M ) ` Y ) ) ) )
37 34 36 eqeq12d 
 |-  ( n = ( m u. { a } ) -> ( ( ( O ` ( P gsum ( x e. n |-> M ) ) ) ` Y ) = ( R gsum ( x e. n |-> ( ( O ` M ) ` Y ) ) ) <-> ( ( O ` ( P gsum ( x e. ( m u. { a } ) |-> M ) ) ) ` Y ) = ( R gsum ( x e. ( m u. { a } ) |-> ( ( O ` M ) ` Y ) ) ) ) )
38 30 37 imbi12d 
 |-  ( n = ( m u. { a } ) -> ( ( ( ph /\ A. x e. n M e. U ) -> ( ( O ` ( P gsum ( x e. n |-> M ) ) ) ` Y ) = ( R gsum ( x e. n |-> ( ( O ` M ) ` Y ) ) ) ) <-> ( ( ph /\ 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 ) ) ) ) ) )
39 raleq 
 |-  ( n = N -> ( A. x e. n M e. U <-> A. x e. N M e. U ) )
40 39 anbi2d 
 |-  ( n = N -> ( ( ph /\ A. x e. n M e. U ) <-> ( ph /\ A. x e. N M e. U ) ) )
41 mpteq1 
 |-  ( n = N -> ( x e. n |-> M ) = ( x e. N |-> M ) )
42 41 oveq2d 
 |-  ( n = N -> ( P gsum ( x e. n |-> M ) ) = ( P gsum ( x e. N |-> M ) ) )
43 42 fveq2d 
 |-  ( n = N -> ( O ` ( P gsum ( x e. n |-> M ) ) ) = ( O ` ( P gsum ( x e. N |-> M ) ) ) )
44 43 fveq1d 
 |-  ( n = N -> ( ( O ` ( P gsum ( x e. n |-> M ) ) ) ` Y ) = ( ( O ` ( P gsum ( x e. N |-> M ) ) ) ` Y ) )
45 mpteq1 
 |-  ( n = N -> ( x e. n |-> ( ( O ` M ) ` Y ) ) = ( x e. N |-> ( ( O ` M ) ` Y ) ) )
46 45 oveq2d 
 |-  ( n = N -> ( R gsum ( x e. n |-> ( ( O ` M ) ` Y ) ) ) = ( R gsum ( x e. N |-> ( ( O ` M ) ` Y ) ) ) )
47 44 46 eqeq12d 
 |-  ( n = N -> ( ( ( O ` ( P gsum ( x e. n |-> M ) ) ) ` Y ) = ( R gsum ( x e. n |-> ( ( O ` M ) ` Y ) ) ) <-> ( ( O ` ( P gsum ( x e. N |-> M ) ) ) ` Y ) = ( R gsum ( x e. N |-> ( ( O ` M ) ` Y ) ) ) ) )
48 40 47 imbi12d 
 |-  ( n = N -> ( ( ( ph /\ A. x e. n M e. U ) -> ( ( O ` ( P gsum ( x e. n |-> M ) ) ) ` Y ) = ( R gsum ( x e. n |-> ( ( O ` M ) ` Y ) ) ) ) <-> ( ( ph /\ A. x e. N M e. U ) -> ( ( O ` ( P gsum ( x e. N |-> M ) ) ) ` Y ) = ( R gsum ( x e. N |-> ( ( O ` M ) ` Y ) ) ) ) ) )
49 mpt0 
 |-  ( x e. (/) |-> M ) = (/)
50 49 oveq2i 
 |-  ( P gsum ( x e. (/) |-> M ) ) = ( P gsum (/) )
51 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
52 51 gsum0 
 |-  ( P gsum (/) ) = ( 0g ` P )
53 50 52 eqtri 
 |-  ( P gsum ( x e. (/) |-> M ) ) = ( 0g ` P )
54 53 fveq2i 
 |-  ( O ` ( P gsum ( x e. (/) |-> M ) ) ) = ( O ` ( 0g ` P ) )
55 crngring 
 |-  ( R e. CRing -> R e. Ring )
56 5 55 syl 
 |-  ( ph -> R e. Ring )
57 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
58 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
59 2 57 58 51 ply1scl0 
 |-  ( R e. Ring -> ( ( algSc ` P ) ` ( 0g ` R ) ) = ( 0g ` P ) )
60 56 59 syl 
 |-  ( ph -> ( ( algSc ` P ) ` ( 0g ` R ) ) = ( 0g ` P ) )
61 60 eqcomd 
 |-  ( ph -> ( 0g ` P ) = ( ( algSc ` P ) ` ( 0g ` R ) ) )
62 61 fveq2d 
 |-  ( ph -> ( O ` ( 0g ` P ) ) = ( O ` ( ( algSc ` P ) ` ( 0g ` R ) ) ) )
63 54 62 syl5eq 
 |-  ( ph -> ( O ` ( P gsum ( x e. (/) |-> M ) ) ) = ( O ` ( ( algSc ` P ) ` ( 0g ` R ) ) ) )
64 63 fveq1d 
 |-  ( ph -> ( ( O ` ( P gsum ( x e. (/) |-> M ) ) ) ` Y ) = ( ( O ` ( ( algSc ` P ) ` ( 0g ` R ) ) ) ` Y ) )
65 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
66 56 65 syl 
 |-  ( ph -> R e. Grp )
67 3 58 grpidcl 
 |-  ( R e. Grp -> ( 0g ` R ) e. B )
68 66 67 syl 
 |-  ( ph -> ( 0g ` R ) e. B )
69 1 2 3 57 4 5 68 6 evl1scad 
 |-  ( ph -> ( ( ( algSc ` P ) ` ( 0g ` R ) ) e. U /\ ( ( O ` ( ( algSc ` P ) ` ( 0g ` R ) ) ) ` Y ) = ( 0g ` R ) ) )
70 69 simprd 
 |-  ( ph -> ( ( O ` ( ( algSc ` P ) ` ( 0g ` R ) ) ) ` Y ) = ( 0g ` R ) )
71 64 70 eqtrd 
 |-  ( ph -> ( ( O ` ( P gsum ( x e. (/) |-> M ) ) ) ` Y ) = ( 0g ` R ) )
72 mpt0 
 |-  ( x e. (/) |-> ( ( O ` M ) ` Y ) ) = (/)
73 72 oveq2i 
 |-  ( R gsum ( x e. (/) |-> ( ( O ` M ) ` Y ) ) ) = ( R gsum (/) )
74 58 gsum0 
 |-  ( R gsum (/) ) = ( 0g ` R )
75 73 74 eqtri 
 |-  ( R gsum ( x e. (/) |-> ( ( O ` M ) ` Y ) ) ) = ( 0g ` R )
76 71 75 eqtr4di 
 |-  ( ph -> ( ( O ` ( P gsum ( x e. (/) |-> M ) ) ) ` Y ) = ( R gsum ( x e. (/) |-> ( ( O ` M ) ` Y ) ) ) )
77 76 adantr 
 |-  ( ( ph /\ A. x e. (/) M e. U ) -> ( ( O ` ( P gsum ( x e. (/) |-> M ) ) ) ` Y ) = ( R gsum ( x e. (/) |-> ( ( O ` M ) ` Y ) ) ) )
78 1 2 3 4 5 6 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 ) ) ) ) ) )
79 78 3expia 
 |-  ( ( 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 ) ) ) ) ) ) )
80 79 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 ) ) ) ) ) -> ( ph -> ( 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 ) ) ) ) ) ) )
81 impexp 
 |-  ( ( ( ph /\ A. x e. m M e. U ) -> ( ( O ` ( P gsum ( x e. m |-> M ) ) ) ` Y ) = ( R gsum ( x e. m |-> ( ( O ` M ) ` Y ) ) ) ) <-> ( ph -> ( A. x e. m M e. U -> ( ( O ` ( P gsum ( x e. m |-> M ) ) ) ` Y ) = ( R gsum ( x e. m |-> ( ( O ` M ) ` Y ) ) ) ) ) )
82 impexp 
 |-  ( ( ( ph /\ 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 ) ) ) ) <-> ( ph -> ( 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 ) ) ) ) ) )
83 80 81 82 3imtr4g 
 |-  ( ( 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 ) ) ) ) -> ( ( ph /\ 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 ) ) ) ) ) )
84 18 28 38 48 77 83 findcard2s 
 |-  ( N e. Fin -> ( ( ph /\ A. x e. N M e. U ) -> ( ( O ` ( P gsum ( x e. N |-> M ) ) ) ` Y ) = ( R gsum ( x e. N |-> ( ( O ` M ) ` Y ) ) ) ) )
85 84 expd 
 |-  ( N e. Fin -> ( ph -> ( A. x e. N M e. U -> ( ( O ` ( P gsum ( x e. N |-> M ) ) ) ` Y ) = ( R gsum ( x e. N |-> ( ( O ` M ) ` Y ) ) ) ) ) )
86 8 85 mpcom 
 |-  ( ph -> ( A. x e. N M e. U -> ( ( O ` ( P gsum ( x e. N |-> M ) ) ) ` Y ) = ( R gsum ( x e. N |-> ( ( O ` M ) ` Y ) ) ) ) )
87 7 86 mpd 
 |-  ( ph -> ( ( O ` ( P gsum ( x e. N |-> M ) ) ) ` Y ) = ( R gsum ( x e. N |-> ( ( O ` M ) ` Y ) ) ) )