Step |
Hyp |
Ref |
Expression |
1 |
|
dchrpt.g |
|- G = ( DChr ` N ) |
2 |
|
dchrpt.z |
|- Z = ( Z/nZ ` N ) |
3 |
|
dchrpt.d |
|- D = ( Base ` G ) |
4 |
|
dchrpt.b |
|- B = ( Base ` Z ) |
5 |
|
dchrpt.1 |
|- .1. = ( 1r ` Z ) |
6 |
|
dchrpt.n |
|- ( ph -> N e. NN ) |
7 |
|
dchrpt.n1 |
|- ( ph -> A =/= .1. ) |
8 |
|
dchrpt.u |
|- U = ( Unit ` Z ) |
9 |
|
dchrpt.h |
|- H = ( ( mulGrp ` Z ) |`s U ) |
10 |
|
dchrpt.m |
|- .x. = ( .g ` H ) |
11 |
|
dchrpt.s |
|- S = ( k e. dom W |-> ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) ) |
12 |
|
dchrpt.au |
|- ( ph -> A e. U ) |
13 |
|
dchrpt.w |
|- ( ph -> W e. Word U ) |
14 |
|
dchrpt.2 |
|- ( ph -> H dom DProd S ) |
15 |
|
dchrpt.3 |
|- ( ph -> ( H DProd S ) = U ) |
16 |
6
|
nnnn0d |
|- ( ph -> N e. NN0 ) |
17 |
2
|
zncrng |
|- ( N e. NN0 -> Z e. CRing ) |
18 |
16 17
|
syl |
|- ( ph -> Z e. CRing ) |
19 |
|
crngring |
|- ( Z e. CRing -> Z e. Ring ) |
20 |
18 19
|
syl |
|- ( ph -> Z e. Ring ) |
21 |
8 9
|
unitgrp |
|- ( Z e. Ring -> H e. Grp ) |
22 |
20 21
|
syl |
|- ( ph -> H e. Grp ) |
23 |
|
grpmnd |
|- ( H e. Grp -> H e. Mnd ) |
24 |
22 23
|
syl |
|- ( ph -> H e. Mnd ) |
25 |
13
|
dmexd |
|- ( ph -> dom W e. _V ) |
26 |
|
eqid |
|- ( 0g ` H ) = ( 0g ` H ) |
27 |
26
|
gsumz |
|- ( ( H e. Mnd /\ dom W e. _V ) -> ( H gsum ( a e. dom W |-> ( 0g ` H ) ) ) = ( 0g ` H ) ) |
28 |
24 25 27
|
syl2anc |
|- ( ph -> ( H gsum ( a e. dom W |-> ( 0g ` H ) ) ) = ( 0g ` H ) ) |
29 |
8 9 5
|
unitgrpid |
|- ( Z e. Ring -> .1. = ( 0g ` H ) ) |
30 |
20 29
|
syl |
|- ( ph -> .1. = ( 0g ` H ) ) |
31 |
30
|
mpteq2dv |
|- ( ph -> ( a e. dom W |-> .1. ) = ( a e. dom W |-> ( 0g ` H ) ) ) |
32 |
31
|
oveq2d |
|- ( ph -> ( H gsum ( a e. dom W |-> .1. ) ) = ( H gsum ( a e. dom W |-> ( 0g ` H ) ) ) ) |
33 |
28 32 30
|
3eqtr4d |
|- ( ph -> ( H gsum ( a e. dom W |-> .1. ) ) = .1. ) |
34 |
7 33
|
neeqtrrd |
|- ( ph -> A =/= ( H gsum ( a e. dom W |-> .1. ) ) ) |
35 |
|
zex |
|- ZZ e. _V |
36 |
35
|
mptex |
|- ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) e. _V |
37 |
36
|
rnex |
|- ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) e. _V |
38 |
37 11
|
dmmpti |
|- dom S = dom W |
39 |
38
|
a1i |
|- ( ph -> dom S = dom W ) |
40 |
|
eqid |
|- ( H dProj S ) = ( H dProj S ) |
41 |
12 15
|
eleqtrrd |
|- ( ph -> A e. ( H DProd S ) ) |
42 |
|
eqid |
|- { h e. X_ i e. dom W ( S ` i ) | h finSupp ( 0g ` H ) } = { h e. X_ i e. dom W ( S ` i ) | h finSupp ( 0g ` H ) } |
43 |
30
|
adantr |
|- ( ( ph /\ a e. dom W ) -> .1. = ( 0g ` H ) ) |
44 |
14 39
|
dprdf2 |
|- ( ph -> S : dom W --> ( SubGrp ` H ) ) |
45 |
44
|
ffvelrnda |
|- ( ( ph /\ a e. dom W ) -> ( S ` a ) e. ( SubGrp ` H ) ) |
46 |
26
|
subg0cl |
|- ( ( S ` a ) e. ( SubGrp ` H ) -> ( 0g ` H ) e. ( S ` a ) ) |
47 |
45 46
|
syl |
|- ( ( ph /\ a e. dom W ) -> ( 0g ` H ) e. ( S ` a ) ) |
48 |
43 47
|
eqeltrd |
|- ( ( ph /\ a e. dom W ) -> .1. e. ( S ` a ) ) |
49 |
5
|
fvexi |
|- .1. e. _V |
50 |
49
|
a1i |
|- ( ph -> .1. e. _V ) |
51 |
25 50
|
fczfsuppd |
|- ( ph -> ( dom W X. { .1. } ) finSupp .1. ) |
52 |
|
fconstmpt |
|- ( dom W X. { .1. } ) = ( a e. dom W |-> .1. ) |
53 |
52
|
eqcomi |
|- ( a e. dom W |-> .1. ) = ( dom W X. { .1. } ) |
54 |
53
|
a1i |
|- ( ph -> ( a e. dom W |-> .1. ) = ( dom W X. { .1. } ) ) |
55 |
30
|
eqcomd |
|- ( ph -> ( 0g ` H ) = .1. ) |
56 |
51 54 55
|
3brtr4d |
|- ( ph -> ( a e. dom W |-> .1. ) finSupp ( 0g ` H ) ) |
57 |
42 14 39 48 56
|
dprdwd |
|- ( ph -> ( a e. dom W |-> .1. ) e. { h e. X_ i e. dom W ( S ` i ) | h finSupp ( 0g ` H ) } ) |
58 |
14 39 40 41 26 42 57
|
dpjeq |
|- ( ph -> ( A = ( H gsum ( a e. dom W |-> .1. ) ) <-> A. a e. dom W ( ( ( H dProj S ) ` a ) ` A ) = .1. ) ) |
59 |
58
|
necon3abid |
|- ( ph -> ( A =/= ( H gsum ( a e. dom W |-> .1. ) ) <-> -. A. a e. dom W ( ( ( H dProj S ) ` a ) ` A ) = .1. ) ) |
60 |
34 59
|
mpbid |
|- ( ph -> -. A. a e. dom W ( ( ( H dProj S ) ` a ) ` A ) = .1. ) |
61 |
|
rexnal |
|- ( E. a e. dom W -. ( ( ( H dProj S ) ` a ) ` A ) = .1. <-> -. A. a e. dom W ( ( ( H dProj S ) ` a ) ` A ) = .1. ) |
62 |
60 61
|
sylibr |
|- ( ph -> E. a e. dom W -. ( ( ( H dProj S ) ` a ) ` A ) = .1. ) |
63 |
|
df-ne |
|- ( ( ( ( H dProj S ) ` a ) ` A ) =/= .1. <-> -. ( ( ( H dProj S ) ` a ) ` A ) = .1. ) |
64 |
6
|
adantr |
|- ( ( ph /\ ( a e. dom W /\ ( ( ( H dProj S ) ` a ) ` A ) =/= .1. ) ) -> N e. NN ) |
65 |
7
|
adantr |
|- ( ( ph /\ ( a e. dom W /\ ( ( ( H dProj S ) ` a ) ` A ) =/= .1. ) ) -> A =/= .1. ) |
66 |
12
|
adantr |
|- ( ( ph /\ ( a e. dom W /\ ( ( ( H dProj S ) ` a ) ` A ) =/= .1. ) ) -> A e. U ) |
67 |
13
|
adantr |
|- ( ( ph /\ ( a e. dom W /\ ( ( ( H dProj S ) ` a ) ` A ) =/= .1. ) ) -> W e. Word U ) |
68 |
14
|
adantr |
|- ( ( ph /\ ( a e. dom W /\ ( ( ( H dProj S ) ` a ) ` A ) =/= .1. ) ) -> H dom DProd S ) |
69 |
15
|
adantr |
|- ( ( ph /\ ( a e. dom W /\ ( ( ( H dProj S ) ` a ) ` A ) =/= .1. ) ) -> ( H DProd S ) = U ) |
70 |
|
eqid |
|- ( od ` H ) = ( od ` H ) |
71 |
|
eqid |
|- ( -u 1 ^c ( 2 / ( ( od ` H ) ` ( W ` a ) ) ) ) = ( -u 1 ^c ( 2 / ( ( od ` H ) ` ( W ` a ) ) ) ) |
72 |
|
simprl |
|- ( ( ph /\ ( a e. dom W /\ ( ( ( H dProj S ) ` a ) ` A ) =/= .1. ) ) -> a e. dom W ) |
73 |
|
simprr |
|- ( ( ph /\ ( a e. dom W /\ ( ( ( H dProj S ) ` a ) ` A ) =/= .1. ) ) -> ( ( ( H dProj S ) ` a ) ` A ) =/= .1. ) |
74 |
|
eqid |
|- ( u e. U |-> ( iota h E. m e. ZZ ( ( ( ( H dProj S ) ` a ) ` u ) = ( m .x. ( W ` a ) ) /\ h = ( ( -u 1 ^c ( 2 / ( ( od ` H ) ` ( W ` a ) ) ) ) ^ m ) ) ) ) = ( u e. U |-> ( iota h E. m e. ZZ ( ( ( ( H dProj S ) ` a ) ` u ) = ( m .x. ( W ` a ) ) /\ h = ( ( -u 1 ^c ( 2 / ( ( od ` H ) ` ( W ` a ) ) ) ) ^ m ) ) ) ) |
75 |
1 2 3 4 5 64 65 8 9 10 11 66 67 68 69 40 70 71 72 73 74
|
dchrptlem2 |
|- ( ( ph /\ ( a e. dom W /\ ( ( ( H dProj S ) ` a ) ` A ) =/= .1. ) ) -> E. x e. D ( x ` A ) =/= 1 ) |
76 |
75
|
expr |
|- ( ( ph /\ a e. dom W ) -> ( ( ( ( H dProj S ) ` a ) ` A ) =/= .1. -> E. x e. D ( x ` A ) =/= 1 ) ) |
77 |
63 76
|
syl5bir |
|- ( ( ph /\ a e. dom W ) -> ( -. ( ( ( H dProj S ) ` a ) ` A ) = .1. -> E. x e. D ( x ` A ) =/= 1 ) ) |
78 |
77
|
rexlimdva |
|- ( ph -> ( E. a e. dom W -. ( ( ( H dProj S ) ` a ) ` A ) = .1. -> E. x e. D ( x ` A ) =/= 1 ) ) |
79 |
62 78
|
mpd |
|- ( ph -> E. x e. D ( x ` A ) =/= 1 ) |