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	ffvelrnda	|- ( ( 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	ffvelrnda	|- ( ( 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 )