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

Theorem ablfac1b 17708
Description: Any abelian group is the direct product of factors of prime power order (with the exact order further matching the prime factorization of the group order). (Contributed by Mario Carneiro, 21-Apr-2016.)
Hypotheses
Ref Expression
ablfac1.b  |-  B  =  ( Base `  G
)
ablfac1.o  |-  O  =  ( od `  G
)
ablfac1.s  |-  S  =  ( p  e.  A  |->  { x  e.  B  |  ( O `  x )  ||  (
p ^ ( p 
pCnt  ( # `  B
) ) ) } )
ablfac1.g  |-  ( ph  ->  G  e.  Abel )
ablfac1.f  |-  ( ph  ->  B  e.  Fin )
ablfac1.1  |-  ( ph  ->  A  C_  Prime )
Assertion
Ref Expression
ablfac1b  |-  ( ph  ->  G dom DProd  S )
Distinct variable groups:    x, p, B    ph, p, x    A, p, x    O, p, x    G, p, x
Allowed substitution hints:    S( x, p)

Proof of Theorem ablfac1b
Dummy variables  a 
b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2423 . 2  |-  (Cntz `  G )  =  (Cntz `  G )
2 eqid 2423 . 2  |-  ( 0g
`  G )  =  ( 0g `  G
)
3 eqid 2423 . 2  |-  (mrCls `  (SubGrp `  G ) )  =  (mrCls `  (SubGrp `  G ) )
4 ablfac1.g . . 3  |-  ( ph  ->  G  e.  Abel )
5 ablgrp 17440 . . 3  |-  ( G  e.  Abel  ->  G  e. 
Grp )
64, 5syl 17 . 2  |-  ( ph  ->  G  e.  Grp )
7 ablfac1.1 . . 3  |-  ( ph  ->  A  C_  Prime )
8 nnex 10628 . . . . 5  |-  NN  e.  _V
9 prmnn 14630 . . . . . 6  |-  ( p  e.  Prime  ->  p  e.  NN )
109ssriv 3474 . . . . 5  |-  Prime  C_  NN
118, 10ssexi 4575 . . . 4  |-  Prime  e.  _V
1211ssex 4574 . . 3  |-  ( A 
C_  Prime  ->  A  e.  _V )
137, 12syl 17 . 2  |-  ( ph  ->  A  e.  _V )
144adantr 467 . . . 4  |-  ( (
ph  /\  p  e.  A )  ->  G  e.  Abel )
157sselda 3470 . . . . . . 7  |-  ( (
ph  /\  p  e.  A )  ->  p  e.  Prime )
1615, 9syl 17 . . . . . 6  |-  ( (
ph  /\  p  e.  A )  ->  p  e.  NN )
17 ablfac1.b . . . . . . . . . . 11  |-  B  =  ( Base `  G
)
1817grpbn0 16700 . . . . . . . . . 10  |-  ( G  e.  Grp  ->  B  =/=  (/) )
196, 18syl 17 . . . . . . . . 9  |-  ( ph  ->  B  =/=  (/) )
20 ablfac1.f . . . . . . . . . 10  |-  ( ph  ->  B  e.  Fin )
21 hashnncl 12559 . . . . . . . . . 10  |-  ( B  e.  Fin  ->  (
( # `  B )  e.  NN  <->  B  =/=  (/) ) )
2220, 21syl 17 . . . . . . . . 9  |-  ( ph  ->  ( ( # `  B
)  e.  NN  <->  B  =/=  (/) ) )
2319, 22mpbird 236 . . . . . . . 8  |-  ( ph  ->  ( # `  B
)  e.  NN )
2423adantr 467 . . . . . . 7  |-  ( (
ph  /\  p  e.  A )  ->  ( # `
 B )  e.  NN )
2515, 24pccld 14805 . . . . . 6  |-  ( (
ph  /\  p  e.  A )  ->  (
p  pCnt  ( # `  B
) )  e.  NN0 )
2616, 25nnexpcld 12449 . . . . 5  |-  ( (
ph  /\  p  e.  A )  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  e.  NN )
2726nnzd 11052 . . . 4  |-  ( (
ph  /\  p  e.  A )  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  e.  ZZ )
28 ablfac1.o . . . . 5  |-  O  =  ( od `  G
)
2928, 17oddvdssubg 17498 . . . 4  |-  ( ( G  e.  Abel  /\  (
p ^ ( p 
pCnt  ( # `  B
) ) )  e.  ZZ )  ->  { x  e.  B  |  ( O `  x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) }  e.  (SubGrp `  G
) )
3014, 27, 29syl2anc 666 . . 3  |-  ( (
ph  /\  p  e.  A )  ->  { x  e.  B  |  ( O `  x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) }  e.  (SubGrp `  G
) )
31 ablfac1.s . . 3  |-  S  =  ( p  e.  A  |->  { x  e.  B  |  ( O `  x )  ||  (
p ^ ( p 
pCnt  ( # `  B
) ) ) } )
3230, 31fmptd 6067 . 2  |-  ( ph  ->  S : A --> (SubGrp `  G ) )
334adantr 467 . . 3  |-  ( (
ph  /\  ( a  e.  A  /\  b  e.  A  /\  a  =/=  b ) )  ->  G  e.  Abel )
3432adantr 467 . . . 4  |-  ( (
ph  /\  ( a  e.  A  /\  b  e.  A  /\  a  =/=  b ) )  ->  S : A --> (SubGrp `  G ) )
35 simpr1 1012 . . . 4  |-  ( (
ph  /\  ( a  e.  A  /\  b  e.  A  /\  a  =/=  b ) )  -> 
a  e.  A )
3634, 35ffvelrnd 6044 . . 3  |-  ( (
ph  /\  ( a  e.  A  /\  b  e.  A  /\  a  =/=  b ) )  -> 
( S `  a
)  e.  (SubGrp `  G ) )
37 simpr2 1013 . . . 4  |-  ( (
ph  /\  ( a  e.  A  /\  b  e.  A  /\  a  =/=  b ) )  -> 
b  e.  A )
3834, 37ffvelrnd 6044 . . 3  |-  ( (
ph  /\  ( a  e.  A  /\  b  e.  A  /\  a  =/=  b ) )  -> 
( S `  b
)  e.  (SubGrp `  G ) )
391, 33, 36, 38ablcntzd 17500 . 2  |-  ( (
ph  /\  ( a  e.  A  /\  b  e.  A  /\  a  =/=  b ) )  -> 
( S `  a
)  C_  ( (Cntz `  G ) `  ( S `  b )
) )
40 id 23 . . . . . . . . . 10  |-  ( p  =  a  ->  p  =  a )
41 oveq1 6318 . . . . . . . . . 10  |-  ( p  =  a  ->  (
p  pCnt  ( # `  B
) )  =  ( a  pCnt  ( # `  B
) ) )
4240, 41oveq12d 6329 . . . . . . . . 9  |-  ( p  =  a  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  =  ( a ^ (
a  pCnt  ( # `  B
) ) ) )
4342breq2d 4441 . . . . . . . 8  |-  ( p  =  a  ->  (
( O `  x
)  ||  ( p ^ ( p  pCnt  (
# `  B )
) )  <->  ( O `  x )  ||  (
a ^ ( a 
pCnt  ( # `  B
) ) ) ) )
4443rabbidv 3076 . . . . . . 7  |-  ( p  =  a  ->  { x  e.  B  |  ( O `  x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) }  =  { x  e.  B  |  ( O `
 x )  ||  ( a ^ (
a  pCnt  ( # `  B
) ) ) } )
45 fvex 5897 . . . . . . . . 9  |-  ( Base `  G )  e.  _V
4617, 45eqeltri 2508 . . . . . . . 8  |-  B  e. 
_V
4746rabex 4581 . . . . . . 7  |-  { x  e.  B  |  ( O `  x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) }  e.  _V
4844, 31, 47fvmpt3i 5975 . . . . . 6  |-  ( a  e.  A  ->  ( S `  a )  =  { x  e.  B  |  ( O `  x )  ||  (
a ^ ( a 
pCnt  ( # `  B
) ) ) } )
4948adantl 468 . . . . 5  |-  ( (
ph  /\  a  e.  A )  ->  ( S `  a )  =  { x  e.  B  |  ( O `  x )  ||  (
a ^ ( a 
pCnt  ( # `  B
) ) ) } )
50 eqimss 3522 . . . . 5  |-  ( ( S `  a )  =  { x  e.  B  |  ( O `
 x )  ||  ( a ^ (
a  pCnt  ( # `  B
) ) ) }  ->  ( S `  a )  C_  { x  e.  B  |  ( O `  x )  ||  ( a ^ (
a  pCnt  ( # `  B
) ) ) } )
5149, 50syl 17 . . . 4  |-  ( (
ph  /\  a  e.  A )  ->  ( S `  a )  C_ 
{ x  e.  B  |  ( O `  x )  ||  (
a ^ ( a 
pCnt  ( # `  B
) ) ) } )
524adantr 467 . . . . . 6  |-  ( (
ph  /\  a  e.  A )  ->  G  e.  Abel )
53 eqid 2423 . . . . . . 7  |-  ( Base `  G )  =  (
Base `  G )
5453subgacs 16857 . . . . . 6  |-  ( G  e.  Grp  ->  (SubGrp `  G )  e.  (ACS
`  ( Base `  G
) ) )
55 acsmre 15563 . . . . . 6  |-  ( (SubGrp `  G )  e.  (ACS
`  ( Base `  G
) )  ->  (SubGrp `  G )  e.  (Moore `  ( Base `  G
) ) )
5652, 5, 54, 554syl 19 . . . . 5  |-  ( (
ph  /\  a  e.  A )  ->  (SubGrp `  G )  e.  (Moore `  ( Base `  G
) ) )
57 df-ima 4872 . . . . . . 7  |-  ( S
" ( A  \  { a } ) )  =  ran  ( S  |`  ( A  \  { a } ) )
587sselda 3470 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  a  e.  A )  ->  a  e.  Prime )
5958ad2antrr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  a  e.  Prime )
6023ad3antrrr 735 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  ( # `
 B )  e.  NN )
61 pcdvds 14818 . . . . . . . . . . . . . . . 16  |-  ( ( a  e.  Prime  /\  ( # `
 B )  e.  NN )  ->  (
a ^ ( a 
pCnt  ( # `  B
) ) )  ||  ( # `  B ) )
6259, 60, 61syl2anc 666 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
a ^ ( a 
pCnt  ( # `  B
) ) )  ||  ( # `  B ) )
637ad3antrrr 735 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  A  C_ 
Prime )
64 eldifi 3593 . . . . . . . . . . . . . . . . . 18  |-  ( p  e.  ( A  \  { a } )  ->  p  e.  A
)
6564ad2antlr 732 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  p  e.  A )
6663, 65sseldd 3471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  p  e.  Prime )
67 pcdvds 14818 . . . . . . . . . . . . . . . 16  |-  ( ( p  e.  Prime  /\  ( # `
 B )  e.  NN )  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  ||  ( # `  B ) )
6866, 60, 67syl2anc 666 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  ||  ( # `  B ) )
69 eqid 2423 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a ^ ( a  pCnt  (
# `  B )
) )  =  ( a ^ ( a 
pCnt  ( # `  B
) ) )
70 eqid 2423 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
# `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  =  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) )
7117, 28, 31, 4, 20, 7, 69, 70ablfac1lem 17706 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  a  e.  A )  ->  (
( ( a ^
( a  pCnt  ( # `
 B ) ) )  e.  NN  /\  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) )  e.  NN )  /\  (
( a ^ (
a  pCnt  ( # `  B
) ) )  gcd  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) )  =  1  /\  ( # `
 B )  =  ( ( a ^
( a  pCnt  ( # `
 B ) ) )  x.  ( (
# `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) ) ) )
7271simp1d 1018 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  a  e.  A )  ->  (
( a ^ (
a  pCnt  ( # `  B
) ) )  e.  NN  /\  ( (
# `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  e.  NN ) )
7372simpld 461 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  a  e.  A )  ->  (
a ^ ( a 
pCnt  ( # `  B
) ) )  e.  NN )
7473ad2antrr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
a ^ ( a 
pCnt  ( # `  B
) ) )  e.  NN )
7574nnzd 11052 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
a ^ ( a 
pCnt  ( # `  B
) ) )  e.  ZZ )
7666, 9syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  p  e.  NN )
7766, 60pccld 14805 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
p  pCnt  ( # `  B
) )  e.  NN0 )
7876, 77nnexpcld 12449 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  e.  NN )
7978nnzd 11052 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  e.  ZZ )
8060nnzd 11052 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  ( # `
 B )  e.  ZZ )
81 eldifsni 4132 . . . . . . . . . . . . . . . . . . . 20  |-  ( p  e.  ( A  \  { a } )  ->  p  =/=  a
)
8281ad2antlr 732 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  p  =/=  a )
8382necomd 2696 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  a  =/=  p )
84 prmrp 14663 . . . . . . . . . . . . . . . . . . 19  |-  ( ( a  e.  Prime  /\  p  e.  Prime )  ->  (
( a  gcd  p
)  =  1  <->  a  =/=  p ) )
8559, 66, 84syl2anc 666 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( a  gcd  p
)  =  1  <->  a  =/=  p ) )
8683, 85mpbird 236 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
a  gcd  p )  =  1 )
87 prmz 14631 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  Prime  ->  a  e.  ZZ )
8859, 87syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  a  e.  ZZ )
89 prmz 14631 . . . . . . . . . . . . . . . . . . 19  |-  ( p  e.  Prime  ->  p  e.  ZZ )
9066, 89syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  p  e.  ZZ )
9159, 60pccld 14805 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
a  pCnt  ( # `  B
) )  e.  NN0 )
92 rpexp12i 14679 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  ZZ  /\  p  e.  ZZ  /\  (
( a  pCnt  ( # `
 B ) )  e.  NN0  /\  (
p  pCnt  ( # `  B
) )  e.  NN0 ) )  ->  (
( a  gcd  p
)  =  1  -> 
( ( a ^
( a  pCnt  ( # `
 B ) ) )  gcd  ( p ^ ( p  pCnt  (
# `  B )
) ) )  =  1 ) )
9388, 90, 91, 77, 92syl112anc 1269 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( a  gcd  p
)  =  1  -> 
( ( a ^
( a  pCnt  ( # `
 B ) ) )  gcd  ( p ^ ( p  pCnt  (
# `  B )
) ) )  =  1 ) )
9486, 93mpd 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( a ^ (
a  pCnt  ( # `  B
) ) )  gcd  ( p ^ (
p  pCnt  ( # `  B
) ) ) )  =  1 )
95 coprmdvds2 14665 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( a ^
( a  pCnt  ( # `
 B ) ) )  e.  ZZ  /\  ( p ^ (
p  pCnt  ( # `  B
) ) )  e.  ZZ  /\  ( # `  B )  e.  ZZ )  /\  ( ( a ^ ( a  pCnt  (
# `  B )
) )  gcd  (
p ^ ( p 
pCnt  ( # `  B
) ) ) )  =  1 )  -> 
( ( ( a ^ ( a  pCnt  (
# `  B )
) )  ||  ( # `
 B )  /\  ( p ^ (
p  pCnt  ( # `  B
) ) )  ||  ( # `  B ) )  ->  ( (
a ^ ( a 
pCnt  ( # `  B
) ) )  x.  ( p ^ (
p  pCnt  ( # `  B
) ) ) ) 
||  ( # `  B
) ) )
9675, 79, 80, 94, 95syl31anc 1268 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( ( a ^
( a  pCnt  ( # `
 B ) ) )  ||  ( # `  B )  /\  (
p ^ ( p 
pCnt  ( # `  B
) ) )  ||  ( # `  B ) )  ->  ( (
a ^ ( a 
pCnt  ( # `  B
) ) )  x.  ( p ^ (
p  pCnt  ( # `  B
) ) ) ) 
||  ( # `  B
) ) )
9762, 68, 96mp2and 684 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( a ^ (
a  pCnt  ( # `  B
) ) )  x.  ( p ^ (
p  pCnt  ( # `  B
) ) ) ) 
||  ( # `  B
) )
9871simp3d 1020 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  a  e.  A )  ->  ( # `
 B )  =  ( ( a ^
( a  pCnt  ( # `
 B ) ) )  x.  ( (
# `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) ) )
9998ad2antrr 731 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  ( # `
 B )  =  ( ( a ^
( a  pCnt  ( # `
 B ) ) )  x.  ( (
# `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) ) )
10097, 99breqtrd 4454 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( a ^ (
a  pCnt  ( # `  B
) ) )  x.  ( p ^ (
p  pCnt  ( # `  B
) ) ) ) 
||  ( ( a ^ ( a  pCnt  (
# `  B )
) )  x.  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) ) )
10172simprd 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  a  e.  A )  ->  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  e.  NN )
102101ad2antrr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  e.  NN )
103102nnzd 11052 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  e.  ZZ )
10474nnne0d 10667 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
a ^ ( a 
pCnt  ( # `  B
) ) )  =/=  0 )
105 dvdscmulr 14336 . . . . . . . . . . . . . 14  |-  ( ( ( p ^ (
p  pCnt  ( # `  B
) ) )  e.  ZZ  /\  ( (
# `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  e.  ZZ  /\  ( ( a ^
( a  pCnt  ( # `
 B ) ) )  e.  ZZ  /\  ( a ^ (
a  pCnt  ( # `  B
) ) )  =/=  0 ) )  -> 
( ( ( a ^ ( a  pCnt  (
# `  B )
) )  x.  (
p ^ ( p 
pCnt  ( # `  B
) ) ) ) 
||  ( ( a ^ ( a  pCnt  (
# `  B )
) )  x.  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) )  <->  ( p ^ ( p  pCnt  (
# `  B )
) )  ||  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) ) )
10679, 103, 75, 104, 105syl112anc 1269 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( ( a ^
( a  pCnt  ( # `
 B ) ) )  x.  ( p ^ ( p  pCnt  (
# `  B )
) ) )  ||  ( ( a ^
( a  pCnt  ( # `
 B ) ) )  x.  ( (
# `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) )  <->  ( p ^ ( p  pCnt  (
# `  B )
) )  ||  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) ) )
107100, 106mpbid 214 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) )
10817, 28odcl 17190 . . . . . . . . . . . . . . 15  |-  ( x  e.  B  ->  ( O `  x )  e.  NN0 )
109108adantl 468 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  ( O `  x )  e.  NN0 )
110109nn0zd 11051 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  ( O `  x )  e.  ZZ )
111 dvdstr 14342 . . . . . . . . . . . . 13  |-  ( ( ( O `  x
)  e.  ZZ  /\  ( p ^ (
p  pCnt  ( # `  B
) ) )  e.  ZZ  /\  ( (
# `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  e.  ZZ )  ->  ( ( ( O `  x ) 
||  ( p ^
( p  pCnt  ( # `
 B ) ) )  /\  ( p ^ ( p  pCnt  (
# `  B )
) )  ||  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) )  -> 
( O `  x
)  ||  ( ( # `
 B )  / 
( a ^ (
a  pCnt  ( # `  B
) ) ) ) ) )
112110, 79, 103, 111syl3anc 1265 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( ( O `  x )  ||  (
p ^ ( p 
pCnt  ( # `  B
) ) )  /\  ( p ^ (
p  pCnt  ( # `  B
) ) )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) )  ->  ( O `  x )  ||  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) ) )
113107, 112mpan2d 679 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( O `  x
)  ||  ( p ^ ( p  pCnt  (
# `  B )
) )  ->  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) ) )
114113ss2rabdv 3548 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  {
a } ) )  ->  { x  e.  B  |  ( O `
 x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) } 
C_  { x  e.  B  |  ( O `
 x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } )
11547elpw 3993 . . . . . . . . . 10  |-  ( { x  e.  B  | 
( O `  x
)  ||  ( p ^ ( p  pCnt  (
# `  B )
) ) }  e.  ~P { x  e.  B  |  ( O `  x )  ||  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) }  <->  { x  e.  B  |  ( O `  x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) } 
C_  { x  e.  B  |  ( O `
 x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } )
116114, 115sylibr 216 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  {
a } ) )  ->  { x  e.  B  |  ( O `
 x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) }  e.  ~P { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } )
11731reseq1i 5126 . . . . . . . . . 10  |-  ( S  |`  ( A  \  {
a } ) )  =  ( ( p  e.  A  |->  { x  e.  B  |  ( O `  x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) } )  |`  ( A  \  { a } ) )
118 difss 3598 . . . . . . . . . . 11  |-  ( A 
\  { a } )  C_  A
119 resmpt 5179 . . . . . . . . . . 11  |-  ( ( A  \  { a } )  C_  A  ->  ( ( p  e.  A  |->  { x  e.  B  |  ( O `
 x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) } )  |`  ( A  \  { a } ) )  =  ( p  e.  ( A  \  { a } ) 
|->  { x  e.  B  |  ( O `  x )  ||  (
p ^ ( p 
pCnt  ( # `  B
) ) ) } ) )
120118, 119ax-mp 5 . . . . . . . . . 10  |-  ( ( p  e.  A  |->  { x  e.  B  | 
( O `  x
)  ||  ( p ^ ( p  pCnt  (
# `  B )
) ) } )  |`  ( A  \  {
a } ) )  =  ( p  e.  ( A  \  {
a } )  |->  { x  e.  B  | 
( O `  x
)  ||  ( p ^ ( p  pCnt  (
# `  B )
) ) } )
121117, 120eqtri 2452 . . . . . . . . 9  |-  ( S  |`  ( A  \  {
a } ) )  =  ( p  e.  ( A  \  {
a } )  |->  { x  e.  B  | 
( O `  x
)  ||  ( p ^ ( p  pCnt  (
# `  B )
) ) } )
122116, 121fmptd 6067 . . . . . . . 8  |-  ( (
ph  /\  a  e.  A )  ->  ( S  |`  ( A  \  { a } ) ) : ( A 
\  { a } ) --> ~P { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } )
123 frn 5758 . . . . . . . 8  |-  ( ( S  |`  ( A  \  { a } ) ) : ( A 
\  { a } ) --> ~P { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) }  ->  ran  ( S  |`  ( A  \  {
a } ) ) 
C_  ~P { x  e.  B  |  ( O `
 x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } )
124122, 123syl 17 . . . . . . 7  |-  ( (
ph  /\  a  e.  A )  ->  ran  ( S  |`  ( A 
\  { a } ) )  C_  ~P { x  e.  B  |  ( O `  x )  ||  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) } )
12557, 124syl5eqss 3514 . . . . . 6  |-  ( (
ph  /\  a  e.  A )  ->  ( S " ( A  \  { a } ) )  C_  ~P { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } )
126 sspwuni 4394 . . . . . 6  |-  ( ( S " ( A 
\  { a } ) )  C_  ~P { x  e.  B  |  ( O `  x )  ||  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) }  <->  U. ( S " ( A  \  { a } ) )  C_  { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } )
127125, 126sylib 200 . . . . 5  |-  ( (
ph  /\  a  e.  A )  ->  U. ( S " ( A  \  { a } ) )  C_  { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } )
128101nnzd 11052 . . . . . 6  |-  ( (
ph  /\  a  e.  A )  ->  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  e.  ZZ )
12928, 17oddvdssubg 17498 . . . . . 6  |-  ( ( G  e.  Abel  /\  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  e.  ZZ )  ->  { x  e.  B  |  ( O `
 x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) }  e.  (SubGrp `  G
) )
13052, 128, 129syl2anc 666 . . . . 5  |-  ( (
ph  /\  a  e.  A )  ->  { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) }  e.  (SubGrp `  G
) )
1313mrcsscl 15531 . . . . 5  |-  ( ( (SubGrp `  G )  e.  (Moore `  ( Base `  G ) )  /\  U. ( S " ( A  \  { a } ) )  C_  { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) }  /\  { x  e.  B  |  ( O `
 x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) }  e.  (SubGrp `  G
) )  ->  (
(mrCls `  (SubGrp `  G
) ) `  U. ( S " ( A 
\  { a } ) ) )  C_  { x  e.  B  | 
( O `  x
)  ||  ( ( # `
 B )  / 
( a ^ (
a  pCnt  ( # `  B
) ) ) ) } )
13256, 127, 130, 131syl3anc 1265 . . . 4  |-  ( (
ph  /\  a  e.  A )  ->  (
(mrCls `  (SubGrp `  G
) ) `  U. ( S " ( A 
\  { a } ) ) )  C_  { x  e.  B  | 
( O `  x
)  ||  ( ( # `
 B )  / 
( a ^ (
a  pCnt  ( # `  B
) ) ) ) } )
133 ss2in 3695 . . . 4  |-  ( ( ( S `  a
)  C_  { x  e.  B  |  ( O `  x )  ||  ( a ^ (
a  pCnt  ( # `  B
) ) ) }  /\  ( (mrCls `  (SubGrp `  G ) ) `
 U. ( S
" ( A  \  { a } ) ) )  C_  { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } )  ->  ( ( S `  a )  i^i  ( (mrCls `  (SubGrp `  G ) ) `  U. ( S " ( A  \  { a } ) ) ) ) 
C_  ( { x  e.  B  |  ( O `  x )  ||  ( a ^ (
a  pCnt  ( # `  B
) ) ) }  i^i  { x  e.  B  |  ( O `
 x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } ) )
13451, 132, 133syl2anc 666 . . 3  |-  ( (
ph  /\  a  e.  A )  ->  (
( S `  a
)  i^i  ( (mrCls `  (SubGrp `  G )
) `  U. ( S
" ( A  \  { a } ) ) ) )  C_  ( { x  e.  B  |  ( O `  x )  ||  (
a ^ ( a 
pCnt  ( # `  B
) ) ) }  i^i  { x  e.  B  |  ( O `
 x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } ) )
135 eqid 2423 . . . . 5  |-  { x  e.  B  |  ( O `  x )  ||  ( a ^ (
a  pCnt  ( # `  B
) ) ) }  =  { x  e.  B  |  ( O `
 x )  ||  ( a ^ (
a  pCnt  ( # `  B
) ) ) }
136 eqid 2423 . . . . 5  |-  { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) }  =  { x  e.  B  |  ( O `
 x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) }
13771simp2d 1019 . . . . 5  |-  ( (
ph  /\  a  e.  A )  ->  (
( a ^ (
a  pCnt  ( # `  B
) ) )  gcd  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) )  =  1 )
138 eqid 2423 . . . . 5  |-  ( LSSum `  G )  =  (
LSSum `  G )
13917, 28, 135, 136, 52, 73, 101, 137, 98, 2, 138ablfacrp 17704 . . . 4  |-  ( (
ph  /\  a  e.  A )  ->  (
( { x  e.  B  |  ( O `
 x )  ||  ( a ^ (
a  pCnt  ( # `  B
) ) ) }  i^i  { x  e.  B  |  ( O `
 x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } )  =  { ( 0g `  G ) }  /\  ( { x  e.  B  | 
( O `  x
)  ||  ( a ^ ( a  pCnt  (
# `  B )
) ) }  ( LSSum `  G ) { x  e.  B  | 
( O `  x
)  ||  ( ( # `
 B )  / 
( a ^ (
a  pCnt  ( # `  B
) ) ) ) } )  =  B ) )
140139simpld 461 . . 3  |-  ( (
ph  /\  a  e.  A )  ->  ( { x  e.  B  |  ( O `  x )  ||  (
a ^ ( a 
pCnt  ( # `  B
) ) ) }  i^i  { x  e.  B  |  ( O `
 x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } )  =  { ( 0g `  G ) } )
141134, 140sseqtrd 3506 . 2  |-  ( (
ph  /\  a  e.  A )  ->  (
( S `  a
)  i^i  ( (mrCls `  (SubGrp `  G )
) `  U. ( S
" ( A  \  { a } ) ) ) )  C_  { ( 0g `  G
) } )
1421, 2, 3, 6, 13, 32, 39, 141dmdprdd 17636 1  |-  ( ph  ->  G dom DProd  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 983    = wceq 1438    e. wcel 1873    =/= wne 2619   {crab 2780   _Vcvv 3085    \ cdif 3439    i^i cin 3441    C_ wss 3442   (/)c0 3767   ~Pcpw 3987   {csn 4004   U.cuni 4225   class class class wbr 4429    |-> cmpt 4488   dom cdm 4859   ran crn 4860    |` cres 4861   "cima 4862   -->wf 5603   ` cfv 5607  (class class class)co 6311   Fincfn 7586   0cc0 9552   1c1 9553    x. cmul 9557    / cdiv 10282   NNcn 10622   NN0cn0 10882   ZZcz 10950   ^cexp 12284   #chash 12527    || cdvds 14310    gcd cgcd 14473   Primecprime 14627    pCnt cpc 14791   Basecbs 15126   0gc0g 15343  Moorecmre 15493  mrClscmrc 15494  ACScacs 15496   Grpcgrp 16674  SubGrpcsubg 16816  Cntzccntz 16974   odcod 17170   LSSumclsm 17291   Abelcabl 17436   DProd cdprd 17630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-8 1875  ax-9 1877  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402  ax-rep 4542  ax-sep 4552  ax-nul 4561  ax-pow 4608  ax-pr 4666  ax-un 6603  ax-inf2 8161  ax-cnex 9608  ax-resscn 9609  ax-1cn 9610  ax-icn 9611  ax-addcl 9612  ax-addrcl 9613  ax-mulcl 9614  ax-mulrcl 9615  ax-mulcom 9616  ax-addass 9617  ax-mulass 9618  ax-distr 9619  ax-i2m1 9620  ax-1ne0 9621  ax-1rid 9622  ax-rnegex 9623  ax-rrecex 9624  ax-cnre 9625  ax-pre-lttri 9626  ax-pre-lttrn 9627  ax-pre-ltadd 9628  ax-pre-mulgt0 9629  ax-pre-sup 9630
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-fal 1444  df-ex 1659  df-nf 1663  df-sb 1792  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3087  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3918  df-pw 3989  df-sn 4005  df-pr 4007  df-tp 4009  df-op 4011  df-uni 4226  df-int 4262  df-iun 4307  df-iin 4308  df-disj 4401  df-br 4430  df-opab 4489  df-mpt 4490  df-tr 4525  df-eprel 4770  df-id 4774  df-po 4780  df-so 4781  df-fr 4818  df-se 4819  df-we 4820  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-rn 4870  df-res 4871  df-ima 4872  df-pred 5405  df-ord 5451  df-on 5452  df-lim 5453  df-suc 5454  df-iota 5571  df-fun 5609  df-fn 5610  df-f 5611  df-f1 5612  df-fo 5613  df-f1o 5614  df-fv 5615  df-isom 5616  df-riota 6273  df-ov 6314  df-oprab 6315  df-mpt2 6316  df-om 6713  df-1st 6813  df-2nd 6814  df-wrecs 7045  df-recs 7107  df-rdg 7145  df-1o 7199  df-2o 7200  df-oadd 7203  df-omul 7204  df-er 7380  df-ec 7382  df-qs 7386  df-map 7491  df-ixp 7540  df-en 7587  df-dom 7588  df-sdom 7589  df-fin 7590  df-sup 7971  df-inf 7972  df-oi 8040  df-card 8387  df-acn 8390  df-pnf 9690  df-mnf 9691  df-xr 9692  df-ltxr 9693  df-le 9694  df-sub 9875  df-neg 9876  df-div 10283  df-nn 10623  df-2 10681  df-3 10682  df-n0 10883  df-z 10951  df-uz 11173  df-q 11278  df-rp 11316  df-fz 11798  df-fzo 11929  df-fl 12040  df-mod 12109  df-seq 12226  df-exp 12285  df-hash 12528  df-cj 13168  df-re 13169  df-im 13170  df-sqrt 13304  df-abs 13305  df-clim 13557  df-sum 13758  df-dvds 14311  df-gcd 14474  df-prm 14628  df-pc 14792  df-ndx 15129  df-slot 15130  df-base 15131  df-sets 15132  df-ress 15133  df-plusg 15208  df-0g 15345  df-mre 15497  df-mrc 15498  df-acs 15500  df-mgm 16493  df-sgrp 16532  df-mnd 16542  df-submnd 16588  df-grp 16678  df-minusg 16679  df-sbg 16680  df-mulg 16681  df-subg 16819  df-eqg 16821  df-cntz 16976  df-od 17177  df-lsm 17293  df-cmn 17437  df-abl 17438  df-dprd 17632
This theorem is referenced by:  ablfac1c  17709  ablfac1eu  17711  ablfaclem2  17724  ablfaclem3  17725
  Copyright terms: Public domain W3C validator