Theorem ablfac1eu

Description: The factorization of ablfac1b is unique, in that any other factorization into prime power factors (even if the exponents are different) must be equal to S . (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	ablfac1.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ablfac1.o	⊢ 𝑂 = ( od ‘ 𝐺 )
	ablfac1.s	⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
	ablfac1.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	ablfac1.f	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	ablfac1.1	⊢ ( 𝜑 → 𝐴 ⊆ ℙ )
	ablfac1c.d	⊢ 𝐷 = { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) }
	ablfac1.2	⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
	ablfac1eu.1	⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑇 ∧ ( 𝐺 DProd 𝑇 ) = 𝐵 ) )
	ablfac1eu.2	⊢ ( 𝜑 → dom 𝑇 = 𝐴 )
	ablfac1eu.3	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐶 ∈ ℕ0 )
	ablfac1eu.4	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = ( 𝑞 ↑ 𝐶 ) )
Assertion	ablfac1eu	⊢ ( 𝜑 → 𝑇 = 𝑆 )

Proof

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