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

Theorem ablfac1eu 16577
Description: The factorization of ablfac1b 16574 is unique, in that any other factorization into prime power factors (even if the exponents are different) must be equal to 
S. (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 )
ablfac1c.d  |-  D  =  { w  e.  Prime  |  w  ||  ( # `  B ) }
ablfac1.2  |-  ( ph  ->  D  C_  A )
ablfac1eu.1  |-  ( ph  ->  ( G dom DProd  T  /\  ( G DProd  T )  =  B ) )
ablfac1eu.2  |-  ( ph  ->  dom  T  =  A )
ablfac1eu.3  |-  ( (
ph  /\  q  e.  A )  ->  C  e.  NN0 )
ablfac1eu.4  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  =  ( q ^ C
) )
Assertion
Ref Expression
ablfac1eu  |-  ( ph  ->  T  =  S )
Distinct variable groups:    q, p, w, x, B    D, p, q, x    ph, p, q, w, x    S, q    A, p, q, x    O, p, q, x    T, q, x    G, p, q, x
Allowed substitution hints:    A( w)    C( x, w, q, p)    D( w)    S( x, w, p)    T( w, p)    G( w)    O( w)

Proof of Theorem ablfac1eu
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 ablfac1eu.1 . . . . 5  |-  ( ph  ->  ( G dom DProd  T  /\  ( G DProd  T )  =  B ) )
21simpld 459 . . . 4  |-  ( ph  ->  G dom DProd  T )
3 ablfac1eu.2 . . . 4  |-  ( ph  ->  dom  T  =  A )
42, 3dprdf2 16494 . . 3  |-  ( ph  ->  T : A --> (SubGrp `  G ) )
5 ffn 5562 . . 3  |-  ( T : A --> (SubGrp `  G )  ->  T  Fn  A )
64, 5syl 16 . 2  |-  ( ph  ->  T  Fn  A )
7 ablfac1.b . . . . 5  |-  B  =  ( Base `  G
)
8 ablfac1.o . . . . 5  |-  O  =  ( od `  G
)
9 ablfac1.s . . . . 5  |-  S  =  ( p  e.  A  |->  { x  e.  B  |  ( O `  x )  ||  (
p ^ ( p 
pCnt  ( # `  B
) ) ) } )
10 ablfac1.g . . . . 5  |-  ( ph  ->  G  e.  Abel )
11 ablfac1.f . . . . 5  |-  ( ph  ->  B  e.  Fin )
12 ablfac1.1 . . . . 5  |-  ( ph  ->  A  C_  Prime )
137, 8, 9, 10, 11, 12ablfac1b 16574 . . . 4  |-  ( ph  ->  G dom DProd  S )
14 fvex 5704 . . . . . . . 8  |-  ( Base `  G )  e.  _V
157, 14eqeltri 2513 . . . . . . 7  |-  B  e. 
_V
1615rabex 4446 . . . . . 6  |-  { x  e.  B  |  ( O `  x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) }  e.  _V
1716, 9dmmpti 5543 . . . . 5  |-  dom  S  =  A
1817a1i 11 . . . 4  |-  ( ph  ->  dom  S  =  A )
1913, 18dprdf2 16494 . . 3  |-  ( ph  ->  S : A --> (SubGrp `  G ) )
20 ffn 5562 . . 3  |-  ( S : A --> (SubGrp `  G )  ->  S  Fn  A )
2119, 20syl 16 . 2  |-  ( ph  ->  S  Fn  A )
2211adantr 465 . . . 4  |-  ( (
ph  /\  q  e.  A )  ->  B  e.  Fin )
2319ffvelrnda 5846 . . . . 5  |-  ( (
ph  /\  q  e.  A )  ->  ( S `  q )  e.  (SubGrp `  G )
)
247subgss 15685 . . . . 5  |-  ( ( S `  q )  e.  (SubGrp `  G
)  ->  ( S `  q )  C_  B
)
2523, 24syl 16 . . . 4  |-  ( (
ph  /\  q  e.  A )  ->  ( S `  q )  C_  B )
26 ssfi 7536 . . . 4  |-  ( ( B  e.  Fin  /\  ( S `  q ) 
C_  B )  -> 
( S `  q
)  e.  Fin )
2722, 25, 26syl2anc 661 . . 3  |-  ( (
ph  /\  q  e.  A )  ->  ( S `  q )  e.  Fin )
284ffvelrnda 5846 . . . . . 6  |-  ( (
ph  /\  q  e.  A )  ->  ( T `  q )  e.  (SubGrp `  G )
)
297subgss 15685 . . . . . 6  |-  ( ( T `  q )  e.  (SubGrp `  G
)  ->  ( T `  q )  C_  B
)
3028, 29syl 16 . . . . 5  |-  ( (
ph  /\  q  e.  A )  ->  ( T `  q )  C_  B )
3128adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( T `  q )  e.  (SubGrp `  G )
)
32 ssfi 7536 . . . . . . . . 9  |-  ( ( B  e.  Fin  /\  ( T `  q ) 
C_  B )  -> 
( T `  q
)  e.  Fin )
3322, 30, 32syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  ( T `  q )  e.  Fin )
3433adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( T `  q )  e.  Fin )
35 simpr 461 . . . . . . 7  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  x  e.  ( T `  q
) )
368odsubdvds 16073 . . . . . . 7  |-  ( ( ( T `  q
)  e.  (SubGrp `  G )  /\  ( T `  q )  e.  Fin  /\  x  e.  ( T `  q
) )  ->  ( O `  x )  ||  ( # `  ( T `  q )
) )
3731, 34, 35, 36syl3anc 1218 . . . . . 6  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( O `  x )  ||  ( # `  ( T `  q )
) )
38 ablfac1eu.4 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  =  ( q ^ C
) )
3912sselda 3359 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  q  e.  Prime )
40 prmz 13770 . . . . . . . . . 10  |-  ( q  e.  Prime  ->  q  e.  ZZ )
4139, 40syl 16 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  q  e.  ZZ )
42 ablfac1eu.3 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  C  e.  NN0 )
4342nn0zd 10748 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  C  e.  ZZ )
44 ablgrp 16285 . . . . . . . . . . . . . . . 16  |-  ( G  e.  Abel  ->  G  e. 
Grp )
4510, 44syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  G  e.  Grp )
467grpbn0 15570 . . . . . . . . . . . . . . 15  |-  ( G  e.  Grp  ->  B  =/=  (/) )
4745, 46syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  =/=  (/) )
48 hashnncl 12137 . . . . . . . . . . . . . . 15  |-  ( B  e.  Fin  ->  (
( # `  B )  e.  NN  <->  B  =/=  (/) ) )
4911, 48syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( # `  B
)  e.  NN  <->  B  =/=  (/) ) )
5047, 49mpbird 232 . . . . . . . . . . . . 13  |-  ( ph  ->  ( # `  B
)  e.  NN )
5150adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 B )  e.  NN )
5239, 51pccld 13920 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  (
q  pCnt  ( # `  B
) )  e.  NN0 )
5352nn0zd 10748 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  (
q  pCnt  ( # `  B
) )  e.  ZZ )
547lagsubg 15746 . . . . . . . . . . . . 13  |-  ( ( ( T `  q
)  e.  (SubGrp `  G )  /\  B  e.  Fin )  ->  ( # `
 ( T `  q ) )  ||  ( # `  B ) )
5528, 22, 54syl2anc 661 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  ||  ( # `  B ) )
5638, 55eqbrtrrd 4317 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ C ) 
||  ( # `  B
) )
5751nnzd 10749 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 B )  e.  ZZ )
58 pcdvdsb 13938 . . . . . . . . . . . 12  |-  ( ( q  e.  Prime  /\  ( # `
 B )  e.  ZZ  /\  C  e. 
NN0 )  ->  ( C  <_  ( q  pCnt  (
# `  B )
)  <->  ( q ^ C )  ||  ( # `
 B ) ) )
5939, 57, 42, 58syl3anc 1218 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  ( C  <_  ( q  pCnt  (
# `  B )
)  <->  ( q ^ C )  ||  ( # `
 B ) ) )
6056, 59mpbird 232 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  C  <_  ( q  pCnt  ( # `
 B ) ) )
61 eluz2 10870 . . . . . . . . . 10  |-  ( ( q  pCnt  ( # `  B
) )  e.  (
ZZ>= `  C )  <->  ( C  e.  ZZ  /\  ( q 
pCnt  ( # `  B
) )  e.  ZZ  /\  C  <_  ( q  pCnt  ( # `  B
) ) ) )
6243, 53, 60, 61syl3anbrc 1172 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  (
q  pCnt  ( # `  B
) )  e.  (
ZZ>= `  C ) )
63 dvdsexp 13592 . . . . . . . . 9  |-  ( ( q  e.  ZZ  /\  C  e.  NN0  /\  (
q  pCnt  ( # `  B
) )  e.  (
ZZ>= `  C ) )  ->  ( q ^ C )  ||  (
q ^ ( q 
pCnt  ( # `  B
) ) ) )
6441, 42, 62, 63syl3anc 1218 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ C ) 
||  ( q ^
( q  pCnt  ( # `
 B ) ) ) )
6538, 64eqbrtrd 4315 . . . . . . 7  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  ||  ( q ^ (
q  pCnt  ( # `  B
) ) ) )
6665adantr 465 . . . . . 6  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( # `
 ( T `  q ) )  ||  ( q ^ (
q  pCnt  ( # `  B
) ) ) )
6730sselda 3359 . . . . . . . . 9  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  x  e.  B )
687, 8odcl 16042 . . . . . . . . 9  |-  ( x  e.  B  ->  ( O `  x )  e.  NN0 )
6967, 68syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( O `  x )  e.  NN0 )
7069nn0zd 10748 . . . . . . 7  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( O `  x )  e.  ZZ )
71 hashcl 12129 . . . . . . . . . 10  |-  ( ( T `  q )  e.  Fin  ->  ( # `
 ( T `  q ) )  e. 
NN0 )
7233, 71syl 16 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  e. 
NN0 )
7372nn0zd 10748 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  e.  ZZ )
7473adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( # `
 ( T `  q ) )  e.  ZZ )
75 prmnn 13769 . . . . . . . . . . 11  |-  ( q  e.  Prime  ->  q  e.  NN )
7639, 75syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  q  e.  NN )
7776, 52nnexpcld 12032 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ ( q 
pCnt  ( # `  B
) ) )  e.  NN )
7877nnzd 10749 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ ( q 
pCnt  ( # `  B
) ) )  e.  ZZ )
7978adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  (
q ^ ( q 
pCnt  ( # `  B
) ) )  e.  ZZ )
80 dvdstr 13569 . . . . . . 7  |-  ( ( ( O `  x
)  e.  ZZ  /\  ( # `  ( T `
 q ) )  e.  ZZ  /\  (
q ^ ( q 
pCnt  ( # `  B
) ) )  e.  ZZ )  ->  (
( ( O `  x )  ||  ( # `
 ( T `  q ) )  /\  ( # `  ( T `
 q ) ) 
||  ( q ^
( q  pCnt  ( # `
 B ) ) ) )  ->  ( O `  x )  ||  ( q ^ (
q  pCnt  ( # `  B
) ) ) ) )
8170, 74, 79, 80syl3anc 1218 . . . . . 6  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  (
( ( O `  x )  ||  ( # `
 ( T `  q ) )  /\  ( # `  ( T `
 q ) ) 
||  ( q ^
( q  pCnt  ( # `
 B ) ) ) )  ->  ( O `  x )  ||  ( q ^ (
q  pCnt  ( # `  B
) ) ) ) )
8237, 66, 81mp2and 679 . . . . 5  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( O `  x )  ||  ( q ^ (
q  pCnt  ( # `  B
) ) ) )
8330, 82ssrabdv 3434 . . . 4  |-  ( (
ph  /\  q  e.  A )  ->  ( T `  q )  C_ 
{ x  e.  B  |  ( O `  x )  ||  (
q ^ ( q 
pCnt  ( # `  B
) ) ) } )
84 id 22 . . . . . . . . 9  |-  ( p  =  q  ->  p  =  q )
85 oveq1 6101 . . . . . . . . 9  |-  ( p  =  q  ->  (
p  pCnt  ( # `  B
) )  =  ( q  pCnt  ( # `  B
) ) )
8684, 85oveq12d 6112 . . . . . . . 8  |-  ( p  =  q  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  =  ( q ^ (
q  pCnt  ( # `  B
) ) ) )
8786breq2d 4307 . . . . . . 7  |-  ( p  =  q  ->  (
( O `  x
)  ||  ( p ^ ( p  pCnt  (
# `  B )
) )  <->  ( O `  x )  ||  (
q ^ ( q 
pCnt  ( # `  B
) ) ) ) )
8887rabbidv 2967 . . . . . 6  |-  ( p  =  q  ->  { x  e.  B  |  ( O `  x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) }  =  { x  e.  B  |  ( O `
 x )  ||  ( q ^ (
q  pCnt  ( # `  B
) ) ) } )
8988, 9, 16fvmpt3i 5781 . . . . 5  |-  ( q  e.  A  ->  ( S `  q )  =  { x  e.  B  |  ( O `  x )  ||  (
q ^ ( q 
pCnt  ( # `  B
) ) ) } )
9089adantl 466 . . . 4  |-  ( (
ph  /\  q  e.  A )  ->  ( S `  q )  =  { x  e.  B  |  ( O `  x )  ||  (
q ^ ( q 
pCnt  ( # `  B
) ) ) } )
9183, 90sseqtr4d 3396 . . 3  |-  ( (
ph  /\  q  e.  A )  ->  ( T `  q )  C_  ( S `  q
) )
9277nnnn0d 10639 . . . . . 6  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ ( q 
pCnt  ( # `  B
) ) )  e. 
NN0 )
93 pcdvds 13933 . . . . . . . . . 10  |-  ( ( q  e.  Prime  /\  ( # `
 B )  e.  NN )  ->  (
q ^ ( q 
pCnt  ( # `  B
) ) )  ||  ( # `  B ) )
9439, 51, 93syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ ( q 
pCnt  ( # `  B
) ) )  ||  ( # `  B ) )
952adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  q  e.  A )  ->  G dom DProd  T )
963adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  q  e.  A )  ->  dom  T  =  A )
97 ablfac1.2 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  D  C_  A )
9897adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  q  e.  A )  ->  D  C_  A )
9995, 96, 98dprdres 16528 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  q  e.  A )  ->  ( G dom DProd  ( T  |`  D )  /\  ( G DProd  ( T  |`  D ) )  C_  ( G DProd  T ) ) )
10099simpld 459 . . . . . . . . . . . . 13  |-  ( (
ph  /\  q  e.  A )  ->  G dom DProd  ( T  |`  D ) )
1014adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  q  e.  A )  ->  T : A --> (SubGrp `  G )
)
102 fssres 5581 . . . . . . . . . . . . . . 15  |-  ( ( T : A --> (SubGrp `  G )  /\  D  C_  A )  ->  ( T  |`  D ) : D --> (SubGrp `  G )
)
103101, 98, 102syl2anc 661 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  q  e.  A )  ->  ( T  |`  D ) : D --> (SubGrp `  G )
)
104 fdm 5566 . . . . . . . . . . . . . 14  |-  ( ( T  |`  D ) : D --> (SubGrp `  G )  ->  dom  ( T  |`  D )  =  D )
105103, 104syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  q  e.  A )  ->  dom  ( T  |`  D )  =  D )
106 difssd 3487 . . . . . . . . . . . . 13  |-  ( (
ph  /\  q  e.  A )  ->  ( D  \  { q } )  C_  D )
107100, 105, 106dprdres 16528 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  ( G dom DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) )  /\  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  C_  ( G DProd  ( T  |`  D ) ) ) )
108107simpld 459 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  G dom DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )
109 dprdsubg 16524 . . . . . . . . . . 11  |-  ( G dom DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  e.  (SubGrp `  G )
)
110108, 109syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  e.  (SubGrp `  G )
)
1117lagsubg 15746 . . . . . . . . . 10  |-  ( ( ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) )  e.  (SubGrp `  G )  /\  B  e.  Fin )  ->  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  ||  ( # `
 B ) )
112110, 22, 111syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  ||  ( # `
 B ) )
113 eqid 2443 . . . . . . . . . . . . . . 15  |-  ( 0g
`  G )  =  ( 0g `  G
)
114113subg0cl 15692 . . . . . . . . . . . . . 14  |-  ( ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  e.  (SubGrp `  G )  ->  ( 0g `  G
)  e.  ( G DProd 
( ( T  |`  D )  |`  ( D  \  { q } ) ) ) )
115110, 114syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  q  e.  A )  ->  ( 0g `  G )  e.  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) )
116 ne0i 3646 . . . . . . . . . . . . 13  |-  ( ( 0g `  G )  e.  ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) )  =/=  (/) )
117115, 116syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  =/=  (/) )
1187dprdssv 16509 . . . . . . . . . . . . . 14  |-  ( G DProd 
( ( T  |`  D )  |`  ( D  \  { q } ) ) )  C_  B
119 ssfi 7536 . . . . . . . . . . . . . 14  |-  ( ( B  e.  Fin  /\  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) 
C_  B )  -> 
( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  e.  Fin )
12022, 118, 119sylancl 662 . . . . . . . . . . . . 13  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  e. 
Fin )
121 hashnncl 12137 . . . . . . . . . . . . 13  |-  ( ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  e. 
Fin  ->  ( ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  e.  NN  <->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  =/=  (/) ) )
122120, 121syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  (
( # `  ( G DProd 
( ( T  |`  D )  |`  ( D  \  { q } ) ) ) )  e.  NN  <->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) )  =/=  (/) ) )
123117, 122mpbird 232 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  e.  NN )
124123nnzd 10749 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  e.  ZZ )
125 eqid 2443 . . . . . . . . . . . . . . . 16  |-  ( p  e.  D  |->  { y  e.  B  |  ( O `  y ) 
||  ( p ^
( p  pCnt  ( # `
 B ) ) ) } )  =  ( p  e.  D  |->  { y  e.  B  |  ( O `  y )  ||  (
p ^ ( p 
pCnt  ( # `  B
) ) ) } )
12610adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  G  e.  Abel )
12711adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  B  e.  Fin )
128 ablfac1c.d . . . . . . . . . . . . . . . . . 18  |-  D  =  { w  e.  Prime  |  w  ||  ( # `  B ) }
129 ssrab2 3440 . . . . . . . . . . . . . . . . . 18  |-  { w  e.  Prime  |  w  ||  ( # `  B ) }  C_  Prime
130128, 129eqsstri 3389 . . . . . . . . . . . . . . . . 17  |-  D  C_  Prime
131130a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  D  C_  Prime )
132 ssid 3378 . . . . . . . . . . . . . . . . 17  |-  D  C_  D
133132a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  D  C_  D
)
1342, 3, 97dprdres 16528 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( G dom DProd  ( T  |`  D )  /\  ( G DProd  ( T  |`  D ) )  C_  ( G DProd  T ) ) )
135134simpld 459 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  G dom DProd  ( T  |`  D ) )
136 dprdsubg 16524 . . . . . . . . . . . . . . . . . . . . 21  |-  ( G dom DProd  ( T  |`  D )  ->  ( G DProd  ( T  |`  D ) )  e.  (SubGrp `  G ) )
137135, 136syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( G DProd  ( T  |`  D ) )  e.  (SubGrp `  G )
)
138 difssd 3487 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( A  \  D
)  C_  A )
1392, 3, 138dprdres 16528 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( G dom DProd  ( T  |`  ( A  \  D
) )  /\  ( G DProd  ( T  |`  ( A  \  D ) ) )  C_  ( G DProd  T ) ) )
140139simpld 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  G dom DProd  ( T  |`  ( A  \  D
) ) )
141 dprdsubg 16524 . . . . . . . . . . . . . . . . . . . . 21  |-  ( G dom DProd  ( T  |`  ( A  \  D ) )  ->  ( G DProd  ( T  |`  ( A  \  D ) ) )  e.  (SubGrp `  G
) )
142140, 141syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( G DProd  ( T  |`  ( A  \  D
) ) )  e.  (SubGrp `  G )
)
143 difss 3486 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A 
\  D )  C_  A
144 fssres 5581 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( T : A --> (SubGrp `  G )  /\  ( A  \  D )  C_  A )  ->  ( T  |`  ( A  \  D ) ) : ( A  \  D
) --> (SubGrp `  G )
)
1454, 143, 144sylancl 662 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( T  |`  ( A  \  D ) ) : ( A  \  D ) --> (SubGrp `  G ) )
146 fdm 5566 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T  |`  ( A  \  D ) ) : ( A  \  D
) --> (SubGrp `  G )  ->  dom  ( T  |`  ( A  \  D ) )  =  ( A 
\  D ) )
147145, 146syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  dom  ( T  |`  ( A  \  D ) )  =  ( A 
\  D ) )
148 fvres 5707 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( q  e.  ( A  \  D )  ->  (
( T  |`  ( A  \  D ) ) `
 q )  =  ( T `  q
) )
149148adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  q  e.  ( A  \  D ) )  ->  ( ( T  |`  ( A  \  D ) ) `  q )  =  ( T `  q ) )
150 eldif 3341 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( q  e.  ( A  \  D )  <->  ( q  e.  A  /\  -.  q  e.  D ) )
15133adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( T `  q
)  e.  Fin )
152113subg0cl 15692 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( T `  q )  e.  (SubGrp `  G
)  ->  ( 0g `  G )  e.  ( T `  q ) )
15328, 152syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  q  e.  A )  ->  ( 0g `  G )  e.  ( T `  q
) )
154153snssd 4021 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  q  e.  A )  ->  { ( 0g `  G ) }  C_  ( T `  q ) )
155154adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  { ( 0g `  G ) }  C_  ( T `  q ) )
15638adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( # `  ( T `
 q ) )  =  ( q ^ C ) )
15739adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  q  e.  A )  /\  C  e.  NN )  ->  q  e.  Prime )
158 iddvdsexp 13559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( q  e.  ZZ  /\  C  e.  NN )  ->  q  ||  ( q ^ C ) )
15941, 158sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  q  e.  A )  /\  C  e.  NN )  ->  q  ||  ( q ^ C
) )
16056adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  q  e.  A )  /\  C  e.  NN )  ->  (
q ^ C ) 
||  ( # `  B
) )
16138, 73eqeltrrd 2518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ C )  e.  ZZ )
162 dvdstr 13569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( q  e.  ZZ  /\  ( q ^ C
)  e.  ZZ  /\  ( # `  B )  e.  ZZ )  -> 
( ( q  ||  ( q ^ C
)  /\  ( q ^ C )  ||  ( # `
 B ) )  ->  q  ||  ( # `
 B ) ) )
16341, 161, 57, 162syl3anc 1218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  q  e.  A )  ->  (
( q  ||  (
q ^ C )  /\  ( q ^ C )  ||  ( # `
 B ) )  ->  q  ||  ( # `
 B ) ) )
164163adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  q  e.  A )  /\  C  e.  NN )  ->  (
( q  ||  (
q ^ C )  /\  ( q ^ C )  ||  ( # `
 B ) )  ->  q  ||  ( # `
 B ) ) )
165159, 160, 164mp2and 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  q  e.  A )  /\  C  e.  NN )  ->  q  ||  ( # `  B
) )
166 breq1 4298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( w  =  q  ->  (
w  ||  ( # `  B
)  <->  q  ||  ( # `
 B ) ) )
167166, 128elrab2 3122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( q  e.  D  <->  ( q  e.  Prime  /\  q  ||  ( # `  B ) ) )
168157, 165, 167sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  q  e.  A )  /\  C  e.  NN )  ->  q  e.  D )
169168ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  q  e.  A )  ->  ( C  e.  NN  ->  q  e.  D ) )
170169con3d 133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  q  e.  A )  ->  ( -.  q  e.  D  ->  -.  C  e.  NN ) )
171170impr 619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  -.  C  e.  NN )
17242adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  C  e.  NN0 )
173 elnn0 10584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( C  e.  NN0  <->  ( C  e.  NN  \/  C  =  0 ) )
174172, 173sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( C  e.  NN  \/  C  =  0
) )
175174ord 377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( -.  C  e.  NN  ->  C  = 
0 ) )
176171, 175mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  C  =  0 )
177176oveq2d 6110 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( q ^ C
)  =  ( q ^ 0 ) )
17876adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
q  e.  NN )
179178nncnd 10341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
q  e.  CC )
180179exp0d 12005 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( q ^ 0 )  =  1 )
181156, 177, 1803eqtrd 2479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( # `  ( T `
 q ) )  =  1 )
182 fvex 5704 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0g
`  G )  e. 
_V
183 hashsng 12139 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 0g `  G )  e.  _V  ->  ( # `
 { ( 0g
`  G ) } )  =  1 )
184182, 183ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( # `  { ( 0g `  G ) } )  =  1
185181, 184syl6reqr 2494 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( # `  { ( 0g `  G ) } )  =  (
# `  ( T `  q ) ) )
186 snfi 7393 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  { ( 0g `  G ) }  e.  Fin
187 hashen 12121 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( { ( 0g `  G ) }  e.  Fin  /\  ( T `  q )  e.  Fin )  ->  ( ( # `  { ( 0g `  G ) } )  =  ( # `  ( T `  q )
)  <->  { ( 0g `  G ) }  ~~  ( T `  q ) ) )
188186, 151, 187sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( ( # `  {
( 0g `  G
) } )  =  ( # `  ( T `  q )
)  <->  { ( 0g `  G ) }  ~~  ( T `  q ) ) )
189185, 188mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  { ( 0g `  G ) }  ~~  ( T `  q ) )
190 fisseneq 7527 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( T `  q
)  e.  Fin  /\  { ( 0g `  G
) }  C_  ( T `  q )  /\  { ( 0g `  G ) }  ~~  ( T `  q ) )  ->  { ( 0g `  G ) }  =  ( T `  q ) )
191151, 155, 189, 190syl3anc 1218 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  { ( 0g `  G ) }  =  ( T `  q ) )
192113subg0cl 15692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( G DProd  ( T  |`  D ) )  e.  (SubGrp `  G )  ->  ( 0g `  G
)  e.  ( G DProd 
( T  |`  D ) ) )
193137, 192syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( 0g `  G
)  e.  ( G DProd 
( T  |`  D ) ) )
194193adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( 0g `  G
)  e.  ( G DProd 
( T  |`  D ) ) )
195194snssd 4021 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  { ( 0g `  G ) }  C_  ( G DProd  ( T  |`  D ) ) )
196191, 195eqsstr3d 3394 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( T `  q
)  C_  ( G DProd  ( T  |`  D )
) )
197150, 196sylan2b 475 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  q  e.  ( A  \  D ) )  ->  ( T `  q )  C_  ( G DProd  ( T  |`  D ) ) )
198149, 197eqsstrd 3393 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  q  e.  ( A  \  D ) )  ->  ( ( T  |`  ( A  \  D ) ) `  q )  C_  ( G DProd  ( T  |`  D ) ) )
199140, 147, 137, 198dprdlub 16526 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( G DProd  ( T  |`  ( A  \  D
) ) )  C_  ( G DProd  ( T  |`  D ) ) )
200 eqid 2443 . . . . . . . . . . . . . . . . . . . . 21  |-  ( LSSum `  G )  =  (
LSSum `  G )
201200lsmss2 16168 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( G DProd  ( T  |`  D ) )  e.  (SubGrp `  G )  /\  ( G DProd  ( T  |`  ( A  \  D
) ) )  e.  (SubGrp `  G )  /\  ( G DProd  ( T  |`  ( A  \  D
) ) )  C_  ( G DProd  ( T  |`  D ) ) )  ->  ( ( G DProd 
( T  |`  D ) ) ( LSSum `  G
) ( G DProd  ( T  |`  ( A  \  D ) ) ) )  =  ( G DProd 
( T  |`  D ) ) )
202137, 142, 199, 201syl3anc 1218 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( G DProd  ( T  |`  D ) ) ( LSSum `  G )
( G DProd  ( T  |`  ( A  \  D
) ) ) )  =  ( G DProd  ( T  |`  D ) ) )
203 disjdif 3754 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( D  i^i  ( A  \  D ) )  =  (/)
204203a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( D  i^i  ( A  \  D ) )  =  (/) )
205 undif2 3758 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( D  u.  ( A  \  D ) )  =  ( D  u.  A
)
206 ssequn1 3529 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( D 
C_  A  <->  ( D  u.  A )  =  A )
20797, 206sylib 196 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( D  u.  A
)  =  A )
208205, 207syl5req 2488 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  =  ( D  u.  ( A  \  D ) ) )
2094, 204, 208, 200, 2dprdsplit 16550 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( G DProd  T )  =  ( ( G DProd 
( T  |`  D ) ) ( LSSum `  G
) ( G DProd  ( T  |`  ( A  \  D ) ) ) ) )
2101simprd 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( G DProd  T )  =  B )
211209, 210eqtr3d 2477 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( G DProd  ( T  |`  D ) ) ( LSSum `  G )
( G DProd  ( T  |`  ( A  \  D
) ) ) )  =  B )
212202, 211eqtr3d 2477 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( G DProd  ( T  |`  D ) )  =  B )
213135, 212jca 532 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( G dom DProd  ( T  |`  D )  /\  ( G DProd  ( T  |`  D ) )  =  B ) )
214213adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  ( G dom DProd  ( T  |`  D )  /\  ( G DProd  ( T  |`  D ) )  =  B ) )
2154, 97, 102syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( T  |`  D ) : D --> (SubGrp `  G ) )
216215, 104syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  ( T  |`  D )  =  D )
217216adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  dom  ( T  |`  D )  =  D )
21897sselda 3359 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  q  e.  D )  ->  q  e.  A )
219218, 42syldan 470 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  q  e.  D )  ->  C  e.  NN0 )
220219adantlr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  Prime )  /\  q  e.  D )  ->  C  e.  NN0 )
221 fvres 5707 . . . . . . . . . . . . . . . . . . . 20  |-  ( q  e.  D  ->  (
( T  |`  D ) `
 q )  =  ( T `  q
) )
222221adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  q  e.  D )  ->  (
( T  |`  D ) `
 q )  =  ( T `  q
) )
223222fveq2d 5698 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  q  e.  D )  ->  ( # `
 ( ( T  |`  D ) `  q
) )  =  (
# `  ( T `  q ) ) )
224218, 38syldan 470 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  q  e.  D )  ->  ( # `
 ( T `  q ) )  =  ( q ^ C
) )
225223, 224eqtrd 2475 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  q  e.  D )  ->  ( # `
 ( ( T  |`  D ) `  q
) )  =  ( q ^ C ) )
226225adantlr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  Prime )  /\  q  e.  D )  ->  ( # `
 ( ( T  |`  D ) `  q
) )  =  ( q ^ C ) )
227 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  x  e.  Prime )
228 fzfid 11798 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 1 ... ( # `
 B ) )  e.  Fin )
229 prmnn 13769 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  Prime  ->  w  e.  NN )
2302293ad2ant2 1010 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  w  e.  Prime  /\  w  ||  ( # `
 B ) )  ->  w  e.  NN )
231 prmz 13770 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  Prime  ->  w  e.  ZZ )
232 dvdsle 13581 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( w  e.  ZZ  /\  ( # `  B )  e.  NN )  -> 
( w  ||  ( # `
 B )  ->  w  <_  ( # `  B
) ) )
233231, 50, 232syl2anr 478 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  w  e.  Prime )  ->  ( w  ||  ( # `  B
)  ->  w  <_  (
# `  B )
) )
2342333impia 1184 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  w  e.  Prime  /\  w  ||  ( # `
 B ) )  ->  w  <_  ( # `
 B ) )
23550nnzd 10749 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( # `  B
)  e.  ZZ )
2362353ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  w  e.  Prime  /\  w  ||  ( # `
 B ) )  ->  ( # `  B
)  e.  ZZ )
237 fznn 11529 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
# `  B )  e.  ZZ  ->  ( w  e.  ( 1 ... ( # `
 B ) )  <-> 
( w  e.  NN  /\  w  <_  ( # `  B
) ) ) )
238236, 237syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  w  e.  Prime  /\  w  ||  ( # `
 B ) )  ->  ( w  e.  ( 1 ... ( # `
 B ) )  <-> 
( w  e.  NN  /\  w  <_  ( # `  B
) ) ) )
239230, 234, 238mpbir2and 913 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  w  e.  Prime  /\  w  ||  ( # `
 B ) )  ->  w  e.  ( 1 ... ( # `  B ) ) )
240239rabssdv 3435 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  { w  e.  Prime  |  w  ||  ( # `  B ) }  C_  ( 1 ... ( # `
 B ) ) )
241128, 240syl5eqss 3403 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  D  C_  ( 1 ... ( # `  B
) ) )
242 ssfi 7536 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1 ... ( # `
 B ) )  e.  Fin  /\  D  C_  ( 1 ... ( # `
 B ) ) )  ->  D  e.  Fin )
243228, 241, 242syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  D  e.  Fin )
244243adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  D  e.  Fin )
2457, 8, 125, 126, 127, 131, 128, 133, 214, 217, 220, 226, 227, 244ablfac1eulem 16576 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  Prime )  ->  -.  x  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { x }
) ) ) ) )
246245ralrimiva 2802 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. x  e.  Prime  -.  x  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
x } ) ) ) ) )
247246adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  q  e.  A )  ->  A. x  e.  Prime  -.  x  ||  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
x } ) ) ) ) )
248 id 22 . . . . . . . . . . . . . . . 16  |-  ( x  =  q  ->  x  =  q )
249 sneq 3890 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  q  ->  { x }  =  { q } )
250249difeq2d 3477 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  q  ->  ( D  \  { x }
)  =  ( D 
\  { q } ) )
251250reseq2d 5113 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  q  ->  (
( T  |`  D )  |`  ( D  \  {
x } ) )  =  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )
252251oveq2d 6110 . . . . . . . . . . . . . . . . 17  |-  ( x  =  q  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { x }
) ) )  =  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) )
253252fveq2d 5698 . . . . . . . . . . . . . . . 16  |-  ( x  =  q  ->  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
x } ) ) ) )  =  (
# `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) )
254248, 253breq12d 4308 . . . . . . . . . . . . . . 15  |-  ( x  =  q  ->  (
x  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { x }
) ) ) )  <-> 
q  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) ) )
255254notbid 294 . . . . . . . . . . . . . 14  |-  ( x  =  q  ->  ( -.  x  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
x } ) ) ) )  <->  -.  q  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) ) )
256255rspcv 3072 . . . . . . . . . . . . 13  |-  ( q  e.  Prime  ->  ( A. x  e.  Prime  -.  x  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { x }
) ) ) )  ->  -.  q  ||  ( # `  ( G DProd 
( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) ) )
25739, 247, 256sylc 60 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  -.  q  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )
258 coprm 13789 . . . . . . . . . . . . 13  |-  ( ( q  e.  Prime  /\  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  e.  ZZ )  ->  ( -.  q  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) )  <-> 
( q  gcd  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) )  =  1 ) )
25939, 124, 258syl2anc 661 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  ( -.  q  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  <->  ( q  gcd  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  =  1 ) )
260257, 259mpbid 210 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  (
q  gcd  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  =  1 )
261 rpexp1i 13810 . . . . . . . . . . . 12  |-  ( ( q  e.  ZZ  /\  ( # `  ( G DProd 
( ( T  |`  D )  |`  ( D  \  { q } ) ) ) )  e.  ZZ  /\  (
q  pCnt  ( # `  B
) )  e.  NN0 )  ->  ( ( q  gcd  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  =  1  -> 
( ( q ^
( q  pCnt  ( # `
 B ) ) )  gcd  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) )  =  1 ) )
26241, 124, 52, 261syl3anc 1218 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  (
( q  gcd  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) )  =  1  ->  ( (
q ^ ( q 
pCnt  ( # `  B
) ) )  gcd  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  =  1 ) )
263260, 262mpd 15 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  (
( q ^ (
q  pCnt  ( # `  B
) ) )  gcd  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  =  1 )
264 coprmdvds2 13792 . . . . . . . . . 10  |-  ( ( ( ( q ^
( q  pCnt  ( # `
 B ) ) )  e.  ZZ  /\  ( # `  ( G DProd 
( ( T  |`  D )  |`  ( D  \  { q } ) ) ) )  e.  ZZ  /\  ( # `
 B )  e.  ZZ )  /\  (
( q ^ (
q  pCnt  ( # `  B
) ) )  gcd  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  =  1 )  ->  ( ( ( q ^ ( q 
pCnt  ( # `  B
) ) )  ||  ( # `  B )  /\  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) 
||  ( # `  B
) )  ->  (
( q ^ (
q  pCnt  ( # `  B
) ) )  x.  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  ||  ( # `  B ) ) )
26578, 124, 57, 263, 264syl31anc 1221 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  (
( ( q ^
( q  pCnt  ( # `
 B ) ) )  ||  ( # `  B )  /\  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  ||  ( # `
 B ) )  ->  ( ( q ^ ( q  pCnt  (
# `  B )
) )  x.  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) )  ||  ( # `  B ) ) )
26694, 112, 265mp2and 679 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  (
( q ^ (
q  pCnt  ( # `  B
) ) )  x.  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  ||  ( # `  B ) )
267 eqid 2443 . . . . . . . . . 10  |-  (Cntz `  G )  =  (Cntz `  G )
268 inss1 3573 . . . . . . . . . . . . . 14  |-  ( D  i^i  { q } )  C_  D
269268a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  q  e.  A )  ->  ( D  i^i  { q } )  C_  D )
270100, 105, 269dprdres 16528 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  ( G dom DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) )  /\  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  C_  ( G DProd  ( T  |`  D ) ) ) )
271270simpld 459 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  G dom DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )
272 dprdsubg 16524 . . . . . . . . . . 11  |-  ( G dom DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  e.  (SubGrp `  G )
)
273271, 272syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  e.  (SubGrp `  G )
)
274 inass 3563 . . . . . . . . . . . . 13  |-  ( ( D  i^i  { q } )  i^i  ( D  \  { q } ) )  =  ( D  i^i  ( { q }  i^i  ( D  \  { q } ) ) )
275 disjdif 3754 . . . . . . . . . . . . . 14  |-  ( { q }  i^i  ( D  \  { q } ) )  =  (/)
276275ineq2i 3552 . . . . . . . . . . . . 13  |-  ( D  i^i  ( { q }  i^i  ( D 
\  { q } ) ) )  =  ( D  i^i  (/) )
277 in0 3666 . . . . . . . . . . . . 13  |-  ( D  i^i  (/) )  =  (/)
278274, 276, 2773eqtri 2467 . . . . . . . . . . . 12  |-  ( ( D  i^i  { q } )  i^i  ( D  \  { q } ) )  =  (/)
279278a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  (
( D  i^i  {
q } )  i^i  ( D  \  {
q } ) )  =  (/) )
280100, 105, 269, 106, 279, 113dprddisj2 16540 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  (
( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  i^i  ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  =  {
( 0g `  G
) } )
281100, 105, 269, 106, 279, 267dprdcntz2 16539 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  C_  ( (Cntz `  G ) `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) )
2827dprdssv 16509 . . . . . . . . . . 11  |-  ( G DProd 
( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  C_  B
283 ssfi 7536 . . . . . . . . . . 11  |-  ( ( B  e.  Fin  /\  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) ) 
C_  B )  -> 
( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  e.  Fin )
28422, 282, 283sylancl 662 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  e. 
Fin )
285200, 113, 267, 273, 110, 280, 281, 284, 120lsmhash 16205 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( ( G DProd 
( ( T  |`  D )  |`  ( D  i^i  { q } ) ) ) (
LSSum `  G ) ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  =  ( (
# `  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  {
q } ) ) ) )  x.  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) ) )
286 inundif 3760 . . . . . . . . . . . . . 14  |-  ( ( D  i^i  { q } )  u.  ( D  \  { q } ) )  =  D
287286eqcomi 2447 . . . . . . . . . . . . 13  |-  D  =  ( ( D  i^i  { q } )  u.  ( D  \  {
q } ) )
288287a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  D  =  ( ( D  i^i  { q } )  u.  ( D 
\  { q } ) ) )
289103, 279, 288, 200, 100dprdsplit 16550 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( T  |`  D ) )  =  ( ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) ) (
LSSum `  G ) ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )
290212adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( T  |`  D ) )  =  B )
291289, 290eqtr3d 2477 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  (
( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) ) ( LSSum `  G )
( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) )  =  B )
292291fveq2d 5698 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( ( G DProd 
( ( T  |`  D )  |`  ( D  i^i  { q } ) ) ) (
LSSum `  G ) ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  =  ( # `  B ) )
293 snssi 4020 . . . . . . . . . . . . . . . . 17  |-  ( q  e.  D  ->  { q }  C_  D )
294293adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  { q }  C_  D )
295 dfss1 3558 . . . . . . . . . . . . . . . 16  |-  ( { q }  C_  D  <->  ( D  i^i  { q } )  =  {
q } )
296294, 295sylib 196 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  ( D  i^i  { q } )  =  { q } )
297296reseq2d 5113 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  (
( T  |`  D )  |`  ( D  i^i  {
q } ) )  =  ( ( T  |`  D )  |`  { q } ) )
298297oveq2d 6110 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  =  ( G DProd  ( ( T  |`  D )  |` 
{ q } ) ) )
299100adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  G dom DProd  ( T  |`  D ) )
300216ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  dom  ( T  |`  D )  =  D )
301 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  q  e.  D )
302299, 300, 301dpjlem 16553 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  ( G DProd  ( ( T  |`  D )  |`  { q } ) )  =  ( ( T  |`  D ) `  q
) )
303221adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  (
( T  |`  D ) `
 q )  =  ( T `  q
) )
304298, 302, 3033eqtrd 2479 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  =  ( T `  q
) )
305 simprr 756 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  -.  q  e.  D
)
306 disjsn 3939 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  i^i  { q } )  =  (/)  <->  -.  q  e.  D )
307305, 306sylibr 212 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( D  i^i  {
q } )  =  (/) )
308307reseq2d 5113 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( ( T  |`  D )  |`  ( D  i^i  { q } ) )  =  ( ( T  |`  D )  |`  (/) ) )
309 res0 5118 . . . . . . . . . . . . . . . 16  |-  ( ( T  |`  D )  |`  (/) )  =  (/)
310308, 309syl6eq 2491 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( ( T  |`  D )  |`  ( D  i^i  { q } ) )  =  (/) )
311310oveq2d 6110 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  =  ( G DProd  (/) ) )
312113dprd0 16531 . . . . . . . . . . . . . . . . 17  |-  ( G  e.  Grp  ->  ( G dom DProd  (/)  /\  ( G DProd  (/) )  =  { ( 0g `  G ) } ) )
31345, 312syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( G dom DProd  (/)  /\  ( G DProd 
(/) )  =  {
( 0g `  G
) } ) )
314313simprd 463 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G DProd  (/) )  =  { ( 0g `  G ) } )
315314adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( G DProd  (/) )  =  { ( 0g `  G ) } )
316311, 315, 1913eqtrd 2479 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  =  ( T `  q ) )
317316anassrs 648 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  q  e.  A )  /\  -.  q  e.  D )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  {
q } ) ) )  =  ( T `
 q ) )
318304, 317pm2.61dan 789 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  =  ( T `  q
) )
319318fveq2d 5698 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  i^i  {
q } ) ) ) )  =  (
# `  ( T `  q ) ) )
320319oveq1d 6109 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  (
( # `  ( G DProd 
( ( T  |`  D )  |`  ( D  i^i  { q } ) ) ) )  x.  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  =  ( (
# `  ( T `  q ) )  x.  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) ) )
321285, 292, 3203eqtr3d 2483 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 B )  =  ( ( # `  ( T `  q )
)  x.  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) ) )
322266, 321breqtrd 4319 . . . . . . 7  |-  ( (
ph  /\  q  e.  A )  ->  (
( q ^ (
q  pCnt  ( # `  B
) ) )  x.  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  ||  ( (
# `  ( T `  q ) )  x.  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) ) )
323123nnne0d 10369 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  =/=  0
)
324 dvdsmulcr 13565 . . . . . . . 8  |-  ( ( ( q ^ (
q  pCnt  ( # `  B
) ) )  e.  ZZ  /\  ( # `  ( T `  q
) )  e.  ZZ  /\  ( ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) )  e.  ZZ  /\  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  =/=  0
) )  ->  (
( ( q ^
( q  pCnt  ( # `
 B ) ) )  x.  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) )  ||  ( ( # `  ( T `  q )
)  x.  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) )  <->  ( q ^ ( q  pCnt  (
# `  B )
) )  ||  ( # `
 ( T `  q ) ) ) )
32578, 73, 124, 323, 324syl112anc 1222 . . . . . . 7  |-  ( (
ph  /\  q  e.  A )  ->  (
( ( q ^
( q  pCnt  ( # `
 B ) ) )  x.  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) )  ||  ( ( # `  ( T `  q )
)  x.  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) )  <->  ( q ^ ( q  pCnt  (
# `  B )
) )  ||  ( # `
 ( T `  q ) ) ) )
326322, 325mpbid 210 . . . . . 6  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ ( q 
pCnt  ( # `  B
) ) )  ||  ( # `  ( T `
 q ) ) )
327 dvdseq 13583 . . . . . 6  |-  ( ( ( ( # `  ( T `  q )
)  e.  NN0  /\  ( q ^ (
q  pCnt  ( # `  B
) ) )  e. 
NN0 )  /\  (
( # `  ( T `
 q ) ) 
||  ( q ^
( q  pCnt  ( # `
 B ) ) )  /\  ( q ^ ( q  pCnt  (
# `  B )
) )  ||  ( # `
 ( T `  q ) ) ) )  ->  ( # `  ( T `  q )
)  =  ( q ^ ( q  pCnt  (
# `  B )
) ) )
32872, 92, 65, 326, 327syl22anc 1219 . . . . 5  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  =  ( q ^ (
q  pCnt  ( # `  B
) ) ) )
3297, 8, 9, 10, 11, 12ablfac1a 16573 . . . . 5  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( S `  q ) )  =  ( q ^ (
q  pCnt  ( # `  B
) ) ) )
330328, 329eqtr4d 2478 . . . 4  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  =  ( # `  ( S `  q )
) )
331 hashen 12121 . . . . 5  |-  ( ( ( T `  q
)  e.  Fin  /\  ( S `  q )  e.  Fin )  -> 
( ( # `  ( T `  q )
)  =  ( # `  ( S `  q
) )  <->  ( T `  q )  ~~  ( S `  q )
) )
33233, 27, 331syl2anc 661 . . . 4  |-  ( (
ph  /\  q  e.  A )  ->  (
( # `  ( T `
 q ) )  =  ( # `  ( S `  q )
)  <->  ( T `  q )  ~~  ( S `  q )
) )
333330, 332mpbid 210 . . 3  |-  ( (
ph  /\  q  e.  A )  ->  ( T `  q )  ~~  ( S `  q
) )
334 fisseneq 7527 . . 3  |-  ( ( ( S `  q
)  e.  Fin  /\  ( T `  q ) 
C_  ( S `  q )  /\  ( T `  q )  ~~  ( S `  q
) )  ->  ( T `  q )  =  ( S `  q ) )
33527, 91, 333, 334syl3anc 1218 . 2  |-  ( (
ph  /\  q  e.  A )  ->  ( T `  q )  =  ( S `  q ) )
3366, 21, 335eqfnfvd 5803 1  |-  ( ph  ->  T  =  S )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756    =/= wne 2609   A.wral 2718   {crab 2722   _Vcvv 2975    \ cdif 3328    u. cun 3329    i^i cin 3330    C_ wss 3331   (/)c0 3640   {csn 3880   class class class wbr 4295    e. cmpt 4353   dom cdm 4843    |` cres 4845    Fn wfn 5416   -->wf 5417   ` cfv 5421  (class class class)co 6094    ~~ cen 7310   Fincfn 7313   0cc0 9285   1c1 9286    x. cmul 9290    <_ cle 9422   NNcn 10325   NN0cn0 10582   ZZcz 10649   ZZ>=cuz 10864   ...cfz 11440   ^cexp 11868   #chash 12106    || cdivides 13538    gcd cgcd 13693   Primecprime 13766    pCnt cpc 13906   Basecbs 14177   0gc0g 14381   Grpcgrp 15413  SubGrpcsubg 15678  Cntzccntz 15836   odcod 16031   LSSumclsm 16136   Abelcabel 16281   DProd cdprd 16478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4406  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375  ax-inf2 7850  ax-cnex 9341  ax-resscn 9342  ax-1cn 9343  ax-icn 9344  ax-addcl 9345  ax-addrcl 9346  ax-mulcl 9347  ax-mulrcl 9348  ax-mulcom 9349  ax-addass 9350  ax-mulass 9351  ax-distr 9352  ax-i2m1 9353  ax-1ne0 9354  ax-1rid 9355  ax-rnegex 9356  ax-rrecex 9357  ax-cnre 9358  ax-pre-lttri 9359  ax-pre-lttrn 9360  ax-pre-ltadd 9361  ax-pre-mulgt0 9362  ax-pre-sup 9363
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-nel 2612  df-ral 2723  df-rex 2724  df-reu 2725  df-rmo 2726  df-rab 2727  df-v 2977  df-sbc 3190  df-csb 3292  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-pss 3347  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-tp 3885  df-op 3887  df-uni 4095  df-int 4132  df-iun 4176  df-iin 4177  df-disj 4266  df-br 4296  df-opab 4354  df-mpt 4355  df-tr 4389  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-se 4683  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-isom 5430  df-riota 6055  df-ov 6097  df-oprab 6098  df-mpt2 6099  df-of 6323  df-om 6480  df-1st 6580  df-2nd 6581  df-supp 6694  df-tpos 6748  df-recs 6835  df-rdg 6869  df-1o 6923  df-2o 6924  df-oadd 6927  df-omul 6928  df-er 7104  df-ec 7106  df-qs 7110  df-map 7219  df-ixp 7267  df-en 7314  df-dom 7315  df-sdom 7316  df-fin 7317  df-fsupp 7624  df-sup 7694  df-oi 7727  df-card 8112  df-acn 8115  df-cda 8340  df-pnf 9423  df-mnf 9424  df-xr 9425  df-ltxr 9426  df-le 9427  df-sub 9600  df-neg 9601  df-div 9997  df-nn 10326  df-2 10383  df-3 10384  df-n0 10583  df-z 10650  df-uz 10865  df-q 10957  df-rp 10995  df-fz 11441  df-fzo 11552  df-fl 11645  df-mod 11712  df-seq 11810  df-exp 11869  df-fac 12055  df-bc 12082  df-hash 12107  df-cj 12591  df-re 12592  df-im 12593  df-sqr 12727  df-abs 12728  df-clim 12969  df-sum 13167  df-dvds 13539  df-gcd 13694  df-prm 13767  df-pc 13907  df-ndx 14180  df-slot 14181  df-base 14182  df-sets 14183  df-ress 14184  df-plusg 14254  df-0g 14383  df-gsum 14384  df-mre 14527  df-mrc 14528  df-acs 14530  df-mnd 15418  df-mhm 15467  df-submnd 15468  df-grp 15548  df-minusg 15549  df-sbg 15550  df-mulg 15551  df-subg 15681  df-eqg 15683  df-ghm 15748  df-gim 15790  df-ga 15811  df-cntz 15838  df-oppg 15864  df-od 16035  df-lsm 16138  df-pj1 16139  df-cmn 16282  df-abl 16283  df-dprd 16480
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator