Metamath Proof Explorer


Theorem pgpfaclem3

Description: Lemma for pgpfac . (Contributed by Mario Carneiro, 27-Apr-2016) (Revised by Mario Carneiro, 3-May-2016)

Ref Expression
Hypotheses pgpfac.b B=BaseG
pgpfac.c C=rSubGrpG|G𝑠rCycGrpranpGrp
pgpfac.g φGAbel
pgpfac.p φPpGrpG
pgpfac.f φBFin
pgpfac.u φUSubGrpG
pgpfac.a φtSubGrpGtUsWordCGdomDProdsGDProds=t
Assertion pgpfaclem3 φsWordCGdomDProdsGDProds=U

Proof

Step Hyp Ref Expression
1 pgpfac.b B=BaseG
2 pgpfac.c C=rSubGrpG|G𝑠rCycGrpranpGrp
3 pgpfac.g φGAbel
4 pgpfac.p φPpGrpG
5 pgpfac.f φBFin
6 pgpfac.u φUSubGrpG
7 pgpfac.a φtSubGrpGtUsWordCGdomDProdsGDProds=t
8 wrd0 WordC
9 ablgrp GAbelGGrp
10 eqid 0G=0G
11 10 dprd0 GGrpGdomDProdGDProd=0G
12 3 9 11 3syl φGdomDProdGDProd=0G
13 12 adantr φgExG𝑠U=1GdomDProdGDProd=0G
14 10 subg0cl USubGrpG0GU
15 6 14 syl φ0GU
16 15 adantr φgExG𝑠U=10GU
17 eqid G𝑠U=G𝑠U
18 17 subgbas USubGrpGU=BaseG𝑠U
19 6 18 syl φU=BaseG𝑠U
20 19 adantr φgExG𝑠U=1U=BaseG𝑠U
21 17 subggrp USubGrpGG𝑠UGrp
22 6 21 syl φG𝑠UGrp
23 grpmnd G𝑠UGrpG𝑠UMnd
24 eqid BaseG𝑠U=BaseG𝑠U
25 eqid gExG𝑠U=gExG𝑠U
26 24 25 gex1 G𝑠UMndgExG𝑠U=1BaseG𝑠U1𝑜
27 22 23 26 3syl φgExG𝑠U=1BaseG𝑠U1𝑜
28 27 biimpa φgExG𝑠U=1BaseG𝑠U1𝑜
29 20 28 eqbrtrd φgExG𝑠U=1U1𝑜
30 en1eqsn 0GUU1𝑜U=0G
31 16 29 30 syl2anc φgExG𝑠U=1U=0G
32 31 eqeq2d φgExG𝑠U=1GDProd=UGDProd=0G
33 32 anbi2d φgExG𝑠U=1GdomDProdGDProd=UGdomDProdGDProd=0G
34 13 33 mpbird φgExG𝑠U=1GdomDProdGDProd=U
35 breq2 s=GdomDProdsGdomDProd
36 oveq2 s=GDProds=GDProd
37 36 eqeq1d s=GDProds=UGDProd=U
38 35 37 anbi12d s=GdomDProdsGDProds=UGdomDProdGDProd=U
39 38 rspcev WordCGdomDProdGDProd=UsWordCGdomDProdsGDProds=U
40 8 34 39 sylancr φgExG𝑠U=1sWordCGdomDProdsGDProds=U
41 17 subgabl GAbelUSubGrpGG𝑠UAbel
42 3 6 41 syl2anc φG𝑠UAbel
43 1 subgss USubGrpGUB
44 6 43 syl φUB
45 5 44 ssfid φUFin
46 19 45 eqeltrrd φBaseG𝑠UFin
47 24 25 gexcl2 G𝑠UGrpBaseG𝑠UFingExG𝑠U
48 22 46 47 syl2anc φgExG𝑠U
49 eqid odG𝑠U=odG𝑠U
50 24 25 49 gexex G𝑠UAbelgExG𝑠UxBaseG𝑠UodG𝑠Ux=gExG𝑠U
51 42 48 50 syl2anc φxBaseG𝑠UodG𝑠Ux=gExG𝑠U
52 51 adantr φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠U
53 eqid mrClsSubGrpG𝑠U=mrClsSubGrpG𝑠U
54 eqid mrClsSubGrpG𝑠Ux=mrClsSubGrpG𝑠Ux
55 eqid 0G𝑠U=0G𝑠U
56 eqid LSSumG𝑠U=LSSumG𝑠U
57 subgpgp PpGrpGUSubGrpGPpGrpG𝑠U
58 4 6 57 syl2anc φPpGrpG𝑠U
59 58 ad2antrr φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UPpGrpG𝑠U
60 42 ad2antrr φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UG𝑠UAbel
61 46 ad2antrr φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UBaseG𝑠UFin
62 simprr φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UodG𝑠Ux=gExG𝑠U
63 simprl φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UxBaseG𝑠U
64 53 54 24 49 25 55 56 59 60 61 62 63 pgpfac1 φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠U
65 3 ad3antrrr φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UGAbel
66 4 ad3antrrr φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UPpGrpG
67 5 ad3antrrr φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UBFin
68 6 ad3antrrr φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UUSubGrpG
69 7 ad3antrrr φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UtSubGrpGtUsWordCGdomDProdsGDProds=t
70 simpllr φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UgExG𝑠U1
71 simplrl φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UxBaseG𝑠U
72 68 18 syl φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UU=BaseG𝑠U
73 71 72 eleqtrrd φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UxU
74 simplrr φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UodG𝑠Ux=gExG𝑠U
75 simprl φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UwSubGrpG𝑠U
76 simprrl φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠U
77 simprrr φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠U
78 77 72 eqtr4d φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=U
79 1 2 65 66 67 68 69 17 53 49 25 55 56 70 73 74 75 76 78 pgpfaclem2 φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UwSubGrpG𝑠UmrClsSubGrpG𝑠Uxw=0G𝑠UmrClsSubGrpG𝑠UxLSSumG𝑠Uw=BaseG𝑠UsWordCGdomDProdsGDProds=U
80 64 79 rexlimddv φgExG𝑠U1xBaseG𝑠UodG𝑠Ux=gExG𝑠UsWordCGdomDProdsGDProds=U
81 52 80 rexlimddv φgExG𝑠U1sWordCGdomDProdsGDProds=U
82 40 81 pm2.61dane φsWordCGdomDProdsGDProds=U