Metamath Proof Explorer


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=BaseG
cygzn.n N=ifBFinB0
cygzn.y Y=/N
cygzn.m ·˙=G
cygzn.l L=ℤRHomY
cygzn.e E=xB|rannn·˙x=B
cygzn.g φGCycGrp
cygzn.x φXE
cygzn.f F=ranmLmm·˙X
Assertion cygznlem2 φMFLM=M·˙X

Proof

Step Hyp Ref Expression
1 cygzn.b B=BaseG
2 cygzn.n N=ifBFinB0
3 cygzn.y Y=/N
4 cygzn.m ·˙=G
5 cygzn.l L=ℤRHomY
6 cygzn.e E=xB|rannn·˙x=B
7 cygzn.g φGCycGrp
8 cygzn.x φXE
9 cygzn.f F=ranmLmm·˙X
10 fvexd φmLmV
11 ovexd φmm·˙XV
12 fveq2 m=MLm=LM
13 oveq1 m=Mm·˙X=M·˙X
14 1 2 3 4 5 6 7 8 9 cygznlem2a φF:BaseYB
15 14 ffund φFunF
16 9 10 11 12 13 15 fliftval φMFLM=M·˙X