Theorem ablfac1eu 17706

Description: The factorization of ablfac1b 17703 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 461	. . . 4 |- ( ph -> G dom DProd T )
3		ablfac1eu.2	. . . 4 |- ( ph -> dom T = A )
4	2, 3	dprdf2 17639	. . 3 |- ( ph -> T : A --> (SubGrp ` G ) )
5		ffn 5728	. . 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 17703	. . . 4 |- ( ph -> G dom DProd S )
14		fvex 5875	. . . . . . . 8 |- ( Base ` G ) e. _V
15	7, 14	eqeltri 2525	. . . . . . 7 |- B e. _V
16	15	rabex 4554	. . . . . 6 |- { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } e. _V
17	16, 9	dmmpti 5707	. . . . 5 |- dom S = A
18	17	a1i 11	. . . 4 |- ( ph -> dom S = A )
19	13, 18	dprdf2 17639	. . 3 |- ( ph -> S : A --> (SubGrp ` G ) )
20		ffn 5728	. . 3 |- ( S : A --> (SubGrp ` G ) -> S Fn A )
21	19, 20	syl 17	. 2 |- ( ph -> S Fn A )
22	11	adantr 467	. . . 4 |- ( ( ph /\ q e. A ) -> B e. Fin )
23	19	ffvelrnda 6022	. . . . 5 |- ( ( ph /\ q e. A ) -> ( S ` q ) e. (SubGrp ` G ) )
24	7	subgss 16818	. . . . 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 7792	. . . 4 |- ( ( B e. Fin /\ ( S ` q ) C_ B ) -> ( S ` q ) e. Fin )
27	22, 25, 26	syl2anc 667	. . 3 |- ( ( ph /\ q e. A ) -> ( S ` q ) e. Fin )
28	4	ffvelrnda 6022	. . . . . 6 |- ( ( ph /\ q e. A ) -> ( T ` q ) e. (SubGrp ` G ) )
29	7	subgss 16818	. . . . . 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 467	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( T ` q ) e. (SubGrp ` G ) )
32		ssfi 7792	. . . . . . . . 9 |- ( ( B e. Fin /\ ( T ` q ) C_ B ) -> ( T ` q ) e. Fin )
33	22, 30, 32	syl2anc 667	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( T ` q ) e. Fin )
34	33	adantr 467	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( T ` q ) e. Fin )
35		simpr 463	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> x e. ( T ` q ) )
36	8	odsubdvds 17220	. . . . . . 7 |- ( ( ( T ` q ) e. (SubGrp ` G ) /\ ( T ` q ) e. Fin /\ x e. ( T ` q ) ) -> ( O ` x ) || ( # ` ( T ` q ) ) )
37	31, 34, 35, 36	syl3anc 1268	. . . . . 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 3432	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> q e. Prime )
40		prmz 14626	. . . . . . . . . 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 11038	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> C e. ZZ )
44		ablgrp 17435	. . . . . . . . . . . . . . . 16 |- ( G e. Abel -> G e. Grp )
45	10, 44	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> G e. Grp )
46	7	grpbn0 16695	. . . . . . . . . . . . . . 15 |- ( G e. Grp -> B =/= (/) )
47	45, 46	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> B =/= (/) )
48		hashnncl 12547	. . . . . . . . . . . . . . 15 |- ( B e. Fin -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
49	11, 48	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
50	47, 49	mpbird 236	. . . . . . . . . . . . 13 |- ( ph -> ( # ` B ) e. NN )
51	50	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( # ` B ) e. NN )
52	39, 51	pccld 14800	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. NN0 )
53	52	nn0zd 11038	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. ZZ )
54	7	lagsubg 16879	. . . . . . . . . . . . 13 |- ( ( ( T ` q ) e. (SubGrp ` G ) /\ B e. Fin ) -> ( # ` ( T ` q ) ) || ( # ` B ) )
55	28, 22, 54	syl2anc 667	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) || ( # ` B ) )
56	38, 55	eqbrtrrd 4425	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( q ^ C ) || ( # ` B ) )
57	51	nnzd 11039	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( # ` B ) e. ZZ )
58		pcdvdsb 14818	. . . . . . . . . . . 12 |- ( ( q e. Prime /\ ( # ` B ) e. ZZ /\ C e. NN0 ) -> ( C <_ ( q pCnt ( # ` B ) ) <-> ( q ^ C ) || ( # ` B ) ) )
59	39, 57, 42, 58	syl3anc 1268	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( C <_ ( q pCnt ( # ` B ) ) <-> ( q ^ C ) || ( # ` B ) ) )
60	56, 59	mpbird 236	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> C <_ ( q pCnt ( # ` B ) ) )
61		eluz2 11165	. . . . . . . . . 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 1192	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. ( ZZ>= ` C ) )
63		dvdsexp 14361	. . . . . . . . 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 1268	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( q ^ C ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
65	38, 64	eqbrtrd 4423	. . . . . . 7 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
66	65	adantr 467	. . . . . 6 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( # ` ( T ` q ) ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
67	30	sselda 3432	. . . . . . . . 9 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> x e. B )
68	7, 8	odcl 17185	. . . . . . . . 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 11038	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( O ` x ) e. ZZ )
71		hashcl 12538	. . . . . . . . . 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 11038	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) e. ZZ )
74	73	adantr 467	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( # ` ( T ` q ) ) e. ZZ )
75		prmnn 14625	. . . . . . . . . . 11 |- ( q e. Prime -> q e. NN )
76	39, 75	syl 17	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> q e. NN )
77	76, 52	nnexpcld 12437	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. NN )
78	77	nnzd 11039	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. ZZ )
79	78	adantr 467	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. ZZ )
80		dvdstr 14337	. . . . . . 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 1268	. . . . . 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 685	. . . . 5 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
83	30, 82	ssrabdv 3508	. . . 4 |- ( ( ph /\ q e. A ) -> ( T ` q ) C_ { x e. B | ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) } )
84		id 22	. . . . . . . . 9 |- ( p = q -> p = q )
85		oveq1 6297	. . . . . . . . 9 |- ( p = q -> ( p pCnt ( # ` B ) ) = ( q pCnt ( # ` B ) ) )
86	84, 85	oveq12d 6308	. . . . . . . 8 |- ( p = q -> ( p ^ ( p pCnt ( # ` B ) ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
87	86	breq2d 4414	. . . . . . 7 |- ( p = q -> ( ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) <-> ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) ) )
88	87	rabbidv 3036	. . . . . 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 5953	. . . . 5 |- ( q e. A -> ( S ` q ) = { x e. B | ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) } )
90	89	adantl 468	. . . 4 |- ( ( ph /\ q e. A ) -> ( S ` q ) = { x e. B | ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) } )
91	83, 90	sseqtr4d 3469	. . 3 |- ( ( ph /\ q e. A ) -> ( T ` q ) C_ ( S ` q ) )
92	77	nnnn0d 10925	. . . . . 6 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. NN0 )
93		pcdvds 14813	. . . . . . . . . 10 |- ( ( q e. Prime /\ ( # ` B ) e. NN ) -> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` B ) )
94	39, 51, 93	syl2anc 667	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` B ) )
95	2	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. A ) -> G dom DProd T )
96	3	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. A ) -> dom T = A )
97		ablfac1.2	. . . . . . . . . . . . . . . 16 |- ( ph -> D C_ A )
98	97	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. A ) -> D C_ A )
99	95, 96, 98	dprdres 17661	. . . . . . . . . . . . . 14 |- ( ( ph /\ q e. A ) -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) C_ ( G DProd T ) ) )
100	99	simpld 461	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> G dom DProd ( T |` D ) )
101	4	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. A ) -> T : A --> (SubGrp ` G ) )
102	101, 98	fssresd 5750	. . . . . . . . . . . . . 14 |- ( ( ph /\ q e. A ) -> ( T |` D ) : D --> (SubGrp ` G ) )
103		fdm 5733	. . . . . . . . . . . . . 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 3561	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> ( D \ { q } ) C_ D )
106	100, 104, 105	dprdres 17661	. . . . . . . . . . . 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 461	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> G dom DProd ( ( T |` D ) |` ( D \ { q } ) ) )
108		dprdsubg 17657	. . . . . . . . . . 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 16879	. . . . . . . . . 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 667	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) || ( # ` B ) )
112		eqid 2451	. . . . . . . . . . . . . . 15 |- ( 0g ` G ) = ( 0g ` G )
113	112	subg0cl 16825	. . . . . . . . . . . . . 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 3737	. . . . . . . . . . . . 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 17649	. . . . . . . . . . . . . 14 |- ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) C_ B
118		ssfi 7792	. . . . . . . . . . . . . 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 668	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. Fin )
120		hashnncl 12547	. . . . . . . . . . . . 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 236	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) e. NN )
123	122	nnzd 11039	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) e. ZZ )
124		eqid 2451	. . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> G e. Abel )
126	11	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> B e. Fin )
127		ablfac1c.d	. . . . . . . . . . . . . . . . . 18 |- D = { w e. Prime | w || ( # ` B ) }
128		ssrab2 3514	. . . . . . . . . . . . . . . . . 18 |- { w e. Prime | w || ( # ` B ) } C_ Prime
129	127, 128	eqsstri 3462	. . . . . . . . . . . . . . . . 17 |- D C_ Prime
130	129	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> D C_ Prime )
131		ssid 3451	. . . . . . . . . . . . . . . . 17 |- D C_ D
132	131	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> D C_ D )
133	2, 3, 97	dprdres 17661	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) C_ ( G DProd T ) ) )
134	133	simpld 461	. . . . . . . . . . . . . . . . . 18 |- ( ph -> G dom DProd ( T |` D ) )
135		dprdsubg 17657	. . . . . . . . . . . . . . . . . . . . 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 3561	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( A \ D ) C_ A )
138	2, 3, 137	dprdres 17661	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( G dom DProd ( T |` ( A \ D ) ) /\ ( G DProd ( T |` ( A \ D ) ) ) C_ ( G DProd T ) ) )
139	138	simpld 461	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> G dom DProd ( T |` ( A \ D ) ) )
140		dprdsubg 17657	. . . . . . . . . . . . . . . . . . . . 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 3560	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A \ D ) C_ A
143		fssres 5749	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( T : A --> (SubGrp ` G ) /\ ( A \ D ) C_ A ) -> ( T |` ( A \ D ) ) : ( A \ D ) --> (SubGrp ` G ) )
144	4, 142, 143	sylancl 668	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( T |` ( A \ D ) ) : ( A \ D ) --> (SubGrp ` G ) )
145		fdm 5733	. . . . . . . . . . . . . . . . . . . . . 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 5879	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( q e. ( A \ D ) -> ( ( T |` ( A \ D ) ) ` q ) = ( T ` q ) )
148	147	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ q e. ( A \ D ) ) -> ( ( T |` ( A \ D ) ) ` q ) = ( T ` q ) )
149		eldif 3414	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( q e. ( A \ D ) <-> ( q e. A /\ -. q e. D ) )
150	33	adantrr 723	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( T ` q ) e. Fin )
151	112	subg0cl 16825	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4117	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ q e. A ) -> { ( 0g ` G ) } C_ ( T ` q ) )
154	153	adantrr 723	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } C_ ( T ` q ) )
155	38	adantrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( # ` ( T ` q ) ) = ( q ^ C ) )
156	39	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q e. Prime )
157		iddvdsexp 14326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( q e. ZZ /\ C e. NN ) -> q || ( q ^ C ) )
158	41, 157	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q || ( q ^ C ) )
159	56	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> ( q ^ C ) || ( # ` B ) )
160	38, 73	eqeltrrd 2530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ q e. A ) -> ( q ^ C ) e. ZZ )
161		dvdstr 14337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ q e. A ) -> ( ( q || ( q ^ C ) /\ ( q ^ C ) || ( # ` B ) ) -> q || ( # ` B ) ) )
163	162	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> ( ( q || ( q ^ C ) /\ ( q ^ C ) || ( # ` B ) ) -> q || ( # ` B ) ) )
164	158, 159, 163	mp2and 685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q || ( # ` B ) )
165		breq1 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( w = q -> ( w || ( # ` B ) <-> q || ( # ` B ) ) )
166	165, 127	elrab2 3198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( q e. D <-> ( q e. Prime /\ q || ( # ` B ) ) )
167	156, 164, 166	sylanbrc 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q e. D )
168	167	ex 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ q e. A ) -> ( C e. NN -> q e. D ) )
169	168	con3d 139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ q e. A ) -> ( -. q e. D -> -. C e. NN ) )
170	169	impr 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> -. C e. NN )
171	42	adantrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> C e. NN0 )
172		elnn0 10871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( C e. NN0 <-> ( C e. NN \/ C = 0 ) )
173	171, 172	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( C e. NN \/ C = 0 ) )
174	173	ord 379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6306	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( q ^ C ) = ( q ^ 0 ) )
177	76	adantrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> q e. NN )
178	177	nncnd 10625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> q e. CC )
179	178	exp0d 12410	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( q ^ 0 ) = 1 )
180	155, 176, 179	3eqtrd 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( # ` ( T ` q ) ) = 1 )
181		fvex 5875	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 0g ` G ) e. _V
182		hashsng 12549	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 0g ` G ) e. _V -> ( # ` { ( 0g ` G ) } ) = 1 )
183	181, 182	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( # ` { ( 0g ` G ) } ) = 1
184	180, 183	syl6reqr 2504	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( # ` { ( 0g ` G ) } ) = ( # ` ( T ` q ) ) )
185		snfi 7650	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- { ( 0g ` G ) } e. Fin
186		hashen 12530	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( { ( 0g ` G ) } e. Fin /\ ( T ` q ) e. Fin ) -> ( ( # ` { ( 0g ` G ) } ) = ( # ` ( T ` q ) ) <-> { ( 0g ` G ) } ~~ ( T ` q ) ) )
187	185, 150, 186	sylancr 669	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( ( # ` { ( 0g ` G ) } ) = ( # ` ( T ` q ) ) <-> { ( 0g ` G ) } ~~ ( T ` q ) ) )
188	184, 187	mpbid 214	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } ~~ ( T ` q ) )
189		fisseneq 7783	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( T ` q ) e. Fin /\ { ( 0g ` G ) } C_ ( T ` q ) /\ { ( 0g ` G ) } ~~ ( T ` q ) ) -> { ( 0g ` G ) } = ( T ` q ) )
190	150, 154, 188, 189	syl3anc 1268	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } = ( T ` q ) )
191	112	subg0cl 16825	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( 0g ` G ) e. ( G DProd ( T |` D ) ) )
194	193	snssd 4117	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } C_ ( G DProd ( T |` D ) ) )
195	190, 194	eqsstr3d 3467	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( T ` q ) C_ ( G DProd ( T |` D ) ) )
196	149, 195	sylan2b 478	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ q e. ( A \ D ) ) -> ( T ` q ) C_ ( G DProd ( T |` D ) ) )
197	148, 196	eqsstrd 3466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ q e. ( A \ D ) ) -> ( ( T |` ( A \ D ) ) ` q ) C_ ( G DProd ( T |` D ) ) )
198	139, 146, 136, 197	dprdlub 17659	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( G DProd ( T |` ( A \ D ) ) ) C_ ( G DProd ( T |` D ) ) )
199		eqid 2451	. . . . . . . . . . . . . . . . . . . . 21 |- ( LSSum ` G ) = ( LSSum ` G )
200	199	lsmss2 17318	. . . . . . . . . . . . . . . . . . . 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 1268	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( G DProd ( T |` D ) ) ( LSSum ` G ) ( G DProd ( T |` ( A \ D ) ) ) ) = ( G DProd ( T |` D ) ) )
202		disjdif 3839	. . . . . . . . . . . . . . . . . . . . . 22 |- ( D i^i ( A \ D ) ) = (/)
203	202	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( D i^i ( A \ D ) ) = (/) )
204		undif2 3843	. . . . . . . . . . . . . . . . . . . . . 22 |- ( D u. ( A \ D ) ) = ( D u. A )
205		ssequn1 3604	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( D C_ A <-> ( D u. A ) = A )
206	97, 205	sylib 200	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( D u. A ) = A )
207	204, 206	syl5req 2498	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> A = ( D u. ( A \ D ) ) )
208	4, 203, 207, 199, 2	dprdsplit 17681	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( G DProd T ) = ( ( G DProd ( T |` D ) ) ( LSSum ` G ) ( G DProd ( T |` ( A \ D ) ) ) ) )
209	1	simprd 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( G DProd T ) = B )
210	208, 209	eqtr3d 2487	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( G DProd ( T |` D ) ) ( LSSum ` G ) ( G DProd ( T |` ( A \ D ) ) ) ) = B )
211	201, 210	eqtr3d 2487	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( G DProd ( T |` D ) ) = B )
212	134, 211	jca 535	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) = B ) )
213	212	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) = B ) )
214	4, 97	fssresd 5750	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( T |` D ) : D --> (SubGrp ` G ) )
215	214, 103	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> dom ( T |` D ) = D )
216	215	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> dom ( T |` D ) = D )
217	97	sselda 3432	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ q e. D ) -> q e. A )
218	217, 42	syldan 473	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ q e. D ) -> C e. NN0 )
219	218	adantlr 721	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. Prime ) /\ q e. D ) -> C e. NN0 )
220		fvres 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( q e. D -> ( ( T |` D ) ` q ) = ( T ` q ) )
221	220	adantl 468	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ q e. D ) -> ( ( T |` D ) ` q ) = ( T ` q ) )
222	221	fveq2d 5869	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ q e. D ) -> ( # ` ( ( T |` D ) ` q ) ) = ( # ` ( T ` q ) ) )
223	217, 38	syldan 473	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ q e. D ) -> ( # ` ( T ` q ) ) = ( q ^ C ) )
224	222, 223	eqtrd 2485	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ q e. D ) -> ( # ` ( ( T |` D ) ` q ) ) = ( q ^ C ) )
225	224	adantlr 721	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. Prime ) /\ q e. D ) -> ( # ` ( ( T |` D ) ` q ) ) = ( q ^ C ) )
226		simpr 463	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> x e. Prime )
227		fzfid 12186	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( 1 ... ( # ` B ) ) e. Fin )
228		prmnn 14625	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w e. Prime -> w e. NN )
229	228	3ad2ant2 1030	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w e. NN )
230		prmz 14626	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w e. Prime -> w e. ZZ )
231		dvdsle 14350	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( w e. ZZ /\ ( # ` B ) e. NN ) -> ( w || ( # ` B ) -> w <_ ( # ` B ) ) )
232	230, 50, 231	syl2anr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ w e. Prime ) -> ( w || ( # ` B ) -> w <_ ( # ` B ) ) )
233	232	3impia 1205	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w <_ ( # ` B ) )
234	50	nnzd 11039	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( # ` B ) e. ZZ )
235	234	3ad2ant1 1029	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> ( # ` B ) e. ZZ )
236		fznn 11863	. . . . . . . . . . . . . . . . . . . . . 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 933	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w e. ( 1 ... ( # ` B ) ) )
239	238	rabssdv 3509	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> { w e. Prime | w || ( # ` B ) } C_ ( 1 ... ( # ` B ) ) )
240	127, 239	syl5eqss 3476	. . . . . . . . . . . . . . . . . 18 |- ( ph -> D C_ ( 1 ... ( # ` B ) ) )
241		ssfi 7792	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 1 ... ( # ` B ) ) e. Fin /\ D C_ ( 1 ... ( # ` B ) ) ) -> D e. Fin )
242	227, 240, 241	syl2anc 667	. . . . . . . . . . . . . . . . 17 |- ( ph -> D e. Fin )
243	242	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> D e. Fin )
244	7, 8, 124, 125, 126, 130, 127, 132, 213, 216, 219, 225, 226, 243	ablfac1eulem 17705	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. Prime ) -> -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) )
245	244	ralrimiva 2802	. . . . . . . . . . . . . 14 |- ( ph -> A. x e. Prime -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) )
246	245	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> A. x e. Prime -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) )
247		id 22	. . . . . . . . . . . . . . . 16 |- ( x = q -> x = q )
248		sneq 3978	. . . . . . . . . . . . . . . . . . . 20 |- ( x = q -> { x } = { q } )
249	248	difeq2d 3551	. . . . . . . . . . . . . . . . . . 19 |- ( x = q -> ( D \ { x } ) = ( D \ { q } ) )
250	249	reseq2d 5105	. . . . . . . . . . . . . . . . . 18 |- ( x = q -> ( ( T |` D ) |` ( D \ { x } ) ) = ( ( T |` D ) |` ( D \ { q } ) ) )
251	250	oveq2d 6306	. . . . . . . . . . . . . . . . 17 |- ( x = q -> ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) = ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) )
252	251	fveq2d 5869	. . . . . . . . . . . . . . . 16 |- ( x = q -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) = ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) )
253	247, 252	breq12d 4415	. . . . . . . . . . . . . . 15 |- ( x = q -> ( x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) <-> q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
254	253	notbid 296	. . . . . . . . . . . . . 14 |- ( x = q -> ( -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) <-> -. q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
255	254	rspcv 3146	. . . . . . . . . . . . 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 14657	. . . . . . . . . . . . 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 667	. . . . . . . . . . . 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 214	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( q gcd ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) = 1 )
260		rpexp1i 14673	. . . . . . . . . . . 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 1268	. . . . . . . . . . 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 14660	. . . . . . . . . 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 1271	. . . . . . . . 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 685	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( ( q ^ ( q pCnt ( # ` B ) ) ) x. ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) || ( # ` B ) )
266		eqid 2451	. . . . . . . . . 10 |- (Cntz ` G ) = (Cntz ` G )
267		inss1 3652	. . . . . . . . . . . . . 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 17661	. . . . . . . . . . . 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 461	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> G dom DProd ( ( T |` D ) |` ( D i^i { q } ) ) )
271		dprdsubg 17657	. . . . . . . . . . 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 3642	. . . . . . . . . . . . 13 |- ( ( D i^i { q } ) i^i ( D \ { q } ) ) = ( D i^i ( { q } i^i ( D \ { q } ) ) )
274		disjdif 3839	. . . . . . . . . . . . . 14 |- ( { q } i^i ( D \ { q } ) ) = (/)
275	274	ineq2i 3631	. . . . . . . . . . . . 13 |- ( D i^i ( { q } i^i ( D \ { q } ) ) ) = ( D i^i (/) )
276		in0 3760	. . . . . . . . . . . . 13 |- ( D i^i (/) ) = (/)
277	273, 275, 276	3eqtri 2477	. . . . . . . . . . . 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 17672	. . . . . . . . . 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 17671	. . . . . . . . . 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 17649	. . . . . . . . . . 11 |- ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) C_ B
282		ssfi 7792	. . . . . . . . . . 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 668	. . . . . . . . . 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 17355	. . . . . . . . 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 3845	. . . . . . . . . . . . . 14 |- ( ( D i^i { q } ) u. ( D \ { q } ) ) = D
286	285	eqcomi 2460	. . . . . . . . . . . . 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 17681	. . . . . . . . . . 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 467	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( G DProd ( T |` D ) ) = B )
290	288, 289	eqtr3d 2487	. . . . . . . . . 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 5869	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( # ` ( ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) ( LSSum ` G ) ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) = ( # ` B ) )
292		snssi 4116	. . . . . . . . . . . . . . . . 17 |- ( q e. D -> { q } C_ D )
293	292	adantl 468	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> { q } C_ D )
294		dfss1 3637	. . . . . . . . . . . . . . . 16 |- ( { q } C_ D <-> ( D i^i { q } ) = { q } )
295	293, 294	sylib 200	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( D i^i { q } ) = { q } )
296	295	reseq2d 5105	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( ( T |` D ) |` ( D i^i { q } ) ) = ( ( T |` D ) |` { q } ) )
297	296	oveq2d 6306	. . . . . . . . . . . . 13 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( G DProd ( ( T |` D ) |` { q } ) ) )
298	100	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> G dom DProd ( T |` D ) )
299	215	ad2antrr 732	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> dom ( T |` D ) = D )
300		simpr 463	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> q e. D )
301	298, 299, 300	dpjlem 17684	. . . . . . . . . . . . 13 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( G DProd ( ( T |` D ) |` { q } ) ) = ( ( T |` D ) ` q ) )
302	220	adantl 468	. . . . . . . . . . . . 13 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( ( T |` D ) ` q ) = ( T ` q ) )
303	297, 301, 302	3eqtrd 2489	. . . . . . . . . . . 12 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
304		simprr 766	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> -. q e. D )
305		disjsn 4032	. . . . . . . . . . . . . . . . . 18 |- ( ( D i^i { q } ) = (/) <-> -. q e. D )
306	304, 305	sylibr 216	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( D i^i { q } ) = (/) )
307	306	reseq2d 5105	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( ( T |` D ) |` ( D i^i { q } ) ) = ( ( T |` D ) |` (/) ) )
308		res0 5109	. . . . . . . . . . . . . . . 16 |- ( ( T |` D ) |` (/) ) = (/)
309	307, 308	syl6eq 2501	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( ( T |` D ) |` ( D i^i { q } ) ) = (/) )
310	309	oveq2d 6306	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( G DProd (/) ) )
311	112	dprd0 17664	. . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . 15 |- ( ph -> ( G DProd (/) ) = { ( 0g ` G ) } )
314	313	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( G DProd (/) ) = { ( 0g ` G ) } )
315	310, 314, 190	3eqtrd 2489	. . . . . . . . . . . . 13 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
316	315	anassrs 654	. . . . . . . . . . . 12 |- ( ( ( ph /\ q e. A ) /\ -. q e. D ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
317	303, 316	pm2.61dan 800	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
318	317	fveq2d 5869	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) ) = ( # ` ( T ` q ) ) )
319	318	oveq1d 6305	. . . . . . . . 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 2493	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( # ` B ) = ( ( # ` ( T ` q ) ) x. ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
321	265, 320	breqtrd 4427	. . . . . . 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 10654	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) =/= 0 )
323		dvdsmulcr 14332	. . . . . . . 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 1272	. . . . . . 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 214	. . . . . 6 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` ( T ` q ) ) )
326		dvdseq 14352	. . . . . 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 1269	. . . . 5 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
328	7, 8, 9, 10, 11, 12	ablfac1a 17702	. . . . 5 |- ( ( ph /\ q e. A ) -> ( # ` ( S ` q ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
329	327, 328	eqtr4d 2488	. . . 4 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) = ( # ` ( S ` q ) ) )
330		hashen 12530	. . . . 5 |- ( ( ( T ` q ) e. Fin /\ ( S ` q ) e. Fin ) -> ( ( # ` ( T ` q ) ) = ( # ` ( S ` q ) ) <-> ( T ` q ) ~~ ( S ` q ) ) )
331	33, 27, 330	syl2anc 667	. . . 4 |- ( ( ph /\ q e. A ) -> ( ( # ` ( T ` q ) ) = ( # ` ( S ` q ) ) <-> ( T ` q ) ~~ ( S ` q ) ) )
332	329, 331	mpbid 214	. . 3 |- ( ( ph /\ q e. A ) -> ( T ` q ) ~~ ( S ` q ) )
333		fisseneq 7783	. . 3 |- ( ( ( S ` q ) e. Fin /\ ( T ` q ) C_ ( S ` q ) /\ ( T ` q ) ~~ ( S ` q ) ) -> ( T ` q ) = ( S ` q ) )
334	27, 91, 332, 333	syl3anc 1268	. 2 |- ( ( ph /\ q e. A ) -> ( T ` q ) = ( S ` q ) )
335	6, 21, 334	eqfnfvd 5979	1 |- ( ph -> T = S )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   /\ w3a 985   = wceq 1444   e. wcel 1887   =/= wne 2622   A.wral 2737   {crab 2741   _Vcvv 3045   \ cdif 3401   u. cun 3402   i^i cin 3403   C_ wss 3404   (/)c0 3731   {csn 3968   class class class wbr 4402   |-> cmpt 4461   dom cdm 4834   |` cres 4836   Fn wfn 5577   -->wf 5578   ` cfv 5582  (class class class)co 6290   ~~ cen 7566   Fincfn 7569   0cc0 9539   1c1 9540   x. cmul 9544   <_ cle 9676   NNcn 10609   NN0cn0 10869   ZZcz 10937   ZZ>=cuz 11159   ...cfz 11784   ^cexp 12272   #chash 12515   || cdvds 14305   gcd cgcd 14468   Primecprime 14622   pCnt cpc 14786   Basecbs 15121   0gc0g 15338   Grpcgrp 16669  SubGrpcsubg 16811  Cntzccntz 16969   odcod 17165   LSSumclsm 17286   Abelcabl 17431   DProd cdprd 17625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-inf2 8146  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-fal 1450  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-iin 4281  df-disj 4374  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-se 4794  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-isom 5591  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-of 6531  df-om 6693  df-1st 6793  df-2nd 6794  df-supp 6915  df-tpos 6973  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-2o 7183  df-oadd 7186  df-omul 7187  df-er 7363  df-ec 7365  df-qs 7369  df-map 7474  df-ixp 7523  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-fsupp 7884  df-sup 7956  df-inf 7957  df-oi 8025  df-card 8373  df-acn 8376  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-n0 10870  df-z 10938  df-uz 11160  df-q 11265  df-rp 11303  df-fz 11785  df-fzo 11916  df-fl 12028  df-mod 12097  df-seq 12214  df-exp 12273  df-fac 12460  df-bc 12488  df-hash 12516  df-cj 13162  df-re 13163  df-im 13164  df-sqrt 13298  df-abs 13299  df-clim 13552  df-sum 13753  df-dvds 14306  df-gcd 14469  df-prm 14623  df-pc 14787  df-ndx 15124  df-slot 15125  df-base 15126  df-sets 15127  df-ress 15128  df-plusg 15203  df-0g 15340  df-gsum 15341  df-mre 15492  df-mrc 15493  df-acs 15495  df-mgm 16488  df-sgrp 16527  df-mnd 16537  df-mhm 16582  df-submnd 16583  df-grp 16673  df-minusg 16674  df-sbg 16675  df-mulg 16676  df-subg 16814  df-eqg 16816  df-ghm 16881  df-gim 16923  df-ga 16944  df-cntz 16971  df-oppg 16997  df-od 17172  df-lsm 17288  df-pj1 17289  df-cmn 17432  df-abl 17433  df-dprd 17627

This theorem is referenced by: (None)