Metamath Proof Explorer

Theorem cygznlem1

Description: Lemma for cygzn . (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses cygzn.b 
|- B = ( Base ` G )
cygzn.n 
|- N = if ( B e. Fin , ( # ` B ) , 0 )
cygzn.y 
|- Y = ( Z/nZ ` N )
cygzn.m 
|- .x. = ( .g ` G )
cygzn.l 
|- L = ( ZRHom ` Y )
cygzn.e 
|- E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }
cygzn.g 
|- ( ph -> G e. CycGrp )
cygzn.x 
|- ( ph -> X e. E )
Assertion cygznlem1 
|- ( ( ph /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( L ` K ) = ( L ` M ) <-> ( K .x. X ) = ( M .x. X ) ) )

Proof

Step Hyp Ref Expression
1 cygzn.b 
 |-  B = ( Base ` G )
2 cygzn.n 
 |-  N = if ( B e. Fin , ( # ` B ) , 0 )
3 cygzn.y 
 |-  Y = ( Z/nZ ` N )
4 cygzn.m 
 |-  .x. = ( .g ` G )
5 cygzn.l 
 |-  L = ( ZRHom ` Y )
6 cygzn.e 
 |-  E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }
7 cygzn.g 
 |-  ( ph -> G e. CycGrp )
8 cygzn.x 
 |-  ( ph -> X e. E )
9 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
10 9 adantl 
 |-  ( ( ph /\ B e. Fin ) -> ( # ` B ) e. NN0 )
11 0nn0 
 |-  0 e. NN0
12 11 a1i 
 |-  ( ( ph /\ -. B e. Fin ) -> 0 e. NN0 )
13 10 12 ifclda 
 |-  ( ph -> if ( B e. Fin , ( # ` B ) , 0 ) e. NN0 )
14 2 13 eqeltrid 
 |-  ( ph -> N e. NN0 )
15 14 adantr 
 |-  ( ( ph /\ ( K e. ZZ /\ M e. ZZ ) ) -> N e. NN0 )
16 simprl 
 |-  ( ( ph /\ ( K e. ZZ /\ M e. ZZ ) ) -> K e. ZZ )
17 simprr 
 |-  ( ( ph /\ ( K e. ZZ /\ M e. ZZ ) ) -> M e. ZZ )
18 3 5 zndvds 
 |-  ( ( N e. NN0 /\ K e. ZZ /\ M e. ZZ ) -> ( ( L ` K ) = ( L ` M ) <-> N || ( K - M ) ) )
19 15 16 17 18 syl3anc 
 |-  ( ( ph /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( L ` K ) = ( L ` M ) <-> N || ( K - M ) ) )
20 cyggrp 
 |-  ( G e. CycGrp -> G e. Grp )
21 7 20 syl 
 |-  ( ph -> G e. Grp )
22 eqid 
 |-  ( od ` G ) = ( od ` G )
23 1 4 6 22 cyggenod2 
 |-  ( ( G e. Grp /\ X e. E ) -> ( ( od ` G ) ` X ) = if ( B e. Fin , ( # ` B ) , 0 ) )
24 21 8 23 syl2anc 
 |-  ( ph -> ( ( od ` G ) ` X ) = if ( B e. Fin , ( # ` B ) , 0 ) )
25 24 2 eqtr4di 
 |-  ( ph -> ( ( od ` G ) ` X ) = N )
26 25 adantr 
 |-  ( ( ph /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( od ` G ) ` X ) = N )
27 26 breq1d 
 |-  ( ( ph /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( ( od ` G ) ` X ) || ( K - M ) <-> N || ( K - M ) ) )
28 21 adantr 
 |-  ( ( ph /\ ( K e. ZZ /\ M e. ZZ ) ) -> G e. Grp )
29 1 4 6 iscyggen 
 |-  ( X e. E <-> ( X e. B /\ ran ( n e. ZZ |-> ( n .x. X ) ) = B ) )
30 29 simplbi 
 |-  ( X e. E -> X e. B )
31 8 30 syl 
 |-  ( ph -> X e. B )
32 31 adantr 
 |-  ( ( ph /\ ( K e. ZZ /\ M e. ZZ ) ) -> X e. B )
33 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
34 1 22 4 33 odcong 
 |-  ( ( G e. Grp /\ X e. B /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( ( od ` G ) ` X ) || ( K - M ) <-> ( K .x. X ) = ( M .x. X ) ) )
35 28 32 16 17 34 syl112anc 
 |-  ( ( ph /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( ( od ` G ) ` X ) || ( K - M ) <-> ( K .x. X ) = ( M .x. X ) ) )
36 19 27 35 3bitr2d 
 |-  ( ( ph /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( L ` K ) = ( L ` M ) <-> ( K .x. X ) = ( M .x. X ) ) )