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 = ( 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 ) } )
ablfaclem2.f 
|- ( ph -> F : A --> Word C )
ablfaclem2.q 
|- ( ph -> A. y e. A ( F ` y ) e. ( W ` ( S ` y ) ) )
ablfaclem2.l 
|- L = U_ y e. A ( { y } X. dom ( F ` y ) )
ablfaclem2.g 
|- ( ph -> H : ( 0 ..^ ( # ` L ) ) -1-1-onto-> L )
Assertion ablfaclem2 
|- ( 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 ablfaclem2.f 
 |-  ( ph -> F : A --> Word C )
10 ablfaclem2.q 
 |-  ( ph -> A. y e. A ( F ` y ) e. ( W ` ( S ` y ) ) )
11 ablfaclem2.l 
 |-  L = U_ y e. A ( { y } X. dom ( F ` y ) )
12 ablfaclem2.g 
 |-  ( ph -> H : ( 0 ..^ ( # ` L ) ) -1-1-onto-> L )
13 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
14 1 subgid 
 |-  ( G e. Grp -> B e. ( SubGrp ` G ) )
15 1 2 3 4 5 6 7 8 ablfaclem1 
 |-  ( B e. ( SubGrp ` G ) -> ( W ` B ) = { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = B ) } )
16 3 13 14 15 4syl 
 |-  ( ph -> ( W ` B ) = { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = B ) } )
17 9 ffvelrnda 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) e. Word C )
18 wrdf 
 |-  ( ( F ` y ) e. Word C -> ( F ` y ) : ( 0 ..^ ( # ` ( F ` y ) ) ) --> C )
19 17 18 syl 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) : ( 0 ..^ ( # ` ( F ` y ) ) ) --> C )
20 19 ffdmd 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) : dom ( F ` y ) --> C )
21 20 ffvelrnda 
 |-  ( ( ( ph /\ y e. A ) /\ z e. dom ( F ` y ) ) -> ( ( F ` y ) ` z ) e. C )
22 21 anasss 
 |-  ( ( ph /\ ( y e. A /\ z e. dom ( F ` y ) ) ) -> ( ( F ` y ) ` z ) e. C )
23 22 ralrimivva 
 |-  ( ph -> A. y e. A A. z e. dom ( F ` y ) ( ( F ` y ) ` z ) e. C )
24 eqid 
 |-  ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) = ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) )
25 24 fmpox 
 |-  ( A. y e. A A. z e. dom ( F ` y ) ( ( F ` y ) ` z ) e. C <-> ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) : U_ y e. A ( { y } X. dom ( F ` y ) ) --> C )
26 23 25 sylib 
 |-  ( ph -> ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) : U_ y e. A ( { y } X. dom ( F ` y ) ) --> C )
27 11 feq2i 
 |-  ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) : L --> C <-> ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) : U_ y e. A ( { y } X. dom ( F ` y ) ) --> C )
28 26 27 sylibr 
 |-  ( ph -> ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) : L --> C )
29 f1of 
 |-  ( H : ( 0 ..^ ( # ` L ) ) -1-1-onto-> L -> H : ( 0 ..^ ( # ` L ) ) --> L )
30 12 29 syl 
 |-  ( ph -> H : ( 0 ..^ ( # ` L ) ) --> L )
31 fco 
 |-  ( ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) : L --> C /\ H : ( 0 ..^ ( # ` L ) ) --> L ) -> ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) : ( 0 ..^ ( # ` L ) ) --> C )
32 28 30 31 syl2anc 
 |-  ( ph -> ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) : ( 0 ..^ ( # ` L ) ) --> C )
33 iswrdi 
 |-  ( ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) : ( 0 ..^ ( # ` L ) ) --> C -> ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) e. Word C )
34 32 33 syl 
 |-  ( ph -> ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) e. Word C )
35 10 r19.21bi 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) e. ( W ` ( S ` y ) ) )
36 6 ssrab3 
 |-  A C_ Prime
37 36 a1i 
 |-  ( ph -> A C_ Prime )
38 1 5 7 3 4 37 ablfac1b 
 |-  ( ph -> G dom DProd S )
39 1 fvexi 
 |-  B e. _V
40 39 rabex 
 |-  { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } e. _V
41 40 7 dmmpti 
 |-  dom S = A
42 41 a1i 
 |-  ( ph -> dom S = A )
43 38 42 dprdf2 
 |-  ( ph -> S : A --> ( SubGrp ` G ) )
44 43 ffvelrnda 
 |-  ( ( ph /\ y e. A ) -> ( S ` y ) e. ( SubGrp ` G ) )
45 1 2 3 4 5 6 7 8 ablfaclem1 
 |-  ( ( S ` y ) e. ( SubGrp ` G ) -> ( W ` ( S ` y ) ) = { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = ( S ` y ) ) } )
46 44 45 syl 
 |-  ( ( ph /\ y e. A ) -> ( W ` ( S ` y ) ) = { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = ( S ` y ) ) } )
47 35 46 eleqtrd 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) e. { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = ( S ` y ) ) } )
48 breq2 
 |-  ( s = ( F ` y ) -> ( G dom DProd s <-> G dom DProd ( F ` y ) ) )
49 oveq2 
 |-  ( s = ( F ` y ) -> ( G DProd s ) = ( G DProd ( F ` y ) ) )
50 49 eqeq1d 
 |-  ( s = ( F ` y ) -> ( ( G DProd s ) = ( S ` y ) <-> ( G DProd ( F ` y ) ) = ( S ` y ) ) )
51 48 50 anbi12d 
 |-  ( s = ( F ` y ) -> ( ( G dom DProd s /\ ( G DProd s ) = ( S ` y ) ) <-> ( G dom DProd ( F ` y ) /\ ( G DProd ( F ` y ) ) = ( S ` y ) ) ) )
52 51 elrab 
 |-  ( ( F ` y ) e. { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = ( S ` y ) ) } <-> ( ( F ` y ) e. Word C /\ ( G dom DProd ( F ` y ) /\ ( G DProd ( F ` y ) ) = ( S ` y ) ) ) )
53 52 simprbi 
 |-  ( ( F ` y ) e. { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = ( S ` y ) ) } -> ( G dom DProd ( F ` y ) /\ ( G DProd ( F ` y ) ) = ( S ` y ) ) )
54 47 53 syl 
 |-  ( ( ph /\ y e. A ) -> ( G dom DProd ( F ` y ) /\ ( G DProd ( F ` y ) ) = ( S ` y ) ) )
55 54 simpld 
 |-  ( ( ph /\ y e. A ) -> G dom DProd ( F ` y ) )
56 dprdf 
 |-  ( G dom DProd ( F ` y ) -> ( F ` y ) : dom ( F ` y ) --> ( SubGrp ` G ) )
57 55 56 syl 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) : dom ( F ` y ) --> ( SubGrp ` G ) )
58 57 ffvelrnda 
 |-  ( ( ( ph /\ y e. A ) /\ z e. dom ( F ` y ) ) -> ( ( F ` y ) ` z ) e. ( SubGrp ` G ) )
59 58 anasss 
 |-  ( ( ph /\ ( y e. A /\ z e. dom ( F ` y ) ) ) -> ( ( F ` y ) ` z ) e. ( SubGrp ` G ) )
60 57 feqmptd 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) = ( z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) )
61 55 60 breqtrd 
 |-  ( ( ph /\ y e. A ) -> G dom DProd ( z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) )
62 43 feqmptd 
 |-  ( ph -> S = ( y e. A |-> ( S ` y ) ) )
63 60 oveq2d 
 |-  ( ( ph /\ y e. A ) -> ( G DProd ( F ` y ) ) = ( G DProd ( z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) ) )
64 54 simprd 
 |-  ( ( ph /\ y e. A ) -> ( G DProd ( F ` y ) ) = ( S ` y ) )
65 63 64 eqtr3d 
 |-  ( ( ph /\ y e. A ) -> ( G DProd ( z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) ) = ( S ` y ) )
66 65 mpteq2dva 
 |-  ( ph -> ( y e. A |-> ( G DProd ( z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) ) ) = ( y e. A |-> ( S ` y ) ) )
67 62 66 eqtr4d 
 |-  ( ph -> S = ( y e. A |-> ( G DProd ( z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) ) ) )
68 38 67 breqtrd 
 |-  ( ph -> G dom DProd ( y e. A |-> ( G DProd ( z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) ) ) )
69 59 61 68 dprd2d2 
 |-  ( ph -> ( G dom DProd ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) /\ ( G DProd ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) ) = ( G DProd ( y e. A |-> ( G DProd ( z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) ) ) ) ) )
70 69 simpld 
 |-  ( ph -> G dom DProd ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) )
71 28 fdmd 
 |-  ( ph -> dom ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) = L )
72 70 71 12 dprdf1o 
 |-  ( ph -> ( G dom DProd ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) /\ ( G DProd ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) ) = ( G DProd ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) ) ) )
73 72 simpld 
 |-  ( ph -> G dom DProd ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) )
74 72 simprd 
 |-  ( ph -> ( G DProd ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) ) = ( G DProd ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) ) )
75 69 simprd 
 |-  ( ph -> ( G DProd ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) ) = ( G DProd ( y e. A |-> ( G DProd ( z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) ) ) ) )
76 67 oveq2d 
 |-  ( ph -> ( G DProd S ) = ( G DProd ( y e. A |-> ( G DProd ( z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) ) ) ) )
77 ssidd 
 |-  ( ph -> A C_ A )
78 1 5 7 3 4 37 6 77 ablfac1c 
 |-  ( ph -> ( G DProd S ) = B )
79 76 78 eqtr3d 
 |-  ( ph -> ( G DProd ( y e. A |-> ( G DProd ( z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) ) ) ) = B )
80 74 75 79 3eqtrd 
 |-  ( ph -> ( G DProd ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) ) = B )
81 breq2 
 |-  ( s = ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) -> ( G dom DProd s <-> G dom DProd ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) ) )
82 oveq2 
 |-  ( s = ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) -> ( G DProd s ) = ( G DProd ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) ) )
83 82 eqeq1d 
 |-  ( s = ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) -> ( ( G DProd s ) = B <-> ( G DProd ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) ) = B ) )
84 81 83 anbi12d 
 |-  ( s = ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) -> ( ( G dom DProd s /\ ( G DProd s ) = B ) <-> ( G dom DProd ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) /\ ( G DProd ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) ) = B ) ) )
85 84 rspcev 
 |-  ( ( ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) e. Word C /\ ( G dom DProd ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) /\ ( G DProd ( ( y e. A , z e. dom ( F ` y ) |-> ( ( F ` y ) ` z ) ) o. H ) ) = B ) ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) )
86 34 73 80 85 syl12anc 
 |-  ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) )
87 rabn0 
 |-  ( { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = B ) } =/= (/) <-> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) )
88 86 87 sylibr 
 |-  ( ph -> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = B ) } =/= (/) )
89 16 88 eqnetrd 
 |-  ( ph -> ( W ` B ) =/= (/) )