Metamath Proof Explorer

Theorem sumdchr2

Description: Lemma for sumdchr . (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses sumdchr.g 
|- G = ( DChr ` N )
sumdchr.d 
|- D = ( Base ` G )
sumdchr2.z 
|- Z = ( Z/nZ ` N )
sumdchr2.1 
|- .1. = ( 1r ` Z )
sumdchr2.b 
|- B = ( Base ` Z )
sumdchr2.n 
|- ( ph -> N e. NN )
sumdchr2.x 
|- ( ph -> A e. B )
Assertion sumdchr2 
|- ( ph -> sum_ x e. D ( x ` A ) = if ( A = .1. , ( # ` D ) , 0 ) )

Proof

Step Hyp Ref Expression
1 sumdchr.g 
 |-  G = ( DChr ` N )
2 sumdchr.d 
 |-  D = ( Base ` G )
3 sumdchr2.z 
 |-  Z = ( Z/nZ ` N )
4 sumdchr2.1 
 |-  .1. = ( 1r ` Z )
5 sumdchr2.b 
 |-  B = ( Base ` Z )
6 sumdchr2.n 
 |-  ( ph -> N e. NN )
7 sumdchr2.x 
 |-  ( ph -> A e. B )
8 eqeq2 
 |-  ( ( # ` D ) = if ( A = .1. , ( # ` D ) , 0 ) -> ( sum_ x e. D ( x ` A ) = ( # ` D ) <-> sum_ x e. D ( x ` A ) = if ( A = .1. , ( # ` D ) , 0 ) ) )
9 eqeq2 
 |-  ( 0 = if ( A = .1. , ( # ` D ) , 0 ) -> ( sum_ x e. D ( x ` A ) = 0 <-> sum_ x e. D ( x ` A ) = if ( A = .1. , ( # ` D ) , 0 ) ) )
10 fveq2 
 |-  ( A = .1. -> ( x ` A ) = ( x ` .1. ) )
11 1 3 2 dchrmhm 
 |-  D C_ ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) )
12 simpr 
 |-  ( ( ph /\ x e. D ) -> x e. D )
13 11 12 sselid 
 |-  ( ( ph /\ x e. D ) -> x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
14 eqid 
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
15 14 4 ringidval 
 |-  .1. = ( 0g ` ( mulGrp ` Z ) )
16 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
17 cnfld1 
 |-  1 = ( 1r ` CCfld )
18 16 17 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
19 15 18 mhm0 
 |-  ( x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) -> ( x ` .1. ) = 1 )
20 13 19 syl 
 |-  ( ( ph /\ x e. D ) -> ( x ` .1. ) = 1 )
21 10 20 sylan9eqr 
 |-  ( ( ( ph /\ x e. D ) /\ A = .1. ) -> ( x ` A ) = 1 )
22 21 an32s 
 |-  ( ( ( ph /\ A = .1. ) /\ x e. D ) -> ( x ` A ) = 1 )
23 22 sumeq2dv 
 |-  ( ( ph /\ A = .1. ) -> sum_ x e. D ( x ` A ) = sum_ x e. D 1 )
24 1 2 dchrfi 
 |-  ( N e. NN -> D e. Fin )
25 6 24 syl 
 |-  ( ph -> D e. Fin )
26 ax-1cn 
 |-  1 e. CC
27 fsumconst 
 |-  ( ( D e. Fin /\ 1 e. CC ) -> sum_ x e. D 1 = ( ( # ` D ) x. 1 ) )
28 25 26 27 sylancl 
 |-  ( ph -> sum_ x e. D 1 = ( ( # ` D ) x. 1 ) )
29 hashcl 
 |-  ( D e. Fin -> ( # ` D ) e. NN0 )
30 6 24 29 3syl 
 |-  ( ph -> ( # ` D ) e. NN0 )
31 30 nn0cnd 
 |-  ( ph -> ( # ` D ) e. CC )
32 31 mulid1d 
 |-  ( ph -> ( ( # ` D ) x. 1 ) = ( # ` D ) )
33 28 32 eqtrd 
 |-  ( ph -> sum_ x e. D 1 = ( # ` D ) )
34 33 adantr 
 |-  ( ( ph /\ A = .1. ) -> sum_ x e. D 1 = ( # ` D ) )
35 23 34 eqtrd 
 |-  ( ( ph /\ A = .1. ) -> sum_ x e. D ( x ` A ) = ( # ` D ) )
36 df-ne 
 |-  ( A =/= .1. <-> -. A = .1. )
37 6 adantr 
 |-  ( ( ph /\ A =/= .1. ) -> N e. NN )
38 simpr 
 |-  ( ( ph /\ A =/= .1. ) -> A =/= .1. )
39 7 adantr 
 |-  ( ( ph /\ A =/= .1. ) -> A e. B )
40 1 3 2 5 4 37 38 39 dchrpt 
 |-  ( ( ph /\ A =/= .1. ) -> E. y e. D ( y ` A ) =/= 1 )
41 37 adantr 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> N e. NN )
42 41 24 syl 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> D e. Fin )
43 simpr 
 |-  ( ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) /\ x e. D ) -> x e. D )
44 1 3 2 5 43 dchrf 
 |-  ( ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) /\ x e. D ) -> x : B --> CC )
45 39 adantr 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> A e. B )
46 45 adantr 
 |-  ( ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) /\ x e. D ) -> A e. B )
47 44 46 ffvelrnd 
 |-  ( ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) /\ x e. D ) -> ( x ` A ) e. CC )
48 42 47 fsumcl 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> sum_ x e. D ( x ` A ) e. CC )
49 0cnd 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> 0 e. CC )
50 simprl 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> y e. D )
51 1 3 2 5 50 dchrf 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> y : B --> CC )
52 51 45 ffvelrnd 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( y ` A ) e. CC )
53 subcl 
 |-  ( ( ( y ` A ) e. CC /\ 1 e. CC ) -> ( ( y ` A ) - 1 ) e. CC )
54 52 26 53 sylancl 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( ( y ` A ) - 1 ) e. CC )
55 simprr 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( y ` A ) =/= 1 )
56 subeq0 
 |-  ( ( ( y ` A ) e. CC /\ 1 e. CC ) -> ( ( ( y ` A ) - 1 ) = 0 <-> ( y ` A ) = 1 ) )
57 52 26 56 sylancl 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( ( ( y ` A ) - 1 ) = 0 <-> ( y ` A ) = 1 ) )
58 57 necon3bid 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( ( ( y ` A ) - 1 ) =/= 0 <-> ( y ` A ) =/= 1 ) )
59 55 58 mpbird 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( ( y ` A ) - 1 ) =/= 0 )
60 oveq2 
 |-  ( z = x -> ( y ( +g ` G ) z ) = ( y ( +g ` G ) x ) )
61 60 fveq1d 
 |-  ( z = x -> ( ( y ( +g ` G ) z ) ` A ) = ( ( y ( +g ` G ) x ) ` A ) )
62 61 cbvsumv 
 |-  sum_ z e. D ( ( y ( +g ` G ) z ) ` A ) = sum_ x e. D ( ( y ( +g ` G ) x ) ` A )
63 eqid 
 |-  ( +g ` G ) = ( +g ` G )
64 50 adantr 
 |-  ( ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) /\ x e. D ) -> y e. D )
65 1 3 2 63 64 43 dchrmul 
 |-  ( ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) /\ x e. D ) -> ( y ( +g ` G ) x ) = ( y oF x. x ) )
66 65 fveq1d 
 |-  ( ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) /\ x e. D ) -> ( ( y ( +g ` G ) x ) ` A ) = ( ( y oF x. x ) ` A ) )
67 51 adantr 
 |-  ( ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) /\ x e. D ) -> y : B --> CC )
68 67 ffnd 
 |-  ( ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) /\ x e. D ) -> y Fn B )
69 44 ffnd 
 |-  ( ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) /\ x e. D ) -> x Fn B )
70 5 fvexi 
 |-  B e. _V
71 70 a1i 
 |-  ( ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) /\ x e. D ) -> B e. _V )
72 fnfvof 
 |-  ( ( ( y Fn B /\ x Fn B ) /\ ( B e. _V /\ A e. B ) ) -> ( ( y oF x. x ) ` A ) = ( ( y ` A ) x. ( x ` A ) ) )
73 68 69 71 46 72 syl22anc 
 |-  ( ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) /\ x e. D ) -> ( ( y oF x. x ) ` A ) = ( ( y ` A ) x. ( x ` A ) ) )
74 66 73 eqtrd 
 |-  ( ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) /\ x e. D ) -> ( ( y ( +g ` G ) x ) ` A ) = ( ( y ` A ) x. ( x ` A ) ) )
75 74 sumeq2dv 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> sum_ x e. D ( ( y ( +g ` G ) x ) ` A ) = sum_ x e. D ( ( y ` A ) x. ( x ` A ) ) )
76 62 75 syl5eq 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> sum_ z e. D ( ( y ( +g ` G ) z ) ` A ) = sum_ x e. D ( ( y ` A ) x. ( x ` A ) ) )
77 fveq1 
 |-  ( x = ( y ( +g ` G ) z ) -> ( x ` A ) = ( ( y ( +g ` G ) z ) ` A ) )
78 1 dchrabl 
 |-  ( N e. NN -> G e. Abel )
79 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
80 41 78 79 3syl 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> G e. Grp )
81 eqid 
 |-  ( a e. D |-> ( b e. D |-> ( a ( +g ` G ) b ) ) ) = ( a e. D |-> ( b e. D |-> ( a ( +g ` G ) b ) ) )
82 81 2 63 grplactf1o 
 |-  ( ( G e. Grp /\ y e. D ) -> ( ( a e. D |-> ( b e. D |-> ( a ( +g ` G ) b ) ) ) ` y ) : D -1-1-onto-> D )
83 80 50 82 syl2anc 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( ( a e. D |-> ( b e. D |-> ( a ( +g ` G ) b ) ) ) ` y ) : D -1-1-onto-> D )
84 81 2 grplactval 
 |-  ( ( y e. D /\ z e. D ) -> ( ( ( a e. D |-> ( b e. D |-> ( a ( +g ` G ) b ) ) ) ` y ) ` z ) = ( y ( +g ` G ) z ) )
85 50 84 sylan 
 |-  ( ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) /\ z e. D ) -> ( ( ( a e. D |-> ( b e. D |-> ( a ( +g ` G ) b ) ) ) ` y ) ` z ) = ( y ( +g ` G ) z ) )
86 77 42 83 85 47 fsumf1o 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> sum_ x e. D ( x ` A ) = sum_ z e. D ( ( y ( +g ` G ) z ) ` A ) )
87 42 52 47 fsummulc2 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( ( y ` A ) x. sum_ x e. D ( x ` A ) ) = sum_ x e. D ( ( y ` A ) x. ( x ` A ) ) )
88 76 86 87 3eqtr4rd 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( ( y ` A ) x. sum_ x e. D ( x ` A ) ) = sum_ x e. D ( x ` A ) )
89 48 mulid2d 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( 1 x. sum_ x e. D ( x ` A ) ) = sum_ x e. D ( x ` A ) )
90 88 89 oveq12d 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( ( ( y ` A ) x. sum_ x e. D ( x ` A ) ) - ( 1 x. sum_ x e. D ( x ` A ) ) ) = ( sum_ x e. D ( x ` A ) - sum_ x e. D ( x ` A ) ) )
91 48 subidd 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( sum_ x e. D ( x ` A ) - sum_ x e. D ( x ` A ) ) = 0 )
92 90 91 eqtrd 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( ( ( y ` A ) x. sum_ x e. D ( x ` A ) ) - ( 1 x. sum_ x e. D ( x ` A ) ) ) = 0 )
93 26 a1i 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> 1 e. CC )
94 52 93 48 subdird 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( ( ( y ` A ) - 1 ) x. sum_ x e. D ( x ` A ) ) = ( ( ( y ` A ) x. sum_ x e. D ( x ` A ) ) - ( 1 x. sum_ x e. D ( x ` A ) ) ) )
95 54 mul01d 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( ( ( y ` A ) - 1 ) x. 0 ) = 0 )
96 92 94 95 3eqtr4d 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> ( ( ( y ` A ) - 1 ) x. sum_ x e. D ( x ` A ) ) = ( ( ( y ` A ) - 1 ) x. 0 ) )
97 48 49 54 59 96 mulcanad 
 |-  ( ( ( ph /\ A =/= .1. ) /\ ( y e. D /\ ( y ` A ) =/= 1 ) ) -> sum_ x e. D ( x ` A ) = 0 )
98 40 97 rexlimddv 
 |-  ( ( ph /\ A =/= .1. ) -> sum_ x e. D ( x ` A ) = 0 )
99 36 98 sylan2br 
 |-  ( ( ph /\ -. A = .1. ) -> sum_ x e. D ( x ` A ) = 0 )
100 8 9 35 99 ifbothda 
 |-  ( ph -> sum_ x e. D ( x ` A ) = if ( A = .1. , ( # ` D ) , 0 ) )