MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pgpfaclem1 Structured version   Unicode version

Theorem pgpfaclem1 15641
Description: Lemma for pgpfac 15644. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
Hypotheses
Ref Expression
pgpfac.b  |-  B  =  ( Base `  G
)
pgpfac.c  |-  C  =  { r  e.  (SubGrp `  G )  |  ( Gs  r )  e.  (CycGrp 
i^i  ran pGrp  ) }
pgpfac.g  |-  ( ph  ->  G  e.  Abel )
pgpfac.p  |-  ( ph  ->  P pGrp  G )
pgpfac.f  |-  ( ph  ->  B  e.  Fin )
pgpfac.u  |-  ( ph  ->  U  e.  (SubGrp `  G ) )
pgpfac.a  |-  ( ph  ->  A. t  e.  (SubGrp `  G ) ( t 
C.  U  ->  E. s  e. Word  C ( G dom DProd  s  /\  ( G DProd  s
)  =  t ) ) )
pgpfac.h  |-  H  =  ( Gs  U )
pgpfac.k  |-  K  =  (mrCls `  (SubGrp `  H
) )
pgpfac.o  |-  O  =  ( od `  H
)
pgpfac.e  |-  E  =  (gEx `  H )
pgpfac.0  |-  .0.  =  ( 0g `  H )
pgpfac.l  |-  .(+)  =  (
LSSum `  H )
pgpfac.1  |-  ( ph  ->  E  =/=  1 )
pgpfac.x  |-  ( ph  ->  X  e.  U )
pgpfac.oe  |-  ( ph  ->  ( O `  X
)  =  E )
pgpfac.w  |-  ( ph  ->  W  e.  (SubGrp `  H ) )
pgpfac.i  |-  ( ph  ->  ( ( K `  { X } )  i^i 
W )  =  {  .0.  } )
pgpfac.s  |-  ( ph  ->  ( ( K `  { X } )  .(+)  W )  =  U )
pgpfac.2  |-  ( ph  ->  S  e. Word  C )
pgpfac.4  |-  ( ph  ->  G dom DProd  S )
pgpfac.5  |-  ( ph  ->  ( G DProd  S )  =  W )
pgpfac.t  |-  T  =  ( S concat  <" ( K `  { X } ) "> )
Assertion
Ref Expression
pgpfaclem1  |-  ( ph  ->  E. s  e. Word  C
( G dom DProd  s  /\  ( G DProd  s )  =  U ) )
Distinct variable groups:    t, s, C    s, r, t, G    K, r, s    ph, t    B, s, t    U, r, s, t    W, s, t    X, r, s    T, s
Allowed substitution hints:    ph( s, r)    B( r)    C( r)    P( t, s, r)    .(+) ( t, s, r)    S( t, s, r)    T( t, r)    E( t, s, r)    H( t, s, r)    K( t)    O( t, s, r)    W( r)    X( t)    .0. ( t,
s, r)

Proof of Theorem pgpfaclem1
StepHypRef Expression
1 pgpfac.t . . 3  |-  T  =  ( S concat  <" ( K `  { X } ) "> )
2 pgpfac.2 . . 3  |-  ( ph  ->  S  e. Word  C )
3 pgpfac.u . . . . . . . . 9  |-  ( ph  ->  U  e.  (SubGrp `  G ) )
4 pgpfac.h . . . . . . . . . 10  |-  H  =  ( Gs  U )
54subggrp 14949 . . . . . . . . 9  |-  ( U  e.  (SubGrp `  G
)  ->  H  e.  Grp )
63, 5syl 16 . . . . . . . 8  |-  ( ph  ->  H  e.  Grp )
7 eqid 2438 . . . . . . . . 9  |-  ( Base `  H )  =  (
Base `  H )
87subgacs 14977 . . . . . . . 8  |-  ( H  e.  Grp  ->  (SubGrp `  H )  e.  (ACS
`  ( Base `  H
) ) )
9 acsmre 13879 . . . . . . . 8  |-  ( (SubGrp `  H )  e.  (ACS
`  ( Base `  H
) )  ->  (SubGrp `  H )  e.  (Moore `  ( Base `  H
) ) )
106, 8, 93syl 19 . . . . . . 7  |-  ( ph  ->  (SubGrp `  H )  e.  (Moore `  ( Base `  H ) ) )
11 pgpfac.x . . . . . . . 8  |-  ( ph  ->  X  e.  U )
124subgbas 14950 . . . . . . . . 9  |-  ( U  e.  (SubGrp `  G
)  ->  U  =  ( Base `  H )
)
133, 12syl 16 . . . . . . . 8  |-  ( ph  ->  U  =  ( Base `  H ) )
1411, 13eleqtrd 2514 . . . . . . 7  |-  ( ph  ->  X  e.  ( Base `  H ) )
15 pgpfac.k . . . . . . . 8  |-  K  =  (mrCls `  (SubGrp `  H
) )
1615mrcsncl 13839 . . . . . . 7  |-  ( ( (SubGrp `  H )  e.  (Moore `  ( Base `  H ) )  /\  X  e.  ( Base `  H ) )  -> 
( K `  { X } )  e.  (SubGrp `  H ) )
1710, 14, 16syl2anc 644 . . . . . 6  |-  ( ph  ->  ( K `  { X } )  e.  (SubGrp `  H ) )
184subsubg 14965 . . . . . . 7  |-  ( U  e.  (SubGrp `  G
)  ->  ( ( K `  { X } )  e.  (SubGrp `  H )  <->  ( ( K `  { X } )  e.  (SubGrp `  G )  /\  ( K `  { X } )  C_  U
) ) )
193, 18syl 16 . . . . . 6  |-  ( ph  ->  ( ( K `  { X } )  e.  (SubGrp `  H )  <->  ( ( K `  { X } )  e.  (SubGrp `  G )  /\  ( K `  { X } )  C_  U
) ) )
2017, 19mpbid 203 . . . . 5  |-  ( ph  ->  ( ( K `  { X } )  e.  (SubGrp `  G )  /\  ( K `  { X } )  C_  U
) )
2120simpld 447 . . . 4  |-  ( ph  ->  ( K `  { X } )  e.  (SubGrp `  G ) )
224oveq1i 6093 . . . . . . 7  |-  ( Hs  ( K `  { X } ) )  =  ( ( Gs  U )s  ( K `  { X } ) )
2320simprd 451 . . . . . . . 8  |-  ( ph  ->  ( K `  { X } )  C_  U
)
24 ressabs 13529 . . . . . . . 8  |-  ( ( U  e.  (SubGrp `  G )  /\  ( K `  { X } )  C_  U
)  ->  ( ( Gs  U )s  ( K `  { X } ) )  =  ( Gs  ( K `
 { X }
) ) )
253, 23, 24syl2anc 644 . . . . . . 7  |-  ( ph  ->  ( ( Gs  U )s  ( K `  { X } ) )  =  ( Gs  ( K `  { X } ) ) )
2622, 25syl5eq 2482 . . . . . 6  |-  ( ph  ->  ( Hs  ( K `  { X } ) )  =  ( Gs  ( K `
 { X }
) ) )
277, 15cycsubgcyg2 15513 . . . . . . 7  |-  ( ( H  e.  Grp  /\  X  e.  ( Base `  H ) )  -> 
( Hs  ( K `  { X } ) )  e. CycGrp )
286, 14, 27syl2anc 644 . . . . . 6  |-  ( ph  ->  ( Hs  ( K `  { X } ) )  e. CycGrp )
2926, 28eqeltrrd 2513 . . . . 5  |-  ( ph  ->  ( Gs  ( K `  { X } ) )  e. CycGrp )
30 pgpfac.p . . . . . . 7  |-  ( ph  ->  P pGrp  G )
31 pgpprm 15229 . . . . . . 7  |-  ( P pGrp 
G  ->  P  e.  Prime )
3230, 31syl 16 . . . . . 6  |-  ( ph  ->  P  e.  Prime )
33 subgpgp 15233 . . . . . . 7  |-  ( ( P pGrp  G  /\  ( K `  { X } )  e.  (SubGrp `  G ) )  ->  P pGrp  ( Gs  ( K `  { X } ) ) )
3430, 21, 33syl2anc 644 . . . . . 6  |-  ( ph  ->  P pGrp  ( Gs  ( K `
 { X }
) ) )
35 brelrng 5101 . . . . . 6  |-  ( ( P  e.  Prime  /\  ( Gs  ( K `  { X } ) )  e. CycGrp  /\  P pGrp  ( Gs  ( K `  { X } ) ) )  ->  ( Gs  ( K `
 { X }
) )  e.  ran pGrp  )
3632, 29, 34, 35syl3anc 1185 . . . . 5  |-  ( ph  ->  ( Gs  ( K `  { X } ) )  e.  ran pGrp  )
37 elin 3532 . . . . 5  |-  ( ( Gs  ( K `  { X } ) )  e.  (CycGrp  i^i  ran pGrp  )  <->  ( ( Gs  ( K `  { X } ) )  e. CycGrp  /\  ( Gs  ( K `  { X } ) )  e.  ran pGrp  ) )
3829, 36, 37sylanbrc 647 . . . 4  |-  ( ph  ->  ( Gs  ( K `  { X } ) )  e.  (CycGrp  i^i  ran pGrp  ) )
39 oveq2 6091 . . . . . 6  |-  ( r  =  ( K `  { X } )  -> 
( Gs  r )  =  ( Gs  ( K `  { X } ) ) )
4039eleq1d 2504 . . . . 5  |-  ( r  =  ( K `  { X } )  -> 
( ( Gs  r )  e.  (CycGrp  i^i  ran pGrp  )  <-> 
( Gs  ( K `  { X } ) )  e.  (CycGrp  i^i  ran pGrp  ) ) )
41 pgpfac.c . . . . 5  |-  C  =  { r  e.  (SubGrp `  G )  |  ( Gs  r )  e.  (CycGrp 
i^i  ran pGrp  ) }
4240, 41elrab2 3096 . . . 4  |-  ( ( K `  { X } )  e.  C  <->  ( ( K `  { X } )  e.  (SubGrp `  G )  /\  ( Gs  ( K `  { X } ) )  e.  (CycGrp  i^i  ran pGrp  ) ) )
4321, 38, 42sylanbrc 647 . . 3  |-  ( ph  ->  ( K `  { X } )  e.  C
)
441, 2, 43cats1cld 11821 . 2  |-  ( ph  ->  T  e. Word  C )
45 wrdf 11735 . . . . 5  |-  ( T  e. Word  C  ->  T : ( 0..^ (
# `  T )
) --> C )
4644, 45syl 16 . . . 4  |-  ( ph  ->  T : ( 0..^ ( # `  T
) ) --> C )
47 ssrab2 3430 . . . . 5  |-  { r  e.  (SubGrp `  G
)  |  ( Gs  r )  e.  (CycGrp  i^i  ran pGrp  ) }  C_  (SubGrp `  G )
4841, 47eqsstri 3380 . . . 4  |-  C  C_  (SubGrp `  G )
49 fss 5601 . . . 4  |-  ( ( T : ( 0..^ ( # `  T
) ) --> C  /\  C  C_  (SubGrp `  G
) )  ->  T : ( 0..^ (
# `  T )
) --> (SubGrp `  G )
)
5046, 48, 49sylancl 645 . . 3  |-  ( ph  ->  T : ( 0..^ ( # `  T
) ) --> (SubGrp `  G ) )
51 fzodisj 11169 . . . 4  |-  ( ( 0..^ ( # `  S
) )  i^i  (
( # `  S )..^ ( ( # `  S
)  +  1 ) ) )  =  (/)
52 lencl 11737 . . . . . . . 8  |-  ( S  e. Word  C  ->  ( # `
 S )  e. 
NN0 )
532, 52syl 16 . . . . . . 7  |-  ( ph  ->  ( # `  S
)  e.  NN0 )
5453nn0zd 10375 . . . . . 6  |-  ( ph  ->  ( # `  S
)  e.  ZZ )
55 fzosn 11183 . . . . . 6  |-  ( (
# `  S )  e.  ZZ  ->  ( ( # `
 S )..^ ( ( # `  S
)  +  1 ) )  =  { (
# `  S ) } )
5654, 55syl 16 . . . . 5  |-  ( ph  ->  ( ( # `  S
)..^ ( ( # `  S )  +  1 ) )  =  {
( # `  S ) } )
5756ineq2d 3544 . . . 4  |-  ( ph  ->  ( ( 0..^ (
# `  S )
)  i^i  ( ( # `
 S )..^ ( ( # `  S
)  +  1 ) ) )  =  ( ( 0..^ ( # `  S ) )  i^i 
{ ( # `  S
) } ) )
5851, 57syl5reqr 2485 . . 3  |-  ( ph  ->  ( ( 0..^ (
# `  S )
)  i^i  { ( # `
 S ) } )  =  (/) )
591fveq2i 5733 . . . . . . 7  |-  ( # `  T )  =  (
# `  ( S concat  <" ( K `  { X } ) "> ) )
6043s1cld 11758 . . . . . . . 8  |-  ( ph  ->  <" ( K `
 { X }
) ">  e. Word  C )
61 ccatlen 11746 . . . . . . . 8  |-  ( ( S  e. Word  C  /\  <" ( K `  { X } ) ">  e. Word  C )  ->  ( # `  ( S concat  <" ( K `
 { X }
) "> )
)  =  ( (
# `  S )  +  ( # `  <" ( K `  { X } ) "> ) ) )
622, 60, 61syl2anc 644 . . . . . . 7  |-  ( ph  ->  ( # `  ( S concat  <" ( K `
 { X }
) "> )
)  =  ( (
# `  S )  +  ( # `  <" ( K `  { X } ) "> ) ) )
6359, 62syl5eq 2482 . . . . . 6  |-  ( ph  ->  ( # `  T
)  =  ( (
# `  S )  +  ( # `  <" ( K `  { X } ) "> ) ) )
64 s1len 11760 . . . . . . 7  |-  ( # `  <" ( K `
 { X }
) "> )  =  1
6564oveq2i 6094 . . . . . 6  |-  ( (
# `  S )  +  ( # `  <" ( K `  { X } ) "> ) )  =  ( ( # `  S
)  +  1 )
6663, 65syl6eq 2486 . . . . 5  |-  ( ph  ->  ( # `  T
)  =  ( (
# `  S )  +  1 ) )
6766oveq2d 6099 . . . 4  |-  ( ph  ->  ( 0..^ ( # `  T ) )  =  ( 0..^ ( (
# `  S )  +  1 ) ) )
68 nn0uz 10522 . . . . . 6  |-  NN0  =  ( ZZ>= `  0 )
6953, 68syl6eleq 2528 . . . . 5  |-  ( ph  ->  ( # `  S
)  e.  ( ZZ>= ` 
0 ) )
70 fzosplitsn 11197 . . . . 5  |-  ( (
# `  S )  e.  ( ZZ>= `  0 )  ->  ( 0..^ ( (
# `  S )  +  1 ) )  =  ( ( 0..^ ( # `  S
) )  u.  {
( # `  S ) } ) )
7169, 70syl 16 . . . 4  |-  ( ph  ->  ( 0..^ ( (
# `  S )  +  1 ) )  =  ( ( 0..^ ( # `  S
) )  u.  {
( # `  S ) } ) )
7267, 71eqtrd 2470 . . 3  |-  ( ph  ->  ( 0..^ ( # `  T ) )  =  ( ( 0..^ (
# `  S )
)  u.  { (
# `  S ) } ) )
73 eqid 2438 . . 3  |-  (Cntz `  G )  =  (Cntz `  G )
74 eqid 2438 . . 3  |-  ( 0g
`  G )  =  ( 0g `  G
)
75 pgpfac.4 . . . 4  |-  ( ph  ->  G dom DProd  S )
76 cats1un 11792 . . . . . . . 8  |-  ( ( S  e. Word  C  /\  ( K `  { X } )  e.  C
)  ->  ( S concat  <" ( K `  { X } ) "> )  =  ( S  u.  { <. (
# `  S ) ,  ( K `  { X } ) >. } ) )
772, 43, 76syl2anc 644 . . . . . . 7  |-  ( ph  ->  ( S concat  <" ( K `  { X } ) "> )  =  ( S  u.  { <. ( # `  S
) ,  ( K `
 { X }
) >. } ) )
781, 77syl5eq 2482 . . . . . 6  |-  ( ph  ->  T  =  ( S  u.  { <. ( # `
 S ) ,  ( K `  { X } ) >. } ) )
7978reseq1d 5147 . . . . 5  |-  ( ph  ->  ( T  |`  (
0..^ ( # `  S
) ) )  =  ( ( S  u.  {
<. ( # `  S
) ,  ( K `
 { X }
) >. } )  |`  ( 0..^ ( # `  S
) ) ) )
80 wrdf 11735 . . . . . . 7  |-  ( S  e. Word  C  ->  S : ( 0..^ (
# `  S )
) --> C )
81 ffn 5593 . . . . . . 7  |-  ( S : ( 0..^ (
# `  S )
) --> C  ->  S  Fn  ( 0..^ ( # `  S ) ) )
822, 80, 813syl 19 . . . . . 6  |-  ( ph  ->  S  Fn  ( 0..^ ( # `  S
) ) )
83 fzonel 11154 . . . . . 6  |-  -.  ( # `
 S )  e.  ( 0..^ ( # `  S ) )
84 fsnunres 5936 . . . . . 6  |-  ( ( S  Fn  ( 0..^ ( # `  S
) )  /\  -.  ( # `  S )  e.  ( 0..^ (
# `  S )
) )  ->  (
( S  u.  { <. ( # `  S
) ,  ( K `
 { X }
) >. } )  |`  ( 0..^ ( # `  S
) ) )  =  S )
8582, 83, 84sylancl 645 . . . . 5  |-  ( ph  ->  ( ( S  u.  {
<. ( # `  S
) ,  ( K `
 { X }
) >. } )  |`  ( 0..^ ( # `  S
) ) )  =  S )
8679, 85eqtrd 2470 . . . 4  |-  ( ph  ->  ( T  |`  (
0..^ ( # `  S
) ) )  =  S )
8775, 86breqtrrd 4240 . . 3  |-  ( ph  ->  G dom DProd  ( T  |`  ( 0..^ ( # `  S ) ) ) )
88 fvex 5744 . . . . . 6  |-  ( # `  S )  e.  _V
89 dprdsn 15596 . . . . . 6  |-  ( ( ( # `  S
)  e.  _V  /\  ( K `  { X } )  e.  (SubGrp `  G ) )  -> 
( G dom DProd  { <. (
# `  S ) ,  ( K `  { X } ) >. }  /\  ( G DProd  { <. (
# `  S ) ,  ( K `  { X } ) >. } )  =  ( K `  { X } ) ) )
9088, 21, 89sylancr 646 . . . . 5  |-  ( ph  ->  ( G dom DProd  { <. (
# `  S ) ,  ( K `  { X } ) >. }  /\  ( G DProd  { <. (
# `  S ) ,  ( K `  { X } ) >. } )  =  ( K `  { X } ) ) )
9190simpld 447 . . . 4  |-  ( ph  ->  G dom DProd  { <. ( # `
 S ) ,  ( K `  { X } ) >. } )
92 ffn 5593 . . . . . . 7  |-  ( T : ( 0..^ (
# `  T )
) --> C  ->  T  Fn  ( 0..^ ( # `  T ) ) )
9344, 45, 923syl 19 . . . . . 6  |-  ( ph  ->  T  Fn  ( 0..^ ( # `  T
) ) )
94 ssun2 3513 . . . . . . . 8  |-  { (
# `  S ) }  C_  ( ( 0..^ ( # `  S
) )  u.  {
( # `  S ) } )
9588snss 3928 . . . . . . . 8  |-  ( (
# `  S )  e.  ( ( 0..^ (
# `  S )
)  u.  { (
# `  S ) } )  <->  { ( # `
 S ) } 
C_  ( ( 0..^ ( # `  S
) )  u.  {
( # `  S ) } ) )
9694, 95mpbir 202 . . . . . . 7  |-  ( # `  S )  e.  ( ( 0..^ ( # `  S ) )  u. 
{ ( # `  S
) } )
9796, 72syl5eleqr 2525 . . . . . 6  |-  ( ph  ->  ( # `  S
)  e.  ( 0..^ ( # `  T
) ) )
98 fnressn 5920 . . . . . 6  |-  ( ( T  Fn  ( 0..^ ( # `  T
) )  /\  ( # `
 S )  e.  ( 0..^ ( # `  T ) ) )  ->  ( T  |`  { ( # `  S
) } )  =  { <. ( # `  S
) ,  ( T `
 ( # `  S
) ) >. } )
9993, 97, 98syl2anc 644 . . . . 5  |-  ( ph  ->  ( T  |`  { (
# `  S ) } )  =  { <. ( # `  S
) ,  ( T `
 ( # `  S
) ) >. } )
1001fveq1i 5731 . . . . . . . . 9  |-  ( T `
 ( # `  S
) )  =  ( ( S concat  <" ( K `  { X } ) "> ) `  ( # `  S
) )
10153nn0cnd 10278 . . . . . . . . . . . 12  |-  ( ph  ->  ( # `  S
)  e.  CC )
102101addid2d 9269 . . . . . . . . . . 11  |-  ( ph  ->  ( 0  +  (
# `  S )
)  =  ( # `  S ) )
103102eqcomd 2443 . . . . . . . . . 10  |-  ( ph  ->  ( # `  S
)  =  ( 0  +  ( # `  S
) ) )
104103fveq2d 5734 . . . . . . . . 9  |-  ( ph  ->  ( ( S concat  <" ( K `  { X } ) "> ) `  ( # `  S
) )  =  ( ( S concat  <" ( K `  { X } ) "> ) `  ( 0  +  ( # `  S
) ) ) )
105100, 104syl5eq 2482 . . . . . . . 8  |-  ( ph  ->  ( T `  ( # `
 S ) )  =  ( ( S concat  <" ( K `  { X } ) "> ) `  (
0  +  ( # `  S ) ) ) )
106 1nn 10013 . . . . . . . . . . . 12  |-  1  e.  NN
107106a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  NN )
10864, 107syl5eqel 2522 . . . . . . . . . 10  |-  ( ph  ->  ( # `  <" ( K `  { X } ) "> )  e.  NN )
109 lbfzo0 11172 . . . . . . . . . 10  |-  ( 0  e.  ( 0..^ (
# `  <" ( K `  { X } ) "> ) )  <->  ( # `  <" ( K `  { X } ) "> )  e.  NN )
110108, 109sylibr 205 . . . . . . . . 9  |-  ( ph  ->  0  e.  ( 0..^ ( # `  <" ( K `  { X } ) "> ) ) )
111 ccatval3 11749 . . . . . . . . 9  |-  ( ( S  e. Word  C  /\  <" ( K `  { X } ) ">  e. Word  C  /\  0  e.  ( 0..^ ( # `  <" ( K `  { X } ) "> ) ) )  -> 
( ( S concat  <" ( K `  { X } ) "> ) `  ( 0  +  ( # `  S
) ) )  =  ( <" ( K `  { X } ) "> `  0 ) )
1122, 60, 110, 111syl3anc 1185 . . . . . . . 8  |-  ( ph  ->  ( ( S concat  <" ( K `  { X } ) "> ) `  ( 0  +  ( # `  S
) ) )  =  ( <" ( K `  { X } ) "> `  0 ) )
113 fvex 5744 . . . . . . . . 9  |-  ( K `
 { X }
)  e.  _V
114 s1fv 11762 . . . . . . . . 9  |-  ( ( K `  { X } )  e.  _V  ->  ( <" ( K `  { X } ) "> `  0 )  =  ( K `  { X } ) )
115113, 114mp1i 12 . . . . . . . 8  |-  ( ph  ->  ( <" ( K `  { X } ) "> `  0 )  =  ( K `  { X } ) )
116105, 112, 1153eqtrd 2474 . . . . . . 7  |-  ( ph  ->  ( T `  ( # `
 S ) )  =  ( K `  { X } ) )
117116opeq2d 3993 . . . . . 6  |-  ( ph  -> 
<. ( # `  S
) ,  ( T `
 ( # `  S
) ) >.  =  <. (
# `  S ) ,  ( K `  { X } ) >.
)
118117sneqd 3829 . . . . 5  |-  ( ph  ->  { <. ( # `  S
) ,  ( T `
 ( # `  S
) ) >. }  =  { <. ( # `  S
) ,  ( K `
 { X }
) >. } )
11999, 118eqtrd 2470 . . . 4  |-  ( ph  ->  ( T  |`  { (
# `  S ) } )  =  { <. ( # `  S
) ,  ( K `
 { X }
) >. } )
12091, 119breqtrrd 4240 . . 3  |-  ( ph  ->  G dom DProd  ( T  |` 
{ ( # `  S
) } ) )
121 pgpfac.g . . . 4  |-  ( ph  ->  G  e.  Abel )
122 dprdsubg 15584 . . . . 5  |-  ( G dom DProd  ( T  |`  ( 0..^ ( # `  S
) ) )  -> 
( G DProd  ( T  |`  ( 0..^ ( # `  S ) ) ) )  e.  (SubGrp `  G ) )
12387, 122syl 16 . . . 4  |-  ( ph  ->  ( G DProd  ( T  |`  ( 0..^ ( # `  S ) ) ) )  e.  (SubGrp `  G ) )
124 dprdsubg 15584 . . . . 5  |-  ( G dom DProd  ( T  |`  { ( # `  S
) } )  -> 
( G DProd  ( T  |` 
{ ( # `  S
) } ) )  e.  (SubGrp `  G
) )
125120, 124syl 16 . . . 4  |-  ( ph  ->  ( G DProd  ( T  |`  { ( # `  S
) } ) )  e.  (SubGrp `  G
) )
12673, 121, 123, 125ablcntzd 15474 . . 3  |-  ( ph  ->  ( G DProd  ( T  |`  ( 0..^ ( # `  S ) ) ) )  C_  ( (Cntz `  G ) `  ( G DProd  ( T  |`  { (
# `  S ) } ) ) ) )
127 pgpfac.i . . . 4  |-  ( ph  ->  ( ( K `  { X } )  i^i 
W )  =  {  .0.  } )
12886oveq2d 6099 . . . . . . 7  |-  ( ph  ->  ( G DProd  ( T  |`  ( 0..^ ( # `  S ) ) ) )  =  ( G DProd 
S ) )
129 pgpfac.5 . . . . . . 7  |-  ( ph  ->  ( G DProd  S )  =  W )
130128, 129eqtrd 2470 . . . . . 6  |-  ( ph  ->  ( G DProd  ( T  |`  ( 0..^ ( # `  S ) ) ) )  =  W )
131119oveq2d 6099 . . . . . . 7  |-  ( ph  ->  ( G DProd  ( T  |`  { ( # `  S
) } ) )  =  ( G DProd  { <. (
# `  S ) ,  ( K `  { X } ) >. } ) )
13290simprd 451 . . . . . . 7  |-  ( ph  ->  ( G DProd  { <. (
# `  S ) ,  ( K `  { X } ) >. } )  =  ( K `  { X } ) )
133131, 132eqtrd 2470 . . . . . 6  |-  ( ph  ->  ( G DProd  ( T  |`  { ( # `  S
) } ) )  =  ( K `  { X } ) )
134130, 133ineq12d 3545 . . . . 5  |-  ( ph  ->  ( ( G DProd  ( T  |`  ( 0..^ (
# `  S )
) ) )  i^i  ( G DProd  ( T  |`  { ( # `  S
) } ) ) )  =  ( W  i^i  ( K `  { X } ) ) )
135 incom 3535 . . . . 5  |-  ( W  i^i  ( K `  { X } ) )  =  ( ( K `
 { X }
)  i^i  W )
136134, 135syl6eq 2486 . . . 4  |-  ( ph  ->  ( ( G DProd  ( T  |`  ( 0..^ (
# `  S )
) ) )  i^i  ( G DProd  ( T  |`  { ( # `  S
) } ) ) )  =  ( ( K `  { X } )  i^i  W
) )
1374, 74subg0 14952 . . . . . . 7  |-  ( U  e.  (SubGrp `  G
)  ->  ( 0g `  G )  =  ( 0g `  H ) )
1383, 137syl 16 . . . . . 6  |-  ( ph  ->  ( 0g `  G
)  =  ( 0g
`  H ) )
139 pgpfac.0 . . . . . 6  |-  .0.  =  ( 0g `  H )
140138, 139syl6eqr 2488 . . . . 5  |-  ( ph  ->  ( 0g `  G
)  =  .0.  )
141140sneqd 3829 . . . 4  |-  ( ph  ->  { ( 0g `  G ) }  =  {  .0.  } )
142127, 136, 1413eqtr4d 2480 . . 3  |-  ( ph  ->  ( ( G DProd  ( T  |`  ( 0..^ (
# `  S )
) ) )  i^i  ( G DProd  ( T  |`  { ( # `  S
) } ) ) )  =  { ( 0g `  G ) } )
14350, 58, 72, 73, 74, 87, 120, 126, 142dmdprdsplit2 15606 . 2  |-  ( ph  ->  G dom DProd  T )
144 eqid 2438 . . . . 5  |-  ( LSSum `  G )  =  (
LSSum `  G )
14550, 58, 72, 144, 143dprdsplit 15608 . . . 4  |-  ( ph  ->  ( G DProd  T )  =  ( ( G DProd 
( T  |`  (
0..^ ( # `  S
) ) ) ) ( LSSum `  G )
( G DProd  ( T  |` 
{ ( # `  S
) } ) ) ) )
146130, 133oveq12d 6101 . . . 4  |-  ( ph  ->  ( ( G DProd  ( T  |`  ( 0..^ (
# `  S )
) ) ) (
LSSum `  G ) ( G DProd  ( T  |`  { ( # `  S
) } ) ) )  =  ( W ( LSSum `  G )
( K `  { X } ) ) )
147130, 123eqeltrrd 2513 . . . . 5  |-  ( ph  ->  W  e.  (SubGrp `  G ) )
148144lsmcom 15475 . . . . 5  |-  ( ( G  e.  Abel  /\  W  e.  (SubGrp `  G )  /\  ( K `  { X } )  e.  (SubGrp `  G ) )  -> 
( W ( LSSum `  G ) ( K `
 { X }
) )  =  ( ( K `  { X } ) ( LSSum `  G ) W ) )
149121, 147, 21, 148syl3anc 1185 . . . 4  |-  ( ph  ->  ( W ( LSSum `  G ) ( K `
 { X }
) )  =  ( ( K `  { X } ) ( LSSum `  G ) W ) )
150145, 146, 1493eqtrd 2474 . . 3  |-  ( ph  ->  ( G DProd  T )  =  ( ( K `
 { X }
) ( LSSum `  G
) W ) )
151 pgpfac.w . . . . . 6  |-  ( ph  ->  W  e.  (SubGrp `  H ) )
1527subgss 14947 . . . . . 6  |-  ( W  e.  (SubGrp `  H
)  ->  W  C_  ( Base `  H ) )
153151, 152syl 16 . . . . 5  |-  ( ph  ->  W  C_  ( Base `  H ) )
154153, 13sseqtr4d 3387 . . . 4  |-  ( ph  ->  W  C_  U )
155 pgpfac.l . . . . 5  |-  .(+)  =  (
LSSum `  H )
1564, 144, 155subglsm 15307 . . . 4  |-  ( ( U  e.  (SubGrp `  G )  /\  ( K `  { X } )  C_  U  /\  W  C_  U )  ->  ( ( K `
 { X }
) ( LSSum `  G
) W )  =  ( ( K `  { X } )  .(+)  W ) )
1573, 23, 154, 156syl3anc 1185 . . 3  |-  ( ph  ->  ( ( K `  { X } ) (
LSSum `  G ) W )  =  ( ( K `  { X } )  .(+)  W ) )
158 pgpfac.s . . 3  |-  ( ph  ->  ( ( K `  { X } )  .(+)  W )  =  U )
159150, 157, 1583eqtrd 2474 . 2  |-  ( ph  ->  ( G DProd  T )  =  U )
160 breq2 4218 . . . 4  |-  ( s  =  T  ->  ( G dom DProd  s  <->  G dom DProd  T ) )
161 oveq2 6091 . . . . 5  |-  ( s  =  T  ->  ( G DProd  s )  =  ( G DProd  T ) )
162161eqeq1d 2446 . . . 4  |-  ( s  =  T  ->  (
( G DProd  s )  =  U  <->  ( G DProd  T
)  =  U ) )
163160, 162anbi12d 693 . . 3  |-  ( s  =  T  ->  (
( G dom DProd  s  /\  ( G DProd  s )  =  U )  <->  ( G dom DProd  T  /\  ( G DProd 
T )  =  U ) ) )
164163rspcev 3054 . 2  |-  ( ( T  e. Word  C  /\  ( G dom DProd  T  /\  ( G DProd  T )  =  U ) )  ->  E. s  e. Word  C ( G dom DProd  s  /\  ( G DProd  s )  =  U ) )
16544, 143, 159, 164syl12anc 1183 1  |-  ( ph  ->  E. s  e. Word  C
( G dom DProd  s  /\  ( G DProd  s )  =  U ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726    =/= wne 2601   A.wral 2707   E.wrex 2708   {crab 2711   _Vcvv 2958    u. cun 3320    i^i cin 3321    C_ wss 3322    C. wpss 3323   (/)c0 3630   {csn 3816   <.cop 3819   class class class wbr 4214   dom cdm 4880   ran crn 4881    |` cres 4882    Fn wfn 5451   -->wf 5452   ` cfv 5456  (class class class)co 6083   Fincfn 7111   0cc0 8992   1c1 8993    + caddc 8995   NNcn 10002   NN0cn0 10223   ZZcz 10284   ZZ>=cuz 10490  ..^cfzo 11137   #chash 11620  Word cword 11719   concat cconcat 11720   <"cs1 11721   Primecprime 13081   Basecbs 13471   ↾s cress 13472   0gc0g 13725  Moorecmre 13809  mrClscmrc 13810  ACScacs 13812   Grpcgrp 14687  SubGrpcsubg 14940  Cntzccntz 15116   odcod 15165  gExcgex 15166   pGrp cpgp 15167   LSSumclsm 15270   Abelcabel 15415  CycGrpccyg 15489   DProd cdprd 15556
This theorem is referenced by:  pgpfaclem2  15642
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4322  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-inf2 7598  ax-cnex 9048  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-mulcom 9056  ax-addass 9057  ax-mulass 9058  ax-distr 9059  ax-i2m1 9060  ax-1ne0 9061  ax-1rid 9062  ax-rnegex 9063  ax-rrecex 9064  ax-cnre 9065  ax-pre-lttri 9066  ax-pre-lttrn 9067  ax-pre-ltadd 9068  ax-pre-mulgt0 9069
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-iin 4098  df-br 4215  df-opab 4269  df-mpt 4270  df-tr 4305  df-eprel 4496  df-id 4500  df-po 4505  df-so 4506  df-fr 4543  df-se 4544  df-we 4545  df-ord 4586  df-on 4587  df-lim 4588  df-suc 4589  df-om 4848  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-isom 5465  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-of 6307  df-1st 6351  df-2nd 6352  df-tpos 6481  df-riota 6551  df-recs 6635  df-rdg 6670  df-1o 6726  df-oadd 6730  df-er 6907  df-map 7022  df-ixp 7066  df-en 7112  df-dom 7113  df-sdom 7114  df-fin 7115  df-sup 7448  df-oi 7481  df-card 7828  df-pnf 9124  df-mnf 9125  df-xr 9126  df-ltxr 9127  df-le 9128  df-sub 9295  df-neg 9296  df-nn 10003  df-2 10060  df-n0 10224  df-z 10285  df-uz 10491  df-fz 11046  df-fzo 11138  df-seq 11326  df-hash 11621  df-word 11725  df-concat 11726  df-s1 11727  df-ndx 13474  df-slot 13475  df-base 13476  df-sets 13477  df-ress 13478  df-plusg 13544  df-0g 13729  df-gsum 13730  df-mre 13813  df-mrc 13814  df-acs 13816  df-mnd 14692  df-mhm 14740  df-submnd 14741  df-grp 14814  df-minusg 14815  df-sbg 14816  df-mulg 14817  df-subg 14943  df-ghm 15006  df-gim 15048  df-cntz 15118  df-oppg 15144  df-od 15169  df-pgp 15171  df-lsm 15272  df-cmn 15416  df-abl 15417  df-cyg 15490  df-dprd 15558
  Copyright terms: Public domain W3C validator