Metamath Proof Explorer


Theorem cygznlem1

Description: Lemma for cygzn . (Contributed by Mario Carneiro, 21-Apr-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
Assertion cygznlem1 φKMLK=LMK·˙X=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 hashcl BFinB0
10 9 adantl φBFinB0
11 0nn0 00
12 11 a1i φ¬BFin00
13 10 12 ifclda φifBFinB00
14 2 13 eqeltrid φN0
15 14 adantr φKMN0
16 simprl φKMK
17 simprr φKMM
18 3 5 zndvds N0KMLK=LMNKM
19 15 16 17 18 syl3anc φKMLK=LMNKM
20 cyggrp GCycGrpGGrp
21 7 20 syl φGGrp
22 eqid odG=odG
23 1 4 6 22 cyggenod2 GGrpXEodGX=ifBFinB0
24 21 8 23 syl2anc φodGX=ifBFinB0
25 24 2 eqtr4di φodGX=N
26 25 adantr φKModGX=N
27 26 breq1d φKModGXKMNKM
28 21 adantr φKMGGrp
29 1 4 6 iscyggen XEXBrannn·˙X=B
30 29 simplbi XEXB
31 8 30 syl φXB
32 31 adantr φKMXB
33 eqid 0G=0G
34 1 22 4 33 odcong GGrpXBKModGXKMK·˙X=M·˙X
35 28 32 16 17 34 syl112anc φKModGXKMK·˙X=M·˙X
36 19 27 35 3bitr2d φKMLK=LMK·˙X=M·˙X