Metamath Proof Explorer

Theorem ablfaclem1

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 ablfaclem1 
|- ( U e. ( SubGrp ` G ) -> ( W ` U ) = { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = U ) } )

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 eqeq2 
 |-  ( g = U -> ( ( G DProd s ) = g <-> ( G DProd s ) = U ) )
10 9 anbi2d 
 |-  ( g = U -> ( ( G dom DProd s /\ ( G DProd s ) = g ) <-> ( G dom DProd s /\ ( G DProd s ) = U ) ) )
11 10 rabbidv 
 |-  ( g = U -> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = g ) } = { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = U ) } )
12 fvex 
 |-  ( SubGrp ` G ) e. _V
13 2 12 rabex2 
 |-  C e. _V
14 13 wrdexi 
 |-  Word C e. _V
15 14 rabex 
 |-  { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = U ) } e. _V
16 11 8 15 fvmpt 
 |-  ( U e. ( SubGrp ` G ) -> ( W ` U ) = { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = U ) } )