| 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 |
|
ovexd |
|- ( ( ph /\ m e. ZZ ) -> ( m .x. X ) e. _V ) |
| 12 |
|
fveq2 |
|- ( m = M -> ( L ` m ) = ( L ` M ) ) |
| 13 |
|
oveq1 |
|- ( m = M -> ( m .x. X ) = ( M .x. X ) ) |
| 14 |
1 2 3 4 5 6 7 8 9
|
cygznlem2a |
|- ( ph -> F : ( Base ` Y ) --> B ) |
| 15 |
14
|
ffund |
|- ( ph -> Fun F ) |
| 16 |
9 10 11 12 13 15
|
fliftval |
|- ( ( ph /\ M e. ZZ ) -> ( F ` ( L ` M ) ) = ( M .x. X ) ) |