ablfac1eu - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ablfac1eu		Structured version Visualization version GIF version

Theorem ablfac1eu 20050

Description: The factorization of ablfac1b 20047 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	⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℕ₀)
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 494	. . . 4 ⊢ (𝜑 → 𝐺dom DProd 𝑇)
3		ablfac1eu.2	. . . 4 ⊢ (𝜑 → dom 𝑇 = 𝐴)
4	2, 3	dprdf2 19984	. . 3 ⊢ (𝜑 → 𝑇:𝐴⟶(SubGrp‘𝐺))
5	4	ffnd 6670	. 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 20047	. . . 4 ⊢ (𝜑 → 𝐺dom DProd 𝑆)
13	6	fvexi 6855	. . . . . . 7 ⊢ 𝐵 ∈ V
14	13	rabex 5281	. . . . . 6 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V
15	14, 8	dmmpti 6643	. . . . 5 ⊢ dom 𝑆 = 𝐴
16	15	a1i 11	. . . 4 ⊢ (𝜑 → dom 𝑆 = 𝐴)
17	12, 16	dprdf2 19984	. . 3 ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))
18	17	ffnd 6670	. 2 ⊢ (𝜑 → 𝑆 Fn 𝐴)
19	10	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐵 ∈ Fin)
20	17	ffvelcdmda 7037	. . . . 5 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ (SubGrp‘𝐺))
21	6	subgss 19103	. . . . 5 ⊢ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) → (𝑆‘𝑞) ⊆ 𝐵)
22	20, 21	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ⊆ 𝐵)
23	19, 22	ssfid 9179	. . 3 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ Fin)
24	4	ffvelcdmda 7037	. . . . . 6 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ∈ (SubGrp‘𝐺))
25	6	subgss 19103	. . . . . 6 ⊢ ((𝑇‘𝑞) ∈ (SubGrp‘𝐺) → (𝑇‘𝑞) ⊆ 𝐵)
26	24, 25	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ 𝐵)
27	26	sselda 3922	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → 𝑥 ∈ 𝐵)
28	6, 7	odcl 19511	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈ ℕ₀)
29	27, 28	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∈ ℕ₀)
30	29	nn0zd 12549	. . . . . 6 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∈ ℤ)
31	19, 26	ssfid 9179	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ∈ Fin)
32		hashcl 14318	. . . . . . . . 9 ⊢ ((𝑇‘𝑞) ∈ Fin → (♯‘(𝑇‘𝑞)) ∈ ℕ₀)
33	31, 32	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∈ ℕ₀)
34	33	nn0zd 12549	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∈ ℤ)
35	34	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (♯‘(𝑇‘𝑞)) ∈ ℤ)
36	11	sselda 3922	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℙ)
37		prmnn 16643	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ ℕ)
38	36, 37	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℕ)
39		ablgrp 19760	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
40	9, 39	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ∈ Grp)
41	6	grpbn0 18942	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
42	40, 41	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ≠ ∅)
43		hashnncl 14328	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
44	10, 43	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
45	42, 44	mpbird 257	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ)
46	45	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) ∈ ℕ)
47	36, 46	pccld 16821	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℕ₀)
48	38, 47	nnexpcld 14207	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ)
49	48	nnzd 12550	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ)
50	49	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ)
51	24	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑇‘𝑞) ∈ (SubGrp‘𝐺))
52	31	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑇‘𝑞) ∈ Fin)
53		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → 𝑥 ∈ (𝑇‘𝑞))
54	7	odsubdvds 19546	. . . . . . 7 ⊢ (((𝑇‘𝑞) ∈ (SubGrp‘𝐺) ∧ (𝑇‘𝑞) ∈ Fin ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞)))
55	51, 52, 53, 54	syl3anc 1374	. . . . . 6 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞)))
56		ablfac1eu.4	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶))
57		prmz 16644	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ ℤ)
58	36, 57	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℤ)
59		ablfac1eu.3	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℕ₀)
60	59	nn0zd 12549	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℤ)
61	47	nn0zd 12549	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℤ)
62	6	lagsubg 19170	. . . . . . . . . . . . 13 ⊢ (((𝑇‘𝑞) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘(𝑇‘𝑞)) ∥ (♯‘𝐵))
63	24, 19, 62	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∥ (♯‘𝐵))
64	56, 63	eqbrtrrd 5110	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∥ (♯‘𝐵))
65	46	nnzd 12550	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) ∈ ℤ)
66		pcdvdsb 16840	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℙ ∧ (♯‘𝐵) ∈ ℤ ∧ 𝐶 ∈ ℕ₀) → (𝐶 ≤ (𝑞 pCnt (♯‘𝐵)) ↔ (𝑞↑𝐶) ∥ (♯‘𝐵)))
67	36, 65, 59, 66	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐶 ≤ (𝑞 pCnt (♯‘𝐵)) ↔ (𝑞↑𝐶) ∥ (♯‘𝐵)))
68	64, 67	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ≤ (𝑞 pCnt (♯‘𝐵)))
69		eluz2 12794	. . . . . . . . . 10 ⊢ ((𝑞 pCnt (♯‘𝐵)) ∈ (ℤ_≥‘𝐶) ↔ (𝐶 ∈ ℤ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℤ ∧ 𝐶 ≤ (𝑞 pCnt (♯‘𝐵))))
70	60, 61, 68, 69	syl3anbrc 1345	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ (ℤ_≥‘𝐶))
71		dvdsexp 16297	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ₀ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ (ℤ_≥‘𝐶)) → (𝑞↑𝐶) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
72	58, 59, 70, 71	syl3anc 1374	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
73	56, 72	eqbrtrd 5108	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
74	73	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
75	30, 35, 50, 55, 74	dvdstrd 16264	. . . . 5 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
76	26, 75	ssrabdv 4014	. . . 4 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))})
77		id 22	. . . . . . . . 9 ⊢ (𝑝 = 𝑞 → 𝑝 = 𝑞)
78		oveq1 7374	. . . . . . . . 9 ⊢ (𝑝 = 𝑞 → (𝑝 pCnt (♯‘𝐵)) = (𝑞 pCnt (♯‘𝐵)))
79	77, 78	oveq12d 7385	. . . . . . . 8 ⊢ (𝑝 = 𝑞 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
80	79	breq2d 5098	. . . . . . 7 ⊢ (𝑝 = 𝑞 → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))))
81	80	rabbidv 3397	. . . . . 6 ⊢ (𝑝 = 𝑞 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))})
82	81, 8, 14	fvmpt3i 6954	. . . . 5 ⊢ (𝑞 ∈ 𝐴 → (𝑆‘𝑞) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))})
83	82	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))})
84	76, 83	sseqtrrd 3960	. . 3 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ (𝑆‘𝑞))
85	48	nnnn0d 12498	. . . . . 6 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ₀)
86		pcdvds 16835	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℙ ∧ (♯‘𝐵) ∈ ℕ) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
87	36, 46, 86	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
88	2	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd 𝑇)
89	3	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom 𝑇 = 𝐴)
90		ablfac1.2	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ⊆ 𝐴)
91	90	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐷 ⊆ 𝐴)
92	88, 89, 91	dprdres 20005	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑇)))
93	92	simpld 494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd (𝑇 ↾ 𝐷))
94	4	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑇:𝐴⟶(SubGrp‘𝐺))
95	94, 91	fssresd 6708	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺))
96	95	fdmd 6679	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom (𝑇 ↾ 𝐷) = 𝐷)
97		difssd 4078	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐷 ∖ {𝑞}) ⊆ 𝐷)
98	93, 96, 97	dprdres 20005	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})) ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))))
99	98	simpld 494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))
100		dprdsubg 20001	. . . . . . . . . . 11 ⊢ (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺))
101	99, 100	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺))
102	6	lagsubg 19170	. . . . . . . . . 10 ⊢ (((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵))
103	101, 19, 102	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵))
104		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
105	104	subg0cl 19110	. . . . . . . . . . . . . 14 ⊢ ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))
106	101, 105	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))
107	106	ne0d 4283	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅)
108	6	dprdssv 19993	. . . . . . . . . . . . . 14 ⊢ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵
109		ssfi 9107	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin)
110	19, 108, 109	sylancl 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin)
111		hashnncl 14328	. . . . . . . . . . . . 13 ⊢ ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅))
112	110, 111	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅))
113	107, 112	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ)
114	113	nnzd 12550	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ)
115		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑞 → 𝑥 = 𝑞)
116		sneq 4578	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑞 → {𝑥} = {𝑞})
117	116	difeq2d 4067	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑞 → (𝐷 ∖ {𝑥}) = (𝐷 ∖ {𝑞}))
118	117	reseq2d 5945	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑞 → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})) = ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))
119	118	oveq2d 7383	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑞 → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))) = (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))
120	119	fveq2d 6845	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑞 → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) = (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))
121	115, 120	breq12d 5099	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑞 → (𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))))
122	121	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑞 → (¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ ¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))))
123		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ (𝑂‘𝑦) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) = (𝑝 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ (𝑂‘𝑦) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
124	9	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐺 ∈ Abel)
125	10	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐵 ∈ Fin)
126		ablfac1c.d	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}
127	126	ssrab3 4023	. . . . . . . . . . . . . . . . 17 ⊢ 𝐷 ⊆ ℙ
128	127	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ⊆ ℙ)
129		ssidd 3946	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ⊆ 𝐷)
130	2, 3, 90	dprdres 20005	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑇)))
131	130	simpld 494	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ 𝐷))
132		dprdsubg 20001	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺dom DProd (𝑇 ↾ 𝐷) → (𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺))
133	131, 132	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺))
134		difssd 4078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ 𝐴)
135	2, 3, 134	dprdres 20005	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd 𝑇)))
136	135	simpld 494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))
137		dprdsubg 20001	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)) → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺))
138	136, 137	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺))
139		difss 4077	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∖ 𝐷) ⊆ 𝐴
140		fssres 6707	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑇:𝐴⟶(SubGrp‘𝐺) ∧ (𝐴 ∖ 𝐷) ⊆ 𝐴) → (𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺))
141	4, 139, 140	sylancl 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺))
142	141	fdmd 6679	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom (𝑇 ↾ (𝐴 ∖ 𝐷)) = (𝐴 ∖ 𝐷))
143		fvres 6860	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 ∈ (𝐴 ∖ 𝐷) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) = (𝑇‘𝑞))
144	143	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) = (𝑇‘𝑞))
145		eldif 3900	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 ∈ (𝐴 ∖ 𝐷) ↔ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷))
146	31	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑇‘𝑞) ∈ Fin)
147	104	subg0cl 19110	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑇‘𝑞) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝑇‘𝑞))
148	24, 147	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝑇‘𝑞))
149	148	snssd 4731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → {(0_g‘𝐺)} ⊆ (𝑇‘𝑞))
150	149	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0_g‘𝐺)} ⊆ (𝑇‘𝑞))
151		fvex 6854	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (0_g‘𝐺) ∈ V
152		hashsng 14331	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0_g‘𝐺) ∈ V → (♯‘{(0_g‘𝐺)}) = 1)
153	151, 152	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (♯‘{(0_g‘𝐺)}) = 1
154	56	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶))
155	36	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ ℙ)
156		iddvdsexp 16248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞↑𝐶))
157	58, 156	sylan 581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞↑𝐶))
158	64	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → (𝑞↑𝐶) ∥ (♯‘𝐵))
159	56, 34	eqeltrrd 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∈ ℤ)
160		dvdstr 16263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑞 ∈ ℤ ∧ (𝑞↑𝐶) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵)))
161	58, 159, 65, 160	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵)))
162	161	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵)))
163	157, 158, 162	mp2and 700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (♯‘𝐵))
164		breq1 5089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑤 = 𝑞 → (𝑤 ∥ (♯‘𝐵) ↔ 𝑞 ∥ (♯‘𝐵)))
165	164, 126	elrab2 3638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑞 ∈ 𝐷 ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ (♯‘𝐵)))
166	155, 163, 165	sylanbrc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ 𝐷)
167	166	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐶 ∈ ℕ → 𝑞 ∈ 𝐷))
168	167	con3d 152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (¬ 𝑞 ∈ 𝐷 → ¬ 𝐶 ∈ ℕ))
169	168	impr 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ¬ 𝐶 ∈ ℕ)
170	59	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝐶 ∈ ℕ₀)
171		elnn0 12439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐶 ∈ ℕ₀ ↔ (𝐶 ∈ ℕ ∨ 𝐶 = 0))
172	170, 171	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐶 ∈ ℕ ∨ 𝐶 = 0))
173	172	ord 865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (¬ 𝐶 ∈ ℕ → 𝐶 = 0))
174	169, 173	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝐶 = 0)
175	174	oveq2d 7383	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑞↑𝐶) = (𝑞↑0))
176	38	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝑞 ∈ ℕ)
177	176	nncnd 12190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝑞 ∈ ℂ)
178	177	exp0d 14102	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑞↑0) = 1)
179	154, 175, 178	3eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (♯‘(𝑇‘𝑞)) = 1)
180	153, 179	eqtr4id 2791	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (♯‘{(0_g‘𝐺)}) = (♯‘(𝑇‘𝑞)))
181		snfi 8990	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {(0_g‘𝐺)} ∈ Fin
182		hashen 14309	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({(0_g‘𝐺)} ∈ Fin ∧ (𝑇‘𝑞) ∈ Fin) → ((♯‘{(0_g‘𝐺)}) = (♯‘(𝑇‘𝑞)) ↔ {(0_g‘𝐺)} ≈ (𝑇‘𝑞)))
183	181, 146, 182	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((♯‘{(0_g‘𝐺)}) = (♯‘(𝑇‘𝑞)) ↔ {(0_g‘𝐺)} ≈ (𝑇‘𝑞)))
184	180, 183	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0_g‘𝐺)} ≈ (𝑇‘𝑞))
185		fisseneq 9173	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑇‘𝑞) ∈ Fin ∧ {(0_g‘𝐺)} ⊆ (𝑇‘𝑞) ∧ {(0_g‘𝐺)} ≈ (𝑇‘𝑞)) → {(0_g‘𝐺)} = (𝑇‘𝑞))
186	146, 150, 184, 185	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0_g‘𝐺)} = (𝑇‘𝑞))
187	104	subg0cl 19110	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷)))
188	133, 187	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (0_g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷)))
189	188	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (0_g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷)))
190	189	snssd 4731	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0_g‘𝐺)} ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))
191	186, 190	eqsstrrd 3958	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑇‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))
192	145, 191	sylan2b 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → (𝑇‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))
193	144, 192	eqsstrd 3957	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))
194	136, 142, 133, 193	dprdlub 20003	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))
195		eqid 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
196	195	lsmss2 19642	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = (𝐺 DProd (𝑇 ↾ 𝐷)))
197	133, 138, 194, 196	syl3anc 1374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = (𝐺 DProd (𝑇 ↾ 𝐷)))
198		disjdif 4413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∩ (𝐴 ∖ 𝐷)) = ∅
199	198	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐷 ∩ (𝐴 ∖ 𝐷)) = ∅)
200		undif2 4418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∪ (𝐴 ∖ 𝐷)) = (𝐷 ∪ 𝐴)
201		ssequn1 4127	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐷 ⊆ 𝐴 ↔ (𝐷 ∪ 𝐴) = 𝐴)
202	90, 201	sylib 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐷 ∪ 𝐴) = 𝐴)
203	200, 202	eqtr2id 2785	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 = (𝐷 ∪ (𝐴 ∖ 𝐷)))
204	4, 199, 203, 195, 2	dprdsplit 20025	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))))
205	1	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝐵)
206	204, 205	eqtr3d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = 𝐵)
207	197, 206	eqtr3d 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵)
208	131, 207	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵))
209	208	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵))
210	4, 90	fssresd 6708	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺))
211	210	fdmd 6679	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom (𝑇 ↾ 𝐷) = 𝐷)
212	211	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → dom (𝑇 ↾ 𝐷) = 𝐷)
213	90	sselda 3922	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → 𝑞 ∈ 𝐴)
214	213, 59	syldan 592	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → 𝐶 ∈ ℕ₀)
215	214	adantlr 716	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℙ) ∧ 𝑞 ∈ 𝐷) → 𝐶 ∈ ℕ₀)
216		fvres 6860	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ 𝐷 → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞))
217	216	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞))
218	217	fveq2d 6845	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (♯‘(𝑇‘𝑞)))
219	213, 56	syldan 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶))
220	218, 219	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (𝑞↑𝐶))
221	220	adantlr 716	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℙ) ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (𝑞↑𝐶))
222		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝑥 ∈ ℙ)
223		fzfid 13935	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1...(♯‘𝐵)) ∈ Fin)
224		prmnn 16643	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℙ → 𝑤 ∈ ℕ)
225	224	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ ℕ)
226		prmz 16644	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℙ → 𝑤 ∈ ℤ)
227		dvdsle 16279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑤 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵)))
228	226, 45, 227	syl2anr 598	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ ℙ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵)))
229	228	3impia 1118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ≤ (♯‘𝐵))
230	45	nnzd 12550	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (♯‘𝐵) ∈ ℤ)
231	230	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
232		fznn 13546	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝐵) ∈ ℤ → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵))))
233	231, 232	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵))))
234	225, 229, 233	mpbir2and 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ (1...(♯‘𝐵)))
235	234	rabssdv 4015	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵)))
236	126, 235	eqsstrid 3961	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ⊆ (1...(♯‘𝐵)))
237	223, 236	ssfid 9179	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐷 ∈ Fin)
238	237	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ∈ Fin)
239	6, 7, 123, 124, 125, 128, 126, 129, 209, 212, 215, 221, 222, 238	ablfac1eulem 20049	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))))
240	239	ralrimiva 3130	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))))
241	240	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))))
242	122, 241, 36	rspcdva 3566	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))
243		coprm 16681	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℙ ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ) → (¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1))
244	36, 114, 243	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1))
245	242, 244	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)
246		rpexp1i 16693	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℤ ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℕ₀) → ((𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1))
247	58, 114, 47, 246	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1))
248	245, 247	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)
249		coprmdvds2 16623	. . . . . . . . . 10 ⊢ ((((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) ∧ ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵)))
250	49, 114, 65, 248, 249	syl31anc 1376	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵)))
251	87, 103, 250	mp2and 700	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵))
252		eqid 2737	. . . . . . . . . 10 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
253		inss1 4178	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∩ {𝑞}) ⊆ 𝐷
254	253	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐷 ∩ {𝑞}) ⊆ 𝐷)
255	93, 96, 254	dprdres 20005	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))))
256	255	simpld 494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))
257		dprdsubg 20001	. . . . . . . . . . 11 ⊢ (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺))
258	256, 257	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺))
259		inass 4169	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞})))
260		disjdif 4413	. . . . . . . . . . . . . 14 ⊢ ({𝑞} ∩ (𝐷 ∖ {𝑞})) = ∅
261	260	ineq2i 4158	. . . . . . . . . . . . 13 ⊢ (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞}))) = (𝐷 ∩ ∅)
262		in0 4336	. . . . . . . . . . . . 13 ⊢ (𝐷 ∩ ∅) = ∅
263	259, 261, 262	3eqtri 2764	. . . . . . . . . . . 12 ⊢ ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅
264	263	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅)
265	93, 96, 254, 97, 264, 104	dprddisj2 20016	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∩ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) = {(0_g‘𝐺)})
266	93, 96, 254, 97, 264, 252	dprdcntz2 20015	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))
267	6	dprdssv 19993	. . . . . . . . . . 11 ⊢ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵
268		ssfi 9107	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin)
269	19, 267, 268	sylancl 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin)
270	195, 104, 252, 258, 101, 265, 266, 269, 110	lsmhash 19680	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))))
271		inundif 4420	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})) = 𝐷
272	271	eqcomi 2746	. . . . . . . . . . . . 13 ⊢ 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞}))
273	272	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})))
274	95, 264, 273, 195, 93	dprdsplit 20025	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd (𝑇 ↾ 𝐷)) = ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))
275	207	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵)
276	274, 275	eqtr3d 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) = 𝐵)
277	276	fveq2d 6845	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = (♯‘𝐵))
278		snssi 4730	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ 𝐷 → {𝑞} ⊆ 𝐷)
279	278	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → {𝑞} ⊆ 𝐷)
280		sseqin2 4164	. . . . . . . . . . . . . . . 16 ⊢ ({𝑞} ⊆ 𝐷 ↔ (𝐷 ∩ {𝑞}) = {𝑞})
281	279, 280	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐷 ∩ {𝑞}) = {𝑞})
282	281	reseq2d 5945	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇 ↾ 𝐷) ↾ {𝑞}))
283	282	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ {𝑞})))
284	93	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → 𝐺dom DProd (𝑇 ↾ 𝐷))
285	211	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → dom (𝑇 ↾ 𝐷) = 𝐷)
286		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → 𝑞 ∈ 𝐷)
287	284, 285, 286	dpjlem 20028	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ {𝑞})) = ((𝑇 ↾ 𝐷)‘𝑞))
288	216	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞))
289	283, 287, 288	3eqtrd 2776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞))
290		simprr 773	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ¬ 𝑞 ∈ 𝐷)
291		disjsn 4656	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∩ {𝑞}) = ∅ ↔ ¬ 𝑞 ∈ 𝐷)
292	290, 291	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐷 ∩ {𝑞}) = ∅)
293	292	reseq2d 5945	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇 ↾ 𝐷) ↾ ∅))
294		res0 5949	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇 ↾ 𝐷) ↾ ∅) = ∅
295	293, 294	eqtrdi 2788	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ∅)
296	295	oveq2d 7383	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ∅))
297	104	dprd0 20008	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ Grp → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = {(0_g‘𝐺)}))
298	40, 297	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = {(0_g‘𝐺)}))
299	298	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺 DProd ∅) = {(0_g‘𝐺)})
300	299	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ∅) = {(0_g‘𝐺)})
301	296, 300, 186	3eqtrd 2776	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞))
302	301	anassrs 467	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ ¬ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞))
303	289, 302	pm2.61dan 813	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞))
304	303	fveq2d 6845	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) = (♯‘(𝑇‘𝑞)))
305	304	oveq1d 7382	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))))
306	270, 277, 305	3eqtr3d 2780	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) = ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))))
307	251, 306	breqtrd 5112	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))))
308	113	nnne0d 12227	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0)
309		dvdsmulcr 16254	. . . . . . . 8 ⊢ (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ ∧ (♯‘(𝑇‘𝑞)) ∈ ℤ ∧ ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0)) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞))))
310	49, 34, 114, 308, 309	syl112anc 1377	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞))))
311	307, 310	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))
312		dvdseq 16283	. . . . . 6 ⊢ ((((♯‘(𝑇‘𝑞)) ∈ ℕ₀ ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ₀) ∧ ((♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))) → (♯‘(𝑇‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
313	33, 85, 73, 311, 312	syl22anc 839	. . . . 5 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
314	6, 7, 8, 9, 10, 11	ablfac1a 20046	. . . . 5 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑆‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
315	313, 314	eqtr4d 2775	. . . 4 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞)))
316		hashen 14309	. . . . 5 ⊢ (((𝑇‘𝑞) ∈ Fin ∧ (𝑆‘𝑞) ∈ Fin) → ((♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞)) ↔ (𝑇‘𝑞) ≈ (𝑆‘𝑞)))
317	31, 23, 316	syl2anc 585	. . . 4 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞)) ↔ (𝑇‘𝑞) ≈ (𝑆‘𝑞)))
318	315, 317	mpbid 232	. . 3 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ≈ (𝑆‘𝑞))
319		fisseneq 9173	. . 3 ⊢ (((𝑆‘𝑞) ∈ Fin ∧ (𝑇‘𝑞) ⊆ (𝑆‘𝑞) ∧ (𝑇‘𝑞) ≈ (𝑆‘𝑞)) → (𝑇‘𝑞) = (𝑆‘𝑞))
320	23, 84, 318, 319	syl3anc 1374	. 2 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) = (𝑆‘𝑞))
321	5, 18, 320	eqfnfvd 6987	1 ⊢ (𝜑 → 𝑇 = 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 {crab 3390 Vcvv 3430 ∖ cdif 3887 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 ∅c0 4274 {csn 4568 class class class wbr 5086 ↦ cmpt 5167 dom cdm 5631 ↾ cres 5633 ⟶wf 6495 ‘cfv 6499 (class class class)co 7367 ≈ cen 8890 Fincfn 8893 0cc0 11038 1c1 11039 · cmul 11043 ≤ cle 11180 ℕcn 12174 ℕ₀cn0 12437 ℤcz 12524 ℤ_≥cuz 12788 ...cfz 13461 ↑cexp 14023 ♯chash 14292 ∥ cdvds 16221 gcd cgcd 16463 ℙcprime 16640 pCnt cpc 16807 Basecbs 17179 0_gc0g 17402 Grpcgrp 18909 SubGrpcsubg 19096 Cntzccntz 19290 odcod 19499 LSSumclsm 19609 Abelcabl 19756 DProd cdprd 19970

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5308 ax-pr 5376 ax-un 7689 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-disj 5054 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6266 df-ord 6327 df-on 6328 df-lim 6329 df-suc 6330 df-iota 6455 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-om 7818 df-1st 7942 df-2nd 7943 df-supp 8111 df-tpos 8176 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-2o 8406 df-oadd 8409 df-omul 8410 df-er 8643 df-ec 8645 df-qs 8649 df-map 8775 df-ixp 8846 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fsupp 9275 df-sup 9355 df-inf 9356 df-oi 9425 df-dju 9825 df-card 9863 df-acn 9866 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-n0 12438 df-xnn0 12511 df-z 12525 df-uz 12789 df-q 12899 df-rp 12943 df-fz 13462 df-fzo 13609 df-fl 13751 df-mod 13829 df-seq 13964 df-exp 14024 df-fac 14236 df-bc 14265 df-hash 14293 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198 df-clim 15450 df-sum 15649 df-dvds 16222 df-gcd 16464 df-prm 16641 df-pc 16808 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-0g 17404 df-gsum 17405 df-mre 17548 df-mrc 17549 df-acs 17551 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-mhm 18751 df-submnd 18752 df-grp 18912 df-minusg 18913 df-sbg 18914 df-mulg 19044 df-subg 19099 df-eqg 19101 df-ghm 19188 df-gim 19234 df-ga 19265 df-cntz 19292 df-oppg 19321 df-od 19503 df-lsm 19611 df-pj1 19612 df-cmn 19757 df-abl 19758 df-dprd 19972

This theorem is referenced by: (None)

W3C validator