Metamath Proof Explorer

Theorem ablfaclem3

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

Ref Expression
Hypotheses ablfac.b 
|- B = ( Base ` G )
ablfac.c 
|- C = { r e. ( SubGrp ` G ) | ( G |`s r ) e. ( CycGrp i^i ran pGrp ) }
ablfac.1 
|- ( ph -> G e. Abel )
ablfac.2 
|- ( ph -> B e. Fin )
ablfac.o 
|- O = ( od ` G )
ablfac.a 
|- A = { w e. Prime | w || ( # ` B ) }
ablfac.s 
|- S = ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )
ablfac.w 
|- W = ( g e. ( SubGrp ` G ) |-> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = g ) } )
Assertion ablfaclem3 
|- ( ph -> ( W ` B ) =/= (/) )

Proof

Step Hyp Ref Expression
1 ablfac.b 
 |-  B = ( Base ` G )
2 ablfac.c 
 |-  C = { r e. ( SubGrp ` G ) | ( G |`s r ) e. ( CycGrp i^i ran pGrp ) }
3 ablfac.1 
 |-  ( ph -> G e. Abel )
4 ablfac.2 
 |-  ( ph -> B e. Fin )
5 ablfac.o 
 |-  O = ( od ` G )
6 ablfac.a 
 |-  A = { w e. Prime | w || ( # ` B ) }
7 ablfac.s 
 |-  S = ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )
8 ablfac.w 
 |-  W = ( g e. ( SubGrp ` G ) |-> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = g ) } )
9 fzfid 
 |-  ( ph -> ( 1 ... ( # ` B ) ) e. Fin )
10 prmnn 
 |-  ( w e. Prime -> w e. NN )
11 10 3ad2ant2 
 |-  ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w e. NN )
12 prmz 
 |-  ( w e. Prime -> w e. ZZ )
13 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
14 1 grpbn0 
 |-  ( G e. Grp -> B =/= (/) )
15 3 13 14 3syl 
 |-  ( ph -> B =/= (/) )
16 hashnncl 
 |-  ( B e. Fin -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
17 4 16 syl 
 |-  ( ph -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
18 15 17 mpbird 
 |-  ( ph -> ( # ` B ) e. NN )
19 dvdsle 
 |-  ( ( w e. ZZ /\ ( # ` B ) e. NN ) -> ( w || ( # ` B ) -> w <_ ( # ` B ) ) )
20 12 18 19 syl2anr 
 |-  ( ( ph /\ w e. Prime ) -> ( w || ( # ` B ) -> w <_ ( # ` B ) ) )
21 20 3impia 
 |-  ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w <_ ( # ` B ) )
22 18 nnzd 
 |-  ( ph -> ( # ` B ) e. ZZ )
23 22 3ad2ant1 
 |-  ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> ( # ` B ) e. ZZ )
24 fznn 
 |-  ( ( # ` B ) e. ZZ -> ( w e. ( 1 ... ( # ` B ) ) <-> ( w e. NN /\ w <_ ( # ` B ) ) ) )
25 23 24 syl 
 |-  ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> ( w e. ( 1 ... ( # ` B ) ) <-> ( w e. NN /\ w <_ ( # ` B ) ) ) )
26 11 21 25 mpbir2and 
 |-  ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w e. ( 1 ... ( # ` B ) ) )
27 26 rabssdv 
 |-  ( ph -> { w e. Prime | w || ( # ` B ) } C_ ( 1 ... ( # ` B ) ) )
28 6 27 eqsstrid 
 |-  ( ph -> A C_ ( 1 ... ( # ` B ) ) )
29 9 28 ssfid 
 |-  ( ph -> A e. Fin )
30 dfin5 
 |-  ( Word C i^i ( W ` ( S ` q ) ) ) = { y e. Word C | y e. ( W ` ( S ` q ) ) }
31 6 ssrab3 
 |-  A C_ Prime
32 31 a1i 
 |-  ( ph -> A C_ Prime )
33 1 5 7 3 4 32 ablfac1b 
 |-  ( ph -> G dom DProd S )
34 1 fvexi 
 |-  B e. _V
35 34 rabex 
 |-  { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } e. _V
36 35 7 dmmpti 
 |-  dom S = A
37 36 a1i 
 |-  ( ph -> dom S = A )
38 33 37 dprdf2 
 |-  ( ph -> S : A --> ( SubGrp ` G ) )
39 38 ffvelcdmda 
 |-  ( ( ph /\ q e. A ) -> ( S ` q ) e. ( SubGrp ` G ) )
40 1 2 3 4 5 6 7 8 ablfaclem1 
 |-  ( ( S ` q ) e. ( SubGrp ` G ) -> ( W ` ( S ` q ) ) = { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = ( S ` q ) ) } )
41 39 40 syl 
 |-  ( ( ph /\ q e. A ) -> ( W ` ( S ` q ) ) = { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = ( S ` q ) ) } )
42 ssrab2 
 |-  { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = ( S ` q ) ) } C_ Word C
43 41 42 eqsstrdi 
 |-  ( ( ph /\ q e. A ) -> ( W ` ( S ` q ) ) C_ Word C )
44 sseqin2 
 |-  ( ( W ` ( S ` q ) ) C_ Word C <-> ( Word C i^i ( W ` ( S ` q ) ) ) = ( W ` ( S ` q ) ) )
45 43 44 sylib 
 |-  ( ( ph /\ q e. A ) -> ( Word C i^i ( W ` ( S ` q ) ) ) = ( W ` ( S ` q ) ) )
46 30 45 eqtr3id 
 |-  ( ( ph /\ q e. A ) -> { y e. Word C | y e. ( W ` ( S ` q ) ) } = ( W ` ( S ` q ) ) )
47 46 41 eqtrd 
 |-  ( ( ph /\ q e. A ) -> { y e. Word C | y e. ( W ` ( S ` q ) ) } = { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = ( S ` q ) ) } )
48 eqid 
 |-  ( Base ` ( G |`s ( S ` q ) ) ) = ( Base ` ( G |`s ( S ` q ) ) )
49 eqid 
 |-  { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } = { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) }
50 eqid 
 |-  ( G |`s ( S ` q ) ) = ( G |`s ( S ` q ) )
51 50 subgabl 
 |-  ( ( G e. Abel /\ ( S ` q ) e. ( SubGrp ` G ) ) -> ( G |`s ( S ` q ) ) e. Abel )
52 3 39 51 syl2an2r 
 |-  ( ( ph /\ q e. A ) -> ( G |`s ( S ` q ) ) e. Abel )
53 32 sselda 
 |-  ( ( ph /\ q e. A ) -> q e. Prime )
54 50 subgbas 
 |-  ( ( S ` q ) e. ( SubGrp ` G ) -> ( S ` q ) = ( Base ` ( G |`s ( S ` q ) ) ) )
55 39 54 syl 
 |-  ( ( ph /\ q e. A ) -> ( S ` q ) = ( Base ` ( G |`s ( S ` q ) ) ) )
56 55 fveq2d 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( S ` q ) ) = ( # ` ( Base ` ( G |`s ( S ` q ) ) ) ) )
57 1 5 7 3 4 32 ablfac1a 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( S ` q ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
58 56 57 eqtr3d 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( Base ` ( G |`s ( S ` q ) ) ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
59 58 oveq2d 
 |-  ( ( ph /\ q e. A ) -> ( q pCnt ( # ` ( Base ` ( G |`s ( S ` q ) ) ) ) ) = ( q pCnt ( q ^ ( q pCnt ( # ` B ) ) ) ) )
60 18 adantr 
 |-  ( ( ph /\ q e. A ) -> ( # ` B ) e. NN )
61 53 60 pccld 
 |-  ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. NN0 )
62 61 nn0zd 
 |-  ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. ZZ )
63 pcid 
 |-  ( ( q e. Prime /\ ( q pCnt ( # ` B ) ) e. ZZ ) -> ( q pCnt ( q ^ ( q pCnt ( # ` B ) ) ) ) = ( q pCnt ( # ` B ) ) )
64 53 62 63 syl2anc 
 |-  ( ( ph /\ q e. A ) -> ( q pCnt ( q ^ ( q pCnt ( # ` B ) ) ) ) = ( q pCnt ( # ` B ) ) )
65 59 64 eqtrd 
 |-  ( ( ph /\ q e. A ) -> ( q pCnt ( # ` ( Base ` ( G |`s ( S ` q ) ) ) ) ) = ( q pCnt ( # ` B ) ) )
66 65 oveq2d 
 |-  ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` ( Base ` ( G |`s ( S ` q ) ) ) ) ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
67 58 66 eqtr4d 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( Base ` ( G |`s ( S ` q ) ) ) ) = ( q ^ ( q pCnt ( # ` ( Base ` ( G |`s ( S ` q ) ) ) ) ) ) )
68 50 subggrp 
 |-  ( ( S ` q ) e. ( SubGrp ` G ) -> ( G |`s ( S ` q ) ) e. Grp )
69 39 68 syl 
 |-  ( ( ph /\ q e. A ) -> ( G |`s ( S ` q ) ) e. Grp )
70 4 adantr 
 |-  ( ( ph /\ q e. A ) -> B e. Fin )
71 1 subgss 
 |-  ( ( S ` q ) e. ( SubGrp ` G ) -> ( S ` q ) C_ B )
72 39 71 syl 
 |-  ( ( ph /\ q e. A ) -> ( S ` q ) C_ B )
73 70 72 ssfid 
 |-  ( ( ph /\ q e. A ) -> ( S ` q ) e. Fin )
74 55 73 eqeltrrd 
 |-  ( ( ph /\ q e. A ) -> ( Base ` ( G |`s ( S ` q ) ) ) e. Fin )
75 48 pgpfi2 
 |-  ( ( ( G |`s ( S ` q ) ) e. Grp /\ ( Base ` ( G |`s ( S ` q ) ) ) e. Fin ) -> ( q pGrp ( G |`s ( S ` q ) ) <-> ( q e. Prime /\ ( # ` ( Base ` ( G |`s ( S ` q ) ) ) ) = ( q ^ ( q pCnt ( # ` ( Base ` ( G |`s ( S ` q ) ) ) ) ) ) ) ) )
76 69 74 75 syl2anc 
 |-  ( ( ph /\ q e. A ) -> ( q pGrp ( G |`s ( S ` q ) ) <-> ( q e. Prime /\ ( # ` ( Base ` ( G |`s ( S ` q ) ) ) ) = ( q ^ ( q pCnt ( # ` ( Base ` ( G |`s ( S ` q ) ) ) ) ) ) ) ) )
77 53 67 76 mpbir2and 
 |-  ( ( ph /\ q e. A ) -> q pGrp ( G |`s ( S ` q ) ) )
78 48 49 52 77 74 pgpfac 
 |-  ( ( ph /\ q e. A ) -> E. s e. Word { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } ( ( G |`s ( S ` q ) ) dom DProd s /\ ( ( G |`s ( S ` q ) ) DProd s ) = ( Base ` ( G |`s ( S ` q ) ) ) ) )
79 ssrab2 
 |-  { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } C_ ( SubGrp ` ( G |`s ( S ` q ) ) )
80 sswrd 
 |-  ( { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } C_ ( SubGrp ` ( G |`s ( S ` q ) ) ) -> Word { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } C_ Word ( SubGrp ` ( G |`s ( S ` q ) ) ) )
81 79 80 ax-mp 
 |-  Word { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } C_ Word ( SubGrp ` ( G |`s ( S ` q ) ) )
82 81 sseli 
 |-  ( s e. Word { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } -> s e. Word ( SubGrp ` ( G |`s ( S ` q ) ) ) )
83 39 adantr 
 |-  ( ( ( ph /\ q e. A ) /\ s e. Word ( SubGrp ` ( G |`s ( S ` q ) ) ) ) -> ( S ` q ) e. ( SubGrp ` G ) )
84 83 adantr 
 |-  ( ( ( ( ph /\ q e. A ) /\ s e. Word ( SubGrp ` ( G |`s ( S ` q ) ) ) ) /\ ( G |`s ( S ` q ) ) dom DProd s ) -> ( S ` q ) e. ( SubGrp ` G ) )
85 50 subgdmdprd 
 |-  ( ( S ` q ) e. ( SubGrp ` G ) -> ( ( G |`s ( S ` q ) ) dom DProd s <-> ( G dom DProd s /\ ran s C_ ~P ( S ` q ) ) ) )
86 83 85 syl 
 |-  ( ( ( ph /\ q e. A ) /\ s e. Word ( SubGrp ` ( G |`s ( S ` q ) ) ) ) -> ( ( G |`s ( S ` q ) ) dom DProd s <-> ( G dom DProd s /\ ran s C_ ~P ( S ` q ) ) ) )
87 86 simprbda 
 |-  ( ( ( ( ph /\ q e. A ) /\ s e. Word ( SubGrp ` ( G |`s ( S ` q ) ) ) ) /\ ( G |`s ( S ` q ) ) dom DProd s ) -> G dom DProd s )
88 86 simplbda 
 |-  ( ( ( ( ph /\ q e. A ) /\ s e. Word ( SubGrp ` ( G |`s ( S ` q ) ) ) ) /\ ( G |`s ( S ` q ) ) dom DProd s ) -> ran s C_ ~P ( S ` q ) )
89 50 84 87 88 subgdprd 
 |-  ( ( ( ( ph /\ q e. A ) /\ s e. Word ( SubGrp ` ( G |`s ( S ` q ) ) ) ) /\ ( G |`s ( S ` q ) ) dom DProd s ) -> ( ( G |`s ( S ` q ) ) DProd s ) = ( G DProd s ) )
90 55 ad2antrr 
 |-  ( ( ( ( ph /\ q e. A ) /\ s e. Word ( SubGrp ` ( G |`s ( S ` q ) ) ) ) /\ ( G |`s ( S ` q ) ) dom DProd s ) -> ( S ` q ) = ( Base ` ( G |`s ( S ` q ) ) ) )
91 90 eqcomd 
 |-  ( ( ( ( ph /\ q e. A ) /\ s e. Word ( SubGrp ` ( G |`s ( S ` q ) ) ) ) /\ ( G |`s ( S ` q ) ) dom DProd s ) -> ( Base ` ( G |`s ( S ` q ) ) ) = ( S ` q ) )
92 89 91 eqeq12d 
 |-  ( ( ( ( ph /\ q e. A ) /\ s e. Word ( SubGrp ` ( G |`s ( S ` q ) ) ) ) /\ ( G |`s ( S ` q ) ) dom DProd s ) -> ( ( ( G |`s ( S ` q ) ) DProd s ) = ( Base ` ( G |`s ( S ` q ) ) ) <-> ( G DProd s ) = ( S ` q ) ) )
93 92 biimpd 
 |-  ( ( ( ( ph /\ q e. A ) /\ s e. Word ( SubGrp ` ( G |`s ( S ` q ) ) ) ) /\ ( G |`s ( S ` q ) ) dom DProd s ) -> ( ( ( G |`s ( S ` q ) ) DProd s ) = ( Base ` ( G |`s ( S ` q ) ) ) -> ( G DProd s ) = ( S ` q ) ) )
94 93 87 jctild 
 |-  ( ( ( ( ph /\ q e. A ) /\ s e. Word ( SubGrp ` ( G |`s ( S ` q ) ) ) ) /\ ( G |`s ( S ` q ) ) dom DProd s ) -> ( ( ( G |`s ( S ` q ) ) DProd s ) = ( Base ` ( G |`s ( S ` q ) ) ) -> ( G dom DProd s /\ ( G DProd s ) = ( S ` q ) ) ) )
95 94 expimpd 
 |-  ( ( ( ph /\ q e. A ) /\ s e. Word ( SubGrp ` ( G |`s ( S ` q ) ) ) ) -> ( ( ( G |`s ( S ` q ) ) dom DProd s /\ ( ( G |`s ( S ` q ) ) DProd s ) = ( Base ` ( G |`s ( S ` q ) ) ) ) -> ( G dom DProd s /\ ( G DProd s ) = ( S ` q ) ) ) )
96 82 95 sylan2 
 |-  ( ( ( ph /\ q e. A ) /\ s e. Word { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } ) -> ( ( ( G |`s ( S ` q ) ) dom DProd s /\ ( ( G |`s ( S ` q ) ) DProd s ) = ( Base ` ( G |`s ( S ` q ) ) ) ) -> ( G dom DProd s /\ ( G DProd s ) = ( S ` q ) ) ) )
97 oveq2 
 |-  ( r = y -> ( ( G |`s ( S ` q ) ) |`s r ) = ( ( G |`s ( S ` q ) ) |`s y ) )
98 97 eleq1d 
 |-  ( r = y -> ( ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) <-> ( ( G |`s ( S ` q ) ) |`s y ) e. ( CycGrp i^i ran pGrp ) ) )
99 98 cbvrabv 
 |-  { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } = { y e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s y ) e. ( CycGrp i^i ran pGrp ) }
100 50 subsubg 
 |-  ( ( S ` q ) e. ( SubGrp ` G ) -> ( y e. ( SubGrp ` ( G |`s ( S ` q ) ) ) <-> ( y e. ( SubGrp ` G ) /\ y C_ ( S ` q ) ) ) )
101 39 100 syl 
 |-  ( ( ph /\ q e. A ) -> ( y e. ( SubGrp ` ( G |`s ( S ` q ) ) ) <-> ( y e. ( SubGrp ` G ) /\ y C_ ( S ` q ) ) ) )
102 101 simprbda 
 |-  ( ( ( ph /\ q e. A ) /\ y e. ( SubGrp ` ( G |`s ( S ` q ) ) ) ) -> y e. ( SubGrp ` G ) )
103 102 3adant3 
 |-  ( ( ( ph /\ q e. A ) /\ y e. ( SubGrp ` ( G |`s ( S ` q ) ) ) /\ ( ( G |`s ( S ` q ) ) |`s y ) e. ( CycGrp i^i ran pGrp ) ) -> y e. ( SubGrp ` G ) )
104 39 3ad2ant1 
 |-  ( ( ( ph /\ q e. A ) /\ y e. ( SubGrp ` ( G |`s ( S ` q ) ) ) /\ ( ( G |`s ( S ` q ) ) |`s y ) e. ( CycGrp i^i ran pGrp ) ) -> ( S ` q ) e. ( SubGrp ` G ) )
105 101 simplbda 
 |-  ( ( ( ph /\ q e. A ) /\ y e. ( SubGrp ` ( G |`s ( S ` q ) ) ) ) -> y C_ ( S ` q ) )
106 105 3adant3 
 |-  ( ( ( ph /\ q e. A ) /\ y e. ( SubGrp ` ( G |`s ( S ` q ) ) ) /\ ( ( G |`s ( S ` q ) ) |`s y ) e. ( CycGrp i^i ran pGrp ) ) -> y C_ ( S ` q ) )
107 ressabs 
 |-  ( ( ( S ` q ) e. ( SubGrp ` G ) /\ y C_ ( S ` q ) ) -> ( ( G |`s ( S ` q ) ) |`s y ) = ( G |`s y ) )
108 104 106 107 syl2anc 
 |-  ( ( ( ph /\ q e. A ) /\ y e. ( SubGrp ` ( G |`s ( S ` q ) ) ) /\ ( ( G |`s ( S ` q ) ) |`s y ) e. ( CycGrp i^i ran pGrp ) ) -> ( ( G |`s ( S ` q ) ) |`s y ) = ( G |`s y ) )
109 simp3 
 |-  ( ( ( ph /\ q e. A ) /\ y e. ( SubGrp ` ( G |`s ( S ` q ) ) ) /\ ( ( G |`s ( S ` q ) ) |`s y ) e. ( CycGrp i^i ran pGrp ) ) -> ( ( G |`s ( S ` q ) ) |`s y ) e. ( CycGrp i^i ran pGrp ) )
110 108 109 eqeltrrd 
 |-  ( ( ( ph /\ q e. A ) /\ y e. ( SubGrp ` ( G |`s ( S ` q ) ) ) /\ ( ( G |`s ( S ` q ) ) |`s y ) e. ( CycGrp i^i ran pGrp ) ) -> ( G |`s y ) e. ( CycGrp i^i ran pGrp ) )
111 oveq2 
 |-  ( r = y -> ( G |`s r ) = ( G |`s y ) )
112 111 eleq1d 
 |-  ( r = y -> ( ( G |`s r ) e. ( CycGrp i^i ran pGrp ) <-> ( G |`s y ) e. ( CycGrp i^i ran pGrp ) ) )
113 112 2 elrab2 
 |-  ( y e. C <-> ( y e. ( SubGrp ` G ) /\ ( G |`s y ) e. ( CycGrp i^i ran pGrp ) ) )
114 103 110 113 sylanbrc 
 |-  ( ( ( ph /\ q e. A ) /\ y e. ( SubGrp ` ( G |`s ( S ` q ) ) ) /\ ( ( G |`s ( S ` q ) ) |`s y ) e. ( CycGrp i^i ran pGrp ) ) -> y e. C )
115 114 rabssdv 
 |-  ( ( ph /\ q e. A ) -> { y e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s y ) e. ( CycGrp i^i ran pGrp ) } C_ C )
116 99 115 eqsstrid 
 |-  ( ( ph /\ q e. A ) -> { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } C_ C )
117 sswrd 
 |-  ( { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } C_ C -> Word { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } C_ Word C )
118 116 117 syl 
 |-  ( ( ph /\ q e. A ) -> Word { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } C_ Word C )
119 118 sselda 
 |-  ( ( ( ph /\ q e. A ) /\ s e. Word { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } ) -> s e. Word C )
120 96 119 jctild 
 |-  ( ( ( ph /\ q e. A ) /\ s e. Word { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } ) -> ( ( ( G |`s ( S ` q ) ) dom DProd s /\ ( ( G |`s ( S ` q ) ) DProd s ) = ( Base ` ( G |`s ( S ` q ) ) ) ) -> ( s e. Word C /\ ( G dom DProd s /\ ( G DProd s ) = ( S ` q ) ) ) ) )
121 120 expimpd 
 |-  ( ( ph /\ q e. A ) -> ( ( s e. Word { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } /\ ( ( G |`s ( S ` q ) ) dom DProd s /\ ( ( G |`s ( S ` q ) ) DProd s ) = ( Base ` ( G |`s ( S ` q ) ) ) ) ) -> ( s e. Word C /\ ( G dom DProd s /\ ( G DProd s ) = ( S ` q ) ) ) ) )
122 121 reximdv2 
 |-  ( ( ph /\ q e. A ) -> ( E. s e. Word { r e. ( SubGrp ` ( G |`s ( S ` q ) ) ) | ( ( G |`s ( S ` q ) ) |`s r ) e. ( CycGrp i^i ran pGrp ) } ( ( G |`s ( S ` q ) ) dom DProd s /\ ( ( G |`s ( S ` q ) ) DProd s ) = ( Base ` ( G |`s ( S ` q ) ) ) ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = ( S ` q ) ) ) )
123 78 122 mpd 
 |-  ( ( ph /\ q e. A ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = ( S ` q ) ) )
124 rabn0 
 |-  ( { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = ( S ` q ) ) } =/= (/) <-> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = ( S ` q ) ) )
125 123 124 sylibr 
 |-  ( ( ph /\ q e. A ) -> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = ( S ` q ) ) } =/= (/) )
126 47 125 eqnetrd 
 |-  ( ( ph /\ q e. A ) -> { y e. Word C | y e. ( W ` ( S ` q ) ) } =/= (/) )
127 rabn0 
 |-  ( { y e. Word C | y e. ( W ` ( S ` q ) ) } =/= (/) <-> E. y e. Word C y e. ( W ` ( S ` q ) ) )
128 126 127 sylib 
 |-  ( ( ph /\ q e. A ) -> E. y e. Word C y e. ( W ` ( S ` q ) ) )
129 128 ralrimiva 
 |-  ( ph -> A. q e. A E. y e. Word C y e. ( W ` ( S ` q ) ) )
130 eleq1 
 |-  ( y = ( f ` q ) -> ( y e. ( W ` ( S ` q ) ) <-> ( f ` q ) e. ( W ` ( S ` q ) ) ) )
131 130 ac6sfi 
 |-  ( ( A e. Fin /\ A. q e. A E. y e. Word C y e. ( W ` ( S ` q ) ) ) -> E. f ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) )
132 29 129 131 syl2anc 
 |-  ( ph -> E. f ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) )
133 sneq 
 |-  ( q = y -> { q } = { y } )
134 fveq2 
 |-  ( q = y -> ( f ` q ) = ( f ` y ) )
135 134 dmeqd 
 |-  ( q = y -> dom ( f ` q ) = dom ( f ` y ) )
136 133 135 xpeq12d 
 |-  ( q = y -> ( { q } X. dom ( f ` q ) ) = ( { y } X. dom ( f ` y ) ) )
137 136 cbviunv 
 |-  U_ q e. A ( { q } X. dom ( f ` q ) ) = U_ y e. A ( { y } X. dom ( f ` y ) )
138 snfi 
 |-  { y } e. Fin
139 simprl 
 |-  ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) -> f : A --> Word C )
140 139 ffvelcdmda 
 |-  ( ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) /\ y e. A ) -> ( f ` y ) e. Word C )
141 wrdf 
 |-  ( ( f ` y ) e. Word C -> ( f ` y ) : ( 0 ..^ ( # ` ( f ` y ) ) ) --> C )
142 fdm 
 |-  ( ( f ` y ) : ( 0 ..^ ( # ` ( f ` y ) ) ) --> C -> dom ( f ` y ) = ( 0 ..^ ( # ` ( f ` y ) ) ) )
143 140 141 142 3syl 
 |-  ( ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) /\ y e. A ) -> dom ( f ` y ) = ( 0 ..^ ( # ` ( f ` y ) ) ) )
144 fzofi 
 |-  ( 0 ..^ ( # ` ( f ` y ) ) ) e. Fin
145 143 144 eqeltrdi 
 |-  ( ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) /\ y e. A ) -> dom ( f ` y ) e. Fin )
146 xpfi 
 |-  ( ( { y } e. Fin /\ dom ( f ` y ) e. Fin ) -> ( { y } X. dom ( f ` y ) ) e. Fin )
147 138 145 146 sylancr 
 |-  ( ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) /\ y e. A ) -> ( { y } X. dom ( f ` y ) ) e. Fin )
148 147 ralrimiva 
 |-  ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) -> A. y e. A ( { y } X. dom ( f ` y ) ) e. Fin )
149 iunfi 
 |-  ( ( A e. Fin /\ A. y e. A ( { y } X. dom ( f ` y ) ) e. Fin ) -> U_ y e. A ( { y } X. dom ( f ` y ) ) e. Fin )
150 29 148 149 syl2an2r 
 |-  ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) -> U_ y e. A ( { y } X. dom ( f ` y ) ) e. Fin )
151 137 150 eqeltrid 
 |-  ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) -> U_ q e. A ( { q } X. dom ( f ` q ) ) e. Fin )
152 hashcl 
 |-  ( U_ q e. A ( { q } X. dom ( f ` q ) ) e. Fin -> ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) e. NN0 )
153 hashfzo0 
 |-  ( ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) e. NN0 -> ( # ` ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) ) = ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) )
154 151 152 153 3syl 
 |-  ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) -> ( # ` ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) ) = ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) )
155 fzofi 
 |-  ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) e. Fin
156 hashen 
 |-  ( ( ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) e. Fin /\ U_ q e. A ( { q } X. dom ( f ` q ) ) e. Fin ) -> ( ( # ` ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) ) = ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) <-> ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) ~~ U_ q e. A ( { q } X. dom ( f ` q ) ) ) )
157 155 151 156 sylancr 
 |-  ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) -> ( ( # ` ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) ) = ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) <-> ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) ~~ U_ q e. A ( { q } X. dom ( f ` q ) ) ) )
158 154 157 mpbid 
 |-  ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) -> ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) ~~ U_ q e. A ( { q } X. dom ( f ` q ) ) )
159 bren 
 |-  ( ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) ~~ U_ q e. A ( { q } X. dom ( f ` q ) ) <-> E. h h : ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -1-1-onto-> U_ q e. A ( { q } X. dom ( f ` q ) ) )
160 158 159 sylib 
 |-  ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) -> E. h h : ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -1-1-onto-> U_ q e. A ( { q } X. dom ( f ` q ) ) )
161 3 adantr 
 |-  ( ( ph /\ ( ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) /\ h : ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -1-1-onto-> U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -> G e. Abel )
162 4 adantr 
 |-  ( ( ph /\ ( ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) /\ h : ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -1-1-onto-> U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -> B e. Fin )
163 breq1 
 |-  ( w = a -> ( w || ( # ` B ) <-> a || ( # ` B ) ) )
164 163 cbvrabv 
 |-  { w e. Prime | w || ( # ` B ) } = { a e. Prime | a || ( # ` B ) }
165 6 164 eqtri 
 |-  A = { a e. Prime | a || ( # ` B ) }
166 fveq2 
 |-  ( x = c -> ( O ` x ) = ( O ` c ) )
167 166 breq1d 
 |-  ( x = c -> ( ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) <-> ( O ` c ) || ( p ^ ( p pCnt ( # ` B ) ) ) ) )
168 167 cbvrabv 
 |-  { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } = { c e. B | ( O ` c ) || ( p ^ ( p pCnt ( # ` B ) ) ) }
169 id 
 |-  ( p = b -> p = b )
170 oveq1 
 |-  ( p = b -> ( p pCnt ( # ` B ) ) = ( b pCnt ( # ` B ) ) )
171 169 170 oveq12d 
 |-  ( p = b -> ( p ^ ( p pCnt ( # ` B ) ) ) = ( b ^ ( b pCnt ( # ` B ) ) ) )
172 171 breq2d 
 |-  ( p = b -> ( ( O ` c ) || ( p ^ ( p pCnt ( # ` B ) ) ) <-> ( O ` c ) || ( b ^ ( b pCnt ( # ` B ) ) ) ) )
173 172 rabbidv 
 |-  ( p = b -> { c e. B | ( O ` c ) || ( p ^ ( p pCnt ( # ` B ) ) ) } = { c e. B | ( O ` c ) || ( b ^ ( b pCnt ( # ` B ) ) ) } )
174 168 173 eqtrid 
 |-  ( p = b -> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } = { c e. B | ( O ` c ) || ( b ^ ( b pCnt ( # ` B ) ) ) } )
175 174 cbvmptv 
 |-  ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } ) = ( b e. A |-> { c e. B | ( O ` c ) || ( b ^ ( b pCnt ( # ` B ) ) ) } )
176 7 175 eqtri 
 |-  S = ( b e. A |-> { c e. B | ( O ` c ) || ( b ^ ( b pCnt ( # ` B ) ) ) } )
177 breq2 
 |-  ( s = t -> ( G dom DProd s <-> G dom DProd t ) )
178 oveq2 
 |-  ( s = t -> ( G DProd s ) = ( G DProd t ) )
179 178 eqeq1d 
 |-  ( s = t -> ( ( G DProd s ) = g <-> ( G DProd t ) = g ) )
180 177 179 anbi12d 
 |-  ( s = t -> ( ( G dom DProd s /\ ( G DProd s ) = g ) <-> ( G dom DProd t /\ ( G DProd t ) = g ) ) )
181 180 cbvrabv 
 |-  { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = g ) } = { t e. Word C | ( G dom DProd t /\ ( G DProd t ) = g ) }
182 181 mpteq2i 
 |-  ( g e. ( SubGrp ` G ) |-> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = g ) } ) = ( g e. ( SubGrp ` G ) |-> { t e. Word C | ( G dom DProd t /\ ( G DProd t ) = g ) } )
183 8 182 eqtri 
 |-  W = ( g e. ( SubGrp ` G ) |-> { t e. Word C | ( G dom DProd t /\ ( G DProd t ) = g ) } )
184 simprll 
 |-  ( ( ph /\ ( ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) /\ h : ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -1-1-onto-> U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -> f : A --> Word C )
185 simprlr 
 |-  ( ( ph /\ ( ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) /\ h : ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -1-1-onto-> U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -> A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) )
186 2fveq3 
 |-  ( q = y -> ( W ` ( S ` q ) ) = ( W ` ( S ` y ) ) )
187 134 186 eleq12d 
 |-  ( q = y -> ( ( f ` q ) e. ( W ` ( S ` q ) ) <-> ( f ` y ) e. ( W ` ( S ` y ) ) ) )
188 187 cbvralvw 
 |-  ( A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) <-> A. y e. A ( f ` y ) e. ( W ` ( S ` y ) ) )
189 185 188 sylib 
 |-  ( ( ph /\ ( ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) /\ h : ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -1-1-onto-> U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -> A. y e. A ( f ` y ) e. ( W ` ( S ` y ) ) )
190 simprr 
 |-  ( ( ph /\ ( ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) /\ h : ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -1-1-onto-> U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -> h : ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -1-1-onto-> U_ q e. A ( { q } X. dom ( f ` q ) ) )
191 1 2 161 162 5 165 176 183 184 189 137 190 ablfaclem2 
 |-  ( ( ph /\ ( ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) /\ h : ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -1-1-onto-> U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -> ( W ` B ) =/= (/) )
192 191 expr 
 |-  ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) -> ( h : ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -1-1-onto-> U_ q e. A ( { q } X. dom ( f ` q ) ) -> ( W ` B ) =/= (/) ) )
193 192 exlimdv 
 |-  ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) -> ( E. h h : ( 0 ..^ ( # ` U_ q e. A ( { q } X. dom ( f ` q ) ) ) ) -1-1-onto-> U_ q e. A ( { q } X. dom ( f ` q ) ) -> ( W ` B ) =/= (/) ) )
194 160 193 mpd 
 |-  ( ( ph /\ ( f : A --> Word C /\ A. q e. A ( f ` q ) e. ( W ` ( S ` q ) ) ) ) -> ( W ` B ) =/= (/) )
195 132 194 exlimddv 
 |-  ( ph -> ( W ` B ) =/= (/) )