Theorem ablfac1eu 16577

Description: The factorization of ablfac1b 16574 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 459	. . . 4 |- ( ph -> G dom DProd T )
3		ablfac1eu.2	. . . 4 |- ( ph -> dom T = A )
4	2, 3	dprdf2 16494	. . 3 |- ( ph -> T : A --> (SubGrp ` G ) )
5		ffn 5562	. . 3 |- ( T : A --> (SubGrp ` G ) -> T Fn A )
6	4, 5	syl 16	. 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 16574	. . . 4 |- ( ph -> G dom DProd S )
14		fvex 5704	. . . . . . . 8 |- ( Base ` G ) e. _V
15	7, 14	eqeltri 2513	. . . . . . 7 |- B e. _V
16	15	rabex 4446	. . . . . 6 |- { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } e. _V
17	16, 9	dmmpti 5543	. . . . 5 |- dom S = A
18	17	a1i 11	. . . 4 |- ( ph -> dom S = A )
19	13, 18	dprdf2 16494	. . 3 |- ( ph -> S : A --> (SubGrp ` G ) )
20		ffn 5562	. . 3 |- ( S : A --> (SubGrp ` G ) -> S Fn A )
21	19, 20	syl 16	. 2 |- ( ph -> S Fn A )
22	11	adantr 465	. . . 4 |- ( ( ph /\ q e. A ) -> B e. Fin )
23	19	ffvelrnda 5846	. . . . 5 |- ( ( ph /\ q e. A ) -> ( S ` q ) e. (SubGrp ` G ) )
24	7	subgss 15685	. . . . 5 |- ( ( S ` q ) e. (SubGrp ` G ) -> ( S ` q ) C_ B )
25	23, 24	syl 16	. . . 4 |- ( ( ph /\ q e. A ) -> ( S ` q ) C_ B )
26		ssfi 7536	. . . 4 |- ( ( B e. Fin /\ ( S ` q ) C_ B ) -> ( S ` q ) e. Fin )
27	22, 25, 26	syl2anc 661	. . 3 |- ( ( ph /\ q e. A ) -> ( S ` q ) e. Fin )
28	4	ffvelrnda 5846	. . . . . 6 |- ( ( ph /\ q e. A ) -> ( T ` q ) e. (SubGrp ` G ) )
29	7	subgss 15685	. . . . . 6 |- ( ( T ` q ) e. (SubGrp ` G ) -> ( T ` q ) C_ B )
30	28, 29	syl 16	. . . . 5 |- ( ( ph /\ q e. A ) -> ( T ` q ) C_ B )
31	28	adantr 465	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( T ` q ) e. (SubGrp ` G ) )
32		ssfi 7536	. . . . . . . . 9 |- ( ( B e. Fin /\ ( T ` q ) C_ B ) -> ( T ` q ) e. Fin )
33	22, 30, 32	syl2anc 661	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( T ` q ) e. Fin )
34	33	adantr 465	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( T ` q ) e. Fin )
35		simpr 461	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> x e. ( T ` q ) )
36	8	odsubdvds 16073	. . . . . . 7 |- ( ( ( T ` q ) e. (SubGrp ` G ) /\ ( T ` q ) e. Fin /\ x e. ( T ` q ) ) -> ( O ` x ) || ( # ` ( T ` q ) ) )
37	31, 34, 35, 36	syl3anc 1218	. . . . . 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 3359	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> q e. Prime )
40		prmz 13770	. . . . . . . . . 10 |- ( q e. Prime -> q e. ZZ )
41	39, 40	syl 16	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> q e. ZZ )
42		ablfac1eu.3	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> C e. NN0 )
43	42	nn0zd 10748	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> C e. ZZ )
44		ablgrp 16285	. . . . . . . . . . . . . . . 16 |- ( G e. Abel -> G e. Grp )
45	10, 44	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> G e. Grp )
46	7	grpbn0 15570	. . . . . . . . . . . . . . 15 |- ( G e. Grp -> B =/= (/) )
47	45, 46	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> B =/= (/) )
48		hashnncl 12137	. . . . . . . . . . . . . . 15 |- ( B e. Fin -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
49	11, 48	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
50	47, 49	mpbird 232	. . . . . . . . . . . . 13 |- ( ph -> ( # ` B ) e. NN )
51	50	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( # ` B ) e. NN )
52	39, 51	pccld 13920	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. NN0 )
53	52	nn0zd 10748	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. ZZ )
54	7	lagsubg 15746	. . . . . . . . . . . . 13 |- ( ( ( T ` q ) e. (SubGrp ` G ) /\ B e. Fin ) -> ( # ` ( T ` q ) ) || ( # ` B ) )
55	28, 22, 54	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) || ( # ` B ) )
56	38, 55	eqbrtrrd 4317	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( q ^ C ) || ( # ` B ) )
57	51	nnzd 10749	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( # ` B ) e. ZZ )
58		pcdvdsb 13938	. . . . . . . . . . . 12 |- ( ( q e. Prime /\ ( # ` B ) e. ZZ /\ C e. NN0 ) -> ( C <_ ( q pCnt ( # ` B ) ) <-> ( q ^ C ) || ( # ` B ) ) )
59	39, 57, 42, 58	syl3anc 1218	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( C <_ ( q pCnt ( # ` B ) ) <-> ( q ^ C ) || ( # ` B ) ) )
60	56, 59	mpbird 232	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> C <_ ( q pCnt ( # ` B ) ) )
61		eluz2 10870	. . . . . . . . . 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 1172	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. ( ZZ>= ` C ) )
63		dvdsexp 13592	. . . . . . . . 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 1218	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( q ^ C ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
65	38, 64	eqbrtrd 4315	. . . . . . 7 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
66	65	adantr 465	. . . . . 6 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( # ` ( T ` q ) ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
67	30	sselda 3359	. . . . . . . . 9 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> x e. B )
68	7, 8	odcl 16042	. . . . . . . . 9 |- ( x e. B -> ( O ` x ) e. NN0 )
69	67, 68	syl 16	. . . . . . . 8 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( O ` x ) e. NN0 )
70	69	nn0zd 10748	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( O ` x ) e. ZZ )
71		hashcl 12129	. . . . . . . . . 10 |- ( ( T ` q ) e. Fin -> ( # ` ( T ` q ) ) e. NN0 )
72	33, 71	syl 16	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) e. NN0 )
73	72	nn0zd 10748	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) e. ZZ )
74	73	adantr 465	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( # ` ( T ` q ) ) e. ZZ )
75		prmnn 13769	. . . . . . . . . . 11 |- ( q e. Prime -> q e. NN )
76	39, 75	syl 16	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> q e. NN )
77	76, 52	nnexpcld 12032	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. NN )
78	77	nnzd 10749	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. ZZ )
79	78	adantr 465	. . . . . . 7 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. ZZ )
80		dvdstr 13569	. . . . . . 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 1218	. . . . . 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 679	. . . . 5 |- ( ( ( ph /\ q e. A ) /\ x e. ( T ` q ) ) -> ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) )
83	30, 82	ssrabdv 3434	. . . 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 6101	. . . . . . . . 9 |- ( p = q -> ( p pCnt ( # ` B ) ) = ( q pCnt ( # ` B ) ) )
86	84, 85	oveq12d 6112	. . . . . . . 8 |- ( p = q -> ( p ^ ( p pCnt ( # ` B ) ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
87	86	breq2d 4307	. . . . . . 7 |- ( p = q -> ( ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) <-> ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) ) )
88	87	rabbidv 2967	. . . . . 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 5781	. . . . 5 |- ( q e. A -> ( S ` q ) = { x e. B | ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) } )
90	89	adantl 466	. . . 4 |- ( ( ph /\ q e. A ) -> ( S ` q ) = { x e. B | ( O ` x ) || ( q ^ ( q pCnt ( # ` B ) ) ) } )
91	83, 90	sseqtr4d 3396	. . 3 |- ( ( ph /\ q e. A ) -> ( T ` q ) C_ ( S ` q ) )
92	77	nnnn0d 10639	. . . . . 6 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) e. NN0 )
93		pcdvds 13933	. . . . . . . . . 10 |- ( ( q e. Prime /\ ( # ` B ) e. NN ) -> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` B ) )
94	39, 51, 93	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` B ) )
95	2	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. A ) -> G dom DProd T )
96	3	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. A ) -> dom T = A )
97		ablfac1.2	. . . . . . . . . . . . . . . 16 |- ( ph -> D C_ A )
98	97	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. A ) -> D C_ A )
99	95, 96, 98	dprdres 16528	. . . . . . . . . . . . . 14 |- ( ( ph /\ q e. A ) -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) C_ ( G DProd T ) ) )
100	99	simpld 459	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> G dom DProd ( T |` D ) )
101	4	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ q e. A ) -> T : A --> (SubGrp ` G ) )
102		fssres 5581	. . . . . . . . . . . . . . 15 |- ( ( T : A --> (SubGrp ` G ) /\ D C_ A ) -> ( T |` D ) : D --> (SubGrp ` G ) )
103	101, 98, 102	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ph /\ q e. A ) -> ( T |` D ) : D --> (SubGrp ` G ) )
104		fdm 5566	. . . . . . . . . . . . . 14 |- ( ( T |` D ) : D --> (SubGrp ` G ) -> dom ( T |` D ) = D )
105	103, 104	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> dom ( T |` D ) = D )
106		difssd 3487	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> ( D \ { q } ) C_ D )
107	100, 105, 106	dprdres 16528	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( G dom DProd ( ( T |` D ) |` ( D \ { q } ) ) /\ ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) C_ ( G DProd ( T |` D ) ) ) )
108	107	simpld 459	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> G dom DProd ( ( T |` D ) |` ( D \ { q } ) ) )
109		dprdsubg 16524	. . . . . . . . . . 11 |- ( G dom DProd ( ( T |` D ) |` ( D \ { q } ) ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. (SubGrp ` G ) )
110	108, 109	syl 16	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. (SubGrp ` G ) )
111	7	lagsubg 15746	. . . . . . . . . 10 |- ( ( ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. (SubGrp ` G ) /\ B e. Fin ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) || ( # ` B ) )
112	110, 22, 111	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) || ( # ` B ) )
113		eqid 2443	. . . . . . . . . . . . . . 15 |- ( 0g ` G ) = ( 0g ` G )
114	113	subg0cl 15692	. . . . . . . . . . . . . 14 |- ( ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. (SubGrp ` G ) -> ( 0g ` G ) e. ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) )
115	110, 114	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> ( 0g ` G ) e. ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) )
116		ne0i 3646	. . . . . . . . . . . . 13 |- ( ( 0g ` G ) e. ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) =/= (/) )
117	115, 116	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) =/= (/) )
118	7	dprdssv 16509	. . . . . . . . . . . . . 14 |- ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) C_ B
119		ssfi 7536	. . . . . . . . . . . . . 14 |- ( ( B e. Fin /\ ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) C_ B ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. Fin )
120	22, 118, 119	sylancl 662	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. Fin )
121		hashnncl 12137	. . . . . . . . . . . . 13 |- ( ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) e. Fin -> ( ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) e. NN <-> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) =/= (/) ) )
122	120, 121	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) e. NN <-> ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) =/= (/) ) )
123	117, 122	mpbird 232	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) e. NN )
124	123	nnzd 10749	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) e. ZZ )
125		eqid 2443	. . . . . . . . . . . . . . . 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 ) ) ) } )
126	10	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> G e. Abel )
127	11	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> B e. Fin )
128		ablfac1c.d	. . . . . . . . . . . . . . . . . 18 |- D = { w e. Prime | w || ( # ` B ) }
129		ssrab2 3440	. . . . . . . . . . . . . . . . . 18 |- { w e. Prime | w || ( # ` B ) } C_ Prime
130	128, 129	eqsstri 3389	. . . . . . . . . . . . . . . . 17 |- D C_ Prime
131	130	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> D C_ Prime )
132		ssid 3378	. . . . . . . . . . . . . . . . 17 |- D C_ D
133	132	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> D C_ D )
134	2, 3, 97	dprdres 16528	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) C_ ( G DProd T ) ) )
135	134	simpld 459	. . . . . . . . . . . . . . . . . 18 |- ( ph -> G dom DProd ( T |` D ) )
136		dprdsubg 16524	. . . . . . . . . . . . . . . . . . . . 21 |- ( G dom DProd ( T |` D ) -> ( G DProd ( T |` D ) ) e. (SubGrp ` G ) )
137	135, 136	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( G DProd ( T |` D ) ) e. (SubGrp ` G ) )
138		difssd 3487	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( A \ D ) C_ A )
139	2, 3, 138	dprdres 16528	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( G dom DProd ( T |` ( A \ D ) ) /\ ( G DProd ( T |` ( A \ D ) ) ) C_ ( G DProd T ) ) )
140	139	simpld 459	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> G dom DProd ( T |` ( A \ D ) ) )
141		dprdsubg 16524	. . . . . . . . . . . . . . . . . . . . 21 |- ( G dom DProd ( T |` ( A \ D ) ) -> ( G DProd ( T |` ( A \ D ) ) ) e. (SubGrp ` G ) )
142	140, 141	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( G DProd ( T |` ( A \ D ) ) ) e. (SubGrp ` G ) )
143		difss 3486	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A \ D ) C_ A
144		fssres 5581	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( T : A --> (SubGrp ` G ) /\ ( A \ D ) C_ A ) -> ( T |` ( A \ D ) ) : ( A \ D ) --> (SubGrp ` G ) )
145	4, 143, 144	sylancl 662	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( T |` ( A \ D ) ) : ( A \ D ) --> (SubGrp ` G ) )
146		fdm 5566	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T |` ( A \ D ) ) : ( A \ D ) --> (SubGrp ` G ) -> dom ( T |` ( A \ D ) ) = ( A \ D ) )
147	145, 146	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> dom ( T |` ( A \ D ) ) = ( A \ D ) )
148		fvres 5707	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( q e. ( A \ D ) -> ( ( T |` ( A \ D ) ) ` q ) = ( T ` q ) )
149	148	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ q e. ( A \ D ) ) -> ( ( T |` ( A \ D ) ) ` q ) = ( T ` q ) )
150		eldif 3341	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( q e. ( A \ D ) <-> ( q e. A /\ -. q e. D ) )
151	33	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( T ` q ) e. Fin )
152	113	subg0cl 15692	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( T ` q ) e. (SubGrp ` G ) -> ( 0g ` G ) e. ( T ` q ) )
153	28, 152	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ q e. A ) -> ( 0g ` G ) e. ( T ` q ) )
154	153	snssd 4021	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ q e. A ) -> { ( 0g ` G ) } C_ ( T ` q ) )
155	154	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } C_ ( T ` q ) )
156	38	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( # ` ( T ` q ) ) = ( q ^ C ) )
157	39	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q e. Prime )
158		iddvdsexp 13559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( q e. ZZ /\ C e. NN ) -> q || ( q ^ C ) )
159	41, 158	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q || ( q ^ C ) )
160	56	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> ( q ^ C ) || ( # ` B ) )
161	38, 73	eqeltrrd 2518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ q e. A ) -> ( q ^ C ) e. ZZ )
162		dvdstr 13569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( q e. ZZ /\ ( q ^ C ) e. ZZ /\ ( # ` B ) e. ZZ ) -> ( ( q || ( q ^ C ) /\ ( q ^ C ) || ( # ` B ) ) -> q || ( # ` B ) ) )
163	41, 161, 57, 162	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ q e. A ) -> ( ( q || ( q ^ C ) /\ ( q ^ C ) || ( # ` B ) ) -> q || ( # ` B ) ) )
164	163	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> ( ( q || ( q ^ C ) /\ ( q ^ C ) || ( # ` B ) ) -> q || ( # ` B ) ) )
165	159, 160, 164	mp2and 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q || ( # ` B ) )
166		breq1 4298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( w = q -> ( w || ( # ` B ) <-> q || ( # ` B ) ) )
167	166, 128	elrab2 3122	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( q e. D <-> ( q e. Prime /\ q || ( # ` B ) ) )
168	157, 165, 167	sylanbrc 664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ q e. A ) /\ C e. NN ) -> q e. D )
169	168	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ q e. A ) -> ( C e. NN -> q e. D ) )
170	169	con3d 133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ q e. A ) -> ( -. q e. D -> -. C e. NN ) )
171	170	impr 619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> -. C e. NN )
172	42	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> C e. NN0 )
173		elnn0 10584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( C e. NN0 <-> ( C e. NN \/ C = 0 ) )
174	172, 173	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( C e. NN \/ C = 0 ) )
175	174	ord 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( -. C e. NN -> C = 0 ) )
176	171, 175	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> C = 0 )
177	176	oveq2d 6110	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( q ^ C ) = ( q ^ 0 ) )
178	76	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> q e. NN )
179	178	nncnd 10341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> q e. CC )
180	179	exp0d 12005	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( q ^ 0 ) = 1 )
181	156, 177, 180	3eqtrd 2479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( # ` ( T ` q ) ) = 1 )
182		fvex 5704	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 0g ` G ) e. _V
183		hashsng 12139	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 0g ` G ) e. _V -> ( # ` { ( 0g ` G ) } ) = 1 )
184	182, 183	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( # ` { ( 0g ` G ) } ) = 1
185	181, 184	syl6reqr 2494	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( # ` { ( 0g ` G ) } ) = ( # ` ( T ` q ) ) )
186		snfi 7393	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- { ( 0g ` G ) } e. Fin
187		hashen 12121	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( { ( 0g ` G ) } e. Fin /\ ( T ` q ) e. Fin ) -> ( ( # ` { ( 0g ` G ) } ) = ( # ` ( T ` q ) ) <-> { ( 0g ` G ) } ~~ ( T ` q ) ) )
188	186, 151, 187	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( ( # ` { ( 0g ` G ) } ) = ( # ` ( T ` q ) ) <-> { ( 0g ` G ) } ~~ ( T ` q ) ) )
189	185, 188	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } ~~ ( T ` q ) )
190		fisseneq 7527	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( T ` q ) e. Fin /\ { ( 0g ` G ) } C_ ( T ` q ) /\ { ( 0g ` G ) } ~~ ( T ` q ) ) -> { ( 0g ` G ) } = ( T ` q ) )
191	151, 155, 189, 190	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } = ( T ` q ) )
192	113	subg0cl 15692	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( G DProd ( T |` D ) ) e. (SubGrp ` G ) -> ( 0g ` G ) e. ( G DProd ( T |` D ) ) )
193	137, 192	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( 0g ` G ) e. ( G DProd ( T |` D ) ) )
194	193	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( 0g ` G ) e. ( G DProd ( T |` D ) ) )
195	194	snssd 4021	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> { ( 0g ` G ) } C_ ( G DProd ( T |` D ) ) )
196	191, 195	eqsstr3d 3394	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( T ` q ) C_ ( G DProd ( T |` D ) ) )
197	150, 196	sylan2b 475	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ q e. ( A \ D ) ) -> ( T ` q ) C_ ( G DProd ( T |` D ) ) )
198	149, 197	eqsstrd 3393	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ q e. ( A \ D ) ) -> ( ( T |` ( A \ D ) ) ` q ) C_ ( G DProd ( T |` D ) ) )
199	140, 147, 137, 198	dprdlub 16526	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( G DProd ( T |` ( A \ D ) ) ) C_ ( G DProd ( T |` D ) ) )
200		eqid 2443	. . . . . . . . . . . . . . . . . . . . 21 |- ( LSSum ` G ) = ( LSSum ` G )
201	200	lsmss2 16168	. . . . . . . . . . . . . . . . . . . 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 ) ) )
202	137, 142, 199, 201	syl3anc 1218	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( G DProd ( T |` D ) ) ( LSSum ` G ) ( G DProd ( T |` ( A \ D ) ) ) ) = ( G DProd ( T |` D ) ) )
203		disjdif 3754	. . . . . . . . . . . . . . . . . . . . . 22 |- ( D i^i ( A \ D ) ) = (/)
204	203	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( D i^i ( A \ D ) ) = (/) )
205		undif2 3758	. . . . . . . . . . . . . . . . . . . . . 22 |- ( D u. ( A \ D ) ) = ( D u. A )
206		ssequn1 3529	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( D C_ A <-> ( D u. A ) = A )
207	97, 206	sylib 196	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( D u. A ) = A )
208	205, 207	syl5req 2488	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> A = ( D u. ( A \ D ) ) )
209	4, 204, 208, 200, 2	dprdsplit 16550	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( G DProd T ) = ( ( G DProd ( T |` D ) ) ( LSSum ` G ) ( G DProd ( T |` ( A \ D ) ) ) ) )
210	1	simprd 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( G DProd T ) = B )
211	209, 210	eqtr3d 2477	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( G DProd ( T |` D ) ) ( LSSum ` G ) ( G DProd ( T |` ( A \ D ) ) ) ) = B )
212	202, 211	eqtr3d 2477	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( G DProd ( T |` D ) ) = B )
213	135, 212	jca 532	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) = B ) )
214	213	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> ( G dom DProd ( T |` D ) /\ ( G DProd ( T |` D ) ) = B ) )
215	4, 97, 102	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( T |` D ) : D --> (SubGrp ` G ) )
216	215, 104	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> dom ( T |` D ) = D )
217	216	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> dom ( T |` D ) = D )
218	97	sselda 3359	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ q e. D ) -> q e. A )
219	218, 42	syldan 470	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ q e. D ) -> C e. NN0 )
220	219	adantlr 714	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. Prime ) /\ q e. D ) -> C e. NN0 )
221		fvres 5707	. . . . . . . . . . . . . . . . . . . 20 |- ( q e. D -> ( ( T |` D ) ` q ) = ( T ` q ) )
222	221	adantl 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ q e. D ) -> ( ( T |` D ) ` q ) = ( T ` q ) )
223	222	fveq2d 5698	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ q e. D ) -> ( # ` ( ( T |` D ) ` q ) ) = ( # ` ( T ` q ) ) )
224	218, 38	syldan 470	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ q e. D ) -> ( # ` ( T ` q ) ) = ( q ^ C ) )
225	223, 224	eqtrd 2475	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ q e. D ) -> ( # ` ( ( T |` D ) ` q ) ) = ( q ^ C ) )
226	225	adantlr 714	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. Prime ) /\ q e. D ) -> ( # ` ( ( T |` D ) ` q ) ) = ( q ^ C ) )
227		simpr 461	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> x e. Prime )
228		fzfid 11798	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( 1 ... ( # ` B ) ) e. Fin )
229		prmnn 13769	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w e. Prime -> w e. NN )
230	229	3ad2ant2 1010	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w e. NN )
231		prmz 13770	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w e. Prime -> w e. ZZ )
232		dvdsle 13581	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( w e. ZZ /\ ( # ` B ) e. NN ) -> ( w || ( # ` B ) -> w <_ ( # ` B ) ) )
233	231, 50, 232	syl2anr 478	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ w e. Prime ) -> ( w || ( # ` B ) -> w <_ ( # ` B ) ) )
234	233	3impia 1184	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w <_ ( # ` B ) )
235	50	nnzd 10749	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( # ` B ) e. ZZ )
236	235	3ad2ant1 1009	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> ( # ` B ) e. ZZ )
237		fznn 11529	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( # ` B ) e. ZZ -> ( w e. ( 1 ... ( # ` B ) ) <-> ( w e. NN /\ w <_ ( # ` B ) ) ) )
238	236, 237	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> ( w e. ( 1 ... ( # ` B ) ) <-> ( w e. NN /\ w <_ ( # ` B ) ) ) )
239	230, 234, 238	mpbir2and 913	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. Prime /\ w || ( # ` B ) ) -> w e. ( 1 ... ( # ` B ) ) )
240	239	rabssdv 3435	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> { w e. Prime | w || ( # ` B ) } C_ ( 1 ... ( # ` B ) ) )
241	128, 240	syl5eqss 3403	. . . . . . . . . . . . . . . . . 18 |- ( ph -> D C_ ( 1 ... ( # ` B ) ) )
242		ssfi 7536	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 1 ... ( # ` B ) ) e. Fin /\ D C_ ( 1 ... ( # ` B ) ) ) -> D e. Fin )
243	228, 241, 242	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ph -> D e. Fin )
244	243	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. Prime ) -> D e. Fin )
245	7, 8, 125, 126, 127, 131, 128, 133, 214, 217, 220, 226, 227, 244	ablfac1eulem 16576	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. Prime ) -> -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) )
246	245	ralrimiva 2802	. . . . . . . . . . . . . 14 |- ( ph -> A. x e. Prime -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) )
247	246	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> A. x e. Prime -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) )
248		id 22	. . . . . . . . . . . . . . . 16 |- ( x = q -> x = q )
249		sneq 3890	. . . . . . . . . . . . . . . . . . . 20 |- ( x = q -> { x } = { q } )
250	249	difeq2d 3477	. . . . . . . . . . . . . . . . . . 19 |- ( x = q -> ( D \ { x } ) = ( D \ { q } ) )
251	250	reseq2d 5113	. . . . . . . . . . . . . . . . . 18 |- ( x = q -> ( ( T |` D ) |` ( D \ { x } ) ) = ( ( T |` D ) |` ( D \ { q } ) ) )
252	251	oveq2d 6110	. . . . . . . . . . . . . . . . 17 |- ( x = q -> ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) = ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) )
253	252	fveq2d 5698	. . . . . . . . . . . . . . . 16 |- ( x = q -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) = ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) )
254	248, 253	breq12d 4308	. . . . . . . . . . . . . . 15 |- ( x = q -> ( x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) <-> q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
255	254	notbid 294	. . . . . . . . . . . . . 14 |- ( x = q -> ( -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) <-> -. q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
256	255	rspcv 3072	. . . . . . . . . . . . 13 |- ( q e. Prime -> ( A. x e. Prime -. x || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { x } ) ) ) ) -> -. q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
257	39, 247, 256	sylc 60	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> -. q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) )
258		coprm 13789	. . . . . . . . . . . . 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 ) )
259	39, 124, 258	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> ( -. q || ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) <-> ( q gcd ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) = 1 ) )
260	257, 259	mpbid 210	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( q gcd ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) = 1 )
261		rpexp1i 13810	. . . . . . . . . . . 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 ) )
262	41, 124, 52, 261	syl3anc 1218	. . . . . . . . . . 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 ) )
263	260, 262	mpd 15	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( ( q ^ ( q pCnt ( # ` B ) ) ) gcd ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) = 1 )
264		coprmdvds2 13792	. . . . . . . . . 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 ) ) )
265	78, 124, 57, 263, 264	syl31anc 1221	. . . . . . . . 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 ) ) )
266	94, 112, 265	mp2and 679	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( ( q ^ ( q pCnt ( # ` B ) ) ) x. ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) || ( # ` B ) )
267		eqid 2443	. . . . . . . . . 10 |- (Cntz ` G ) = (Cntz ` G )
268		inss1 3573	. . . . . . . . . . . . . 14 |- ( D i^i { q } ) C_ D
269	268	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ q e. A ) -> ( D i^i { q } ) C_ D )
270	100, 105, 269	dprdres 16528	. . . . . . . . . . . 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 ) ) ) )
271	270	simpld 459	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> G dom DProd ( ( T |` D ) |` ( D i^i { q } ) ) )
272		dprdsubg 16524	. . . . . . . . . . 11 |- ( G dom DProd ( ( T |` D ) |` ( D i^i { q } ) ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) e. (SubGrp ` G ) )
273	271, 272	syl 16	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) e. (SubGrp ` G ) )
274		inass 3563	. . . . . . . . . . . . 13 |- ( ( D i^i { q } ) i^i ( D \ { q } ) ) = ( D i^i ( { q } i^i ( D \ { q } ) ) )
275		disjdif 3754	. . . . . . . . . . . . . 14 |- ( { q } i^i ( D \ { q } ) ) = (/)
276	275	ineq2i 3552	. . . . . . . . . . . . 13 |- ( D i^i ( { q } i^i ( D \ { q } ) ) ) = ( D i^i (/) )
277		in0 3666	. . . . . . . . . . . . 13 |- ( D i^i (/) ) = (/)
278	274, 276, 277	3eqtri 2467	. . . . . . . . . . . 12 |- ( ( D i^i { q } ) i^i ( D \ { q } ) ) = (/)
279	278	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( ( D i^i { q } ) i^i ( D \ { q } ) ) = (/) )
280	100, 105, 269, 106, 279, 113	dprddisj2 16540	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) i^i ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) = { ( 0g ` G ) } )
281	100, 105, 269, 106, 279, 267	dprdcntz2 16539	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) C_ ( (Cntz ` G ) ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) )
282	7	dprdssv 16509	. . . . . . . . . . 11 |- ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) C_ B
283		ssfi 7536	. . . . . . . . . . 11 |- ( ( B e. Fin /\ ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) C_ B ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) e. Fin )
284	22, 282, 283	sylancl 662	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) e. Fin )
285	200, 113, 267, 273, 110, 280, 281, 284, 120	lsmhash 16205	. . . . . . . . 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 } ) ) ) ) ) )
286		inundif 3760	. . . . . . . . . . . . . 14 |- ( ( D i^i { q } ) u. ( D \ { q } ) ) = D
287	286	eqcomi 2447	. . . . . . . . . . . . 13 |- D = ( ( D i^i { q } ) u. ( D \ { q } ) )
288	287	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ q e. A ) -> D = ( ( D i^i { q } ) u. ( D \ { q } ) ) )
289	103, 279, 288, 200, 100	dprdsplit 16550	. . . . . . . . . . 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 } ) ) ) ) )
290	212	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( G DProd ( T |` D ) ) = B )
291	289, 290	eqtr3d 2477	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) ( LSSum ` G ) ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) = B )
292	291	fveq2d 5698	. . . . . . . . 9 |- ( ( ph /\ q e. A ) -> ( # ` ( ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) ( LSSum ` G ) ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) = ( # ` B ) )
293		snssi 4020	. . . . . . . . . . . . . . . . 17 |- ( q e. D -> { q } C_ D )
294	293	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> { q } C_ D )
295		dfss1 3558	. . . . . . . . . . . . . . . 16 |- ( { q } C_ D <-> ( D i^i { q } ) = { q } )
296	294, 295	sylib 196	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( D i^i { q } ) = { q } )
297	296	reseq2d 5113	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( ( T |` D ) |` ( D i^i { q } ) ) = ( ( T |` D ) |` { q } ) )
298	297	oveq2d 6110	. . . . . . . . . . . . 13 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( G DProd ( ( T |` D ) |` { q } ) ) )
299	100	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> G dom DProd ( T |` D ) )
300	216	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> dom ( T |` D ) = D )
301		simpr 461	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> q e. D )
302	299, 300, 301	dpjlem 16553	. . . . . . . . . . . . 13 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( G DProd ( ( T |` D ) |` { q } ) ) = ( ( T |` D ) ` q ) )
303	221	adantl 466	. . . . . . . . . . . . 13 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( ( T |` D ) ` q ) = ( T ` q ) )
304	298, 302, 303	3eqtrd 2479	. . . . . . . . . . . 12 |- ( ( ( ph /\ q e. A ) /\ q e. D ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
305		simprr 756	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> -. q e. D )
306		disjsn 3939	. . . . . . . . . . . . . . . . . 18 |- ( ( D i^i { q } ) = (/) <-> -. q e. D )
307	305, 306	sylibr 212	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( D i^i { q } ) = (/) )
308	307	reseq2d 5113	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( ( T |` D ) |` ( D i^i { q } ) ) = ( ( T |` D ) |` (/) ) )
309		res0 5118	. . . . . . . . . . . . . . . 16 |- ( ( T |` D ) |` (/) ) = (/)
310	308, 309	syl6eq 2491	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( ( T |` D ) |` ( D i^i { q } ) ) = (/) )
311	310	oveq2d 6110	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( G DProd (/) ) )
312	113	dprd0 16531	. . . . . . . . . . . . . . . . 17 |- ( G e. Grp -> ( G dom DProd (/) /\ ( G DProd (/) ) = { ( 0g ` G ) } ) )
313	45, 312	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( G dom DProd (/) /\ ( G DProd (/) ) = { ( 0g ` G ) } ) )
314	313	simprd 463	. . . . . . . . . . . . . . 15 |- ( ph -> ( G DProd (/) ) = { ( 0g ` G ) } )
315	314	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( G DProd (/) ) = { ( 0g ` G ) } )
316	311, 315, 191	3eqtrd 2479	. . . . . . . . . . . . 13 |- ( ( ph /\ ( q e. A /\ -. q e. D ) ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
317	316	anassrs 648	. . . . . . . . . . . 12 |- ( ( ( ph /\ q e. A ) /\ -. q e. D ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
318	304, 317	pm2.61dan 789	. . . . . . . . . . 11 |- ( ( ph /\ q e. A ) -> ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) = ( T ` q ) )
319	318	fveq2d 5698	. . . . . . . . . 10 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D i^i { q } ) ) ) ) = ( # ` ( T ` q ) ) )
320	319	oveq1d 6109	. . . . . . . . 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 } ) ) ) ) ) )
321	285, 292, 320	3eqtr3d 2483	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( # ` B ) = ( ( # ` ( T ` q ) ) x. ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) ) )
322	266, 321	breqtrd 4319	. . . . . . 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 } ) ) ) ) ) )
323	123	nnne0d 10369	. . . . . . . 8 |- ( ( ph /\ q e. A ) -> ( # ` ( G DProd ( ( T |` D ) |` ( D \ { q } ) ) ) ) =/= 0 )
324		dvdsmulcr 13565	. . . . . . . 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 ) ) ) )
325	78, 73, 124, 323, 324	syl112anc 1222	. . . . . . 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 ) ) ) )
326	322, 325	mpbid 210	. . . . . 6 |- ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` ( T ` q ) ) )
327		dvdseq 13583	. . . . . 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 ) ) ) )
328	72, 92, 65, 326, 327	syl22anc 1219	. . . . 5 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
329	7, 8, 9, 10, 11, 12	ablfac1a 16573	. . . . 5 |- ( ( ph /\ q e. A ) -> ( # ` ( S ` q ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
330	328, 329	eqtr4d 2478	. . . 4 |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) = ( # ` ( S ` q ) ) )
331		hashen 12121	. . . . 5 |- ( ( ( T ` q ) e. Fin /\ ( S ` q ) e. Fin ) -> ( ( # ` ( T ` q ) ) = ( # ` ( S ` q ) ) <-> ( T ` q ) ~~ ( S ` q ) ) )
332	33, 27, 331	syl2anc 661	. . . 4 |- ( ( ph /\ q e. A ) -> ( ( # ` ( T ` q ) ) = ( # ` ( S ` q ) ) <-> ( T ` q ) ~~ ( S ` q ) ) )
333	330, 332	mpbid 210	. . 3 |- ( ( ph /\ q e. A ) -> ( T ` q ) ~~ ( S ` q ) )
334		fisseneq 7527	. . 3 |- ( ( ( S ` q ) e. Fin /\ ( T ` q ) C_ ( S ` q ) /\ ( T ` q ) ~~ ( S ` q ) ) -> ( T ` q ) = ( S ` q ) )
335	27, 91, 333, 334	syl3anc 1218	. 2 |- ( ( ph /\ q e. A ) -> ( T ` q ) = ( S ` q ) )
336	6, 21, 335	eqfnfvd 5803	1 |- ( ph -> T = S )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 965   = wceq 1369   e. wcel 1756   =/= wne 2609   A.wral 2718   {crab 2722   _Vcvv 2975   \ cdif 3328   u. cun 3329   i^i cin 3330   C_ wss 3331   (/)c0 3640   {csn 3880   class class class wbr 4295   e. cmpt 4353   dom cdm 4843   |` cres 4845   Fn wfn 5416   -->wf 5417   ` cfv 5421  (class class class)co 6094   ~~ cen 7310   Fincfn 7313   0cc0 9285   1c1 9286   x. cmul 9290   <_ cle 9422   NNcn 10325   NN0cn0 10582   ZZcz 10649   ZZ>=cuz 10864   ...cfz 11440   ^cexp 11868   #chash 12106   || cdivides 13538   gcd cgcd 13693   Primecprime 13766   pCnt cpc 13906   Basecbs 14177   0gc0g 14381   Grpcgrp 15413  SubGrpcsubg 15678  Cntzccntz 15836   odcod 16031   LSSumclsm 16136   Abelcabel 16281   DProd cdprd 16478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4406  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375  ax-inf2 7850  ax-cnex 9341  ax-resscn 9342  ax-1cn 9343  ax-icn 9344  ax-addcl 9345  ax-addrcl 9346  ax-mulcl 9347  ax-mulrcl 9348  ax-mulcom 9349  ax-addass 9350  ax-mulass 9351  ax-distr 9352  ax-i2m1 9353  ax-1ne0 9354  ax-1rid 9355  ax-rnegex 9356  ax-rrecex 9357  ax-cnre 9358  ax-pre-lttri 9359  ax-pre-lttrn 9360  ax-pre-ltadd 9361  ax-pre-mulgt0 9362  ax-pre-sup 9363

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-nel 2612  df-ral 2723  df-rex 2724  df-reu 2725  df-rmo 2726  df-rab 2727  df-v 2977  df-sbc 3190  df-csb 3292  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-pss 3347  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-tp 3885  df-op 3887  df-uni 4095  df-int 4132  df-iun 4176  df-iin 4177  df-disj 4266  df-br 4296  df-opab 4354  df-mpt 4355  df-tr 4389  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-se 4683  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-isom 5430  df-riota 6055  df-ov 6097  df-oprab 6098  df-mpt2 6099  df-of 6323  df-om 6480  df-1st 6580  df-2nd 6581  df-supp 6694  df-tpos 6748  df-recs 6835  df-rdg 6869  df-1o 6923  df-2o 6924  df-oadd 6927  df-omul 6928  df-er 7104  df-ec 7106  df-qs 7110  df-map 7219  df-ixp 7267  df-en 7314  df-dom 7315  df-sdom 7316  df-fin 7317  df-fsupp 7624  df-sup 7694  df-oi 7727  df-card 8112  df-acn 8115  df-cda 8340  df-pnf 9423  df-mnf 9424  df-xr 9425  df-ltxr 9426  df-le 9427  df-sub 9600  df-neg 9601  df-div 9997  df-nn 10326  df-2 10383  df-3 10384  df-n0 10583  df-z 10650  df-uz 10865  df-q 10957  df-rp 10995  df-fz 11441  df-fzo 11552  df-fl 11645  df-mod 11712  df-seq 11810  df-exp 11869  df-fac 12055  df-bc 12082  df-hash 12107  df-cj 12591  df-re 12592  df-im 12593  df-sqr 12727  df-abs 12728  df-clim 12969  df-sum 13167  df-dvds 13539  df-gcd 13694  df-prm 13767  df-pc 13907  df-ndx 14180  df-slot 14181  df-base 14182  df-sets 14183  df-ress 14184  df-plusg 14254  df-0g 14383  df-gsum 14384  df-mre 14527  df-mrc 14528  df-acs 14530  df-mnd 15418  df-mhm 15467  df-submnd 15468  df-grp 15548  df-minusg 15549  df-sbg 15550  df-mulg 15551  df-subg 15681  df-eqg 15683  df-ghm 15748  df-gim 15790  df-ga 15811  df-cntz 15838  df-oppg 15864  df-od 16035  df-lsm 16138  df-pj1 16139  df-cmn 16282  df-abl 16283  df-dprd 16480

This theorem is referenced by: (None)