Theorem cygznlem2

Description: Lemma for cygzn . (Contributed by Mario Carneiro, 21-Apr-2016) (Revised 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	cygznlem2	|- ( ( ph /\ M e. ZZ ) -> ( F ` ( L ` M ) ) = ( 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		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 ) )