Metamath Proof Explorer

Theorem dchrptlem3

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

Ref Expression
Hypotheses dchrpt.g 
|- G = ( DChr ` N )
dchrpt.z 
|- Z = ( Z/nZ ` N )
dchrpt.d 
|- D = ( Base ` G )
dchrpt.b 
|- B = ( Base ` Z )
dchrpt.1 
|- .1. = ( 1r ` Z )
dchrpt.n 
|- ( ph -> N e. NN )
dchrpt.n1 
|- ( ph -> A =/= .1. )
dchrpt.u 
|- U = ( Unit ` Z )
dchrpt.h 
|- H = ( ( mulGrp ` Z ) |`s U )
dchrpt.m 
|- .x. = ( .g ` H )
dchrpt.s 
|- S = ( k e. dom W |-> ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) )
dchrpt.au 
|- ( ph -> A e. U )
dchrpt.w 
|- ( ph -> W e. Word U )
dchrpt.2 
|- ( ph -> H dom DProd S )
dchrpt.3 
|- ( ph -> ( H DProd S ) = U )
Assertion dchrptlem3 
|- ( ph -> E. x e. D ( x ` A ) =/= 1 )

Proof

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