Step |
Hyp |
Ref |
Expression |
1 |
|
sum2dchr.g |
|- G = ( DChr ` N ) |
2 |
|
sum2dchr.d |
|- D = ( Base ` G ) |
3 |
|
sum2dchr.z |
|- Z = ( Z/nZ ` N ) |
4 |
|
sum2dchr.b |
|- B = ( Base ` Z ) |
5 |
|
sum2dchr.u |
|- U = ( Unit ` Z ) |
6 |
|
sum2dchr.n |
|- ( ph -> N e. NN ) |
7 |
|
sum2dchr.a |
|- ( ph -> A e. B ) |
8 |
|
sum2dchr.c |
|- ( ph -> C e. U ) |
9 |
|
eqid |
|- ( 1r ` Z ) = ( 1r ` Z ) |
10 |
6
|
nnnn0d |
|- ( ph -> N e. NN0 ) |
11 |
3
|
zncrng |
|- ( N e. NN0 -> Z e. CRing ) |
12 |
|
crngring |
|- ( Z e. CRing -> Z e. Ring ) |
13 |
10 11 12
|
3syl |
|- ( ph -> Z e. Ring ) |
14 |
|
eqid |
|- ( /r ` Z ) = ( /r ` Z ) |
15 |
4 5 14
|
dvrcl |
|- ( ( Z e. Ring /\ A e. B /\ C e. U ) -> ( A ( /r ` Z ) C ) e. B ) |
16 |
13 7 8 15
|
syl3anc |
|- ( ph -> ( A ( /r ` Z ) C ) e. B ) |
17 |
1 2 3 9 4 6 16
|
sumdchr |
|- ( ph -> sum_ x e. D ( x ` ( A ( /r ` Z ) C ) ) = if ( ( A ( /r ` Z ) C ) = ( 1r ` Z ) , ( phi ` N ) , 0 ) ) |
18 |
|
eqid |
|- ( .r ` Z ) = ( .r ` Z ) |
19 |
|
eqid |
|- ( invr ` Z ) = ( invr ` Z ) |
20 |
4 18 5 19 14
|
dvrval |
|- ( ( A e. B /\ C e. U ) -> ( A ( /r ` Z ) C ) = ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) ) |
21 |
7 8 20
|
syl2anc |
|- ( ph -> ( A ( /r ` Z ) C ) = ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) ) |
22 |
21
|
adantr |
|- ( ( ph /\ x e. D ) -> ( A ( /r ` Z ) C ) = ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) ) |
23 |
22
|
fveq2d |
|- ( ( ph /\ x e. D ) -> ( x ` ( A ( /r ` Z ) C ) ) = ( x ` ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) ) ) |
24 |
1 3 2
|
dchrmhm |
|- D C_ ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) |
25 |
|
simpr |
|- ( ( ph /\ x e. D ) -> x e. D ) |
26 |
24 25
|
sselid |
|- ( ( ph /\ x e. D ) -> x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) |
27 |
7
|
adantr |
|- ( ( ph /\ x e. D ) -> A e. B ) |
28 |
4 5
|
unitss |
|- U C_ B |
29 |
5 19
|
unitinvcl |
|- ( ( Z e. Ring /\ C e. U ) -> ( ( invr ` Z ) ` C ) e. U ) |
30 |
13 8 29
|
syl2anc |
|- ( ph -> ( ( invr ` Z ) ` C ) e. U ) |
31 |
30
|
adantr |
|- ( ( ph /\ x e. D ) -> ( ( invr ` Z ) ` C ) e. U ) |
32 |
28 31
|
sselid |
|- ( ( ph /\ x e. D ) -> ( ( invr ` Z ) ` C ) e. B ) |
33 |
|
eqid |
|- ( mulGrp ` Z ) = ( mulGrp ` Z ) |
34 |
33 4
|
mgpbas |
|- B = ( Base ` ( mulGrp ` Z ) ) |
35 |
33 18
|
mgpplusg |
|- ( .r ` Z ) = ( +g ` ( mulGrp ` Z ) ) |
36 |
|
eqid |
|- ( mulGrp ` CCfld ) = ( mulGrp ` CCfld ) |
37 |
|
cnfldmul |
|- x. = ( .r ` CCfld ) |
38 |
36 37
|
mgpplusg |
|- x. = ( +g ` ( mulGrp ` CCfld ) ) |
39 |
34 35 38
|
mhmlin |
|- ( ( x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A e. B /\ ( ( invr ` Z ) ` C ) e. B ) -> ( x ` ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) ) = ( ( x ` A ) x. ( x ` ( ( invr ` Z ) ` C ) ) ) ) |
40 |
26 27 32 39
|
syl3anc |
|- ( ( ph /\ x e. D ) -> ( x ` ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) ) = ( ( x ` A ) x. ( x ` ( ( invr ` Z ) ` C ) ) ) ) |
41 |
|
eqid |
|- ( ( mulGrp ` Z ) |`s U ) = ( ( mulGrp ` Z ) |`s U ) |
42 |
|
eqid |
|- ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |
43 |
1 3 2 5 41 42 25
|
dchrghm |
|- ( ( ph /\ x e. D ) -> ( x |` U ) e. ( ( ( mulGrp ` Z ) |`s U ) GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ) |
44 |
8
|
adantr |
|- ( ( ph /\ x e. D ) -> C e. U ) |
45 |
5 41
|
unitgrpbas |
|- U = ( Base ` ( ( mulGrp ` Z ) |`s U ) ) |
46 |
5 41 19
|
invrfval |
|- ( invr ` Z ) = ( invg ` ( ( mulGrp ` Z ) |`s U ) ) |
47 |
|
cnfldbas |
|- CC = ( Base ` CCfld ) |
48 |
|
cnfld0 |
|- 0 = ( 0g ` CCfld ) |
49 |
|
cndrng |
|- CCfld e. DivRing |
50 |
47 48 49
|
drngui |
|- ( CC \ { 0 } ) = ( Unit ` CCfld ) |
51 |
|
eqid |
|- ( invr ` CCfld ) = ( invr ` CCfld ) |
52 |
50 42 51
|
invrfval |
|- ( invr ` CCfld ) = ( invg ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) |
53 |
45 46 52
|
ghminv |
|- ( ( ( x |` U ) e. ( ( ( mulGrp ` Z ) |`s U ) GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) /\ C e. U ) -> ( ( x |` U ) ` ( ( invr ` Z ) ` C ) ) = ( ( invr ` CCfld ) ` ( ( x |` U ) ` C ) ) ) |
54 |
43 44 53
|
syl2anc |
|- ( ( ph /\ x e. D ) -> ( ( x |` U ) ` ( ( invr ` Z ) ` C ) ) = ( ( invr ` CCfld ) ` ( ( x |` U ) ` C ) ) ) |
55 |
31
|
fvresd |
|- ( ( ph /\ x e. D ) -> ( ( x |` U ) ` ( ( invr ` Z ) ` C ) ) = ( x ` ( ( invr ` Z ) ` C ) ) ) |
56 |
44
|
fvresd |
|- ( ( ph /\ x e. D ) -> ( ( x |` U ) ` C ) = ( x ` C ) ) |
57 |
56
|
fveq2d |
|- ( ( ph /\ x e. D ) -> ( ( invr ` CCfld ) ` ( ( x |` U ) ` C ) ) = ( ( invr ` CCfld ) ` ( x ` C ) ) ) |
58 |
1 3 2 4 25
|
dchrf |
|- ( ( ph /\ x e. D ) -> x : B --> CC ) |
59 |
28 44
|
sselid |
|- ( ( ph /\ x e. D ) -> C e. B ) |
60 |
58 59
|
ffvelrnd |
|- ( ( ph /\ x e. D ) -> ( x ` C ) e. CC ) |
61 |
1 3 2 4 5 25 59
|
dchrn0 |
|- ( ( ph /\ x e. D ) -> ( ( x ` C ) =/= 0 <-> C e. U ) ) |
62 |
44 61
|
mpbird |
|- ( ( ph /\ x e. D ) -> ( x ` C ) =/= 0 ) |
63 |
|
cnfldinv |
|- ( ( ( x ` C ) e. CC /\ ( x ` C ) =/= 0 ) -> ( ( invr ` CCfld ) ` ( x ` C ) ) = ( 1 / ( x ` C ) ) ) |
64 |
60 62 63
|
syl2anc |
|- ( ( ph /\ x e. D ) -> ( ( invr ` CCfld ) ` ( x ` C ) ) = ( 1 / ( x ` C ) ) ) |
65 |
|
recval |
|- ( ( ( x ` C ) e. CC /\ ( x ` C ) =/= 0 ) -> ( 1 / ( x ` C ) ) = ( ( * ` ( x ` C ) ) / ( ( abs ` ( x ` C ) ) ^ 2 ) ) ) |
66 |
60 62 65
|
syl2anc |
|- ( ( ph /\ x e. D ) -> ( 1 / ( x ` C ) ) = ( ( * ` ( x ` C ) ) / ( ( abs ` ( x ` C ) ) ^ 2 ) ) ) |
67 |
1 2 25 3 5 44
|
dchrabs |
|- ( ( ph /\ x e. D ) -> ( abs ` ( x ` C ) ) = 1 ) |
68 |
67
|
oveq1d |
|- ( ( ph /\ x e. D ) -> ( ( abs ` ( x ` C ) ) ^ 2 ) = ( 1 ^ 2 ) ) |
69 |
|
sq1 |
|- ( 1 ^ 2 ) = 1 |
70 |
68 69
|
eqtrdi |
|- ( ( ph /\ x e. D ) -> ( ( abs ` ( x ` C ) ) ^ 2 ) = 1 ) |
71 |
70
|
oveq2d |
|- ( ( ph /\ x e. D ) -> ( ( * ` ( x ` C ) ) / ( ( abs ` ( x ` C ) ) ^ 2 ) ) = ( ( * ` ( x ` C ) ) / 1 ) ) |
72 |
60
|
cjcld |
|- ( ( ph /\ x e. D ) -> ( * ` ( x ` C ) ) e. CC ) |
73 |
72
|
div1d |
|- ( ( ph /\ x e. D ) -> ( ( * ` ( x ` C ) ) / 1 ) = ( * ` ( x ` C ) ) ) |
74 |
66 71 73
|
3eqtrd |
|- ( ( ph /\ x e. D ) -> ( 1 / ( x ` C ) ) = ( * ` ( x ` C ) ) ) |
75 |
57 64 74
|
3eqtrd |
|- ( ( ph /\ x e. D ) -> ( ( invr ` CCfld ) ` ( ( x |` U ) ` C ) ) = ( * ` ( x ` C ) ) ) |
76 |
54 55 75
|
3eqtr3d |
|- ( ( ph /\ x e. D ) -> ( x ` ( ( invr ` Z ) ` C ) ) = ( * ` ( x ` C ) ) ) |
77 |
76
|
oveq2d |
|- ( ( ph /\ x e. D ) -> ( ( x ` A ) x. ( x ` ( ( invr ` Z ) ` C ) ) ) = ( ( x ` A ) x. ( * ` ( x ` C ) ) ) ) |
78 |
23 40 77
|
3eqtrd |
|- ( ( ph /\ x e. D ) -> ( x ` ( A ( /r ` Z ) C ) ) = ( ( x ` A ) x. ( * ` ( x ` C ) ) ) ) |
79 |
78
|
sumeq2dv |
|- ( ph -> sum_ x e. D ( x ` ( A ( /r ` Z ) C ) ) = sum_ x e. D ( ( x ` A ) x. ( * ` ( x ` C ) ) ) ) |
80 |
4 5 14 9
|
dvreq1 |
|- ( ( Z e. Ring /\ A e. B /\ C e. U ) -> ( ( A ( /r ` Z ) C ) = ( 1r ` Z ) <-> A = C ) ) |
81 |
13 7 8 80
|
syl3anc |
|- ( ph -> ( ( A ( /r ` Z ) C ) = ( 1r ` Z ) <-> A = C ) ) |
82 |
81
|
ifbid |
|- ( ph -> if ( ( A ( /r ` Z ) C ) = ( 1r ` Z ) , ( phi ` N ) , 0 ) = if ( A = C , ( phi ` N ) , 0 ) ) |
83 |
17 79 82
|
3eqtr3d |
|- ( ph -> sum_ x e. D ( ( x ` A ) x. ( * ` ( x ` C ) ) ) = if ( A = C , ( phi ` N ) , 0 ) ) |