Metamath Proof Explorer

Theorem cygznlem2a

Description: Lemma for cygzn . (Contributed by Mario Carneiro, 23-Dec-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 )
cygzn.f 
|- F = ran ( m e. ZZ |-> <. ( L ` m ) , ( m .x. X ) >. )
Assertion cygznlem2a 
|- ( ph -> F : ( Base ` Y ) --> B )

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 cygzn.f 
 |-  F = ran ( m e. ZZ |-> <. ( L ` m ) , ( m .x. X ) >. )
10 fvexd 
 |-  ( ( ph /\ m e. ZZ ) -> ( L ` m ) e. _V )
11 cyggrp 
 |-  ( G e. CycGrp -> G e. Grp )
12 7 11 syl 
 |-  ( ph -> G e. Grp )
13 12 adantr 
 |-  ( ( ph /\ m e. ZZ ) -> G e. Grp )
14 simpr 
 |-  ( ( ph /\ m e. ZZ ) -> m e. ZZ )
15 6 ssrab3 
 |-  E C_ B
16 15 8 sselid 
 |-  ( ph -> X e. B )
17 16 adantr 
 |-  ( ( ph /\ m e. ZZ ) -> X e. B )
18 1 4 mulgcl 
 |-  ( ( G e. Grp /\ m e. ZZ /\ X e. B ) -> ( m .x. X ) e. B )
19 13 14 17 18 syl3anc 
 |-  ( ( ph /\ m e. ZZ ) -> ( m .x. X ) e. B )
20 fveq2 
 |-  ( m = k -> ( L ` m ) = ( L ` k ) )
21 oveq1 
 |-  ( m = k -> ( m .x. X ) = ( k .x. X ) )
22 1 2 3 4 5 6 7 8 cygznlem1 
 |-  ( ( ph /\ ( m e. ZZ /\ k e. ZZ ) ) -> ( ( L ` m ) = ( L ` k ) <-> ( m .x. X ) = ( k .x. X ) ) )
23 22 biimpd 
 |-  ( ( ph /\ ( m e. ZZ /\ k e. ZZ ) ) -> ( ( L ` m ) = ( L ` k ) -> ( m .x. X ) = ( k .x. X ) ) )
24 23 exp32 
 |-  ( ph -> ( m e. ZZ -> ( k e. ZZ -> ( ( L ` m ) = ( L ` k ) -> ( m .x. X ) = ( k .x. X ) ) ) ) )
25 24 3imp2 
 |-  ( ( ph /\ ( m e. ZZ /\ k e. ZZ /\ ( L ` m ) = ( L ` k ) ) ) -> ( m .x. X ) = ( k .x. X ) )
26 9 10 19 20 21 25 fliftfund 
 |-  ( ph -> Fun F )
27 9 10 19 fliftf 
 |-  ( ph -> ( Fun F <-> F : ran ( m e. ZZ |-> ( L ` m ) ) --> B ) )
28 26 27 mpbid 
 |-  ( ph -> F : ran ( m e. ZZ |-> ( L ` m ) ) --> B )
29 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
30 29 adantl 
 |-  ( ( ph /\ B e. Fin ) -> ( # ` B ) e. NN0 )
31 0nn0 
 |-  0 e. NN0
32 31 a1i 
 |-  ( ( ph /\ -. B e. Fin ) -> 0 e. NN0 )
33 30 32 ifclda 
 |-  ( ph -> if ( B e. Fin , ( # ` B ) , 0 ) e. NN0 )
34 2 33 eqeltrid 
 |-  ( ph -> N e. NN0 )
35 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
36 3 35 5 znzrhfo 
 |-  ( N e. NN0 -> L : ZZ -onto-> ( Base ` Y ) )
37 34 36 syl 
 |-  ( ph -> L : ZZ -onto-> ( Base ` Y ) )
38 fof 
 |-  ( L : ZZ -onto-> ( Base ` Y ) -> L : ZZ --> ( Base ` Y ) )
39 37 38 syl 
 |-  ( ph -> L : ZZ --> ( Base ` Y ) )
40 39 feqmptd 
 |-  ( ph -> L = ( m e. ZZ |-> ( L ` m ) ) )
41 40 rneqd 
 |-  ( ph -> ran L = ran ( m e. ZZ |-> ( L ` m ) ) )
42 forn 
 |-  ( L : ZZ -onto-> ( Base ` Y ) -> ran L = ( Base ` Y ) )
43 37 42 syl 
 |-  ( ph -> ran L = ( Base ` Y ) )
44 41 43 eqtr3d 
 |-  ( ph -> ran ( m e. ZZ |-> ( L ` m ) ) = ( Base ` Y ) )
45 44 feq2d 
 |-  ( ph -> ( F : ran ( m e. ZZ |-> ( L ` m ) ) --> B <-> F : ( Base ` Y ) --> B ) )
46 28 45 mpbid 
 |-  ( ph -> F : ( Base ` Y ) --> B )