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

Theorem ablfac1eu 15324
Description: The factorization of ablfac1b 15321 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 445 . . . 4  |-  ( ph  ->  G dom DProd  T )
3 ablfac1eu.2 . . . 4  |-  ( ph  ->  dom  T  =  A )
42, 3dprdf2 15258 . . 3  |-  ( ph  ->  T : A --> (SubGrp `  G ) )
5 ffn 5405 . . 3  |-  ( T : A --> (SubGrp `  G )  ->  T  Fn  A )
64, 5syl 15 . 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 15321 . . . 4  |-  ( ph  ->  G dom DProd  S )
14 fvex 5555 . . . . . . . 8  |-  ( Base `  G )  e.  _V
157, 14eqeltri 2366 . . . . . . 7  |-  B  e. 
_V
1615rabex 4181 . . . . . 6  |-  { x  e.  B  |  ( O `  x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) }  e.  _V
1716, 9dmmpti 5389 . . . . 5  |-  dom  S  =  A
1817a1i 10 . . . 4  |-  ( ph  ->  dom  S  =  A )
1913, 18dprdf2 15258 . . 3  |-  ( ph  ->  S : A --> (SubGrp `  G ) )
20 ffn 5405 . . 3  |-  ( S : A --> (SubGrp `  G )  ->  S  Fn  A )
2119, 20syl 15 . 2  |-  ( ph  ->  S  Fn  A )
2211adantr 451 . . . 4  |-  ( (
ph  /\  q  e.  A )  ->  B  e.  Fin )
23 ffvelrn 5679 . . . . . 6  |-  ( ( S : A --> (SubGrp `  G )  /\  q  e.  A )  ->  ( S `  q )  e.  (SubGrp `  G )
)
2419, 23sylan 457 . . . . 5  |-  ( (
ph  /\  q  e.  A )  ->  ( S `  q )  e.  (SubGrp `  G )
)
257subgss 14638 . . . . 5  |-  ( ( S `  q )  e.  (SubGrp `  G
)  ->  ( S `  q )  C_  B
)
2624, 25syl 15 . . . 4  |-  ( (
ph  /\  q  e.  A )  ->  ( S `  q )  C_  B )
27 ssfi 7099 . . . 4  |-  ( ( B  e.  Fin  /\  ( S `  q ) 
C_  B )  -> 
( S `  q
)  e.  Fin )
2822, 26, 27syl2anc 642 . . 3  |-  ( (
ph  /\  q  e.  A )  ->  ( S `  q )  e.  Fin )
29 ffvelrn 5679 . . . . . . 7  |-  ( ( T : A --> (SubGrp `  G )  /\  q  e.  A )  ->  ( T `  q )  e.  (SubGrp `  G )
)
304, 29sylan 457 . . . . . 6  |-  ( (
ph  /\  q  e.  A )  ->  ( T `  q )  e.  (SubGrp `  G )
)
317subgss 14638 . . . . . 6  |-  ( ( T `  q )  e.  (SubGrp `  G
)  ->  ( T `  q )  C_  B
)
3230, 31syl 15 . . . . 5  |-  ( (
ph  /\  q  e.  A )  ->  ( T `  q )  C_  B )
3330adantr 451 . . . . . . 7  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( T `  q )  e.  (SubGrp `  G )
)
34 ssfi 7099 . . . . . . . . 9  |-  ( ( B  e.  Fin  /\  ( T `  q ) 
C_  B )  -> 
( T `  q
)  e.  Fin )
3522, 32, 34syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  ( T `  q )  e.  Fin )
3635adantr 451 . . . . . . 7  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( T `  q )  e.  Fin )
37 simpr 447 . . . . . . 7  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  x  e.  ( T `  q
) )
388odsubdvds 14898 . . . . . . 7  |-  ( ( ( T `  q
)  e.  (SubGrp `  G )  /\  ( T `  q )  e.  Fin  /\  x  e.  ( T `  q
) )  ->  ( O `  x )  ||  ( # `  ( T `  q )
) )
3933, 36, 37, 38syl3anc 1182 . . . . . 6  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( O `  x )  ||  ( # `  ( T `  q )
) )
40 ablfac1eu.4 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  =  ( q ^ C
) )
4112sselda 3193 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  q  e.  Prime )
42 prmz 12778 . . . . . . . . . 10  |-  ( q  e.  Prime  ->  q  e.  ZZ )
4341, 42syl 15 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  q  e.  ZZ )
44 ablfac1eu.3 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  C  e.  NN0 )
4544nn0zd 10131 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  C  e.  ZZ )
46 ablgrp 15110 . . . . . . . . . . . . . . . 16  |-  ( G  e.  Abel  ->  G  e. 
Grp )
4710, 46syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  G  e.  Grp )
487grpbn0 14527 . . . . . . . . . . . . . . 15  |-  ( G  e.  Grp  ->  B  =/=  (/) )
4947, 48syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  =/=  (/) )
50 hashnncl 11370 . . . . . . . . . . . . . . 15  |-  ( B  e.  Fin  ->  (
( # `  B )  e.  NN  <->  B  =/=  (/) ) )
5111, 50syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( # `  B
)  e.  NN  <->  B  =/=  (/) ) )
5249, 51mpbird 223 . . . . . . . . . . . . 13  |-  ( ph  ->  ( # `  B
)  e.  NN )
5352adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 B )  e.  NN )
5441, 53pccld 12919 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  (
q  pCnt  ( # `  B
) )  e.  NN0 )
5554nn0zd 10131 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  (
q  pCnt  ( # `  B
) )  e.  ZZ )
567lagsubg 14695 . . . . . . . . . . . . 13  |-  ( ( ( T `  q
)  e.  (SubGrp `  G )  /\  B  e.  Fin )  ->  ( # `
 ( T `  q ) )  ||  ( # `  B ) )
5730, 22, 56syl2anc 642 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  ||  ( # `  B ) )
5840, 57eqbrtrrd 4061 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ C ) 
||  ( # `  B
) )
5953nnzd 10132 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 B )  e.  ZZ )
60 pcdvdsb 12937 . . . . . . . . . . . 12  |-  ( ( q  e.  Prime  /\  ( # `
 B )  e.  ZZ  /\  C  e. 
NN0 )  ->  ( C  <_  ( q  pCnt  (
# `  B )
)  <->  ( q ^ C )  ||  ( # `
 B ) ) )
6141, 59, 44, 60syl3anc 1182 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  ( C  <_  ( q  pCnt  (
# `  B )
)  <->  ( q ^ C )  ||  ( # `
 B ) ) )
6258, 61mpbird 223 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  C  <_  ( q  pCnt  ( # `
 B ) ) )
63 eluz2 10252 . . . . . . . . . 10  |-  ( ( q  pCnt  ( # `  B
) )  e.  (
ZZ>= `  C )  <->  ( C  e.  ZZ  /\  ( q 
pCnt  ( # `  B
) )  e.  ZZ  /\  C  <_  ( q  pCnt  ( # `  B
) ) ) )
6445, 55, 62, 63syl3anbrc 1136 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  (
q  pCnt  ( # `  B
) )  e.  (
ZZ>= `  C ) )
65 dvdsexp 12600 . . . . . . . . 9  |-  ( ( q  e.  ZZ  /\  C  e.  NN0  /\  (
q  pCnt  ( # `  B
) )  e.  (
ZZ>= `  C ) )  ->  ( q ^ C )  ||  (
q ^ ( q 
pCnt  ( # `  B
) ) ) )
6643, 44, 64, 65syl3anc 1182 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ C ) 
||  ( q ^
( q  pCnt  ( # `
 B ) ) ) )
6740, 66eqbrtrd 4059 . . . . . . 7  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  ||  ( q ^ (
q  pCnt  ( # `  B
) ) ) )
6867adantr 451 . . . . . 6  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( # `
 ( T `  q ) )  ||  ( q ^ (
q  pCnt  ( # `  B
) ) ) )
6932sselda 3193 . . . . . . . . 9  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  x  e.  B )
707, 8odcl 14867 . . . . . . . . 9  |-  ( x  e.  B  ->  ( O `  x )  e.  NN0 )
7169, 70syl 15 . . . . . . . 8  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( O `  x )  e.  NN0 )
7271nn0zd 10131 . . . . . . 7  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( O `  x )  e.  ZZ )
73 hashcl 11366 . . . . . . . . . 10  |-  ( ( T `  q )  e.  Fin  ->  ( # `
 ( T `  q ) )  e. 
NN0 )
7435, 73syl 15 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  e. 
NN0 )
7574nn0zd 10131 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  e.  ZZ )
7675adantr 451 . . . . . . 7  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( # `
 ( T `  q ) )  e.  ZZ )
77 prmnn 12777 . . . . . . . . . . 11  |-  ( q  e.  Prime  ->  q  e.  NN )
7841, 77syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  q  e.  NN )
7978, 54nnexpcld 11282 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ ( q 
pCnt  ( # `  B
) ) )  e.  NN )
8079nnzd 10132 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ ( q 
pCnt  ( # `  B
) ) )  e.  ZZ )
8180adantr 451 . . . . . . 7  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  (
q ^ ( q 
pCnt  ( # `  B
) ) )  e.  ZZ )
82 dvdstr 12578 . . . . . . 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
) ) ) ) )
8372, 76, 81, 82syl3anc 1182 . . . . . 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
) ) ) ) )
8439, 68, 83mp2and 660 . . . . 5  |-  ( ( ( ph  /\  q  e.  A )  /\  x  e.  ( T `  q
) )  ->  ( O `  x )  ||  ( q ^ (
q  pCnt  ( # `  B
) ) ) )
8532, 84ssrabdv 3265 . . . 4  |-  ( (
ph  /\  q  e.  A )  ->  ( T `  q )  C_ 
{ x  e.  B  |  ( O `  x )  ||  (
q ^ ( q 
pCnt  ( # `  B
) ) ) } )
86 id 19 . . . . . . . . 9  |-  ( p  =  q  ->  p  =  q )
87 oveq1 5881 . . . . . . . . 9  |-  ( p  =  q  ->  (
p  pCnt  ( # `  B
) )  =  ( q  pCnt  ( # `  B
) ) )
8886, 87oveq12d 5892 . . . . . . . 8  |-  ( p  =  q  ->  (
p ^ ( p 
pCnt  ( # `  B
) ) )  =  ( q ^ (
q  pCnt  ( # `  B
) ) ) )
8988breq2d 4051 . . . . . . 7  |-  ( p  =  q  ->  (
( O `  x
)  ||  ( p ^ ( p  pCnt  (
# `  B )
) )  <->  ( O `  x )  ||  (
q ^ ( q 
pCnt  ( # `  B
) ) ) ) )
9089rabbidv 2793 . . . . . 6  |-  ( p  =  q  ->  { x  e.  B  |  ( O `  x )  ||  ( p ^ (
p  pCnt  ( # `  B
) ) ) }  =  { x  e.  B  |  ( O `
 x )  ||  ( q ^ (
q  pCnt  ( # `  B
) ) ) } )
9190, 9, 16fvmpt3i 5621 . . . . 5  |-  ( q  e.  A  ->  ( S `  q )  =  { x  e.  B  |  ( O `  x )  ||  (
q ^ ( q 
pCnt  ( # `  B
) ) ) } )
9291adantl 452 . . . 4  |-  ( (
ph  /\  q  e.  A )  ->  ( S `  q )  =  { x  e.  B  |  ( O `  x )  ||  (
q ^ ( q 
pCnt  ( # `  B
) ) ) } )
9385, 92sseqtr4d 3228 . . 3  |-  ( (
ph  /\  q  e.  A )  ->  ( T `  q )  C_  ( S `  q
) )
9479nnnn0d 10034 . . . . . 6  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ ( q 
pCnt  ( # `  B
) ) )  e. 
NN0 )
95 pcdvds 12932 . . . . . . . . . 10  |-  ( ( q  e.  Prime  /\  ( # `
 B )  e.  NN )  ->  (
q ^ ( q 
pCnt  ( # `  B
) ) )  ||  ( # `  B ) )
9641, 53, 95syl2anc 642 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ ( q 
pCnt  ( # `  B
) ) )  ||  ( # `  B ) )
972adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  q  e.  A )  ->  G dom DProd  T )
983adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  q  e.  A )  ->  dom  T  =  A )
99 ablfac1.2 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  D  C_  A )
10099adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  q  e.  A )  ->  D  C_  A )
10197, 98, 100dprdres 15279 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  q  e.  A )  ->  ( G dom DProd  ( T  |`  D )  /\  ( G DProd  ( T  |`  D ) )  C_  ( G DProd  T ) ) )
102101simpld 445 . . . . . . . . . . . . 13  |-  ( (
ph  /\  q  e.  A )  ->  G dom DProd  ( T  |`  D ) )
1034adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  q  e.  A )  ->  T : A --> (SubGrp `  G )
)
104 fssres 5424 . . . . . . . . . . . . . . 15  |-  ( ( T : A --> (SubGrp `  G )  /\  D  C_  A )  ->  ( T  |`  D ) : D --> (SubGrp `  G )
)
105103, 100, 104syl2anc 642 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  q  e.  A )  ->  ( T  |`  D ) : D --> (SubGrp `  G )
)
106 fdm 5409 . . . . . . . . . . . . . 14  |-  ( ( T  |`  D ) : D --> (SubGrp `  G )  ->  dom  ( T  |`  D )  =  D )
107105, 106syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  q  e.  A )  ->  dom  ( T  |`  D )  =  D )
108 difss 3316 . . . . . . . . . . . . . 14  |-  ( D 
\  { q } )  C_  D
109108a1i 10 . . . . . . . . . . . . 13  |-  ( (
ph  /\  q  e.  A )  ->  ( D  \  { q } )  C_  D )
110102, 107, 109dprdres 15279 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  ( G dom DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) )  /\  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  C_  ( G DProd  ( T  |`  D ) ) ) )
111110simpld 445 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  G dom DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )
112 dprdsubg 15275 . . . . . . . . . . 11  |-  ( G dom DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  e.  (SubGrp `  G )
)
113111, 112syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  e.  (SubGrp `  G )
)
1147lagsubg 14695 . . . . . . . . . 10  |-  ( ( ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) )  e.  (SubGrp `  G )  /\  B  e.  Fin )  ->  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  ||  ( # `
 B ) )
115113, 22, 114syl2anc 642 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  ||  ( # `
 B ) )
116 eqid 2296 . . . . . . . . . . . . . . 15  |-  ( 0g
`  G )  =  ( 0g `  G
)
117116subg0cl 14645 . . . . . . . . . . . . . 14  |-  ( ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  e.  (SubGrp `  G )  ->  ( 0g `  G
)  e.  ( G DProd 
( ( T  |`  D )  |`  ( D  \  { q } ) ) ) )
118113, 117syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  q  e.  A )  ->  ( 0g `  G )  e.  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) )
119 ne0i 3474 . . . . . . . . . . . . 13  |-  ( ( 0g `  G )  e.  ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) )  =/=  (/) )
120118, 119syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  =/=  (/) )
1217dprdssv 15267 . . . . . . . . . . . . . 14  |-  ( G DProd 
( ( T  |`  D )  |`  ( D  \  { q } ) ) )  C_  B
122 ssfi 7099 . . . . . . . . . . . . . 14  |-  ( ( B  e.  Fin  /\  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) 
C_  B )  -> 
( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  e.  Fin )
12322, 121, 122sylancl 643 . . . . . . . . . . . . 13  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  e. 
Fin )
124 hashnncl 11370 . . . . . . . . . . . . 13  |-  ( ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  e. 
Fin  ->  ( ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  e.  NN  <->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )  =/=  (/) ) )
125123, 124syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  (
( # `  ( G DProd 
( ( T  |`  D )  |`  ( D  \  { q } ) ) ) )  e.  NN  <->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) )  =/=  (/) ) )
126120, 125mpbird 223 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  e.  NN )
127126nnzd 10132 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  e.  ZZ )
128 eqid 2296 . . . . . . . . . . . . . . . 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
) ) ) } )
12910adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  G  e.  Abel )
13011adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  B  e.  Fin )
131 ablfac1c.d . . . . . . . . . . . . . . . . . 18  |-  D  =  { w  e.  Prime  |  w  ||  ( # `  B ) }
132 ssrab2 3271 . . . . . . . . . . . . . . . . . 18  |-  { w  e.  Prime  |  w  ||  ( # `  B ) }  C_  Prime
133131, 132eqsstri 3221 . . . . . . . . . . . . . . . . 17  |-  D  C_  Prime
134133a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  D  C_  Prime )
135 ssid 3210 . . . . . . . . . . . . . . . . 17  |-  D  C_  D
136135a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  D  C_  D
)
1372, 3, 99dprdres 15279 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( G dom DProd  ( T  |`  D )  /\  ( G DProd  ( T  |`  D ) )  C_  ( G DProd  T ) ) )
138137simpld 445 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  G dom DProd  ( T  |`  D ) )
139 dprdsubg 15275 . . . . . . . . . . . . . . . . . . . . 21  |-  ( G dom DProd  ( T  |`  D )  ->  ( G DProd  ( T  |`  D ) )  e.  (SubGrp `  G ) )
140138, 139syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( G DProd  ( T  |`  D ) )  e.  (SubGrp `  G )
)
141 difss 3316 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A 
\  D )  C_  A
142141a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( A  \  D
)  C_  A )
1432, 3, 142dprdres 15279 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( G dom DProd  ( T  |`  ( A  \  D
) )  /\  ( G DProd  ( T  |`  ( A  \  D ) ) )  C_  ( G DProd  T ) ) )
144143simpld 445 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  G dom DProd  ( T  |`  ( A  \  D
) ) )
145 dprdsubg 15275 . . . . . . . . . . . . . . . . . . . . 21  |-  ( G dom DProd  ( T  |`  ( A  \  D ) )  ->  ( G DProd  ( T  |`  ( A  \  D ) ) )  e.  (SubGrp `  G
) )
146144, 145syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( G DProd  ( T  |`  ( A  \  D
) ) )  e.  (SubGrp `  G )
)
147 fssres 5424 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( T : A --> (SubGrp `  G )  /\  ( A  \  D )  C_  A )  ->  ( T  |`  ( A  \  D ) ) : ( A  \  D
) --> (SubGrp `  G )
)
1484, 141, 147sylancl 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( T  |`  ( A  \  D ) ) : ( A  \  D ) --> (SubGrp `  G ) )
149 fdm 5409 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T  |`  ( A  \  D ) ) : ( A  \  D
) --> (SubGrp `  G )  ->  dom  ( T  |`  ( A  \  D ) )  =  ( A 
\  D ) )
150148, 149syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  dom  ( T  |`  ( A  \  D ) )  =  ( A 
\  D ) )
151 fvres 5558 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( q  e.  ( A  \  D )  ->  (
( T  |`  ( A  \  D ) ) `
 q )  =  ( T `  q
) )
152151adantl 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  q  e.  ( A  \  D ) )  ->  ( ( T  |`  ( A  \  D ) ) `  q )  =  ( T `  q ) )
153 eldif 3175 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( q  e.  ( A  \  D )  <->  ( q  e.  A  /\  -.  q  e.  D ) )
15435adantrr 697 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( T `  q
)  e.  Fin )
155116subg0cl 14645 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( T `  q )  e.  (SubGrp `  G
)  ->  ( 0g `  G )  e.  ( T `  q ) )
15630, 155syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  q  e.  A )  ->  ( 0g `  G )  e.  ( T `  q
) )
157156snssd 3776 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  q  e.  A )  ->  { ( 0g `  G ) }  C_  ( T `  q ) )
158157adantrr 697 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  { ( 0g `  G ) }  C_  ( T `  q ) )
15940adantrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( # `  ( T `
 q ) )  =  ( q ^ C ) )
16041adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  q  e.  A )  /\  C  e.  NN )  ->  q  e.  Prime )
161 iddvdsexp 12568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( q  e.  ZZ  /\  C  e.  NN )  ->  q  ||  ( q ^ C ) )
16243, 161sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  q  e.  A )  /\  C  e.  NN )  ->  q  ||  ( q ^ C
) )
16358adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  q  e.  A )  /\  C  e.  NN )  ->  (
q ^ C ) 
||  ( # `  B
) )
16440, 75eqeltrrd 2371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ C )  e.  ZZ )
165 dvdstr 12578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( q  e.  ZZ  /\  ( q ^ C
)  e.  ZZ  /\  ( # `  B )  e.  ZZ )  -> 
( ( q  ||  ( q ^ C
)  /\  ( q ^ C )  ||  ( # `
 B ) )  ->  q  ||  ( # `
 B ) ) )
16643, 164, 59, 165syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  q  e.  A )  ->  (
( q  ||  (
q ^ C )  /\  ( q ^ C )  ||  ( # `
 B ) )  ->  q  ||  ( # `
 B ) ) )
167166adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  q  e.  A )  /\  C  e.  NN )  ->  (
( q  ||  (
q ^ C )  /\  ( q ^ C )  ||  ( # `
 B ) )  ->  q  ||  ( # `
 B ) ) )
168162, 163, 167mp2and 660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  q  e.  A )  /\  C  e.  NN )  ->  q  ||  ( # `  B
) )
169 breq1 4042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( w  =  q  ->  (
w  ||  ( # `  B
)  <->  q  ||  ( # `
 B ) ) )
170169, 131elrab2 2938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( q  e.  D  <->  ( q  e.  Prime  /\  q  ||  ( # `  B ) ) )
171160, 168, 170sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  q  e.  A )  /\  C  e.  NN )  ->  q  e.  D )
172171ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  q  e.  A )  ->  ( C  e.  NN  ->  q  e.  D ) )
173172con3d 125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  q  e.  A )  ->  ( -.  q  e.  D  ->  -.  C  e.  NN ) )
174173impr 602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  -.  C  e.  NN )
17544adantrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  C  e.  NN0 )
176 elnn0 9983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( C  e.  NN0  <->  ( C  e.  NN  \/  C  =  0 ) )
177175, 176sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( C  e.  NN  \/  C  =  0
) )
178177ord 366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( -.  C  e.  NN  ->  C  = 
0 ) )
179174, 178mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  C  =  0 )
180179oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( q ^ C
)  =  ( q ^ 0 ) )
18178adantrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
q  e.  NN )
182181nncnd 9778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
q  e.  CC )
183182exp0d 11255 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( q ^ 0 )  =  1 )
184159, 180, 1833eqtrd 2332 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( # `  ( T `
 q ) )  =  1 )
185 fvex 5555 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0g
`  G )  e. 
_V
186 hashsng 11372 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 0g `  G )  e.  _V  ->  ( # `
 { ( 0g
`  G ) } )  =  1 )
187185, 186ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( # `  { ( 0g `  G ) } )  =  1
188184, 187syl6reqr 2347 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( # `  { ( 0g `  G ) } )  =  (
# `  ( T `  q ) ) )
189 snfi 6957 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  { ( 0g `  G ) }  e.  Fin
190 hashen 11362 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( { ( 0g `  G ) }  e.  Fin  /\  ( T `  q )  e.  Fin )  ->  ( ( # `  { ( 0g `  G ) } )  =  ( # `  ( T `  q )
)  <->  { ( 0g `  G ) }  ~~  ( T `  q ) ) )
191189, 154, 190sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( ( # `  {
( 0g `  G
) } )  =  ( # `  ( T `  q )
)  <->  { ( 0g `  G ) }  ~~  ( T `  q ) ) )
192188, 191mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  { ( 0g `  G ) }  ~~  ( T `  q ) )
193 fisseneq 7090 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( T `  q
)  e.  Fin  /\  { ( 0g `  G
) }  C_  ( T `  q )  /\  { ( 0g `  G ) }  ~~  ( T `  q ) )  ->  { ( 0g `  G ) }  =  ( T `  q ) )
194154, 158, 192, 193syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  { ( 0g `  G ) }  =  ( T `  q ) )
195116subg0cl 14645 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( G DProd  ( T  |`  D ) )  e.  (SubGrp `  G )  ->  ( 0g `  G
)  e.  ( G DProd 
( T  |`  D ) ) )
196140, 195syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( 0g `  G
)  e.  ( G DProd 
( T  |`  D ) ) )
197196adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( 0g `  G
)  e.  ( G DProd 
( T  |`  D ) ) )
198197snssd 3776 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  { ( 0g `  G ) }  C_  ( G DProd  ( T  |`  D ) ) )
199194, 198eqsstr3d 3226 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( T `  q
)  C_  ( G DProd  ( T  |`  D )
) )
200153, 199sylan2b 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  q  e.  ( A  \  D ) )  ->  ( T `  q )  C_  ( G DProd  ( T  |`  D ) ) )
201152, 200eqsstrd 3225 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  q  e.  ( A  \  D ) )  ->  ( ( T  |`  ( A  \  D ) ) `  q )  C_  ( G DProd  ( T  |`  D ) ) )
202144, 150, 140, 201dprdlub 15277 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( G DProd  ( T  |`  ( A  \  D
) ) )  C_  ( G DProd  ( T  |`  D ) ) )
203 eqid 2296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( LSSum `  G )  =  (
LSSum `  G )
204203lsmss2 14993 . . . . . . . . . . . . . . . . . . . 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 ) ) )
205140, 146, 202, 204syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( G DProd  ( T  |`  D ) ) ( LSSum `  G )
( G DProd  ( T  |`  ( A  \  D
) ) ) )  =  ( G DProd  ( T  |`  D ) ) )
206 disjdif 3539 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( D  i^i  ( A  \  D ) )  =  (/)
207206a1i 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( D  i^i  ( A  \  D ) )  =  (/) )
208 undif2 3543 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( D  u.  ( A  \  D ) )  =  ( D  u.  A
)
209 ssequn1 3358 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( D 
C_  A  <->  ( D  u.  A )  =  A )
21099, 209sylib 188 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( D  u.  A
)  =  A )
211208, 210syl5req 2341 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  =  ( D  u.  ( A  \  D ) ) )
2124, 207, 211, 203, 2dprdsplit 15299 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( G DProd  T )  =  ( ( G DProd 
( T  |`  D ) ) ( LSSum `  G
) ( G DProd  ( T  |`  ( A  \  D ) ) ) ) )
2131simprd 449 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( G DProd  T )  =  B )
214212, 213eqtr3d 2330 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( G DProd  ( T  |`  D ) ) ( LSSum `  G )
( G DProd  ( T  |`  ( A  \  D
) ) ) )  =  B )
215205, 214eqtr3d 2330 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( G DProd  ( T  |`  D ) )  =  B )
216138, 215jca 518 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( G dom DProd  ( T  |`  D )  /\  ( G DProd  ( T  |`  D ) )  =  B ) )
217216adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  ( G dom DProd  ( T  |`  D )  /\  ( G DProd  ( T  |`  D ) )  =  B ) )
2184, 99, 104syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( T  |`  D ) : D --> (SubGrp `  G ) )
219218, 106syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  ( T  |`  D )  =  D )
220219adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  dom  ( T  |`  D )  =  D )
22199sselda 3193 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  q  e.  D )  ->  q  e.  A )
222221, 44syldan 456 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  q  e.  D )  ->  C  e.  NN0 )
223222adantlr 695 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  Prime )  /\  q  e.  D )  ->  C  e.  NN0 )
224 fvres 5558 . . . . . . . . . . . . . . . . . . . 20  |-  ( q  e.  D  ->  (
( T  |`  D ) `
 q )  =  ( T `  q
) )
225224adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  q  e.  D )  ->  (
( T  |`  D ) `
 q )  =  ( T `  q
) )
226225fveq2d 5545 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  q  e.  D )  ->  ( # `
 ( ( T  |`  D ) `  q
) )  =  (
# `  ( T `  q ) ) )
227221, 40syldan 456 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  q  e.  D )  ->  ( # `
 ( T `  q ) )  =  ( q ^ C
) )
228226, 227eqtrd 2328 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  q  e.  D )  ->  ( # `
 ( ( T  |`  D ) `  q
) )  =  ( q ^ C ) )
229228adantlr 695 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  Prime )  /\  q  e.  D )  ->  ( # `
 ( ( T  |`  D ) `  q
) )  =  ( q ^ C ) )
230 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  x  e.  Prime )
231 fzfid 11051 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 1 ... ( # `
 B ) )  e.  Fin )
232 prmnn 12777 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  Prime  ->  w  e.  NN )
2332323ad2ant2 977 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  w  e.  Prime  /\  w  ||  ( # `
 B ) )  ->  w  e.  NN )
234 prmz 12778 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  Prime  ->  w  e.  ZZ )
235 dvdsle 12590 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( w  e.  ZZ  /\  ( # `  B )  e.  NN )  -> 
( w  ||  ( # `
 B )  ->  w  <_  ( # `  B
) ) )
236234, 52, 235syl2anr 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  w  e.  Prime )  ->  ( w  ||  ( # `  B
)  ->  w  <_  (
# `  B )
) )
2372363impia 1148 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  w  e.  Prime  /\  w  ||  ( # `
 B ) )  ->  w  <_  ( # `
 B ) )
23852nnzd 10132 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( # `  B
)  e.  ZZ )
2392383ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  w  e.  Prime  /\  w  ||  ( # `
 B ) )  ->  ( # `  B
)  e.  ZZ )
240 fznn 10868 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
# `  B )  e.  ZZ  ->  ( w  e.  ( 1 ... ( # `
 B ) )  <-> 
( w  e.  NN  /\  w  <_  ( # `  B
) ) ) )
241239, 240syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  w  e.  Prime  /\  w  ||  ( # `
 B ) )  ->  ( w  e.  ( 1 ... ( # `
 B ) )  <-> 
( w  e.  NN  /\  w  <_  ( # `  B
) ) ) )
242233, 237, 241mpbir2and 888 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  w  e.  Prime  /\  w  ||  ( # `
 B ) )  ->  w  e.  ( 1 ... ( # `  B ) ) )
243242rabssdv 3266 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  { w  e.  Prime  |  w  ||  ( # `  B ) }  C_  ( 1 ... ( # `
 B ) ) )
244131, 243syl5eqss 3235 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  D  C_  ( 1 ... ( # `  B
) ) )
245 ssfi 7099 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1 ... ( # `
 B ) )  e.  Fin  /\  D  C_  ( 1 ... ( # `
 B ) ) )  ->  D  e.  Fin )
246231, 244, 245syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  D  e.  Fin )
247246adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  Prime )  ->  D  e.  Fin )
2487, 8, 128, 129, 130, 134, 131, 136, 217, 220, 223, 229, 230, 247ablfac1eulem 15323 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  Prime )  ->  -.  x  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { x }
) ) ) ) )
249248ralrimiva 2639 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. x  e.  Prime  -.  x  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
x } ) ) ) ) )
250249adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  q  e.  A )  ->  A. x  e.  Prime  -.  x  ||  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
x } ) ) ) ) )
251 id 19 . . . . . . . . . . . . . . . 16  |-  ( x  =  q  ->  x  =  q )
252 sneq 3664 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  q  ->  { x }  =  { q } )
253252difeq2d 3307 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  q  ->  ( D  \  { x }
)  =  ( D 
\  { q } ) )
254253reseq2d 4971 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  q  ->  (
( T  |`  D )  |`  ( D  \  {
x } ) )  =  ( ( T  |`  D )  |`  ( D  \  { q } ) ) )
255254oveq2d 5890 . . . . . . . . . . . . . . . . 17  |-  ( x  =  q  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { x }
) ) )  =  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) )
256255fveq2d 5545 . . . . . . . . . . . . . . . 16  |-  ( x  =  q  ->  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
x } ) ) ) )  =  (
# `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) )
257251, 256breq12d 4052 . . . . . . . . . . . . . . 15  |-  ( x  =  q  ->  (
x  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { x }
) ) ) )  <-> 
q  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) ) )
258257notbid 285 . . . . . . . . . . . . . 14  |-  ( x  =  q  ->  ( -.  x  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
x } ) ) ) )  <->  -.  q  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) ) )
259258rspcv 2893 . . . . . . . . . . . . 13  |-  ( q  e.  Prime  ->  ( A. x  e.  Prime  -.  x  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { x }
) ) ) )  ->  -.  q  ||  ( # `  ( G DProd 
( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) ) )
26041, 250, 259sylc 56 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  -.  q  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )
261 coprm 12795 . . . . . . . . . . . . 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 ) )
26241, 127, 261syl2anc 642 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  ( -.  q  ||  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  <->  ( q  gcd  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  =  1 ) )
263260, 262mpbid 201 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  (
q  gcd  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  =  1 )
264 rpexp1i 12816 . . . . . . . . . . . 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 ) )
26543, 127, 54, 264syl3anc 1182 . . . . . . . . . . 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 ) )
266263, 265mpd 14 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  (
( q ^ (
q  pCnt  ( # `  B
) ) )  gcd  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  =  1 )
267 coprmdvds2 12798 . . . . . . . . . 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 ) ) )
26880, 127, 59, 266, 267syl31anc 1185 . . . . . . . . 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 ) ) )
26996, 115, 268mp2and 660 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  (
( q ^ (
q  pCnt  ( # `  B
) ) )  x.  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  ||  ( # `  B ) )
270 eqid 2296 . . . . . . . . . 10  |-  (Cntz `  G )  =  (Cntz `  G )
271 inss1 3402 . . . . . . . . . . . . . 14  |-  ( D  i^i  { q } )  C_  D
272271a1i 10 . . . . . . . . . . . . 13  |-  ( (
ph  /\  q  e.  A )  ->  ( D  i^i  { q } )  C_  D )
273102, 107, 272dprdres 15279 . . . . . . . . . . . 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 ) ) ) )
274273simpld 445 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  G dom DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )
275 dprdsubg 15275 . . . . . . . . . . 11  |-  ( G dom DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  e.  (SubGrp `  G )
)
276274, 275syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  e.  (SubGrp `  G )
)
277 inass 3392 . . . . . . . . . . . . 13  |-  ( ( D  i^i  { q } )  i^i  ( D  \  { q } ) )  =  ( D  i^i  ( { q }  i^i  ( D  \  { q } ) ) )
278 disjdif 3539 . . . . . . . . . . . . . 14  |-  ( { q }  i^i  ( D  \  { q } ) )  =  (/)
279278ineq2i 3380 . . . . . . . . . . . . 13  |-  ( D  i^i  ( { q }  i^i  ( D 
\  { q } ) ) )  =  ( D  i^i  (/) )
280 in0 3493 . . . . . . . . . . . . 13  |-  ( D  i^i  (/) )  =  (/)
281277, 279, 2803eqtri 2320 . . . . . . . . . . . 12  |-  ( ( D  i^i  { q } )  i^i  ( D  \  { q } ) )  =  (/)
282281a1i 10 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  (
( D  i^i  {
q } )  i^i  ( D  \  {
q } ) )  =  (/) )
283102, 107, 272, 109, 282, 116dprddisj2 15290 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  (
( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  i^i  ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  =  {
( 0g `  G
) } )
284102, 107, 272, 109, 282, 270dprdcntz2 15289 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  C_  ( (Cntz `  G ) `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) )
2857dprdssv 15267 . . . . . . . . . . 11  |-  ( G DProd 
( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  C_  B
286 ssfi 7099 . . . . . . . . . . 11  |-  ( ( B  e.  Fin  /\  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) ) 
C_  B )  -> 
( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  e.  Fin )
28722, 285, 286sylancl 643 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  e. 
Fin )
288203, 116, 270, 276, 113, 283, 284, 287, 123lsmhash 15030 . . . . . . . . 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 } ) ) ) ) ) )
289 inundif 3545 . . . . . . . . . . . . . 14  |-  ( ( D  i^i  { q } )  u.  ( D  \  { q } ) )  =  D
290289eqcomi 2300 . . . . . . . . . . . . 13  |-  D  =  ( ( D  i^i  { q } )  u.  ( D  \  {
q } ) )
291290a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  q  e.  A )  ->  D  =  ( ( D  i^i  { q } )  u.  ( D 
\  { q } ) ) )
292105, 282, 291, 203, 102dprdsplit 15299 . . . . . . . . . . 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 } ) ) ) ) )
293215adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( T  |`  D ) )  =  B )
294292, 293eqtr3d 2330 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  (
( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) ) ( LSSum `  G )
( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) )  =  B )
295294fveq2d 5545 . . . . . . . . 9  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( ( G DProd 
( ( T  |`  D )  |`  ( D  i^i  { q } ) ) ) (
LSSum `  G ) ( G DProd  ( ( T  |`  D )  |`  ( D  \  { q } ) ) ) ) )  =  ( # `  B ) )
296 snssi 3775 . . . . . . . . . . . . . . . . 17  |-  ( q  e.  D  ->  { q }  C_  D )
297296adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  { q }  C_  D )
298 dfss1 3386 . . . . . . . . . . . . . . . 16  |-  ( { q }  C_  D  <->  ( D  i^i  { q } )  =  {
q } )
299297, 298sylib 188 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  ( D  i^i  { q } )  =  { q } )
300299reseq2d 4971 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  (
( T  |`  D )  |`  ( D  i^i  {
q } ) )  =  ( ( T  |`  D )  |`  { q } ) )
301300oveq2d 5890 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  =  ( G DProd  ( ( T  |`  D )  |` 
{ q } ) ) )
302102adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  G dom DProd  ( T  |`  D ) )
303219ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  dom  ( T  |`  D )  =  D )
304 simpr 447 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  q  e.  D )
305302, 303, 304dpjlem 15302 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  ( G DProd  ( ( T  |`  D )  |`  { q } ) )  =  ( ( T  |`  D ) `  q
) )
306224adantl 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  (
( T  |`  D ) `
 q )  =  ( T `  q
) )
307301, 305, 3063eqtrd 2332 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  q  e.  A )  /\  q  e.  D )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  =  ( T `  q
) )
308 simprr 733 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  ->  -.  q  e.  D
)
309 disjsn 3706 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  i^i  { q } )  =  (/)  <->  -.  q  e.  D )
310308, 309sylibr 203 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( D  i^i  {
q } )  =  (/) )
311310reseq2d 4971 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( ( T  |`  D )  |`  ( D  i^i  { q } ) )  =  ( ( T  |`  D )  |`  (/) ) )
312 res0 4975 . . . . . . . . . . . . . . . 16  |-  ( ( T  |`  D )  |`  (/) )  =  (/)
313311, 312syl6eq 2344 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( ( T  |`  D )  |`  ( D  i^i  { q } ) )  =  (/) )
314313oveq2d 5890 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  =  ( G DProd  (/) ) )
315116dprd0 15282 . . . . . . . . . . . . . . . . 17  |-  ( G  e.  Grp  ->  ( G dom DProd  (/)  /\  ( G DProd  (/) )  =  { ( 0g `  G ) } ) )
31647, 315syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( G dom DProd  (/)  /\  ( G DProd 
(/) )  =  {
( 0g `  G
) } ) )
317316simprd 449 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G DProd  (/) )  =  { ( 0g `  G ) } )
318317adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( G DProd  (/) )  =  { ( 0g `  G ) } )
319314, 318, 1943eqtrd 2332 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( q  e.  A  /\  -.  q  e.  D ) )  -> 
( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  =  ( T `  q ) )
320319anassrs 629 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  q  e.  A )  /\  -.  q  e.  D )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  {
q } ) ) )  =  ( T `
 q ) )
321307, 320pm2.61dan 766 . . . . . . . . . . 11  |-  ( (
ph  /\  q  e.  A )  ->  ( G DProd  ( ( T  |`  D )  |`  ( D  i^i  { q } ) ) )  =  ( T `  q
) )
322321fveq2d 5545 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  i^i  {
q } ) ) ) )  =  (
# `  ( T `  q ) ) )
323322oveq1d 5889 . . . . . . . . 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 } ) ) ) ) ) )
324288, 295, 3233eqtr3d 2336 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 B )  =  ( ( # `  ( T `  q )
)  x.  ( # `  ( G DProd  ( ( T  |`  D )  |`  ( D  \  {
q } ) ) ) ) ) )
325269, 324breqtrd 4063 . . . . . . 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 } ) ) ) ) ) )
326126nnne0d 9806 . . . . . . . 8  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( G DProd  (
( T  |`  D )  |`  ( D  \  {
q } ) ) ) )  =/=  0
)
327 dvdsmulcr 12574 . . . . . . . 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 ) ) ) )
32880, 75, 127, 326, 327syl112anc 1186 . . . . . . 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 ) ) ) )
329325, 328mpbid 201 . . . . . 6  |-  ( (
ph  /\  q  e.  A )  ->  (
q ^ ( q 
pCnt  ( # `  B
) ) )  ||  ( # `  ( T `
 q ) ) )
330 dvdseq 12592 . . . . . 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 )
) ) )
33174, 94, 67, 329, 330syl22anc 1183 . . . . 5  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  =  ( q ^ (
q  pCnt  ( # `  B
) ) ) )
3327, 8, 9, 10, 11, 12ablfac1a 15320 . . . . 5  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( S `  q ) )  =  ( q ^ (
q  pCnt  ( # `  B
) ) ) )
333331, 332eqtr4d 2331 . . . 4  |-  ( (
ph  /\  q  e.  A )  ->  ( # `
 ( T `  q ) )  =  ( # `  ( S `  q )
) )
334 hashen 11362 . . . . 5  |-  ( ( ( T `  q
)  e.  Fin  /\  ( S `  q )  e.  Fin )  -> 
( ( # `  ( T `  q )
)  =  ( # `  ( S `  q
) )  <->  ( T `  q )  ~~  ( S `  q )
) )
33535, 28, 334syl2anc 642 . . . 4  |-  ( (
ph  /\  q  e.  A )  ->  (
( # `  ( T `
 q ) )  =  ( # `  ( S `  q )
)  <->  ( T `  q )  ~~  ( S `  q )
) )
336333, 335mpbid 201 . . 3  |-  ( (
ph  /\  q  e.  A )  ->  ( T `  q )  ~~  ( S `  q
) )
337 fisseneq 7090 . . 3  |-  ( ( ( S `  q
)  e.  Fin  /\  ( T `  q ) 
C_  ( S `  q )  /\  ( T `  q )  ~~  ( S `  q
) )  ->  ( T `  q )  =  ( S `  q ) )
33828, 93, 336, 337syl3anc 1182 . 2  |-  ( (
ph  /\  q  e.  A )  ->  ( T `  q )  =  ( S `  q ) )
3396, 21, 338eqfnfvd 5641 1  |-  ( ph  ->  T  =  S )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 934    = wceq 1632    e. wcel 1696    =/= wne 2459   A.wral 2556   {crab 2560   _Vcvv 2801    \ cdif 3162    u. cun 3163    i^i cin 3164    C_ wss 3165   (/)c0 3468   {csn 3653   class class class wbr 4039    e. cmpt 4093   dom cdm 4705    |` cres 4707    Fn wfn 5266   -->wf 5267   ` cfv 5271  (class class class)co 5874    ~~ cen 6876   Fincfn 6879   0cc0 8753   1c1 8754    x. cmul 8758    <_ cle 8884   NNcn 9762   NN0cn0 9981   ZZcz 10040   ZZ>=cuz 10246   ...cfz 10798   ^cexp 11120   #chash 11353    || cdivides 12547    gcd cgcd 12701   Primecprime 12774    pCnt cpc 12905   Basecbs 13164   0gc0g 13416   Grpcgrp 14378  SubGrpcsubg 14631  Cntzccntz 14807   odcod 14856   LSSumclsm 14961   Abelcabel 15106   DProd cdprd 15247
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-inf2 7358  ax-cnex 8809  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829  ax-pre-mulgt0 8830  ax-pre-sup 8831
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-iin 3924  df-disj 4010  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-se 4369  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-isom 5280  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-of 6094  df-1st 6138  df-2nd 6139  df-tpos 6250  df-riota 6320  df-recs 6404  df-rdg 6439  df-1o 6495  df-2o 6496  df-oadd 6499  df-omul 6500  df-er 6676  df-ec 6678  df-qs 6682  df-map 6790  df-ixp 6834  df-en 6880  df-dom 6881  df-sdom 6882  df-fin 6883  df-sup 7210  df-oi 7241  df-card 7588  df-acn 7591  df-cda 7810  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889  df-sub 9055  df-neg 9056  df-div 9440  df-nn 9763  df-2 9820  df-3 9821  df-n0 9982  df-z 10041  df-uz 10247  df-q 10333  df-rp 10371  df-fz 10799  df-fzo 10887  df-fl 10941  df-mod 10990  df-seq 11063  df-exp 11121  df-fac 11305  df-bc 11332  df-hash 11354  df-cj 11600  df-re 11601  df-im 11602  df-sqr 11736  df-abs 11737  df-clim 11978  df-sum 12175  df-dvds 12548  df-gcd 12702  df-prm 12775  df-pc 12906  df-ndx 13167  df-slot 13168  df-base 13169  df-sets 13170  df-ress 13171  df-plusg 13237  df-0g 13420  df-gsum 13421  df-mre 13504  df-mrc 13505  df-acs 13507  df-mnd 14383  df-mhm 14431  df-submnd 14432  df-grp 14505  df-minusg 14506  df-sbg 14507  df-mulg 14508  df-subg 14634  df-eqg 14636  df-ghm 14697  df-gim 14739  df-ga 14760  df-cntz 14809  df-oppg 14835  df-od 14860  df-lsm 14963  df-pj1 14964  df-cmn 15107  df-abl 15108  df-dprd 15249
  Copyright terms: Public domain W3C validator