Theorem ablfac1eu 19945

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

Hypotheses

Ref	Expression
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

Ref	Expression
ablfac1eu	⊢ (𝜑 → 𝑇 = 𝑆)

Distinct variable groups:   𝑞,𝑝,𝑤,𝑥,𝐵   𝐷,𝑝,𝑞,𝑥   𝜑,𝑝,𝑞,𝑤,𝑥   𝑆,𝑞   𝐴,𝑝,𝑞,𝑥   𝑂,𝑝,𝑞,𝑥   𝑇,𝑞,𝑥   𝐺,𝑝,𝑞,𝑥

Allowed substitution hints:   𝐴(𝑤)   𝐶(𝑥,𝑤,𝑞,𝑝)   𝐷(𝑤)   𝑆(𝑥,𝑤,𝑝)   𝑇(𝑤,𝑝)   𝐺(𝑤)   𝑂(𝑤)

Proof of Theorem ablfac1eu

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ablfac1eu.1	. . . . 5 ⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵))
2	1	simpld 495	. . . 4 ⊢ (𝜑 → 𝐺dom DProd 𝑇)
3		ablfac1eu.2	. . . 4 ⊢ (𝜑 → dom 𝑇 = 𝐴)
4	2, 3	dprdf2 19879	. . 3 ⊢ (𝜑 → 𝑇:𝐴⟶(SubGrp‘𝐺))
5	4	ffnd 6718	. 2 ⊢ (𝜑 → 𝑇 Fn 𝐴)
6		ablfac1.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐺)
7		ablfac1.o	. . . . 5 ⊢ 𝑂 = (od‘𝐺)
8		ablfac1.s	. . . . 5 ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
9		ablfac1.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ Abel)
10		ablfac1.f	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ Fin)
11		ablfac1.1	. . . . 5 ⊢ (𝜑 → 𝐴 ⊆ ℙ)
12	6, 7, 8, 9, 10, 11	ablfac1b 19942	. . . 4 ⊢ (𝜑 → 𝐺dom DProd 𝑆)
13	6	fvexi 6905	. . . . . . 7 ⊢ 𝐵 ∈ V
14	13	rabex 5332	. . . . . 6 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V
15	14, 8	dmmpti 6694	. . . . 5 ⊢ dom 𝑆 = 𝐴
16	15	a1i 11	. . . 4 ⊢ (𝜑 → dom 𝑆 = 𝐴)
17	12, 16	dprdf2 19879	. . 3 ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))
18	17	ffnd 6718	. 2 ⊢ (𝜑 → 𝑆 Fn 𝐴)
19	10	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐵 ∈ Fin)
20	17	ffvelcdmda 7086	. . . . 5 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ (SubGrp‘𝐺))
21	6	subgss 19009	. . . . 5 ⊢ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) → (𝑆‘𝑞) ⊆ 𝐵)
22	20, 21	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ⊆ 𝐵)
23	19, 22	ssfid 9269	. . 3 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ Fin)
24	4	ffvelcdmda 7086	. . . . . 6 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ∈ (SubGrp‘𝐺))
25	6	subgss 19009	. . . . . 6 ⊢ ((𝑇‘𝑞) ∈ (SubGrp‘𝐺) → (𝑇‘𝑞) ⊆ 𝐵)
26	24, 25	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ 𝐵)
27	26	sselda 3982	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → 𝑥 ∈ 𝐵)
28	6, 7	odcl 19406	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈ ℕ0)
29	27, 28	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∈ ℕ0)
30	29	nn0zd 12586	. . . . . 6 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∈ ℤ)
31	19, 26	ssfid 9269	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ∈ Fin)
32		hashcl 14318	. . . . . . . . 9 ⊢ ((𝑇‘𝑞) ∈ Fin → (♯‘(𝑇‘𝑞)) ∈ ℕ0)
33	31, 32	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∈ ℕ0)
34	33	nn0zd 12586	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∈ ℤ)
35	34	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (♯‘(𝑇‘𝑞)) ∈ ℤ)
36	11	sselda 3982	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℙ)
37		prmnn 16613	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ ℕ)
38	36, 37	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℕ)
39		ablgrp 19655	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
40	9, 39	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ∈ Grp)
41	6	grpbn0 18853	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
42	40, 41	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ≠ ∅)
43		hashnncl 14328	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
44	10, 43	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
45	42, 44	mpbird 256	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ)
46	45	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) ∈ ℕ)
47	36, 46	pccld 16785	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℕ0)
48	38, 47	nnexpcld 14210	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ)
49	48	nnzd 12587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ)
50	49	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ)
51	24	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑇‘𝑞) ∈ (SubGrp‘𝐺))
52	31	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑇‘𝑞) ∈ Fin)
53		simpr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → 𝑥 ∈ (𝑇‘𝑞))
54	7	odsubdvds 19441	. . . . . . 7 ⊢ (((𝑇‘𝑞) ∈ (SubGrp‘𝐺) ∧ (𝑇‘𝑞) ∈ Fin ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞)))
55	51, 52, 53, 54	syl3anc 1371	. . . . . 6 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞)))
56		ablfac1eu.4	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶))
57		prmz 16614	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ ℤ)
58	36, 57	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℤ)
59		ablfac1eu.3	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℕ0)
60	59	nn0zd 12586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℤ)
61	47	nn0zd 12586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℤ)
62	6	lagsubg 19074	. . . . . . . . . . . . 13 ⊢ (((𝑇‘𝑞) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘(𝑇‘𝑞)) ∥ (♯‘𝐵))
63	24, 19, 62	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∥ (♯‘𝐵))
64	56, 63	eqbrtrrd 5172	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∥ (♯‘𝐵))
65	46	nnzd 12587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) ∈ ℤ)
66		pcdvdsb 16804	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℙ ∧ (♯‘𝐵) ∈ ℤ ∧ 𝐶 ∈ ℕ0) → (𝐶 ≤ (𝑞 pCnt (♯‘𝐵)) ↔ (𝑞↑𝐶) ∥ (♯‘𝐵)))
67	36, 65, 59, 66	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐶 ≤ (𝑞 pCnt (♯‘𝐵)) ↔ (𝑞↑𝐶) ∥ (♯‘𝐵)))
68	64, 67	mpbird 256	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ≤ (𝑞 pCnt (♯‘𝐵)))
69		eluz2 12830	. . . . . . . . . 10 ⊢ ((𝑞 pCnt (♯‘𝐵)) ∈ (ℤ≥‘𝐶) ↔ (𝐶 ∈ ℤ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℤ ∧ 𝐶 ≤ (𝑞 pCnt (♯‘𝐵))))
70	60, 61, 68, 69	syl3anbrc 1343	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ (ℤ≥‘𝐶))
71		dvdsexp 16273	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ∧ (𝑞 pCnt (♯‘𝐵)) ∈ (ℤ≥‘𝐶)) → (𝑞↑𝐶) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
72	58, 59, 70, 71	syl3anc 1371	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
73	56, 72	eqbrtrd 5170	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
74	73	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
75	30, 35, 50, 55, 74	dvdstrd 16240	. . . . 5 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
76	26, 75	ssrabdv 4071	. . . 4 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))})
77		id 22	. . . . . . . . 9 ⊢ (𝑝 = 𝑞 → 𝑝 = 𝑞)
78		oveq1 7418	. . . . . . . . 9 ⊢ (𝑝 = 𝑞 → (𝑝 pCnt (♯‘𝐵)) = (𝑞 pCnt (♯‘𝐵)))
79	77, 78	oveq12d 7429	. . . . . . . 8 ⊢ (𝑝 = 𝑞 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
80	79	breq2d 5160	. . . . . . 7 ⊢ (𝑝 = 𝑞 → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))))
81	80	rabbidv 3440	. . . . . 6 ⊢ (𝑝 = 𝑞 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))})
82	81, 8, 14	fvmpt3i 7003	. . . . 5 ⊢ (𝑞 ∈ 𝐴 → (𝑆‘𝑞) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))})
83	82	adantl 482	. . . 4 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))})
84	76, 83	sseqtrrd 4023	. . 3 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ (𝑆‘𝑞))
85	48	nnnn0d 12534	. . . . . 6 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ0)
86		pcdvds 16799	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℙ ∧ (♯‘𝐵) ∈ ℕ) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
87	36, 46, 86	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
88	2	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd 𝑇)
89	3	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom 𝑇 = 𝐴)
90		ablfac1.2	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ⊆ 𝐴)
91	90	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐷 ⊆ 𝐴)
92	88, 89, 91	dprdres 19900	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑇)))
93	92	simpld 495	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd (𝑇 ↾ 𝐷))
94	4	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑇:𝐴⟶(SubGrp‘𝐺))
95	94, 91	fssresd 6758	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺))
96	95	fdmd 6728	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom (𝑇 ↾ 𝐷) = 𝐷)
97		difssd 4132	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐷 ∖ {𝑞}) ⊆ 𝐷)
98	93, 96, 97	dprdres 19900	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})) ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))))
99	98	simpld 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))
100		dprdsubg 19896	. . . . . . . . . . 11 ⊢ (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺))
101	99, 100	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺))
102	6	lagsubg 19074	. . . . . . . . . 10 ⊢ (((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵))
103	101, 19, 102	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵))
104		eqid 2732	. . . . . . . . . . . . . . 15 ⊢ (0g‘𝐺) = (0g‘𝐺)
105	104	subg0cl 19016	. . . . . . . . . . . . . 14 ⊢ ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))
106	101, 105	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (0g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))
107	106	ne0d 4335	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅)
108	6	dprdssv 19888	. . . . . . . . . . . . . 14 ⊢ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵
109		ssfi 9175	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin)
110	19, 108, 109	sylancl 586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin)
111		hashnncl 14328	. . . . . . . . . . . . 13 ⊢ ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅))
112	110, 111	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅))
113	107, 112	mpbird 256	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ)
114	113	nnzd 12587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ)
115		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑞 → 𝑥 = 𝑞)
116		sneq 4638	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑞 → {𝑥} = {𝑞})
117	116	difeq2d 4122	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑞 → (𝐷 ∖ {𝑥}) = (𝐷 ∖ {𝑞}))
118	117	reseq2d 5981	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑞 → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})) = ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))
119	118	oveq2d 7427	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑞 → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))) = (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))
120	119	fveq2d 6895	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑞 → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) = (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))
121	115, 120	breq12d 5161	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑞 → (𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))))
122	121	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑞 → (¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ ¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))))
123		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ (𝑂‘𝑦) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) = (𝑝 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ (𝑂‘𝑦) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
124	9	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐺 ∈ Abel)
125	10	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐵 ∈ Fin)
126		ablfac1c.d	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}
127	126	ssrab3 4080	. . . . . . . . . . . . . . . . 17 ⊢ 𝐷 ⊆ ℙ
128	127	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ⊆ ℙ)
129		ssidd 4005	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ⊆ 𝐷)
130	2, 3, 90	dprdres 19900	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑇)))
131	130	simpld 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ 𝐷))
132		dprdsubg 19896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺dom DProd (𝑇 ↾ 𝐷) → (𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺))
133	131, 132	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺))
134		difssd 4132	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ 𝐴)
135	2, 3, 134	dprdres 19900	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd 𝑇)))
136	135	simpld 495	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))
137		dprdsubg 19896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)) → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺))
138	136, 137	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺))
139		difss 4131	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∖ 𝐷) ⊆ 𝐴
140		fssres 6757	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑇:𝐴⟶(SubGrp‘𝐺) ∧ (𝐴 ∖ 𝐷) ⊆ 𝐴) → (𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺))
141	4, 139, 140	sylancl 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺))
142	141	fdmd 6728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom (𝑇 ↾ (𝐴 ∖ 𝐷)) = (𝐴 ∖ 𝐷))
143		fvres 6910	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 ∈ (𝐴 ∖ 𝐷) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) = (𝑇‘𝑞))
144	143	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) = (𝑇‘𝑞))
145		eldif 3958	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 ∈ (𝐴 ∖ 𝐷) ↔ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷))
146	31	adantrr 715	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑇‘𝑞) ∈ Fin)
147	104	subg0cl 19016	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑇‘𝑞) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝑇‘𝑞))
148	24, 147	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (0g‘𝐺) ∈ (𝑇‘𝑞))
149	148	snssd 4812	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → {(0g‘𝐺)} ⊆ (𝑇‘𝑞))
150	149	adantrr 715	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ⊆ (𝑇‘𝑞))
151		fvex 6904	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (0g‘𝐺) ∈ V
152		hashsng 14331	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0g‘𝐺) ∈ V → (♯‘{(0g‘𝐺)}) = 1)
153	151, 152	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (♯‘{(0g‘𝐺)}) = 1
154	56	adantrr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶))
155	36	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ ℙ)
156		iddvdsexp 16225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞↑𝐶))
157	58, 156	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞↑𝐶))
158	64	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → (𝑞↑𝐶) ∥ (♯‘𝐵))
159	56, 34	eqeltrrd 2834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∈ ℤ)
160		dvdstr 16239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑞 ∈ ℤ ∧ (𝑞↑𝐶) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵)))
161	58, 159, 65, 160	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵)))
162	161	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵)))
163	157, 158, 162	mp2and 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (♯‘𝐵))
164		breq1 5151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑤 = 𝑞 → (𝑤 ∥ (♯‘𝐵) ↔ 𝑞 ∥ (♯‘𝐵)))
165	164, 126	elrab2 3686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑞 ∈ 𝐷 ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ (♯‘𝐵)))
166	155, 163, 165	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ 𝐷)
167	166	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐶 ∈ ℕ → 𝑞 ∈ 𝐷))
168	167	con3d 152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (¬ 𝑞 ∈ 𝐷 → ¬ 𝐶 ∈ ℕ))
169	168	impr 455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ¬ 𝐶 ∈ ℕ)
170	59	adantrr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝐶 ∈ ℕ0)
171		elnn0 12476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐶 ∈ ℕ0 ↔ (𝐶 ∈ ℕ ∨ 𝐶 = 0))
172	170, 171	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐶 ∈ ℕ ∨ 𝐶 = 0))
173	172	ord 862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (¬ 𝐶 ∈ ℕ → 𝐶 = 0))
174	169, 173	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝐶 = 0)
175	174	oveq2d 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑞↑𝐶) = (𝑞↑0))
176	38	adantrr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝑞 ∈ ℕ)
177	176	nncnd 12230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝑞 ∈ ℂ)
178	177	exp0d 14107	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑞↑0) = 1)
179	154, 175, 178	3eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (♯‘(𝑇‘𝑞)) = 1)
180	153, 179	eqtr4id 2791	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞)))
181		snfi 9046	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {(0g‘𝐺)} ∈ Fin
182		hashen 14309	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({(0g‘𝐺)} ∈ Fin ∧ (𝑇‘𝑞) ∈ Fin) → ((♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞)) ↔ {(0g‘𝐺)} ≈ (𝑇‘𝑞)))
183	181, 146, 182	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞)) ↔ {(0g‘𝐺)} ≈ (𝑇‘𝑞)))
184	180, 183	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ≈ (𝑇‘𝑞))
185		fisseneq 9259	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑇‘𝑞) ∈ Fin ∧ {(0g‘𝐺)} ⊆ (𝑇‘𝑞) ∧ {(0g‘𝐺)} ≈ (𝑇‘𝑞)) → {(0g‘𝐺)} = (𝑇‘𝑞))
186	146, 150, 184, 185	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} = (𝑇‘𝑞))
187	104	subg0cl 19016	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷)))
188	133, 187	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷)))
189	188	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷)))
190	189	snssd 4812	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))
191	186, 190	eqsstrrd 4021	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑇‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))
192	145, 191	sylan2b 594	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → (𝑇‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))
193	144, 192	eqsstrd 4020	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))
194	136, 142, 133, 193	dprdlub 19898	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))
195		eqid 2732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
196	195	lsmss2 19537	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = (𝐺 DProd (𝑇 ↾ 𝐷)))
197	133, 138, 194, 196	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = (𝐺 DProd (𝑇 ↾ 𝐷)))
198		disjdif 4471	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∩ (𝐴 ∖ 𝐷)) = ∅
199	198	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐷 ∩ (𝐴 ∖ 𝐷)) = ∅)
200		undif2 4476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∪ (𝐴 ∖ 𝐷)) = (𝐷 ∪ 𝐴)
201		ssequn1 4180	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐷 ⊆ 𝐴 ↔ (𝐷 ∪ 𝐴) = 𝐴)
202	90, 201	sylib 217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐷 ∪ 𝐴) = 𝐴)
203	200, 202	eqtr2id 2785	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 = (𝐷 ∪ (𝐴 ∖ 𝐷)))
204	4, 199, 203, 195, 2	dprdsplit 19920	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))))
205	1	simprd 496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝐵)
206	204, 205	eqtr3d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = 𝐵)
207	197, 206	eqtr3d 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵)
208	131, 207	jca 512	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵))
209	208	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵))
210	4, 90	fssresd 6758	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺))
211	210	fdmd 6728	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom (𝑇 ↾ 𝐷) = 𝐷)
212	211	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → dom (𝑇 ↾ 𝐷) = 𝐷)
213	90	sselda 3982	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → 𝑞 ∈ 𝐴)
214	213, 59	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → 𝐶 ∈ ℕ0)
215	214	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℙ) ∧ 𝑞 ∈ 𝐷) → 𝐶 ∈ ℕ0)
216		fvres 6910	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ 𝐷 → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞))
217	216	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞))
218	217	fveq2d 6895	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (♯‘(𝑇‘𝑞)))
219	213, 56	syldan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶))
220	218, 219	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (𝑞↑𝐶))
221	220	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℙ) ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (𝑞↑𝐶))
222		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝑥 ∈ ℙ)
223		fzfid 13940	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1...(♯‘𝐵)) ∈ Fin)
224		prmnn 16613	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℙ → 𝑤 ∈ ℕ)
225	224	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ ℕ)
226		prmz 16614	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℙ → 𝑤 ∈ ℤ)
227		dvdsle 16255	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑤 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵)))
228	226, 45, 227	syl2anr 597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ ℙ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵)))
229	228	3impia 1117	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ≤ (♯‘𝐵))
230	45	nnzd 12587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (♯‘𝐵) ∈ ℤ)
231	230	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
232		fznn 13571	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝐵) ∈ ℤ → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵))))
233	231, 232	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵))))
234	225, 229, 233	mpbir2and 711	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ (1...(♯‘𝐵)))
235	234	rabssdv 4072	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵)))
236	126, 235	eqsstrid 4030	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ⊆ (1...(♯‘𝐵)))
237	223, 236	ssfid 9269	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐷 ∈ Fin)
238	237	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ∈ Fin)
239	6, 7, 123, 124, 125, 128, 126, 129, 209, 212, 215, 221, 222, 238	ablfac1eulem 19944	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))))
240	239	ralrimiva 3146	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))))
241	240	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))))
242	122, 241, 36	rspcdva 3613	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))
243		coprm 16650	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℙ ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ) → (¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1))
244	36, 114, 243	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1))
245	242, 244	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)
246		rpexp1i 16662	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℤ ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℕ0) → ((𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1))
247	58, 114, 47, 246	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1))
248	245, 247	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)
249		coprmdvds2 16593	. . . . . . . . . 10 ⊢ ((((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) ∧ ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵)))
250	49, 114, 65, 248, 249	syl31anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵)))
251	87, 103, 250	mp2and 697	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵))
252		eqid 2732	. . . . . . . . . 10 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
253		inss1 4228	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∩ {𝑞}) ⊆ 𝐷
254	253	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐷 ∩ {𝑞}) ⊆ 𝐷)
255	93, 96, 254	dprdres 19900	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))))
256	255	simpld 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))
257		dprdsubg 19896	. . . . . . . . . . 11 ⊢ (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺))
258	256, 257	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺))
259		inass 4219	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞})))
260		disjdif 4471	. . . . . . . . . . . . . 14 ⊢ ({𝑞} ∩ (𝐷 ∖ {𝑞})) = ∅
261	260	ineq2i 4209	. . . . . . . . . . . . 13 ⊢ (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞}))) = (𝐷 ∩ ∅)
262		in0 4391	. . . . . . . . . . . . 13 ⊢ (𝐷 ∩ ∅) = ∅
263	259, 261, 262	3eqtri 2764	. . . . . . . . . . . 12 ⊢ ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅
264	263	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅)
265	93, 96, 254, 97, 264, 104	dprddisj2 19911	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∩ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) = {(0g‘𝐺)})
266	93, 96, 254, 97, 264, 252	dprdcntz2 19910	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))
267	6	dprdssv 19888	. . . . . . . . . . 11 ⊢ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵
268		ssfi 9175	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin)
269	19, 267, 268	sylancl 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin)
270	195, 104, 252, 258, 101, 265, 266, 269, 110	lsmhash 19575	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))))
271		inundif 4478	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})) = 𝐷
272	271	eqcomi 2741	. . . . . . . . . . . . 13 ⊢ 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞}))
273	272	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})))
274	95, 264, 273, 195, 93	dprdsplit 19920	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd (𝑇 ↾ 𝐷)) = ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))
275	207	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵)
276	274, 275	eqtr3d 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) = 𝐵)
277	276	fveq2d 6895	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = (♯‘𝐵))
278		snssi 4811	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ 𝐷 → {𝑞} ⊆ 𝐷)
279	278	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → {𝑞} ⊆ 𝐷)
280		sseqin2 4215	. . . . . . . . . . . . . . . 16 ⊢ ({𝑞} ⊆ 𝐷 ↔ (𝐷 ∩ {𝑞}) = {𝑞})
281	279, 280	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐷 ∩ {𝑞}) = {𝑞})
282	281	reseq2d 5981	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇 ↾ 𝐷) ↾ {𝑞}))
283	282	oveq2d 7427	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ {𝑞})))
284	93	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → 𝐺dom DProd (𝑇 ↾ 𝐷))
285	211	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → dom (𝑇 ↾ 𝐷) = 𝐷)
286		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → 𝑞 ∈ 𝐷)
287	284, 285, 286	dpjlem 19923	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ {𝑞})) = ((𝑇 ↾ 𝐷)‘𝑞))
288	216	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞))
289	283, 287, 288	3eqtrd 2776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞))
290		simprr 771	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ¬ 𝑞 ∈ 𝐷)
291		disjsn 4715	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∩ {𝑞}) = ∅ ↔ ¬ 𝑞 ∈ 𝐷)
292	290, 291	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐷 ∩ {𝑞}) = ∅)
293	292	reseq2d 5981	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇 ↾ 𝐷) ↾ ∅))
294		res0 5985	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇 ↾ 𝐷) ↾ ∅) = ∅
295	293, 294	eqtrdi 2788	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ∅)
296	295	oveq2d 7427	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ∅))
297	104	dprd0 19903	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ Grp → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = {(0g‘𝐺)}))
298	40, 297	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = {(0g‘𝐺)}))
299	298	simprd 496	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺 DProd ∅) = {(0g‘𝐺)})
300	299	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ∅) = {(0g‘𝐺)})
301	296, 300, 186	3eqtrd 2776	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞))
302	301	anassrs 468	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ ¬ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞))
303	289, 302	pm2.61dan 811	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞))
304	303	fveq2d 6895	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) = (♯‘(𝑇‘𝑞)))
305	304	oveq1d 7426	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))))
306	270, 277, 305	3eqtr3d 2780	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) = ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))))
307	251, 306	breqtrd 5174	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))))
308	113	nnne0d 12264	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0)
309		dvdsmulcr 16231	. . . . . . . 8 ⊢ (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ ∧ (♯‘(𝑇‘𝑞)) ∈ ℤ ∧ ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0)) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞))))
310	49, 34, 114, 308, 309	syl112anc 1374	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞))))
311	307, 310	mpbid 231	. . . . . 6 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))
312		dvdseq 16259	. . . . . 6 ⊢ ((((♯‘(𝑇‘𝑞)) ∈ ℕ0 ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ0) ∧ ((♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))) → (♯‘(𝑇‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
313	33, 85, 73, 311, 312	syl22anc 837	. . . . 5 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
314	6, 7, 8, 9, 10, 11	ablfac1a 19941	. . . . 5 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑆‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
315	313, 314	eqtr4d 2775	. . . 4 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞)))
316		hashen 14309	. . . . 5 ⊢ (((𝑇‘𝑞) ∈ Fin ∧ (𝑆‘𝑞) ∈ Fin) → ((♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞)) ↔ (𝑇‘𝑞) ≈ (𝑆‘𝑞)))
317	31, 23, 316	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞)) ↔ (𝑇‘𝑞) ≈ (𝑆‘𝑞)))
318	315, 317	mpbid 231	. . 3 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ≈ (𝑆‘𝑞))
319		fisseneq 9259	. . 3 ⊢ (((𝑆‘𝑞) ∈ Fin ∧ (𝑇‘𝑞) ⊆ (𝑆‘𝑞) ∧ (𝑇‘𝑞) ≈ (𝑆‘𝑞)) → (𝑇‘𝑞) = (𝑆‘𝑞))
320	23, 84, 318, 319	syl3anc 1371	. 2 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) = (𝑆‘𝑞))
321	5, 18, 320	eqfnfvd 7035	1 ⊢ (𝜑 → 𝑇 = 𝑆)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2940  ∀wral 3061  {crab 3432  Vcvv 3474   ∖ cdif 3945   ∪ cun 3946   ∩ cin 3947   ⊆ wss 3948  ∅c0 4322  {csn 4628   class class class wbr 5148   ↦ cmpt 5231  dom cdm 5676   ↾ cres 5678  ⟶wf 6539  ‘cfv 6543  (class class class)co 7411   ≈ cen 8938  Fincfn 8941  0cc0 11112  1c1 11113   · cmul 11117   ≤ cle 11251  ℕcn 12214  ℕ₀cn0 12474  ℤcz 12560  ℤ_≥cuz 12824  ...cfz 13486  ↑cexp 14029  ♯chash 14292   ∥ cdvds 16199   gcd cgcd 16437  ℙcprime 16610   pCnt cpc 16771  Basecbs 17146  0_gc0g 17387  Grpcgrp 18821  SubGrpcsubg 19002  Cntzccntz 19181  odcod 19394  LSSumclsm 19504  Abelcabl 19651   DProd cdprd 19865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-disj 5114  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-tpos 8213  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-oadd 8472  df-omul 8473  df-er 8705  df-ec 8707  df-qs 8711  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-acn 9939  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-n0 12475  df-xnn0 12547  df-z 12561  df-uz 12825  df-q 12935  df-rp 12977  df-fz 13487  df-fzo 13630  df-fl 13759  df-mod 13837  df-seq 13969  df-exp 14030  df-fac 14236  df-bc 14265  df-hash 14293  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-clim 15434  df-sum 15635  df-dvds 16200  df-gcd 16438  df-prm 16611  df-pc 16772  df-sets 17099  df-slot 17117  df-ndx 17129  df-base 17147  df-ress 17176  df-plusg 17212  df-0g 17389  df-gsum 17390  df-mre 17532  df-mrc 17533  df-acs 17535  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-mhm 18673  df-submnd 18674  df-grp 18824  df-minusg 18825  df-sbg 18826  df-mulg 18953  df-subg 19005  df-eqg 19007  df-ghm 19092  df-gim 19135  df-ga 19156  df-cntz 19183  df-oppg 19212  df-od 19398  df-lsm 19506  df-pj1 19507  df-cmn 19652  df-abl 19653  df-dprd 19867

This theorem is referenced by: (None)