Metamath Proof Explorer


Theorem cygznlem2a

Description: Lemma for cygzn . (Contributed 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 cygznlem2a φF:BaseYB

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 cyggrp GCycGrpGGrp
12 7 11 syl φGGrp
13 12 adantr φmGGrp
14 simpr φmm
15 6 ssrab3 EB
16 15 8 sselid φXB
17 16 adantr φmXB
18 1 4 mulgcl GGrpmXBm·˙XB
19 13 14 17 18 syl3anc φmm·˙XB
20 fveq2 m=kLm=Lk
21 oveq1 m=km·˙X=k·˙X
22 1 2 3 4 5 6 7 8 cygznlem1 φmkLm=Lkm·˙X=k·˙X
23 22 biimpd φmkLm=Lkm·˙X=k·˙X
24 23 exp32 φmkLm=Lkm·˙X=k·˙X
25 24 3imp2 φmkLm=Lkm·˙X=k·˙X
26 9 10 19 20 21 25 fliftfund φFunF
27 9 10 19 fliftf φFunFF:ranmLmB
28 26 27 mpbid φF:ranmLmB
29 hashcl BFinB0
30 29 adantl φBFinB0
31 0nn0 00
32 31 a1i φ¬BFin00
33 30 32 ifclda φifBFinB00
34 2 33 eqeltrid φN0
35 eqid BaseY=BaseY
36 3 35 5 znzrhfo N0L:ontoBaseY
37 34 36 syl φL:ontoBaseY
38 fof L:ontoBaseYL:BaseY
39 37 38 syl φL:BaseY
40 39 feqmptd φL=mLm
41 40 rneqd φranL=ranmLm
42 forn L:ontoBaseYranL=BaseY
43 37 42 syl φranL=BaseY
44 41 43 eqtr3d φranmLm=BaseY
45 44 feq2d φF:ranmLmBF:BaseYB
46 28 45 mpbid φF:BaseYB