This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ablfac1eu

Description: The factorization of ablfac1b 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)

Ref Expression
Hypotheses 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 ablfac1eu 
|- ( ph -> T = S )

Proof

Step Hyp Ref Expression
1 ablfac1.b 
 |-  B = ( Base ` G )
2 ablfac1.o 
 |-  O = ( od ` G )
3 ablfac1.s 
 |-  S = ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )
4 ablfac1.g 
 |-  ( ph -> G e. Abel )
5 ablfac1.f 
 |-  ( ph -> B e. Fin )
6 ablfac1.1 
 |-  ( ph -> A C_ Prime )
7 ablfac1c.d 
 |-  D = { w e. Prime | w || ( # ` B ) }
8 ablfac1.2 
 |-  ( ph -> D C_ A )
9 ablfac1eu.1 
 |-  ( ph -> ( G dom DProd T /\ ( G DProd T ) = B ) )
10 ablfac1eu.2 
 |-  ( ph -> dom T = A )
11 ablfac1eu.3 
 |-  ( ( ph /\ q e. A ) -> C e. NN0 )
12 ablfac1eu.4 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) = ( q ^ C ) )
13 9 simpld 
 |-  ( ph -> G dom DProd T )
14 13 10 dprdf2 
 |-  ( ph -> T : A --> ( SubGrp ` G ) )
15 14 ffnd 
 |-  ( ph -> T Fn A )
16 1 2 3 4 5 6 ablfac1b 
 |-  ( ph -> G dom DProd S )
17 1 fvexi 
 |-  B e. _V
18 17 rabex 
 |-  { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } e. _V
19 18 3 dmmpti 
 |-  dom S = A
20 19 a1i 
 |-  ( ph -> dom S = A )
21 16 20 dprdf2 
 |-  ( ph -> S : A --> ( SubGrp ` G ) )
22 21 ffnd 
 |-  ( ph -> S Fn A )
23 5 adantr 
 |-  ( ( ph /\ q e. A ) -> B e. Fin )
24 21 ffvelcdmda 
 |-  ( ( ph /\ q e. A ) -> ( S ` q ) e. ( SubGrp ` G ) )
25 1 subgss 
 |-  ( ( S ` q ) e. ( SubGrp ` G ) -> ( S ` q ) C_ B )
26 24 25 syl 
 |-  ( ( ph /\ q e. A ) -> ( S ` q ) C_ B )
27 23 26 ssfid 
 |-  ( ( ph /\ q e. A ) -> ( S ` q ) e. Fin )
28 14 ffvelcdmda 
 |-  ( ( ph /\ q e. A ) -> ( T ` q ) e. ( SubGrp ` G ) )
29 1 subgss 
 |-  ( ( T ` q ) e. ( SubGrp ` G ) -> ( T ` q ) C_ B )
30 28 29 syl 
 |-  ( ( ph /\ q e. A ) -> ( T ` q ) C_ B )
31 30 sselda 
 |-  ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> x e. B )
32 1 2 odcl 
 |-  ( x e. B -> ( O ` x ) e. NN0 )
33 31 32 syl 
 |-  ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( O ` x ) e. NN0 )
34 33 nn0zd 
 |-  ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( O ` x ) e. ZZ )
35 23 30 ssfid 
 |-  ( ( ph /\ q e. A ) -> ( T ` q ) e. Fin )
36 hashcl 
 |-  ( ( T ` q ) e. Fin -> ( # ` ( T ` q ) ) e. NN0 )
37 35 36 syl 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) e. NN0 )
38 37 nn0zd 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) e. ZZ )
39 38 adantr 
 |-  ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( # ` ( T ` q ) ) e. ZZ )
40 6 sselda 
 |-  ( ( ph /\ q e. A ) -> q e. Prime )
41 prmnn 
 |-  ( q e. Prime -> q e. NN )
42 40 41 syl 
 |-  ( ( ph /\ q e. A ) -> q e. NN )
43 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
44 4 43 syl 
 |-  ( ph -> G e. Grp )
45 1 grpbn0 
 |-  ( G e. Grp -> B =/= (/) )
46 44 45 syl 
 |-  ( ph -> B =/= (/) )
47 hashnncl 
 |-  ( B e. Fin -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
48 5 47 syl 
 |-  ( ph -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
49 46 48 mpbird 
 |-  ( ph -> ( # ` B ) e. NN )
50 49 adantr 
 |-  ( ( ph /\ q e. A ) -> ( # ` B ) e. NN )
51 40 50 pccld 
 |-  ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. NN0 )
52 42 51 nnexpcld 
 |-  ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. NN )
53 52 nnzd 
 |-  ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. ZZ )
54 53 adantr 
 |-  ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. ZZ )
55 28 adantr 
 |-  ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( T ` q ) e. ( SubGrp ` G ) )
56 35 adantr 
 |-  ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( T ` q ) e. Fin )
57 simpr 
 |-  ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> x e. ( T ` q ) )
58 2 odsubdvds 
 |-  ( ( ( T ` q ) e. ( SubGrp ` G ) /\ ( T ` q ) e. Fin /\ x e. ( T ` q ) ) -> ( O ` x ) || ( # ` ( T ` q ) ) )
59 55 56 57 58 syl3anc 
 |-  ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( O ` x ) || ( # ` ( T ` q ) ) )
60 prmz 
 |-  ( q e. Prime -> q e. ZZ )
61 40 60 syl 
 |-  ( ( ph /\ q e. A ) -> q e. ZZ )
62 11 nn0zd 
 |-  ( ( ph /\ q e. A ) -> C e. ZZ )
63 51 nn0zd 
 |-  ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. ZZ )
64 1 lagsubg 
 |-  ( ( ( T ` q ) e. ( SubGrp ` G ) /\ B e. Fin ) -> ( # ` ( T ` q ) ) || ( # ` B ) )
65 28 23 64 syl2anc 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) || ( # ` B ) )
66 12 65 eqbrtrrd 
 |-  ( ( ph /\ q e. A ) -> ( q ^ C ) || ( # ` B ) )
67 50 nnzd 
 |-  ( ( ph /\ q e. A ) -> ( # ` B ) e. ZZ )
68 pcdvdsb 
 |-  ( ( q e. Prime /\ ( # ` B ) e. ZZ /\ C e. NN0 ) -> ( C <_ ( q pCnt ( # ` B ) ) <-> ( q ^ C ) || ( # ` B ) ) )
69 40 67 11 68 syl3anc 
 |-  ( ( ph /\ q e. A ) -> ( C <_ ( q pCnt ( # ` B ) ) <-> ( q ^ C ) || ( # ` B ) ) )
70 66 69 mpbird 
 |-  ( ( ph /\ q e. A ) -> C <_ ( q pCnt ( # ` B ) ) )
71 eluz2 
 |-  ( ( q pCnt ( # ` B ) ) e. ( ZZ>= ` C ) <-> ( C e. ZZ /\ ( q pCnt ( # ` B ) ) e. ZZ /\ C <_ ( q pCnt ( # ` B ) ) ) )
72 62 63 70 71 syl3anbrc 
 |-  ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. ( ZZ>= ` C ) )
73 dvdsexp 
 |-  ( ( q e. ZZ /\ C e. NN0 /\ ( q pCnt ( # ` B ) ) e. ( ZZ>= ` C ) ) -> ( q ^ C ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
74 61 11 72 73 syl3anc 
 |-  ( ( ph /\ q e. A ) -> ( q ^ C ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
75 12 74 eqbrtrd 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
76 75 adantr 
 |-  ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( # ` ( T ` q ) ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
77 34 39 54 59 76 dvdstrd 
 |-  ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
78 30 77 ssrabdv 
 |-  ( ( ph /\ q e. A ) -> ( T ` q ) C_ { x e. B | ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) } )
79 id 
 |-  ( p = q -> p = q )
80 oveq1 
 |-  ( p = q -> ( p pCnt ( # ` B ) ) = ( q pCnt ( # ` B ) ) )
81 79 80 oveq12d 
 |-  ( p = q -> ( p ^ ( p pCnt ( # ` B ) ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
82 81 breq2d 
 |-  ( p = q -> ( ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) <-> ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) ) )
83 82 rabbidv 
 |-  ( p = q -> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } = { x e. B | ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) } )
84 83 3 18 fvmpt3i 
 |-  ( q e. A -> ( S ` q ) = { x e. B | ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) } )
85 84 adantl 
 |-  ( ( ph /\ q e. A ) -> ( S ` q ) = { x e. B | ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) } )
86 78 85 sseqtrrd 
 |-  ( ( ph /\ q e. A ) -> ( T ` q ) C_ ( S ` q ) )
87 52 nnnn0d 
 |-  ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. NN0 )
88 pcdvds 
 |-  ( ( q e. Prime /\ ( # ` B ) e. NN ) -> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` B ) )
89 40 50 88 syl2anc 
 |-  ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` B ) )
90 13 adantr 
 |-  ( ( ph /\ q e. A ) -> G dom DProd T )
91 10 adantr 
 |-  ( ( ph /\ q e. A ) -> dom T = A )
92 8 adantr 
 |-  ( ( ph /\ q e. A ) -> D C_ A )
93 90 91 92 dprdres 
 |-  ( ( ph /\ q e. A ) -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) C_ ( G DProd T ) ) )
94 93 simpld 
 |-  ( ( ph /\ q e. A ) -> G dom DProd ( T |` D ) )
95 14 adantr 
 |-  ( ( ph /\ q e. A ) -> T : A --> ( SubGrp ` G ) )
96 95 92 fssresd 
 |-  ( ( ph /\ q e. A ) -> ( T |` D ) : D --> ( SubGrp ` G ) )
97 96 fdmd 
 |-  ( ( ph /\ q e. A ) -> dom ( T |` D ) = D )
98 difssd 
 |-  ( ( ph /\ q e. A ) -> ( D \ { q } ) C_ D )
99 94 97 98 dprdres 
 |-  ( ( ph /\ q e. A ) -> ( G dom DProd ( ( T |` D ) |` ( D \ { q } ) ) /\ ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) C_ ( G DProd ( T |` D ) ) ) )
100 99 simpld 
 |-  ( ( ph /\ q e. A ) -> G dom DProd ( ( T |` D ) |` ( D \ { q } ) ) )
101 dprdsubg 
 |-  ( G dom DProd ( ( T |` D ) |` ( D \ { q } ) ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. ( SubGrp ` G ) )
102 100 101 syl 
 |-  ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. ( SubGrp ` G ) )
103 1 lagsubg 
 |-  ( ( ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. ( SubGrp ` G ) /\ B e. Fin ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) || ( # ` B ) )
104 102 23 103 syl2anc 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) || ( # ` B ) )
105 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
106 105 subg0cl 
 |-  ( ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. ( SubGrp ` G ) -> ( 0g ` G ) e. ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) )
107 102 106 syl 
 |-  ( ( ph /\ q e. A ) -> ( 0g ` G ) e. ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) )
108 107 ne0d 
 |-  ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) =/= (/) )
109 1 dprdssv 
 |-  ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) C_ B
110 ssfi 
 |-  ( ( B e. Fin /\ ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) C_ B ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. Fin )
111 23 109 110 sylancl 
 |-  ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. Fin )
112 hashnncl 
 |-  ( ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. Fin -> ( ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) e. NN <-> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) =/= (/) ) )
113 111 112 syl 
 |-  ( ( ph /\ q e. A ) -> ( ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) e. NN <-> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) =/= (/) ) )
114 108 113 mpbird 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) e. NN )
115 114 nnzd 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) e. ZZ )
116 id 
 |-  ( x = q -> x = q )
117 sneq 
 |-  ( x = q -> { x } = { q } )
118 117 difeq2d 
 |-  ( x = q -> ( D \ { x } ) = ( D \ { q } ) )
119 118 reseq2d 
 |-  ( x = q -> ( ( T |` D ) |` ( D \ { x } ) ) = ( ( T |` D ) |` ( D \ { q } ) ) )
120 119 oveq2d 
 |-  ( x = q -> ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) = ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) )
121 120 fveq2d 
 |-  ( x = q -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) = ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) )
122 116 121 breq12d 
 |-  ( x = q -> ( x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) <-> q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
123 122 notbid 
 |-  ( x = q -> ( -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) <-> -. q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
124 eqid 
 |-  ( p e. D |-> { y e. B | ( O ` y ) || ( p ^ ( p pCnt ( # ` B ) ) ) } ) = ( p e. D |-> { y e. B | ( O ` y ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )
125 4 adantr 
 |-  ( ( ph /\ x e. Prime ) -> G e. Abel )
126 5 adantr 
 |-  ( ( ph /\ x e. Prime ) -> B e. Fin )
127 7 ssrab3 
 |-  D C_ Prime
128 127 a1i 
 |-  ( ( ph /\ x e. Prime ) -> D C_ Prime )
129 ssidd 
 |-  ( ( ph /\ x e. Prime ) -> D C_ D )
130 13 10 8 dprdres 
 |-  ( ph -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) C_ ( G DProd T ) ) )
131 130 simpld 
 |-  ( ph -> G dom DProd ( T |` D ) )
132 dprdsubg 
 |-  ( G dom DProd ( T |` D ) -> ( G DProd ( T |` D ) ) e. ( SubGrp ` G ) )
133 131 132 syl 
 |-  ( ph -> ( G DProd ( T |` D ) ) e. ( SubGrp ` G ) )
134 difssd 
 |-  ( ph -> ( A \ D ) C_ A )
135 13 10 134 dprdres 
 |-  ( ph -> ( G dom DProd ( T |` ( A \ D ) ) /\ ( G DProd ( T |` ( A \ D ) ) ) C_ ( G DProd T ) ) )
136 135 simpld 
 |-  ( ph -> G dom DProd ( T |` ( A \ D ) ) )
137 dprdsubg 
 |-  ( G dom DProd ( T |` ( A \ D ) ) -> ( G DProd ( T |` ( A \ D ) ) ) e. ( SubGrp ` G ) )
138 136 137 syl 
 |-  ( ph -> ( G DProd ( T |` ( A \ D ) ) ) e. ( SubGrp ` G ) )
139 difss 
 |-  ( A \ D ) C_ A
140 fssres 
 |-  ( ( T : A --> ( SubGrp ` G ) /\ ( A \ D ) C_ A ) -> ( T |` ( A \ D ) ) : ( A \ D ) --> ( SubGrp ` G ) )
141 14 139 140 sylancl 
 |-  ( ph -> ( T |` ( A \ D ) ) : ( A \ D ) --> ( SubGrp ` G ) )
142 141 fdmd 
 |-  ( ph -> dom ( T |` ( A \ D ) ) = ( A \ D ) )
143 fvres 
 |-  ( q e. ( A \ D ) -> ( ( T |` ( A \ D ) ) ` q ) = ( T ` q ) )
144 143 adantl 
 |-  ( ( ph /\ q e. ( A \ D ) ) -> ( ( T |` ( A \ D ) ) ` q ) = ( T ` q ) )
145 eldif 
 |-  ( q e. ( A \ D ) <-> ( q e. A /\ -. q e. D ) )
146 35 adantrr 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( T ` q ) e. Fin )
147 105 subg0cl 
 |-  ( ( T ` q ) e. ( SubGrp ` G ) -> ( 0g ` G ) e. ( T ` q ) )
148 28 147 syl 
 |-  ( ( ph /\ q e. A ) -> ( 0g ` G ) e. ( T ` q ) )
149 148 snssd 
 |-  ( ( ph /\ q e. A ) -> { ( 0g ` G ) } C_ ( T ` q ) )
150 149 adantrr 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } C_ ( T ` q ) )
151 fvex 
 |-  ( 0g ` G ) e. _V
152 hashsng 
 |-  ( ( 0g ` G ) e. _V -> ( # ` { ( 0g ` G ) } ) = 1 )
153 151 152 ax-mp 
 |-  ( # ` { ( 0g ` G ) } ) = 1
154 12 adantrr 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( # ` ( T ` q ) ) = ( q ^ C ) )
155 40 adantr 
 |-  ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q e. Prime )
156 iddvdsexp 
 |-  ( ( q e. ZZ /\ C e. NN ) -> q || ( q ^ C ) )
157 61 156 sylan 
 |-  ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q || ( q ^ C ) )
158 66 adantr 
 |-  ( ( ( ph /\ q e. A ) /\ C e. NN ) -> ( q ^ C ) || ( # ` B ) )
159 12 38 eqeltrrd 
 |-  ( ( ph /\ q e. A ) -> ( q ^ C ) e. ZZ )
160 dvdstr 
 |-  ( ( q e. ZZ /\ ( q ^ C ) e. ZZ /\ ( # ` B ) e. ZZ ) -> ( ( q || ( q ^ C ) /\ ( q ^ C ) || ( # ` B ) ) -> q || ( # ` B ) ) )
161 61 159 67 160 syl3anc 
 |-  ( ( ph /\ q e. A ) -> ( ( q || ( q ^ C ) /\ ( q ^ C ) || ( # ` B ) ) -> q || ( # ` B ) ) )
162 161 adantr 
 |-  ( ( ( ph /\ q e. A ) /\ C e. NN ) -> ( ( q || ( q ^ C ) /\ ( q ^ C ) || ( # ` B ) ) -> q || ( # ` B ) ) )
163 157 158 162 mp2and 
 |-  ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q || ( # ` B ) )
164 breq1 
 |-  ( w = q -> ( w || ( # ` B ) <-> q || ( # ` B ) ) )
165 164 7 elrab2 
 |-  ( q e. D <-> ( q e. Prime /\ q || ( # ` B ) ) )
166 155 163 165 sylanbrc 
 |-  ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q e. D )
167 166 ex 
 |-  ( ( ph /\ q e. A ) -> ( C e. NN -> q e. D ) )
168 167 con3d 
 |-  ( ( ph /\ q e. A ) -> ( -. q e. D -> -. C e. NN ) )
169 168 impr 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> -. C e. NN )
170 11 adantrr 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> C e. NN0 )
171 elnn0 
 |-  ( C e. NN0 <-> ( C e. NN \/ C = 0 ) )
172 170 171 sylib 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( C e. NN \/ C = 0 ) )
173 172 ord 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( -. C e. NN -> C = 0 ) )
174 169 173 mpd 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> C = 0 )
175 174 oveq2d 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( q ^ C ) = ( q ^ 0 ) )
176 42 adantrr 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> q e. NN )
177 176 nncnd 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> q e. CC )
178 177 exp0d 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( q ^ 0 ) = 1 )
179 154 175 178 3eqtrd 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( # ` ( T ` q ) ) = 1 )
180 153 179 eqtr4id 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( # ` { ( 0g ` G ) } ) = ( # ` ( T ` q ) ) )
181 snfi 
 |-  { ( 0g ` G ) } e. Fin
182 hashen 
 |-  ( ( { ( 0g ` G ) } e. Fin /\ ( T ` q ) e. Fin ) -> ( ( # ` { ( 0g ` G ) } ) = ( # ` ( T ` q ) ) <-> { ( 0g ` G ) } ~~ ( T ` q ) ) )
183 181 146 182 sylancr 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( ( # ` { ( 0g ` G ) } ) = ( # ` ( T ` q ) ) <-> { ( 0g ` G ) } ~~ ( T ` q ) ) )
184 180 183 mpbid 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } ~~ ( T ` q ) )
185 fisseneq 
 |-  ( ( ( T ` q ) e. Fin /\ { ( 0g ` G ) } C_ ( T ` q ) /\ { ( 0g ` G ) } ~~ ( T ` q ) ) -> { ( 0g ` G ) } = ( T ` q ) )
186 146 150 184 185 syl3anc 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } = ( T ` q ) )
187 105 subg0cl 
 |-  ( ( G DProd ( T |` D ) ) e. ( SubGrp ` G ) -> ( 0g ` G ) e. ( G DProd ( T |` D ) ) )
188 133 187 syl 
 |-  ( ph -> ( 0g ` G ) e. ( G DProd ( T |` D ) ) )
189 188 adantr 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( 0g ` G ) e. ( G DProd ( T |` D ) ) )
190 189 snssd 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } C_ ( G DProd ( T |` D ) ) )
191 186 190 eqsstrrd 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( T ` q ) C_ ( G DProd ( T |` D ) ) )
192 145 191 sylan2b 
 |-  ( ( ph /\ q e. ( A \ D ) ) -> ( T ` q ) C_ ( G DProd ( T |` D ) ) )
193 144 192 eqsstrd 
 |-  ( ( ph /\ q e. ( A \ D ) ) -> ( ( T |` ( A \ D ) ) ` q ) C_ ( G DProd ( T |` D ) ) )
194 136 142 133 193 dprdlub 
 |-  ( ph -> ( G DProd ( T |` ( A \ D ) ) ) C_ ( G DProd ( T |` D ) ) )
195 eqid 
 |-  ( LSSum ` G ) = ( LSSum ` G )
196 195 lsmss2 
 |-  ( ( ( 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 ) ) )
197 133 138 194 196 syl3anc 
 |-  ( ph -> ( ( G DProd ( T |` D ) ) ( LSSum ` G ) ( G DProd ( T |` ( A \ D ) ) ) ) = ( G DProd ( T |` D ) ) )
198 disjdif 
 |-  ( D i^i ( A \ D ) ) = (/)
199 198 a1i 
 |-  ( ph -> ( D i^i ( A \ D ) ) = (/) )
200 undif2 
 |-  ( D u. ( A \ D ) ) = ( D u. A )
201 ssequn1 
 |-  ( D C_ A <-> ( D u. A ) = A )
202 8 201 sylib 
 |-  ( ph -> ( D u. A ) = A )
203 200 202 eqtr2id 
 |-  ( ph -> A = ( D u. ( A \ D ) ) )
204 14 199 203 195 13 dprdsplit 
 |-  ( ph -> ( G DProd T ) = ( ( G DProd ( T |` D ) ) ( LSSum ` G ) ( G DProd ( T |` ( A \ D ) ) ) ) )
205 9 simprd 
 |-  ( ph -> ( G DProd T ) = B )
206 204 205 eqtr3d 
 |-  ( ph -> ( ( G DProd ( T |` D ) ) ( LSSum ` G ) ( G DProd ( T |` ( A \ D ) ) ) ) = B )
207 197 206 eqtr3d 
 |-  ( ph -> ( G DProd ( T |` D ) ) = B )
208 131 207 jca 
 |-  ( ph -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) = B ) )
209 208 adantr 
 |-  ( ( ph /\ x e. Prime ) -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) = B ) )
210 14 8 fssresd 
 |-  ( ph -> ( T |` D ) : D --> ( SubGrp ` G ) )
211 210 fdmd 
 |-  ( ph -> dom ( T |` D ) = D )
212 211 adantr 
 |-  ( ( ph /\ x e. Prime ) -> dom ( T |` D ) = D )
213 8 sselda 
 |-  ( ( ph /\ q e. D ) -> q e. A )
214 213 11 syldan 
 |-  ( ( ph /\ q e. D ) -> C e. NN0 )
215 214 adantlr 
 |-  ( ( ( ph /\ x e. Prime ) /\ q e. D ) -> C e. NN0 )
216 fvres 
 |-  ( q e. D -> ( ( T |` D ) ` q ) = ( T ` q ) )
217 216 adantl 
 |-  ( ( ph /\ q e. D ) -> ( ( T |` D ) ` q ) = ( T ` q ) )
218 217 fveq2d 
 |-  ( ( ph /\ q e. D ) -> ( # ` ( ( T |` D ) ` q ) ) = ( # ` ( T ` q ) ) )
219 213 12 syldan 
 |-  ( ( ph /\ q e. D ) -> ( # ` ( T ` q ) ) = ( q ^ C ) )
220 218 219 eqtrd 
 |-  ( ( ph /\ q e. D ) -> ( # ` ( ( T |` D ) ` q ) ) = ( q ^ C ) )
221 220 adantlr 
 |-  ( ( ( ph /\ x e. Prime ) /\ q e. D ) -> ( # ` ( ( T |` D ) ` q ) ) = ( q ^ C ) )
222 simpr 
 |-  ( ( ph /\ x e. Prime ) -> x e. Prime )
223 fzfid 
 |-  ( ph -> ( 1 ... ( # ` B ) ) e. Fin )
224 prmnn 
 |-  ( w e. Prime -> w e. NN )
225 224 3ad2ant2 
 |-  ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w e. NN )
226 prmz 
 |-  ( w e. Prime -> w e. ZZ )
227 dvdsle 
 |-  ( ( w e. ZZ /\ ( # ` B ) e. NN ) -> ( w || ( # ` B ) -> w <_ ( # ` B ) ) )
228 226 49 227 syl2anr 
 |-  ( ( ph /\ w e. Prime ) -> ( w || ( # ` B ) -> w <_ ( # ` B ) ) )
229 228 3impia 
 |-  ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w <_ ( # ` B ) )
230 49 nnzd 
 |-  ( ph -> ( # ` B ) e. ZZ )
231 230 3ad2ant1 
 |-  ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> ( # ` B ) e. ZZ )
232 fznn 
 |-  ( ( # ` B ) e. ZZ -> ( w e. ( 1 ... ( # ` B ) ) <-> ( w e. NN /\ w <_ ( # ` B ) ) ) )
233 231 232 syl 
 |-  ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> ( w e. ( 1 ... ( # ` B ) ) <-> ( w e. NN /\ w <_ ( # ` B ) ) ) )
234 225 229 233 mpbir2and 
 |-  ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w e. ( 1 ... ( # ` B ) ) )
235 234 rabssdv 
 |-  ( ph -> { w e. Prime | w || ( # ` B ) } C_ ( 1 ... ( # ` B ) ) )
236 7 235 eqsstrid 
 |-  ( ph -> D C_ ( 1 ... ( # ` B ) ) )
237 223 236 ssfid 
 |-  ( ph -> D e. Fin )
238 237 adantr 
 |-  ( ( ph /\ x e. Prime ) -> D e. Fin )
239 1 2 124 125 126 128 7 129 209 212 215 221 222 238 ablfac1eulem 
 |-  ( ( ph /\ x e. Prime ) -> -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) )
240 239 ralrimiva 
 |-  ( ph -> A. x e. Prime -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) )
241 240 adantr 
 |-  ( ( ph /\ q e. A ) -> A. x e. Prime -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) )
242 123 241 40 rspcdva 
 |-  ( ( ph /\ q e. A ) -> -. q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) )
243 coprm 
 |-  ( ( 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 ) )
244 40 115 243 syl2anc 
 |-  ( ( ph /\ q e. A ) -> ( -. q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) <-> ( q gcd ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) = 1 ) )
245 242 244 mpbid 
 |-  ( ( ph /\ q e. A ) -> ( q gcd ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) = 1 )
246 rpexp1i 
 |-  ( ( 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 ) )
247 61 115 51 246 syl3anc 
 |-  ( ( 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 ) )
248 245 247 mpd 
 |-  ( ( ph /\ q e. A ) -> ( ( q ^ ( q pCnt ( # ` B ) ) ) gcd ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) = 1 )
249 coprmdvds2 
 |-  ( ( ( ( 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 ) ) )
250 53 115 67 248 249 syl31anc 
 |-  ( ( 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 ) ) )
251 89 104 250 mp2and 
 |-  ( ( ph /\ q e. A ) -> ( ( q ^ ( q pCnt ( # ` B ) ) ) x. ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) || ( # ` B ) )
252 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
253 inss1 
 |-  ( D i^i { q } ) C_ D
254 253 a1i 
 |-  ( ( ph /\ q e. A ) -> ( D i^i { q } ) C_ D )
255 94 97 254 dprdres 
 |-  ( ( 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 ) ) ) )
256 255 simpld 
 |-  ( ( ph /\ q e. A ) -> G dom DProd ( ( T |` D ) |` ( D i^i { q } ) ) )
257 dprdsubg 
 |-  ( G dom DProd ( ( T |` D ) |` ( D i^i { q } ) ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) e. ( SubGrp ` G ) )
258 256 257 syl 
 |-  ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) e. ( SubGrp ` G ) )
259 inass 
 |-  ( ( D i^i { q } ) i^i ( D \ { q } ) ) = ( D i^i ( { q } i^i ( D \ { q } ) ) )
260 disjdif 
 |-  ( { q } i^i ( D \ { q } ) ) = (/)
261 260 ineq2i 
 |-  ( D i^i ( { q } i^i ( D \ { q } ) ) ) = ( D i^i (/) )
262 in0 
 |-  ( D i^i (/) ) = (/)
263 259 261 262 3eqtri 
 |-  ( ( D i^i { q } ) i^i ( D \ { q } ) ) = (/)
264 263 a1i 
 |-  ( ( ph /\ q e. A ) -> ( ( D i^i { q } ) i^i ( D \ { q } ) ) = (/) )
265 94 97 254 98 264 105 dprddisj2 
 |-  ( ( ph /\ q e. A ) -> ( ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) i^i ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) = { ( 0g ` G ) } )
266 94 97 254 98 264 252 dprdcntz2 
 |-  ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) C_ ( ( Cntz ` G ) ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) )
267 1 dprdssv 
 |-  ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) C_ B
268 ssfi 
 |-  ( ( B e. Fin /\ ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) C_ B ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) e. Fin )
269 23 267 268 sylancl 
 |-  ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) e. Fin )
270 195 105 252 258 102 265 266 269 111 lsmhash 
 |-  ( ( 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 } ) ) ) ) ) )
271 inundif 
 |-  ( ( D i^i { q } ) u. ( D \ { q } ) ) = D
272 271 eqcomi 
 |-  D = ( ( D i^i { q } ) u. ( D \ { q } ) )
273 272 a1i 
 |-  ( ( ph /\ q e. A ) -> D = ( ( D i^i { q } ) u. ( D \ { q } ) ) )
274 96 264 273 195 94 dprdsplit 
 |-  ( ( ph /\ q e. A ) -> ( G DProd ( T |` D ) ) = ( ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) ( LSSum ` G ) ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) )
275 207 adantr 
 |-  ( ( ph /\ q e. A ) -> ( G DProd ( T |` D ) ) = B )
276 274 275 eqtr3d 
 |-  ( ( ph /\ q e. A ) -> ( ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) ( LSSum ` G ) ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) = B )
277 276 fveq2d 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) ( LSSum ` G ) ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) = ( # ` B ) )
278 snssi 
 |-  ( q e. D -> { q } C_ D )
279 278 adantl 
 |-  ( ( ( ph /\ q e. A ) /\ q e. D ) -> { q } C_ D )
280 sseqin2 
 |-  ( { q } C_ D <-> ( D i^i { q } ) = { q } )
281 279 280 sylib 
 |-  ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( D i^i { q } ) = { q } )
282 281 reseq2d 
 |-  ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( ( T |` D ) |` ( D i^i { q } ) ) = ( ( T |` D ) |` { q } ) )
283 282 oveq2d 
 |-  ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( G DProd ( ( T |` D ) |` { q } ) ) )
284 94 adantr 
 |-  ( ( ( ph /\ q e. A ) /\ q e. D ) -> G dom DProd ( T |` D ) )
285 211 ad2antrr 
 |-  ( ( ( ph /\ q e. A ) /\ q e. D ) -> dom ( T |` D ) = D )
286 simpr 
 |-  ( ( ( ph /\ q e. A ) /\ q e. D ) -> q e. D )
287 284 285 286 dpjlem 
 |-  ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( G DProd ( ( T |` D ) |` { q } ) ) = ( ( T |` D ) ` q ) )
288 216 adantl 
 |-  ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( ( T |` D ) ` q ) = ( T ` q ) )
289 283 287 288 3eqtrd 
 |-  ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
290 simprr 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> -. q e. D )
291 disjsn 
 |-  ( ( D i^i { q } ) = (/) <-> -. q e. D )
292 290 291 sylibr 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( D i^i { q } ) = (/) )
293 292 reseq2d 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( ( T |` D ) |` ( D i^i { q } ) ) = ( ( T |` D ) |` (/) ) )
294 res0 
 |-  ( ( T |` D ) |` (/) ) = (/)
295 293 294 eqtrdi 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( ( T |` D ) |` ( D i^i { q } ) ) = (/) )
296 295 oveq2d 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( G DProd (/) ) )
297 105 dprd0 
 |-  ( G e. Grp -> ( G dom DProd (/) /\ ( G DProd (/) ) = { ( 0g ` G ) } ) )
298 44 297 syl 
 |-  ( ph -> ( G dom DProd (/) /\ ( G DProd (/) ) = { ( 0g ` G ) } ) )
299 298 simprd 
 |-  ( ph -> ( G DProd (/) ) = { ( 0g ` G ) } )
300 299 adantr 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( G DProd (/) ) = { ( 0g ` G ) } )
301 296 300 186 3eqtrd 
 |-  ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
302 301 anassrs 
 |-  ( ( ( ph /\ q e. A ) /\ -. q e. D ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
303 289 302 pm2.61dan 
 |-  ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
304 303 fveq2d 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) ) = ( # ` ( T ` q ) ) )
305 304 oveq1d 
 |-  ( ( 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 } ) ) ) ) ) )
306 270 277 305 3eqtr3d 
 |-  ( ( ph /\ q e. A ) -> ( # ` B ) = ( ( # ` ( T ` q ) ) x. ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
307 251 306 breqtrd 
 |-  ( ( ph /\ q e. A ) -> ( ( q ^ ( q pCnt ( # ` B ) ) ) x. ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) || ( ( # ` ( T ` q ) ) x. ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
308 114 nnne0d 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) =/= 0 )
309 dvdsmulcr 
 |-  ( ( ( 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 ) ) ) )
310 53 38 115 308 309 syl112anc 
 |-  ( ( 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 ) ) ) )
311 307 310 mpbid 
 |-  ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` ( T ` q ) ) )
312 dvdseq 
 |-  ( ( ( ( # ` ( 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 ) ) ) )
313 37 87 75 311 312 syl22anc 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
314 1 2 3 4 5 6 ablfac1a 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( S ` q ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
315 313 314 eqtr4d 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) = ( # ` ( S ` q ) ) )
316 hashen 
 |-  ( ( ( T ` q ) e. Fin /\ ( S ` q ) e. Fin ) -> ( ( # ` ( T ` q ) ) = ( # ` ( S ` q ) ) <-> ( T ` q ) ~~ ( S ` q ) ) )
317 35 27 316 syl2anc 
 |-  ( ( ph /\ q e. A ) -> ( ( # ` ( T ` q ) ) = ( # ` ( S ` q ) ) <-> ( T ` q ) ~~ ( S ` q ) ) )
318 315 317 mpbid 
 |-  ( ( ph /\ q e. A ) -> ( T ` q ) ~~ ( S ` q ) )
319 fisseneq 
 |-  ( ( ( S ` q ) e. Fin /\ ( T ` q ) C_ ( S ` q ) /\ ( T ` q ) ~~ ( S ` q ) ) -> ( T ` q ) = ( S ` q ) )
320 27 86 318 319 syl3anc 
 |-  ( ( ph /\ q e. A ) -> ( T ` q ) = ( S ` q ) )
321 15 22 320 eqfnfvd 
 |-  ( ph -> T = S )