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

Theorem ablfac1b 15659
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 2442 . 2  |-  (Cntz `  G )  =  (Cntz `  G )
2 eqid 2442 . 2  |-  ( 0g
`  G )  =  ( 0g `  G
)
3 eqid 2442 . 2  |-  (mrCls `  (SubGrp `  G ) )  =  (mrCls `  (SubGrp `  G ) )
4 ablfac1.g . . 3  |-  ( ph  ->  G  e.  Abel )
5 ablgrp 15448 . . 3  |-  ( G  e.  Abel  ->  G  e. 
Grp )
64, 5syl 16 . 2  |-  ( ph  ->  G  e.  Grp )
7 ablfac1.1 . . 3  |-  ( ph  ->  A  C_  Prime )
8 nnex 10037 . . . . 5  |-  NN  e.  _V
9 prmnn 13113 . . . . . 6  |-  ( p  e.  Prime  ->  p  e.  NN )
109ssriv 3338 . . . . 5  |-  Prime  C_  NN
118, 10ssexi 4377 . . . 4  |-  Prime  e.  _V
1211ssex 4376 . . 3  |-  ( A 
C_  Prime  ->  A  e.  _V )
137, 12syl 16 . 2  |-  ( ph  ->  A  e.  _V )
144adantr 453 . . . 4  |-  ( (
ph  /\  p  e.  A )  ->  G  e.  Abel )
157sselda 3334 . . . . . . 7  |-  ( (
ph  /\  p  e.  A )  ->  p  e.  Prime )
1615, 9syl 16 . . . . . 6  |-  ( (
ph  /\  p  e.  A )  ->  p  e.  NN )
17 ablfac1.b . . . . . . . . . . 11  |-  B  =  ( Base `  G
)
1817grpbn0 14865 . . . . . . . . . 10  |-  ( G  e.  Grp  ->  B  =/=  (/) )
196, 18syl 16 . . . . . . . . 9  |-  ( ph  ->  B  =/=  (/) )
20 ablfac1.f . . . . . . . . . 10  |-  ( ph  ->  B  e.  Fin )
21 hashnncl 11676 . . . . . . . . . 10  |-  ( B  e.  Fin  ->  (
( # `  B )  e.  NN  <->  B  =/=  (/) ) )
2220, 21syl 16 . . . . . . . . 9  |-  ( ph  ->  ( ( # `  B
)  e.  NN  <->  B  =/=  (/) ) )
2319, 22mpbird 225 . . . . . . . 8  |-  ( ph  ->  ( # `  B
)  e.  NN )
2423adantr 453 . . . . . . 7  |-  ( (
ph  /\  p  e.  A )  ->  ( # `
 B )  e.  NN )
2515, 24pccld 13255 . . . . . 6  |-  ( (
ph  /\  p  e.  A )  ->  (
p  pCnt  ( # `  B
) )  e.  NN0 )
2616, 25nnexpcld 11575 . . . . 5  |-  ( (
ph  /\  p  e.  A )  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  e.  NN )
2726nnzd 10405 . . . 4  |-  ( (
ph  /\  p  e.  A )  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  e.  ZZ )
28 ablfac1.o . . . . 5  |-  O  =  ( od `  G
)
2928, 17oddvdssubg 15501 . . . 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 644 . . 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 5922 . 2  |-  ( ph  ->  S : A --> (SubGrp `  G ) )
334adantr 453 . . 3  |-  ( (
ph  /\  ( a  e.  A  /\  b  e.  A  /\  a  =/=  b ) )  ->  G  e.  Abel )
3432adantr 453 . . . 4  |-  ( (
ph  /\  ( a  e.  A  /\  b  e.  A  /\  a  =/=  b ) )  ->  S : A --> (SubGrp `  G ) )
35 simpr1 964 . . . 4  |-  ( (
ph  /\  ( a  e.  A  /\  b  e.  A  /\  a  =/=  b ) )  -> 
a  e.  A )
3634, 35ffvelrnd 5900 . . 3  |-  ( (
ph  /\  ( a  e.  A  /\  b  e.  A  /\  a  =/=  b ) )  -> 
( S `  a
)  e.  (SubGrp `  G ) )
37 simpr2 965 . . . 4  |-  ( (
ph  /\  ( a  e.  A  /\  b  e.  A  /\  a  =/=  b ) )  -> 
b  e.  A )
3834, 37ffvelrnd 5900 . . 3  |-  ( (
ph  /\  ( a  e.  A  /\  b  e.  A  /\  a  =/=  b ) )  -> 
( S `  b
)  e.  (SubGrp `  G ) )
391, 33, 36, 38ablcntzd 15503 . 2  |-  ( (
ph  /\  ( a  e.  A  /\  b  e.  A  /\  a  =/=  b ) )  -> 
( S `  a
)  C_  ( (Cntz `  G ) `  ( S `  b )
) )
40 id 21 . . . . . . . . . 10  |-  ( p  =  a  ->  p  =  a )
41 oveq1 6117 . . . . . . . . . 10  |-  ( p  =  a  ->  (
p  pCnt  ( # `  B
) )  =  ( a  pCnt  ( # `  B
) ) )
4240, 41oveq12d 6128 . . . . . . . . 9  |-  ( p  =  a  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  =  ( a ^ (
a  pCnt  ( # `  B
) ) ) )
4342breq2d 4249 . . . . . . . 8  |-  ( p  =  a  ->  (
( O `  x
)  ||  ( p ^ ( p  pCnt  (
# `  B )
) )  <->  ( O `  x )  ||  (
a ^ ( a 
pCnt  ( # `  B
) ) ) ) )
4443rabbidv 2954 . . . . . . 7  |-  ( p  =  a  ->  { x  e.  B  |  ( O `  x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) }  =  { x  e.  B  |  ( O `
 x )  ||  ( a ^ (
a  pCnt  ( # `  B
) ) ) } )
45 fvex 5771 . . . . . . . . 9  |-  ( Base `  G )  e.  _V
4617, 45eqeltri 2512 . . . . . . . 8  |-  B  e. 
_V
4746rabex 4383 . . . . . . 7  |-  { x  e.  B  |  ( O `  x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) }  e.  _V
4844, 31, 47fvmpt3i 5838 . . . . . 6  |-  ( a  e.  A  ->  ( S `  a )  =  { x  e.  B  |  ( O `  x )  ||  (
a ^ ( a 
pCnt  ( # `  B
) ) ) } )
4948adantl 454 . . . . 5  |-  ( (
ph  /\  a  e.  A )  ->  ( S `  a )  =  { x  e.  B  |  ( O `  x )  ||  (
a ^ ( a 
pCnt  ( # `  B
) ) ) } )
50 eqimss 3386 . . . . 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 16 . . . 4  |-  ( (
ph  /\  a  e.  A )  ->  ( S `  a )  C_ 
{ x  e.  B  |  ( O `  x )  ||  (
a ^ ( a 
pCnt  ( # `  B
) ) ) } )
524adantr 453 . . . . . 6  |-  ( (
ph  /\  a  e.  A )  ->  G  e.  Abel )
53 eqid 2442 . . . . . . 7  |-  ( Base `  G )  =  (
Base `  G )
5453subgacs 15006 . . . . . 6  |-  ( G  e.  Grp  ->  (SubGrp `  G )  e.  (ACS
`  ( Base `  G
) ) )
55 acsmre 13908 . . . . . 6  |-  ( (SubGrp `  G )  e.  (ACS
`  ( Base `  G
) )  ->  (SubGrp `  G )  e.  (Moore `  ( Base `  G
) ) )
5652, 5, 54, 554syl 20 . . . . 5  |-  ( (
ph  /\  a  e.  A )  ->  (SubGrp `  G )  e.  (Moore `  ( Base `  G
) ) )
57 df-ima 4920 . . . . . . 7  |-  ( S
" ( A  \  { a } ) )  =  ran  ( S  |`  ( A  \  { a } ) )
587sselda 3334 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  a  e.  A )  ->  a  e.  Prime )
5958ad2antrr 708 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  a  e.  Prime )
6023ad3antrrr 712 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  ( # `
 B )  e.  NN )
61 pcdvds 13268 . . . . . . . . . . . . . . . 16  |-  ( ( a  e.  Prime  /\  ( # `
 B )  e.  NN )  ->  (
a ^ ( a 
pCnt  ( # `  B
) ) )  ||  ( # `  B ) )
6259, 60, 61syl2anc 644 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
a ^ ( a 
pCnt  ( # `  B
) ) )  ||  ( # `  B ) )
637ad3antrrr 712 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  A  C_ 
Prime )
64 eldifi 3455 . . . . . . . . . . . . . . . . . 18  |-  ( p  e.  ( A  \  { a } )  ->  p  e.  A
)
6564ad2antlr 709 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  p  e.  A )
6663, 65sseldd 3335 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  p  e.  Prime )
67 pcdvds 13268 . . . . . . . . . . . . . . . 16  |-  ( ( p  e.  Prime  /\  ( # `
 B )  e.  NN )  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  ||  ( # `  B ) )
6866, 60, 67syl2anc 644 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  ||  ( # `  B ) )
69 eqid 2442 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a ^ ( a  pCnt  (
# `  B )
) )  =  ( a ^ ( a 
pCnt  ( # `  B
) ) )
70 eqid 2442 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
# `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  =  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) )
7117, 28, 31, 4, 20, 7, 69, 70ablfac1lem 15657 . . . . . . . . . . . . . . . . . . . 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 970 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  a  e.  A )  ->  (
( a ^ (
a  pCnt  ( # `  B
) ) )  e.  NN  /\  ( (
# `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  e.  NN ) )
7372simpld 447 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  a  e.  A )  ->  (
a ^ ( a 
pCnt  ( # `  B
) ) )  e.  NN )
7473ad2antrr 708 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
a ^ ( a 
pCnt  ( # `  B
) ) )  e.  NN )
7574nnzd 10405 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
a ^ ( a 
pCnt  ( # `  B
) ) )  e.  ZZ )
7666, 9syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  p  e.  NN )
7766, 60pccld 13255 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
p  pCnt  ( # `  B
) )  e.  NN0 )
7876, 77nnexpcld 11575 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  e.  NN )
7978nnzd 10405 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  e.  ZZ )
8060nnzd 10405 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  ( # `
 B )  e.  ZZ )
81 eldifsni 3952 . . . . . . . . . . . . . . . . . . . 20  |-  ( p  e.  ( A  \  { a } )  ->  p  =/=  a
)
8281ad2antlr 709 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  p  =/=  a )
8382necomd 2693 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  a  =/=  p )
84 prmrp 13132 . . . . . . . . . . . . . . . . . . 19  |-  ( ( a  e.  Prime  /\  p  e.  Prime )  ->  (
( a  gcd  p
)  =  1  <->  a  =/=  p ) )
8559, 66, 84syl2anc 644 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( a  gcd  p
)  =  1  <->  a  =/=  p ) )
8683, 85mpbird 225 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
a  gcd  p )  =  1 )
87 prmz 13114 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  Prime  ->  a  e.  ZZ )
8859, 87syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  a  e.  ZZ )
89 prmz 13114 . . . . . . . . . . . . . . . . . . 19  |-  ( p  e.  Prime  ->  p  e.  ZZ )
9066, 89syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  p  e.  ZZ )
9159, 60pccld 13255 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
a  pCnt  ( # `  B
) )  e.  NN0 )
92 rpexp12i 13153 . . . . . . . . . . . . . . . . . 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 1189 . . . . . . . . . . . . . . . . 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 13134 . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . 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 662 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( a ^ (
a  pCnt  ( # `  B
) ) )  x.  ( p ^ (
p  pCnt  ( # `  B
) ) ) ) 
||  ( # `  B
) )
9871simp3d 972 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  a  e.  A )  ->  ( # `
 B )  =  ( ( a ^
( a  pCnt  ( # `
 B ) ) )  x.  ( (
# `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) ) )
9998ad2antrr 708 . . . . . . . . . . . . . 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 4261 . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  a  e.  A )  ->  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  e.  NN )
102101ad2antrr 708 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  e.  NN )
103102nnzd 10405 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  e.  ZZ )
10474nnne0d 10075 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
a ^ ( a 
pCnt  ( # `  B
) ) )  =/=  0 )
105 dvdscmulr 12909 . . . . . . . . . . . . . 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 1189 . . . . . . . . . . . . 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 203 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) )
10817, 28odcl 15205 . . . . . . . . . . . . . . 15  |-  ( x  e.  B  ->  ( O `  x )  e.  NN0 )
109108adantl 454 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  ( O `  x )  e.  NN0 )
110109nn0zd 10404 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  a  e.  A )  /\  p  e.  ( A  \  { a } ) )  /\  x  e.  B )  ->  ( O `  x )  e.  ZZ )
111 dvdstr 12914 . . . . . . . . . . . . 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 1185 . . . . . . . . . . . 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 657 . . . . . . . . . . 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 3410 . . . . . . . . . 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 3829 . . . . . . . . . 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 205 . . . . . . . . 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 5171 . . . . . . . . . 10  |-  ( S  |`  ( A  \  {
a } ) )  =  ( ( p  e.  A  |->  { x  e.  B  |  ( O `  x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) } )  |`  ( A  \  { a } ) )
118 difss 3460 . . . . . . . . . . 11  |-  ( A 
\  { a } )  C_  A
119 resmpt 5220 . . . . . . . . . . 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 2462 . . . . . . . . 9  |-  ( S  |`  ( A  \  {
a } ) )  =  ( p  e.  ( A  \  {
a } )  |->  { x  e.  B  | 
( O `  x
)  ||  ( p ^ ( p  pCnt  (
# `  B )
) ) } )
122116, 121fmptd 5922 . . . . . . . 8  |-  ( (
ph  /\  a  e.  A )  ->  ( S  |`  ( A  \  { a } ) ) : ( A 
\  { a } ) --> ~P { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } )
123 frn 5626 . . . . . . . 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 16 . . . . . . 7  |-  ( (
ph  /\  a  e.  A )  ->  ran  ( S  |`  ( A 
\  { a } ) )  C_  ~P { x  e.  B  |  ( O `  x )  ||  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) ) } )
12557, 124syl5eqss 3378 . . . . . 6  |-  ( (
ph  /\  a  e.  A )  ->  ( S " ( A  \  { a } ) )  C_  ~P { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } )
126 sspwuni 4201 . . . . . 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 190 . . . . 5  |-  ( (
ph  /\  a  e.  A )  ->  U. ( S " ( A  \  { a } ) )  C_  { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) } )
128101nnzd 10405 . . . . . 6  |-  ( (
ph  /\  a  e.  A )  ->  (
( # `  B )  /  ( a ^
( a  pCnt  ( # `
 B ) ) ) )  e.  ZZ )
12928, 17oddvdssubg 15501 . . . . . 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 644 . . . . 5  |-  ( (
ph  /\  a  e.  A )  ->  { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) }  e.  (SubGrp `  G
) )
1313mrcsscl 13876 . . . . 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 1185 . . . 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 3553 . . . 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 644 . . 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 2442 . . . . 5  |-  { x  e.  B  |  ( O `  x )  ||  ( a ^ (
a  pCnt  ( # `  B
) ) ) }  =  { x  e.  B  |  ( O `
 x )  ||  ( a ^ (
a  pCnt  ( # `  B
) ) ) }
136 eqid 2442 . . . . 5  |-  { x  e.  B  |  ( O `  x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) }  =  { x  e.  B  |  ( O `
 x )  ||  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) }
13771simp2d 971 . . . . 5  |-  ( (
ph  /\  a  e.  A )  ->  (
( a ^ (
a  pCnt  ( # `  B
) ) )  gcd  ( ( # `  B
)  /  ( a ^ ( a  pCnt  (
# `  B )
) ) ) )  =  1 )
138 eqid 2442 . . . . 5  |-  ( LSSum `  G )  =  (
LSSum `  G )
13917, 28, 135, 136, 52, 73, 101, 137, 98, 2, 138ablfacrp 15655 . . . 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 447 . . 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 3370 . 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 15591 1  |-  ( ph  ->  G dom DProd  S )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    /\ w3a 937    = wceq 1653    e. wcel 1727    =/= wne 2605   {crab 2715   _Vcvv 2962    \ cdif 3303    i^i cin 3305    C_ wss 3306   (/)c0 3613   ~Pcpw 3823   {csn 3838   U.cuni 4039   class class class wbr 4237    e. cmpt 4291   dom cdm 4907   ran crn 4908    |` cres 4909   "cima 4910   -->wf 5479   ` cfv 5483  (class class class)co 6110   Fincfn 7138   0cc0 9021   1c1 9022    x. cmul 9026    / cdiv 9708   NNcn 10031   NN0cn0 10252   ZZcz 10313   ^cexp 11413   #chash 11649    || cdivides 12883    gcd cgcd 13037   Primecprime 13110    pCnt cpc 13241   Basecbs 13500   0gc0g 13754  Moorecmre 13838  mrClscmrc 13839  ACScacs 13841   Grpcgrp 14716  SubGrpcsubg 14969  Cntzccntz 15145   odcod 15194   LSSumclsm 15299   Abelcabel 15444   DProd cdprd 15585
This theorem is referenced by:  ablfac1c  15660  ablfac1eu  15662  ablfaclem2  15675  ablfaclem3  15676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-rep 4345  ax-sep 4355  ax-nul 4363  ax-pow 4406  ax-pr 4432  ax-un 4730  ax-inf2 7625  ax-cnex 9077  ax-resscn 9078  ax-1cn 9079  ax-icn 9080  ax-addcl 9081  ax-addrcl 9082  ax-mulcl 9083  ax-mulrcl 9084  ax-mulcom 9085  ax-addass 9086  ax-mulass 9087  ax-distr 9088  ax-i2m1 9089  ax-1ne0 9090  ax-1rid 9091  ax-rnegex 9092  ax-rrecex 9093  ax-cnre 9094  ax-pre-lttri 9095  ax-pre-lttrn 9096  ax-pre-ltadd 9097  ax-pre-mulgt0 9098  ax-pre-sup 9099
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 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-nel 2608  df-ral 2716  df-rex 2717  df-reu 2718  df-rmo 2719  df-rab 2720  df-v 2964  df-sbc 3168  df-csb 3268  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-pss 3322  df-nul 3614  df-if 3764  df-pw 3825  df-sn 3844  df-pr 3845  df-tp 3846  df-op 3847  df-uni 4040  df-int 4075  df-iun 4119  df-iin 4120  df-disj 4208  df-br 4238  df-opab 4292  df-mpt 4293  df-tr 4328  df-eprel 4523  df-id 4527  df-po 4532  df-so 4533  df-fr 4570  df-se 4571  df-we 4572  df-ord 4613  df-on 4614  df-lim 4615  df-suc 4616  df-om 4875  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-rn 4918  df-res 4919  df-ima 4920  df-iota 5447  df-fun 5485  df-fn 5486  df-f 5487  df-f1 5488  df-fo 5489  df-f1o 5490  df-fv 5491  df-isom 5492  df-ov 6113  df-oprab 6114  df-mpt2 6115  df-1st 6378  df-2nd 6379  df-riota 6578  df-recs 6662  df-rdg 6697  df-1o 6753  df-2o 6754  df-oadd 6757  df-omul 6758  df-er 6934  df-ec 6936  df-qs 6940  df-map 7049  df-ixp 7093  df-en 7139  df-dom 7140  df-sdom 7141  df-fin 7142  df-sup 7475  df-oi 7508  df-card 7857  df-acn 7860  df-pnf 9153  df-mnf 9154  df-xr 9155  df-ltxr 9156  df-le 9157  df-sub 9324  df-neg 9325  df-div 9709  df-nn 10032  df-2 10089  df-3 10090  df-n0 10253  df-z 10314  df-uz 10520  df-q 10606  df-rp 10644  df-fz 11075  df-fzo 11167  df-fl 11233  df-mod 11282  df-seq 11355  df-exp 11414  df-hash 11650  df-cj 11935  df-re 11936  df-im 11937  df-sqr 12071  df-abs 12072  df-clim 12313  df-sum 12511  df-dvds 12884  df-gcd 13038  df-prm 13111  df-pc 13242  df-ndx 13503  df-slot 13504  df-base 13505  df-sets 13506  df-ress 13507  df-plusg 13573  df-0g 13758  df-mre 13842  df-mrc 13843  df-acs 13845  df-mnd 14721  df-submnd 14770  df-grp 14843  df-minusg 14844  df-sbg 14845  df-mulg 14846  df-subg 14972  df-eqg 14974  df-cntz 15147  df-od 15198  df-lsm 15301  df-cmn 15445  df-abl 15446  df-dprd 15587
  Copyright terms: Public domain W3C validator