Theorem ablfac1eu 17634

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

Step	Hyp	Ref	Expression
1		ablfac1eu.1	. . . . 5 |- ( ph -> ( G dom DProd T /\ ( G DProd T ) = B ) )
2	1	simpld 460	. . . 4 |- ( ph -> G dom DProd T )
3		ablfac1eu.2	. . . 4 |- ( ph -> dom T = A )
4	2, 3	dprdf2 17567	. . 3 |- ( ph -> T : A --> (SubGrp ` G ) )
5		ffn 5737	. . 3 |- ( T : A --> (SubGrp ` G ) -> T Fn A )
6	4, 5	syl 17	. 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 )
13	7, 8, 9, 10, 11, 12	ablfac1b 17631	. . . 4 |- ( ph -> G dom DProd S )
14		fvex 5882	. . . . . . . 8 |- ( Base ` G ) e. _V
15	7, 14	eqeltri 2504	. . . . . . 7 |- B e. _V
16	15	rabex 4567	. . . . . 6 |- { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } e. _V
17	16, 9	dmmpti 5716	. . . . 5 |- dom S = A
18	17	a1i 11	. . . 4 |- ( ph -> dom S = A )
19	13, 18	dprdf2 17567	. . 3 |- ( ph -> S : A --> (SubGrp ` G ) )
20		ffn 5737	. . 3 |- ( S : A --> (SubGrp ` G ) -> S Fn A )
21	19, 20	syl 17	. 2 |- ( ph -> S Fn A )
22	11	adantr 466	. . . 4 |- ( ( ph /\ q e. A ) -> B e. Fin )
23	19	ffvelrnda 6028	. . . . 5 |- ( ( ph /\ q e. A ) -> ( S ` q ) e. (SubGrp ` G ) )
24	7	subgss 16762	. . . . 5 |- ( ( S ` q ) e. (SubGrp ` G ) -> ( S ` q ) C_ B )
25	23, 24	syl 17	. . . 4 |- ( ( ph /\ q e. A ) -> ( S ` q ) C_ B )
26		ssfi 7789	. . . 4 |- ( ( B e. Fin /\ ( S ` q ) C_ B ) -> ( S ` q ) e. Fin )
27	22, 25, 26	syl2anc 665	. . 3 |- ( ( ph /\ q e. A ) -> ( S ` q ) e. Fin )
28	4	ffvelrnda 6028	. . . . . 6 |- ( ( ph /\ q e. A ) -> ( T ` q ) e. (SubGrp ` G ) )
29	7	subgss 16762	. . . . . 6 |- ( ( T ` q ) e. (SubGrp ` G ) -> ( T ` q ) C_ B )
30	28, 29	syl 17	. . . . 5 |- ( ( ph /\ q e. A ) -> ( T ` q ) C_ B )
31	28	adantr 466	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( T ` q ) e. (SubGrp ` G ) )
32		ssfi 7789	. . . . . . . . 9 |- ( ( B e. Fin /\ ( T ` q ) C_ B ) -> ( T ` q ) e. Fin )
33	22, 30, 32	syl2anc 665	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( T ` q ) e. Fin )
34	33	adantr 466	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( T ` q ) e. Fin )
35		simpr 462	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> x e. ( T ` q ) )
36	8	odsubdvds 17151	. . . . . . 7 |- ( ( ( T ` q ) e. (SubGrp ` G ) /\ ( T ` q ) e. Fin /\ x e. ( T ` q ) ) -> ( O ` x ) || ( # ` ( T ` q ) ) )
37	31, 34, 35, 36	syl3anc 1264	. . . . . 6 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( O ` x ) || ( # ` ( T ` q ) ) )
38		ablfac1eu.4	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) = ( q ^ C ) )
39	12	sselda 3461	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> q e. Prime )
40		prmz 14586	. . . . . . . . . 10 |- ( q e. Prime -> q e. ZZ )
41	39, 40	syl 17	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> q e. ZZ )
42		ablfac1eu.3	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> C e. NN0 )
43	42	nn0zd 11027	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> C e. ZZ )
44		ablgrp 17363	. . . . . . . . . . . . . . . 16 |- ( G e. Abel -> G e. Grp )
45	10, 44	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> G e. Grp )
46	7	grpbn0 16639	. . . . . . . . . . . . . . 15 |- ( G e. Grp -> B =/= (/) )
47	45, 46	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> B =/= (/) )
48		hashnncl 12533	. . . . . . . . . . . . . . 15 |- ( B e. Fin -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
49	11, 48	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
50	47, 49	mpbird 235	. . . . . . . . . . . . 13 |- ( ph -> ( # ` B ) e. NN )
51	50	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( # ` B ) e. NN )
52	39, 51	pccld 14752	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. NN0 )
53	52	nn0zd 11027	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. ZZ )
54	7	lagsubg 16823	. . . . . . . . . . . . 13 |- ( ( ( T ` q ) e. (SubGrp ` G ) /\ B e. Fin ) -> ( # ` ( T ` q ) ) || ( # ` B ) )
55	28, 22, 54	syl2anc 665	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) || ( # ` B ) )
56	38, 55	eqbrtrrd 4439	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( q ^ C ) || ( # ` B ) )
57	51	nnzd 11028	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( # ` B ) e. ZZ )
58		pcdvdsb 14770	. . . . . . . . . . . 12 |- ( ( q e. Prime /\ ( # ` B ) e. ZZ /\ C e. NN0 ) -> ( C <_ ( q pCnt ( # ` B ) ) <-> ( q ^ C ) || ( # ` B ) ) )
59	39, 57, 42, 58	syl3anc 1264	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( C <_ ( q pCnt ( # ` B ) ) <-> ( q ^ C ) || ( # ` B ) ) )
60	56, 59	mpbird 235	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> C <_ ( q pCnt ( # ` B ) ) )
61		eluz2 11154	. . . . . . . . . 10 |- ( ( q pCnt ( # ` B ) ) e. ( ZZ>= ` C ) <-> ( C e. ZZ /\ ( q pCnt ( # ` B ) ) e. ZZ /\ C <_ ( q pCnt ( # ` B ) ) ) )
62	43, 53, 60, 61	syl3anbrc 1189	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. ( ZZ>= ` C ) )
63		dvdsexp 14328	. . . . . . . . 9 |- ( ( q e. ZZ /\ C e. NN0 /\ ( q pCnt ( # ` B ) ) e. ( ZZ>= ` C ) ) -> ( q ^ C ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
64	41, 42, 62, 63	syl3anc 1264	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( q ^ C ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
65	38, 64	eqbrtrd 4437	. . . . . . 7 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
66	65	adantr 466	. . . . . 6 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( # ` ( T ` q ) ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
67	30	sselda 3461	. . . . . . . . 9 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> x e. B )
68	7, 8	odcl 17120	. . . . . . . . 9 |- ( x e. B -> ( O ` x ) e. NN0 )
69	67, 68	syl 17	. . . . . . . 8 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( O ` x ) e. NN0 )
70	69	nn0zd 11027	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( O ` x ) e. ZZ )
71		hashcl 12524	. . . . . . . . . 10 |- ( ( T ` q ) e. Fin -> ( # ` ( T ` q ) ) e. NN0 )
72	33, 71	syl 17	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) e. NN0 )
73	72	nn0zd 11027	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) e. ZZ )
74	73	adantr 466	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( # ` ( T ` q ) ) e. ZZ )
75		prmnn 14585	. . . . . . . . . . 11 |- ( q e. Prime -> q e. NN )
76	39, 75	syl 17	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> q e. NN )
77	76, 52	nnexpcld 12423	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. NN )
78	77	nnzd 11028	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. ZZ )
79	78	adantr 466	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. ZZ )
80		dvdstr 14304	. . . . . . 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 ) ) ) ) )
81	70, 74, 79, 80	syl3anc 1264	. . . . . 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 ) ) ) ) )
82	37, 66, 81	mp2and 683	. . . . 5 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
83	30, 82	ssrabdv 3537	. . . 4 |- ( ( ph /\ q e. A ) -> ( T ` q ) C_ { x e. B | ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) } )
84		id 23	. . . . . . . . 9 |- ( p = q -> p = q )
85		oveq1 6303	. . . . . . . . 9 |- ( p = q -> ( p pCnt ( # ` B ) ) = ( q pCnt ( # ` B ) ) )
86	84, 85	oveq12d 6314	. . . . . . . 8 |- ( p = q -> ( p ^ ( p pCnt ( # ` B ) ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
87	86	breq2d 4429	. . . . . . 7 |- ( p = q -> ( ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) <-> ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) ) )
88	87	rabbidv 3070	. . . . . 6 |- ( p = q -> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } = { x e. B | ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) } )
89	88, 9, 16	fvmpt3i 5960	. . . . 5 |- ( q e. A -> ( S ` q ) = { x e. B | ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) } )
90	89	adantl 467	. . . 4 |- ( ( ph /\ q e. A ) -> ( S ` q ) = { x e. B | ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) } )
91	83, 90	sseqtr4d 3498	. . 3 |- ( ( ph /\ q e. A ) -> ( T ` q ) C_ ( S ` q ) )
92	77	nnnn0d 10914	. . . . . 6 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. NN0 )
93		pcdvds 14765	. . . . . . . . . 10 |- ( ( q e. Prime /\ ( # ` B ) e. NN ) -> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` B ) )
94	39, 51, 93	syl2anc 665	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` B ) )
95	2	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. A ) -> G dom DProd T )
96	3	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. A ) -> dom T = A )
97		ablfac1.2	. . . . . . . . . . . . . . . 16 |- ( ph -> D C_ A )
98	97	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. A ) -> D C_ A )
99	95, 96, 98	dprdres 17589	. . . . . . . . . . . . . 14 |- ( ( ph /\ q e. A ) -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) C_ ( G DProd T ) ) )
100	99	simpld 460	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> G dom DProd ( T |` D ) )
101	4	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. A ) -> T : A --> (SubGrp ` G ) )
102	101, 98	fssresd 5758	. . . . . . . . . . . . . 14 |- ( ( ph /\ q e. A ) -> ( T |` D ) : D --> (SubGrp ` G ) )
103		fdm 5741	. . . . . . . . . . . . . 14 |- ( ( T |` D ) : D --> (SubGrp ` G ) -> dom ( T |` D ) = D )
104	102, 103	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> dom ( T |` D ) = D )
105		difssd 3590	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> ( D \ { q } ) C_ D )
106	100, 104, 105	dprdres 17589	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( G dom DProd ( ( T |` D ) |` ( D \ { q } ) ) /\ ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) C_ ( G DProd ( T |` D ) ) ) )
107	106	simpld 460	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> G dom DProd ( ( T |` D ) |` ( D \ { q } ) ) )
108		dprdsubg 17585	. . . . . . . . . . 11 |- ( G dom DProd ( ( T |` D ) |` ( D \ { q } ) ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. (SubGrp ` G ) )
109	107, 108	syl 17	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. (SubGrp ` G ) )
110	7	lagsubg 16823	. . . . . . . . . 10 |- ( ( ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. (SubGrp ` G ) /\ B e. Fin ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) || ( # ` B ) )
111	109, 22, 110	syl2anc 665	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) || ( # ` B ) )
112		eqid 2420	. . . . . . . . . . . . . . 15 |- ( 0g ` G ) = ( 0g ` G )
113	112	subg0cl 16769	. . . . . . . . . . . . . 14 |- ( ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. (SubGrp ` G ) -> ( 0g ` G ) e. ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) )
114	109, 113	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> ( 0g ` G ) e. ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) )
115		ne0i 3764	. . . . . . . . . . . . 13 |- ( ( 0g ` G ) e. ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) =/= (/) )
116	114, 115	syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) =/= (/) )
117	7	dprdssv 17577	. . . . . . . . . . . . . 14 |- ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) C_ B
118		ssfi 7789	. . . . . . . . . . . . . 14 |- ( ( B e. Fin /\ ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) C_ B ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. Fin )
119	22, 117, 118	sylancl 666	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. Fin )
120		hashnncl 12533	. . . . . . . . . . . . 13 |- ( ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. Fin -> ( ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) e. NN <-> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) =/= (/) ) )
121	119, 120	syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) e. NN <-> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) =/= (/) ) )
122	116, 121	mpbird 235	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) e. NN )
123	122	nnzd 11028	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) e. ZZ )
124		eqid 2420	. . . . . . . . . . . . . . . 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 ) ) ) } )
125	10	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> G e. Abel )
126	11	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> B e. Fin )
127		ablfac1c.d	. . . . . . . . . . . . . . . . . 18 |- D = { w e. Prime | w || ( # ` B ) }
128		ssrab2 3543	. . . . . . . . . . . . . . . . . 18 |- { w e. Prime | w || ( # ` B ) } C_ Prime
129	127, 128	eqsstri 3491	. . . . . . . . . . . . . . . . 17 |- D C_ Prime
130	129	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> D C_ Prime )
131		ssid 3480	. . . . . . . . . . . . . . . . 17 |- D C_ D
132	131	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> D C_ D )
133	2, 3, 97	dprdres 17589	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) C_ ( G DProd T ) ) )
134	133	simpld 460	. . . . . . . . . . . . . . . . . 18 |- ( ph -> G dom DProd ( T |` D ) )
135		dprdsubg 17585	. . . . . . . . . . . . . . . . . . . . 21 |- ( G dom DProd ( T |` D ) -> ( G DProd ( T |` D ) ) e. (SubGrp ` G ) )
136	134, 135	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( G DProd ( T |` D ) ) e. (SubGrp ` G ) )
137		difssd 3590	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( A \ D ) C_ A )
138	2, 3, 137	dprdres 17589	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( G dom DProd ( T |` ( A \ D ) ) /\ ( G DProd ( T |` ( A \ D ) ) ) C_ ( G DProd T ) ) )
139	138	simpld 460	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> G dom DProd ( T |` ( A \ D ) ) )
140		dprdsubg 17585	. . . . . . . . . . . . . . . . . . . . 21 |- ( G dom DProd ( T |` ( A \ D ) ) -> ( G DProd ( T |` ( A \ D ) ) ) e. (SubGrp ` G ) )
141	139, 140	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( G DProd ( T |` ( A \ D ) ) ) e. (SubGrp ` G ) )
142		difss 3589	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A \ D ) C_ A
143		fssres 5757	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( T : A --> (SubGrp ` G ) /\ ( A \ D ) C_ A ) -> ( T |` ( A \ D ) ) : ( A \ D ) --> (SubGrp ` G ) )
144	4, 142, 143	sylancl 666	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( T |` ( A \ D ) ) : ( A \ D ) --> (SubGrp ` G ) )
145		fdm 5741	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T |` ( A \ D ) ) : ( A \ D ) --> (SubGrp ` G ) -> dom ( T |` ( A \ D ) ) = ( A \ D ) )
146	144, 145	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> dom ( T |` ( A \ D ) ) = ( A \ D ) )
147		fvres 5886	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( q e. ( A \ D ) -> ( ( T |` ( A \ D ) ) ` q ) = ( T ` q ) )
148	147	adantl 467	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ q e. ( A \ D ) ) -> ( ( T |` ( A \ D ) ) ` q ) = ( T ` q ) )
149		eldif 3443	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( q e. ( A \ D ) <-> ( q e. A /\ -. q e. D ) )
150	33	adantrr 721	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( T ` q ) e. Fin )
151	112	subg0cl 16769	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( T ` q ) e. (SubGrp ` G ) -> ( 0g ` G ) e. ( T ` q ) )
152	28, 151	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ q e. A ) -> ( 0g ` G ) e. ( T ` q ) )
153	152	snssd 4139	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ q e. A ) -> { ( 0g ` G ) } C_ ( T ` q ) )
154	153	adantrr 721	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } C_ ( T ` q ) )
155	38	adantrr 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( # ` ( T ` q ) ) = ( q ^ C ) )
156	39	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q e. Prime )
157		iddvdsexp 14293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( q e. ZZ /\ C e. NN ) -> q || ( q ^ C ) )
158	41, 157	sylan 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q || ( q ^ C ) )
159	56	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> ( q ^ C ) || ( # ` B ) )
160	38, 73	eqeltrrd 2509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ q e. A ) -> ( q ^ C ) e. ZZ )
161		dvdstr 14304	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( q e. ZZ /\ ( q ^ C ) e. ZZ /\ ( # ` B ) e. ZZ ) -> ( ( q || ( q ^ C ) /\ ( q ^ C ) || ( # ` B ) ) -> q || ( # ` B ) ) )
162	41, 160, 57, 161	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ q e. A ) -> ( ( q || ( q ^ C ) /\ ( q ^ C ) || ( # ` B ) ) -> q || ( # ` B ) ) )
163	162	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> ( ( q || ( q ^ C ) /\ ( q ^ C ) || ( # ` B ) ) -> q || ( # ` B ) ) )
164	158, 159, 163	mp2and 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q || ( # ` B ) )
165		breq1 4420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( w = q -> ( w || ( # ` B ) <-> q || ( # ` B ) ) )
166	165, 127	elrab2 3228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( q e. D <-> ( q e. Prime /\ q || ( # ` B ) ) )
167	156, 164, 166	sylanbrc 668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q e. D )
168	167	ex 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ q e. A ) -> ( C e. NN -> q e. D ) )
169	168	con3d 138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ q e. A ) -> ( -. q e. D -> -. C e. NN ) )
170	169	impr 623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> -. C e. NN )
171	42	adantrr 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> C e. NN0 )
172		elnn0 10860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( C e. NN0 <-> ( C e. NN \/ C = 0 ) )
173	171, 172	sylib 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( C e. NN \/ C = 0 ) )
174	173	ord 378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( -. C e. NN -> C = 0 ) )
175	170, 174	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> C = 0 )
176	175	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( q ^ C ) = ( q ^ 0 ) )
177	76	adantrr 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> q e. NN )
178	177	nncnd 10614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> q e. CC )
179	178	exp0d 12396	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( q ^ 0 ) = 1 )
180	155, 176, 179	3eqtrd 2465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( # ` ( T ` q ) ) = 1 )
181		fvex 5882	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 0g ` G ) e. _V
182		hashsng 12535	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 0g ` G ) e. _V -> ( # ` { ( 0g ` G ) } ) = 1 )
183	181, 182	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( # ` { ( 0g ` G ) } ) = 1
184	180, 183	syl6reqr 2480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( # ` { ( 0g ` G ) } ) = ( # ` ( T ` q ) ) )
185		snfi 7648	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- { ( 0g ` G ) } e. Fin
186		hashen 12516	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( { ( 0g ` G ) } e. Fin /\ ( T ` q ) e. Fin ) -> ( ( # ` { ( 0g ` G ) } ) = ( # ` ( T ` q ) ) <-> { ( 0g ` G ) } ~~ ( T ` q ) ) )
187	185, 150, 186	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( ( # ` { ( 0g ` G ) } ) = ( # ` ( T ` q ) ) <-> { ( 0g ` G ) } ~~ ( T ` q ) ) )
188	184, 187	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } ~~ ( T ` q ) )
189		fisseneq 7780	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( T ` q ) e. Fin /\ { ( 0g ` G ) } C_ ( T ` q ) /\ { ( 0g ` G ) } ~~ ( T ` q ) ) -> { ( 0g ` G ) } = ( T ` q ) )
190	150, 154, 188, 189	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } = ( T ` q ) )
191	112	subg0cl 16769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( G DProd ( T |` D ) ) e. (SubGrp ` G ) -> ( 0g ` G ) e. ( G DProd ( T |` D ) ) )
192	136, 191	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( 0g ` G ) e. ( G DProd ( T |` D ) ) )
193	192	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( 0g ` G ) e. ( G DProd ( T |` D ) ) )
194	193	snssd 4139	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } C_ ( G DProd ( T |` D ) ) )
195	190, 194	eqsstr3d 3496	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( T ` q ) C_ ( G DProd ( T |` D ) ) )
196	149, 195	sylan2b 477	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ q e. ( A \ D ) ) -> ( T ` q ) C_ ( G DProd ( T |` D ) ) )
197	148, 196	eqsstrd 3495	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ q e. ( A \ D ) ) -> ( ( T |` ( A \ D ) ) ` q ) C_ ( G DProd ( T |` D ) ) )
198	139, 146, 136, 197	dprdlub 17587	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( G DProd ( T |` ( A \ D ) ) ) C_ ( G DProd ( T |` D ) ) )
199		eqid 2420	. . . . . . . . . . . . . . . . . . . . 21 |- ( LSSum ` G ) = ( LSSum ` G )
200	199	lsmss2 17246	. . . . . . . . . . . . . . . . . . . 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 ) ) )
201	136, 141, 198, 200	syl3anc 1264	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( G DProd ( T |` D ) ) ( LSSum ` G ) ( G DProd ( T |` ( A \ D ) ) ) ) = ( G DProd ( T |` D ) ) )
202		disjdif 3864	. . . . . . . . . . . . . . . . . . . . . 22 |- ( D i^i ( A \ D ) ) = (/)
203	202	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( D i^i ( A \ D ) ) = (/) )
204		undif2 3868	. . . . . . . . . . . . . . . . . . . . . 22 |- ( D u. ( A \ D ) ) = ( D u. A )
205		ssequn1 3633	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( D C_ A <-> ( D u. A ) = A )
206	97, 205	sylib 199	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( D u. A ) = A )
207	204, 206	syl5req 2474	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> A = ( D u. ( A \ D ) ) )
208	4, 203, 207, 199, 2	dprdsplit 17609	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( G DProd T ) = ( ( G DProd ( T |` D ) ) ( LSSum ` G ) ( G DProd ( T |` ( A \ D ) ) ) ) )
209	1	simprd 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( G DProd T ) = B )
210	208, 209	eqtr3d 2463	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( G DProd ( T |` D ) ) ( LSSum ` G ) ( G DProd ( T |` ( A \ D ) ) ) ) = B )
211	201, 210	eqtr3d 2463	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( G DProd ( T |` D ) ) = B )
212	134, 211	jca 534	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) = B ) )
213	212	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) = B ) )
214	4, 97	fssresd 5758	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( T |` D ) : D --> (SubGrp ` G ) )
215	214, 103	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> dom ( T |` D ) = D )
216	215	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> dom ( T |` D ) = D )
217	97	sselda 3461	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ q e. D ) -> q e. A )
218	217, 42	syldan 472	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ q e. D ) -> C e. NN0 )
219	218	adantlr 719	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. Prime ) /\ q e. D ) -> C e. NN0 )
220		fvres 5886	. . . . . . . . . . . . . . . . . . . 20 |- ( q e. D -> ( ( T |` D ) ` q ) = ( T ` q ) )
221	220	adantl 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ q e. D ) -> ( ( T |` D ) ` q ) = ( T ` q ) )
222	221	fveq2d 5876	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ q e. D ) -> ( # ` ( ( T |` D ) ` q ) ) = ( # ` ( T ` q ) ) )
223	217, 38	syldan 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ q e. D ) -> ( # ` ( T ` q ) ) = ( q ^ C ) )
224	222, 223	eqtrd 2461	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ q e. D ) -> ( # ` ( ( T |` D ) ` q ) ) = ( q ^ C ) )
225	224	adantlr 719	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. Prime ) /\ q e. D ) -> ( # ` ( ( T |` D ) ` q ) ) = ( q ^ C ) )
226		simpr 462	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> x e. Prime )
227		fzfid 12172	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( 1 ... ( # ` B ) ) e. Fin )
228		prmnn 14585	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w e. Prime -> w e. NN )
229	228	3ad2ant2 1027	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w e. NN )
230		prmz 14586	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w e. Prime -> w e. ZZ )
231		dvdsle 14317	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( w e. ZZ /\ ( # ` B ) e. NN ) -> ( w || ( # ` B ) -> w <_ ( # ` B ) ) )
232	230, 50, 231	syl2anr 480	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ w e. Prime ) -> ( w || ( # ` B ) -> w <_ ( # ` B ) ) )
233	232	3impia 1202	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w <_ ( # ` B ) )
234	50	nnzd 11028	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( # ` B ) e. ZZ )
235	234	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> ( # ` B ) e. ZZ )
236		fznn 11850	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( # ` B ) e. ZZ -> ( w e. ( 1 ... ( # ` B ) ) <-> ( w e. NN /\ w <_ ( # ` B ) ) ) )
237	235, 236	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> ( w e. ( 1 ... ( # ` B ) ) <-> ( w e. NN /\ w <_ ( # ` B ) ) ) )
238	229, 233, 237	mpbir2and 930	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w e. ( 1 ... ( # ` B ) ) )
239	238	rabssdv 3538	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> { w e. Prime | w || ( # ` B ) } C_ ( 1 ... ( # ` B ) ) )
240	127, 239	syl5eqss 3505	. . . . . . . . . . . . . . . . . 18 |- ( ph -> D C_ ( 1 ... ( # ` B ) ) )
241		ssfi 7789	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 1 ... ( # ` B ) ) e. Fin /\ D C_ ( 1 ... ( # ` B ) ) ) -> D e. Fin )
242	227, 240, 241	syl2anc 665	. . . . . . . . . . . . . . . . 17 |- ( ph -> D e. Fin )
243	242	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> D e. Fin )
244	7, 8, 124, 125, 126, 130, 127, 132, 213, 216, 219, 225, 226, 243	ablfac1eulem 17633	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. Prime ) -> -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) )
245	244	ralrimiva 2837	. . . . . . . . . . . . . 14 |- ( ph -> A. x e. Prime -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) )
246	245	adantr 466	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> A. x e. Prime -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) )
247		id 23	. . . . . . . . . . . . . . . 16 |- ( x = q -> x = q )
248		sneq 4003	. . . . . . . . . . . . . . . . . . . 20 |- ( x = q -> { x } = { q } )
249	248	difeq2d 3580	. . . . . . . . . . . . . . . . . . 19 |- ( x = q -> ( D \ { x } ) = ( D \ { q } ) )
250	249	reseq2d 5116	. . . . . . . . . . . . . . . . . 18 |- ( x = q -> ( ( T |` D ) |` ( D \ { x } ) ) = ( ( T |` D ) |` ( D \ { q } ) ) )
251	250	oveq2d 6312	. . . . . . . . . . . . . . . . 17 |- ( x = q -> ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) = ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) )
252	251	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( x = q -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) = ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) )
253	247, 252	breq12d 4430	. . . . . . . . . . . . . . 15 |- ( x = q -> ( x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) <-> q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
254	253	notbid 295	. . . . . . . . . . . . . 14 |- ( x = q -> ( -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) <-> -. q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
255	254	rspcv 3175	. . . . . . . . . . . . 13 |- ( q e. Prime -> ( A. x e. Prime -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) -> -. q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
256	39, 246, 255	sylc 62	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> -. q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) )
257		coprm 14617	. . . . . . . . . . . . 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 ) )
258	39, 123, 257	syl2anc 665	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( -. q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) <-> ( q gcd ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) = 1 ) )
259	256, 258	mpbid 213	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( q gcd ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) = 1 )
260		rpexp1i 14633	. . . . . . . . . . . 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 ) )
261	41, 123, 52, 260	syl3anc 1264	. . . . . . . . . . 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 ) )
262	259, 261	mpd 15	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( ( q ^ ( q pCnt ( # ` B ) ) ) gcd ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) = 1 )
263		coprmdvds2 14620	. . . . . . . . . 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 ) ) )
264	78, 123, 57, 262, 263	syl31anc 1267	. . . . . . . . 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 ) ) )
265	94, 111, 264	mp2and 683	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( ( q ^ ( q pCnt ( # ` B ) ) ) x. ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) || ( # ` B ) )
266		eqid 2420	. . . . . . . . . 10 |- (Cntz ` G ) = (Cntz ` G )
267		inss1 3679	. . . . . . . . . . . . . 14 |- ( D i^i { q } ) C_ D
268	267	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> ( D i^i { q } ) C_ D )
269	100, 104, 268	dprdres 17589	. . . . . . . . . . . 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 ) ) ) )
270	269	simpld 460	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> G dom DProd ( ( T |` D ) |` ( D i^i { q } ) ) )
271		dprdsubg 17585	. . . . . . . . . . 11 |- ( G dom DProd ( ( T |` D ) |` ( D i^i { q } ) ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) e. (SubGrp ` G ) )
272	270, 271	syl 17	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) e. (SubGrp ` G ) )
273		inass 3669	. . . . . . . . . . . . 13 |- ( ( D i^i { q } ) i^i ( D \ { q } ) ) = ( D i^i ( { q } i^i ( D \ { q } ) ) )
274		disjdif 3864	. . . . . . . . . . . . . 14 |- ( { q } i^i ( D \ { q } ) ) = (/)
275	274	ineq2i 3658	. . . . . . . . . . . . 13 |- ( D i^i ( { q } i^i ( D \ { q } ) ) ) = ( D i^i (/) )
276		in0 3785	. . . . . . . . . . . . 13 |- ( D i^i (/) ) = (/)
277	273, 275, 276	3eqtri 2453	. . . . . . . . . . . 12 |- ( ( D i^i { q } ) i^i ( D \ { q } ) ) = (/)
278	277	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( ( D i^i { q } ) i^i ( D \ { q } ) ) = (/) )
279	100, 104, 268, 105, 278, 112	dprddisj2 17600	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) i^i ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) = { ( 0g ` G ) } )
280	100, 104, 268, 105, 278, 266	dprdcntz2 17599	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) C_ ( (Cntz ` G ) ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) )
281	7	dprdssv 17577	. . . . . . . . . . 11 |- ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) C_ B
282		ssfi 7789	. . . . . . . . . . 11 |- ( ( B e. Fin /\ ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) C_ B ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) e. Fin )
283	22, 281, 282	sylancl 666	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) e. Fin )
284	199, 112, 266, 272, 109, 279, 280, 283, 119	lsmhash 17283	. . . . . . . . 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 } ) ) ) ) ) )
285		inundif 3870	. . . . . . . . . . . . . 14 |- ( ( D i^i { q } ) u. ( D \ { q } ) ) = D
286	285	eqcomi 2433	. . . . . . . . . . . . 13 |- D = ( ( D i^i { q } ) u. ( D \ { q } ) )
287	286	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> D = ( ( D i^i { q } ) u. ( D \ { q } ) ) )
288	102, 278, 287, 199, 100	dprdsplit 17609	. . . . . . . . . . 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 } ) ) ) ) )
289	211	adantr 466	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( G DProd ( T |` D ) ) = B )
290	288, 289	eqtr3d 2463	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) ( LSSum ` G ) ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) = B )
291	290	fveq2d 5876	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( # ` ( ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) ( LSSum ` G ) ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) = ( # ` B ) )
292		snssi 4138	. . . . . . . . . . . . . . . . 17 |- ( q e. D -> { q } C_ D )
293	292	adantl 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> { q } C_ D )
294		dfss1 3664	. . . . . . . . . . . . . . . 16 |- ( { q } C_ D <-> ( D i^i { q } ) = { q } )
295	293, 294	sylib 199	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( D i^i { q } ) = { q } )
296	295	reseq2d 5116	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( ( T |` D ) |` ( D i^i { q } ) ) = ( ( T |` D ) |` { q } ) )
297	296	oveq2d 6312	. . . . . . . . . . . . 13 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( G DProd ( ( T |` D ) |` { q } ) ) )
298	100	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> G dom DProd ( T |` D ) )
299	215	ad2antrr 730	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> dom ( T |` D ) = D )
300		simpr 462	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> q e. D )
301	298, 299, 300	dpjlem 17612	. . . . . . . . . . . . 13 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( G DProd ( ( T |` D ) |` { q } ) ) = ( ( T |` D ) ` q ) )
302	220	adantl 467	. . . . . . . . . . . . 13 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( ( T |` D ) ` q ) = ( T ` q ) )
303	297, 301, 302	3eqtrd 2465	. . . . . . . . . . . 12 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
304		simprr 764	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> -. q e. D )
305		disjsn 4054	. . . . . . . . . . . . . . . . . 18 |- ( ( D i^i { q } ) = (/) <-> -. q e. D )
306	304, 305	sylibr 215	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( D i^i { q } ) = (/) )
307	306	reseq2d 5116	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( ( T |` D ) |` ( D i^i { q } ) ) = ( ( T |` D ) |` (/) ) )
308		res0 5120	. . . . . . . . . . . . . . . 16 |- ( ( T |` D ) |` (/) ) = (/)
309	307, 308	syl6eq 2477	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( ( T |` D ) |` ( D i^i { q } ) ) = (/) )
310	309	oveq2d 6312	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( G DProd (/) ) )
311	112	dprd0 17592	. . . . . . . . . . . . . . . . 17 |- ( G e. Grp -> ( G dom DProd (/) /\ ( G DProd (/) ) = { ( 0g ` G ) } ) )
312	45, 311	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> ( G dom DProd (/) /\ ( G DProd (/) ) = { ( 0g ` G ) } ) )
313	312	simprd 464	. . . . . . . . . . . . . . 15 |- ( ph -> ( G DProd (/) ) = { ( 0g ` G ) } )
314	313	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( G DProd (/) ) = { ( 0g ` G ) } )
315	310, 314, 190	3eqtrd 2465	. . . . . . . . . . . . 13 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
316	315	anassrs 652	. . . . . . . . . . . 12 |- ( ( ( ph /\ q e. A ) /\ -. q e. D ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
317	303, 316	pm2.61dan 798	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
318	317	fveq2d 5876	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) ) = ( # ` ( T ` q ) ) )
319	318	oveq1d 6311	. . . . . . . . 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 } ) ) ) ) ) )
320	284, 291, 319	3eqtr3d 2469	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( # ` B ) = ( ( # ` ( T ` q ) ) x. ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
321	265, 320	breqtrd 4441	. . . . . . 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 } ) ) ) ) ) )
322	122	nnne0d 10643	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) =/= 0 )
323		dvdsmulcr 14299	. . . . . . . 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 ) ) ) )
324	78, 73, 123, 322, 323	syl112anc 1268	. . . . . . 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 ) ) ) )
325	321, 324	mpbid 213	. . . . . 6 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` ( T ` q ) ) )
326		dvdseq 14319	. . . . . 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 ) ) ) )
327	72, 92, 65, 325, 326	syl22anc 1265	. . . . 5 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
328	7, 8, 9, 10, 11, 12	ablfac1a 17630	. . . . 5 |- ( ( ph /\ q e. A ) -> ( # ` ( S ` q ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
329	327, 328	eqtr4d 2464	. . . 4 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) = ( # ` ( S ` q ) ) )
330		hashen 12516	. . . . 5 |- ( ( ( T ` q ) e. Fin /\ ( S ` q ) e. Fin ) -> ( ( # ` ( T ` q ) ) = ( # ` ( S ` q ) ) <-> ( T ` q ) ~~ ( S ` q ) ) )
331	33, 27, 330	syl2anc 665	. . . 4 |- ( ( ph /\ q e. A ) -> ( ( # ` ( T ` q ) ) = ( # ` ( S ` q ) ) <-> ( T ` q ) ~~ ( S ` q ) ) )
332	329, 331	mpbid 213	. . 3 |- ( ( ph /\ q e. A ) -> ( T ` q ) ~~ ( S ` q ) )
333		fisseneq 7780	. . 3 |- ( ( ( S ` q ) e. Fin /\ ( T ` q ) C_ ( S ` q ) /\ ( T ` q ) ~~ ( S ` q ) ) -> ( T ` q ) = ( S ` q ) )
334	27, 91, 332, 333	syl3anc 1264	. 2 |- ( ( ph /\ q e. A ) -> ( T ` q ) = ( S ` q ) )
335	6, 21, 334	eqfnfvd 5985	1 |- ( ph -> T = S )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1867   =/= wne 2616   A.wral 2773   {crab 2777   _Vcvv 3078   \ cdif 3430   u. cun 3431   i^i cin 3432   C_ wss 3433   (/)c0 3758   {csn 3993   class class class wbr 4417   |-> cmpt 4475   dom cdm 4845   |` cres 4847   Fn wfn 5587   -->wf 5588   ` cfv 5592  (class class class)co 6296   ~~ cen 7565   Fincfn 7568   0cc0 9528   1c1 9529   x. cmul 9533   <_ cle 9665   NNcn 10598   NN0cn0 10858   ZZcz 10926   ZZ>=cuz 11148   ...cfz 11771   ^cexp 12258   #chash 12501   || cdvds 14272   gcd cgcd 14431   Primecprime 14582   pCnt cpc 14738   Basecbs 15073   0gc0g 15290   Grpcgrp 16613  SubGrpcsubg 16755  Cntzccntz 16913   odcod 17109   LSSumclsm 17214   Abelcabl 17359   DProd cdprd 17553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4529  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-inf2 8137  ax-cnex 9584  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604  ax-pre-mulgt0 9605  ax-pre-sup 9606

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-int 4250  df-iun 4295  df-iin 4296  df-disj 4389  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-se 4805  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-isom 5601  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-of 6536  df-om 6698  df-1st 6798  df-2nd 6799  df-supp 6917  df-tpos 6972  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-1o 7181  df-2o 7182  df-oadd 7185  df-omul 7186  df-er 7362  df-ec 7364  df-qs 7368  df-map 7473  df-ixp 7522  df-en 7569  df-dom 7570  df-sdom 7571  df-fin 7572  df-fsupp 7881  df-sup 7953  df-inf 7954  df-oi 8016  df-card 8363  df-acn 8366  df-cda 8587  df-pnf 9666  df-mnf 9667  df-xr 9668  df-ltxr 9669  df-le 9670  df-sub 9851  df-neg 9852  df-div 10259  df-nn 10599  df-2 10657  df-3 10658  df-n0 10859  df-z 10927  df-uz 11149  df-q 11254  df-rp 11292  df-fz 11772  df-fzo 11903  df-fl 12014  df-mod 12083  df-seq 12200  df-exp 12259  df-fac 12446  df-bc 12474  df-hash 12502  df-cj 13130  df-re 13131  df-im 13132  df-sqrt 13266  df-abs 13267  df-clim 13519  df-sum 13720  df-dvds 14273  df-gcd 14432  df-prm 14583  df-pc 14739  df-ndx 15076  df-slot 15077  df-base 15078  df-sets 15079  df-ress 15080  df-plusg 15155  df-0g 15292  df-gsum 15293  df-mre 15436  df-mrc 15437  df-acs 15439  df-mgm 16432  df-sgrp 16471  df-mnd 16481  df-mhm 16526  df-submnd 16527  df-grp 16617  df-minusg 16618  df-sbg 16619  df-mulg 16620  df-subg 16758  df-eqg 16760  df-ghm 16825  df-gim 16867  df-ga 16888  df-cntz 16915  df-oppg 16941  df-od 17113  df-lsm 17216  df-pj1 17217  df-cmn 17360  df-abl 17361  df-dprd 17555

This theorem is referenced by: (None)