Metamath Proof Explorer


Theorem ablfaclem2

Description: Lemma for ablfac . (Contributed by Mario Carneiro, 27-Apr-2016) (Proof shortened by Mario Carneiro, 3-May-2016)

Ref Expression
Hypotheses ablfac.b B=BaseG
ablfac.c C=rSubGrpG|G𝑠rCycGrpranpGrp
ablfac.1 φGAbel
ablfac.2 φBFin
ablfac.o O=odG
ablfac.a A=w|wB
ablfac.s S=pAxB|OxpppCntB
ablfac.w W=gSubGrpGsWordC|GdomDProdsGDProds=g
ablfaclem2.f φF:AWordC
ablfaclem2.q φyAFyWSy
ablfaclem2.l L=yAy×domFy
ablfaclem2.g φH:0..^L1-1 ontoL
Assertion ablfaclem2 φWB

Proof

Step Hyp Ref Expression
1 ablfac.b B=BaseG
2 ablfac.c C=rSubGrpG|G𝑠rCycGrpranpGrp
3 ablfac.1 φGAbel
4 ablfac.2 φBFin
5 ablfac.o O=odG
6 ablfac.a A=w|wB
7 ablfac.s S=pAxB|OxpppCntB
8 ablfac.w W=gSubGrpGsWordC|GdomDProdsGDProds=g
9 ablfaclem2.f φF:AWordC
10 ablfaclem2.q φyAFyWSy
11 ablfaclem2.l L=yAy×domFy
12 ablfaclem2.g φH:0..^L1-1 ontoL
13 ablgrp GAbelGGrp
14 1 subgid GGrpBSubGrpG
15 1 2 3 4 5 6 7 8 ablfaclem1 BSubGrpGWB=sWordC|GdomDProdsGDProds=B
16 3 13 14 15 4syl φWB=sWordC|GdomDProdsGDProds=B
17 9 ffvelrnda φyAFyWordC
18 wrdf FyWordCFy:0..^FyC
19 17 18 syl φyAFy:0..^FyC
20 19 ffdmd φyAFy:domFyC
21 20 ffvelrnda φyAzdomFyFyzC
22 21 anasss φyAzdomFyFyzC
23 22 ralrimivva φyAzdomFyFyzC
24 eqid yA,zdomFyFyz=yA,zdomFyFyz
25 24 fmpox yAzdomFyFyzCyA,zdomFyFyz:yAy×domFyC
26 23 25 sylib φyA,zdomFyFyz:yAy×domFyC
27 11 feq2i yA,zdomFyFyz:LCyA,zdomFyFyz:yAy×domFyC
28 26 27 sylibr φyA,zdomFyFyz:LC
29 f1of H:0..^L1-1 ontoLH:0..^LL
30 12 29 syl φH:0..^LL
31 fco yA,zdomFyFyz:LCH:0..^LLyA,zdomFyFyzH:0..^LC
32 28 30 31 syl2anc φyA,zdomFyFyzH:0..^LC
33 iswrdi yA,zdomFyFyzH:0..^LCyA,zdomFyFyzHWordC
34 32 33 syl φyA,zdomFyFyzHWordC
35 10 r19.21bi φyAFyWSy
36 6 ssrab3 A
37 36 a1i φA
38 1 5 7 3 4 37 ablfac1b φGdomDProdS
39 1 fvexi BV
40 39 rabex xB|OxpppCntBV
41 40 7 dmmpti domS=A
42 41 a1i φdomS=A
43 38 42 dprdf2 φS:ASubGrpG
44 43 ffvelrnda φyASySubGrpG
45 1 2 3 4 5 6 7 8 ablfaclem1 SySubGrpGWSy=sWordC|GdomDProdsGDProds=Sy
46 44 45 syl φyAWSy=sWordC|GdomDProdsGDProds=Sy
47 35 46 eleqtrd φyAFysWordC|GdomDProdsGDProds=Sy
48 breq2 s=FyGdomDProdsGdomDProdFy
49 oveq2 s=FyGDProds=GDProdFy
50 49 eqeq1d s=FyGDProds=SyGDProdFy=Sy
51 48 50 anbi12d s=FyGdomDProdsGDProds=SyGdomDProdFyGDProdFy=Sy
52 51 elrab FysWordC|GdomDProdsGDProds=SyFyWordCGdomDProdFyGDProdFy=Sy
53 52 simprbi FysWordC|GdomDProdsGDProds=SyGdomDProdFyGDProdFy=Sy
54 47 53 syl φyAGdomDProdFyGDProdFy=Sy
55 54 simpld φyAGdomDProdFy
56 dprdf GdomDProdFyFy:domFySubGrpG
57 55 56 syl φyAFy:domFySubGrpG
58 57 ffvelrnda φyAzdomFyFyzSubGrpG
59 58 anasss φyAzdomFyFyzSubGrpG
60 57 feqmptd φyAFy=zdomFyFyz
61 55 60 breqtrd φyAGdomDProdzdomFyFyz
62 43 feqmptd φS=yASy
63 60 oveq2d φyAGDProdFy=GDProdzdomFyFyz
64 54 simprd φyAGDProdFy=Sy
65 63 64 eqtr3d φyAGDProdzdomFyFyz=Sy
66 65 mpteq2dva φyAGDProdzdomFyFyz=yASy
67 62 66 eqtr4d φS=yAGDProdzdomFyFyz
68 38 67 breqtrd φGdomDProdyAGDProdzdomFyFyz
69 59 61 68 dprd2d2 φGdomDProdyA,zdomFyFyzGDProdyA,zdomFyFyz=GDProdyAGDProdzdomFyFyz
70 69 simpld φGdomDProdyA,zdomFyFyz
71 28 fdmd φdomyA,zdomFyFyz=L
72 70 71 12 dprdf1o φGdomDProdyA,zdomFyFyzHGDProdyA,zdomFyFyzH=GDProdyA,zdomFyFyz
73 72 simpld φGdomDProdyA,zdomFyFyzH
74 72 simprd φGDProdyA,zdomFyFyzH=GDProdyA,zdomFyFyz
75 69 simprd φGDProdyA,zdomFyFyz=GDProdyAGDProdzdomFyFyz
76 67 oveq2d φGDProdS=GDProdyAGDProdzdomFyFyz
77 ssidd φAA
78 1 5 7 3 4 37 6 77 ablfac1c φGDProdS=B
79 76 78 eqtr3d φGDProdyAGDProdzdomFyFyz=B
80 74 75 79 3eqtrd φGDProdyA,zdomFyFyzH=B
81 breq2 s=yA,zdomFyFyzHGdomDProdsGdomDProdyA,zdomFyFyzH
82 oveq2 s=yA,zdomFyFyzHGDProds=GDProdyA,zdomFyFyzH
83 82 eqeq1d s=yA,zdomFyFyzHGDProds=BGDProdyA,zdomFyFyzH=B
84 81 83 anbi12d s=yA,zdomFyFyzHGdomDProdsGDProds=BGdomDProdyA,zdomFyFyzHGDProdyA,zdomFyFyzH=B
85 84 rspcev yA,zdomFyFyzHWordCGdomDProdyA,zdomFyFyzHGDProdyA,zdomFyFyzH=BsWordCGdomDProdsGDProds=B
86 34 73 80 85 syl12anc φsWordCGdomDProdsGDProds=B
87 rabn0 sWordC|GdomDProdsGDProds=BsWordCGdomDProdsGDProds=B
88 86 87 sylibr φsWordC|GdomDProdsGDProds=B
89 16 88 eqnetrd φWB