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 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 )