Theorem grpods 43447

Description: Relate sums of elements of orders and roots of unity. (Contributed by metakunt, 14-Jul-2025.)

Hypotheses

Ref	Expression
grpods.1	⊢ 𝐵 = (Base‘𝐺)
grpods.2	⊢ ↑ = (.g‘𝐺)
grpods.3	⊢ (𝜑 → 𝐺 ∈ Grp)
grpods.4	⊢ (𝜑 → 𝐵 ∈ Fin)
grpods.5	⊢ (𝜑 → 𝑁 ∈ ℕ)

Assertion

Ref	Expression
grpods	⊢ (𝜑 → Σ𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)}))

Distinct variable groups:   𝑥, ↑   𝐵,𝑘,𝑥   𝑘,𝐺,𝑚   𝑥,𝐺   𝑘,𝑁,𝑚   𝑥,𝑁   𝜑,𝑘

Allowed substitution hints:   𝜑(𝑥, 𝑚)   𝐵(𝑚)   ↑ (𝑘, 𝑚)

Proof of Theorem grpods

Dummy variables 𝑑 𝑙 𝑦 𝑖 𝑤 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7454	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑁 ↑ 𝑥) = (𝑁 ↑ 𝑦))
2	1	eqeq1d 2765	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝑁 ↑ 𝑥) = (0g‘𝐺) ↔ (𝑁 ↑ 𝑦) = (0g‘𝐺)))
3	2	elrab 3648	. . . . . . . 8 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)} ↔ (𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺)))
4	3	bilani 510	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)}) → (𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺)))
5		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺))) → 𝜑)
6		simprl 783	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺))) → 𝑦 ∈ 𝐵)
7	5, 6	jca 521	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺))) → (𝜑 ∧ 𝑦 ∈ 𝐵))
8		simprr 785	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺))) → (𝑁 ↑ 𝑦) = (0g‘𝐺))
9		grpods.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ Grp)
10	5, 9	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺))) → 𝐺 ∈ Grp)
11		grpmnd 19183	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
12	10, 11	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺))) → 𝐺 ∈ Mnd)
13		grpods.5	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℕ)
14	5, 13	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺))) → 𝑁 ∈ ℕ)
15	14	nnnn0d 12697	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺))) → 𝑁 ∈ ℕ0)
16		grpods.1	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝐺)
17		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (od‘𝐺) = (od‘𝐺)
18		grpods.2	. . . . . . . . . . . . . 14 ⊢ ↑ = (.g‘𝐺)
19		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (0g‘𝐺) = (0g‘𝐺)
20	16, 17, 18, 19	oddvdsnn0 19791	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0) → (((od‘𝐺)‘𝑦) ∥ 𝑁 ↔ (𝑁 ↑ 𝑦) = (0g‘𝐺)))
21	12, 6, 15, 20	syl3anc 1399	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺))) → (((od‘𝐺)‘𝑦) ∥ 𝑁 ↔ (𝑁 ↑ 𝑦) = (0g‘𝐺)))
22	8, 21	mpbird 260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺))) → ((od‘𝐺)‘𝑦) ∥ 𝑁)
23	7, 22	jca 521	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺))) → ((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁))
24		breq1 5109	. . . . . . . . . . . 12 ⊢ (𝑚 = ((od‘𝐺)‘𝑦) → (𝑚 ∥ 𝑁 ↔ ((od‘𝐺)‘𝑦) ∥ 𝑁))
25		1zzd 12757	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → 1 ∈ ℤ)
26	13	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → 𝑁 ∈ ℕ)
27	26	nnzd 12749	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → 𝑁 ∈ ℤ)
28		dvdszrcl 16459	. . . . . . . . . . . . . . 15 ⊢ (((od‘𝐺)‘𝑦) ∥ 𝑁 → (((od‘𝐺)‘𝑦) ∈ ℤ ∧ 𝑁 ∈ ℤ))
29	28	simpld 500	. . . . . . . . . . . . . 14 ⊢ (((od‘𝐺)‘𝑦) ∥ 𝑁 → ((od‘𝐺)‘𝑦) ∈ ℤ)
30	29	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → ((od‘𝐺)‘𝑦) ∈ ℤ)
31	9	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → 𝐺 ∈ Grp)
32		grpods.4	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ∈ Fin)
33	32	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → 𝐵 ∈ Fin)
34		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → 𝑦 ∈ 𝐵)
35	16, 17	odcl2 19812	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑦 ∈ 𝐵) → ((od‘𝐺)‘𝑦) ∈ ℕ)
36	31, 33, 34, 35	syl3anc 1399	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → ((od‘𝐺)‘𝑦) ∈ ℕ)
37	36	nnge1d 12416	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → 1 ≤ ((od‘𝐺)‘𝑦))
38	30, 26	jca 521	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → (((od‘𝐺)‘𝑦) ∈ ℤ ∧ 𝑁 ∈ ℕ))
39		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → ((od‘𝐺)‘𝑦) ∥ 𝑁)
40		dvdsle 16512	. . . . . . . . . . . . . . 15 ⊢ ((((od‘𝐺)‘𝑦) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((od‘𝐺)‘𝑦) ∥ 𝑁 → ((od‘𝐺)‘𝑦) ≤ 𝑁))
41	40	imp 412	. . . . . . . . . . . . . 14 ⊢ (((((od‘𝐺)‘𝑦) ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → ((od‘𝐺)‘𝑦) ≤ 𝑁)
42	38, 39, 41	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → ((od‘𝐺)‘𝑦) ≤ 𝑁)
43	25, 27, 30, 37, 42	elfzd 13677	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → ((od‘𝐺)‘𝑦) ∈ (1...𝑁))
44	24, 43, 39	elrabd 3650	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → ((od‘𝐺)‘𝑦) ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁})
45		fveqeq2 6920	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (((od‘𝐺)‘𝑥) = ((od‘𝐺)‘𝑦) ↔ ((od‘𝐺)‘𝑦) = ((od‘𝐺)‘𝑦)))
46		eqidd 2764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → ((od‘𝐺)‘𝑦) = ((od‘𝐺)‘𝑦))
47	45, 34, 46	elrabd 3650	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = ((od‘𝐺)‘𝑦)})
48		eqeq2 2775	. . . . . . . . . . . . 13 ⊢ (𝑘 = ((od‘𝐺)‘𝑦) → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘𝑥) = ((od‘𝐺)‘𝑦)))
49	48	rabbidv 3423	. . . . . . . . . . . 12 ⊢ (𝑘 = ((od‘𝐺)‘𝑦) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = ((od‘𝐺)‘𝑦)})
50	49	eliuni 4960	. . . . . . . . . . 11 ⊢ ((((od‘𝐺)‘𝑦) ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = ((od‘𝐺)‘𝑦)}) → 𝑦 ∈ ∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
51	44, 47, 50	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑦) ∥ 𝑁) → 𝑦 ∈ ∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
52	23, 51	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺))) → 𝑦 ∈ ∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
53	52	ex 418	. . . . . . . 8 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺)) → 𝑦 ∈ ∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
54	53	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)}) → ((𝑦 ∈ 𝐵 ∧ (𝑁 ↑ 𝑦) = (0g‘𝐺)) → 𝑦 ∈ ∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
55	4, 54	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)}) → 𝑦 ∈ ∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
56	55	ex 418	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)} → 𝑦 ∈ ∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
57		eliun 4958	. . . . . . . 8 ⊢ (𝑦 ∈ ∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ↔ ∃𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
58	57	bilani 510	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) → ∃𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
59		simplll 787	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∃𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}) → 𝜑)
60		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∃𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}) → 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁})
61	59, 60	jca 521	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ∃𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}) → (𝜑 ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}))
62		simpr 490	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ∃𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}) → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙})
63	61, 62	jca 521	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ∃𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}) → ((𝜑 ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}))
64		elrabi 3644	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙} → 𝑦 ∈ 𝐵)
65	64	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}) → 𝑦 ∈ 𝐵)
66		simpll 779	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}) → 𝜑)
67		breq1 5109	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑙 → (𝑚 ∥ 𝑁 ↔ 𝑙 ∥ 𝑁))
68	67	elrab 3648	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} ↔ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁))
69	68	bilani 510	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) → (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁))
70	69	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}) → (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁))
71	66, 70	jca 521	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}) → (𝜑 ∧ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁)))
72		fveqeq2 6920	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (((od‘𝐺)‘𝑥) = 𝑙 ↔ ((od‘𝐺)‘𝑦) = 𝑙))
73	72	elrab 3648	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙} ↔ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙))
74	73	bilani 510	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}) → (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙))
75	71, 74	jca 521	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}) → ((𝜑 ∧ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁)) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)))
76		simpll 779	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁)) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) → 𝜑)
77		simprr 785	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁)) → 𝑙 ∥ 𝑁)
78		elfzelz 13686	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑙 ∈ (1...𝑁) → 𝑙 ∈ ℤ)
79	78	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁) → 𝑙 ∈ ℤ)
80	79	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁)) → 𝑙 ∈ ℤ)
81	13	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁)) → 𝑁 ∈ ℕ)
82	81	nnzd 12749	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁)) → 𝑁 ∈ ℤ)
83		divides 16456	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑙 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑙 ∥ 𝑁 ↔ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁))
84	80, 82, 83	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁)) → (𝑙 ∥ 𝑁 ↔ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁))
85	77, 84	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁)) → ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁)
86	85	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁)) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) → ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁)
87	76, 86	jca 521	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁)) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) → (𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁))
88		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁)) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) → (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙))
89	87, 88	jca 521	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁)) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) → ((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)))
90		oveq1 7453	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 · 𝑙) = 𝑁 → ((𝑑 · 𝑙) ↑ 𝑦) = (𝑁 ↑ 𝑦))
91	90	eqcomd 2769	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 · 𝑙) = 𝑁 → (𝑁 ↑ 𝑦) = ((𝑑 · 𝑙) ↑ 𝑦))
92	91	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) ∧ 𝑑 ∈ ℤ) ∧ (𝑑 · 𝑙) = 𝑁) → (𝑁 ↑ 𝑦) = ((𝑑 · 𝑙) ↑ 𝑦))
93		simplrr 790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) ∧ 𝑑 ∈ ℤ) → ((od‘𝐺)‘𝑦) = 𝑙)
94	93	oveq2d 7462	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) ∧ 𝑑 ∈ ℤ) → (𝑑 · ((od‘𝐺)‘𝑦)) = (𝑑 · 𝑙))
95	94	eqcomd 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) ∧ 𝑑 ∈ ℤ) → (𝑑 · 𝑙) = (𝑑 · ((od‘𝐺)‘𝑦)))
96	95	oveq1d 7461	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) ∧ 𝑑 ∈ ℤ) → ((𝑑 · 𝑙) ↑ 𝑦) = ((𝑑 · ((od‘𝐺)‘𝑦)) ↑ 𝑦))
97		simplll 787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) ∧ 𝑑 ∈ ℤ) → 𝜑)
98		simplrl 789	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) ∧ 𝑑 ∈ ℤ) → 𝑦 ∈ 𝐵)
99	97, 98	jca 521	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) ∧ 𝑑 ∈ ℤ) → (𝜑 ∧ 𝑦 ∈ 𝐵))
100		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) ∧ 𝑑 ∈ ℤ) → 𝑑 ∈ ℤ)
101	99, 100	jca 521	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) ∧ 𝑑 ∈ ℤ) → ((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑑 ∈ ℤ))
102	9	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑑 ∈ ℤ) → 𝐺 ∈ Grp)
103		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑑 ∈ ℤ) → 𝑑 ∈ ℤ)
104	16, 17	odcl 19783	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ 𝐵 → ((od‘𝐺)‘𝑦) ∈ ℕ0)
105	104	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑑 ∈ ℤ) → ((od‘𝐺)‘𝑦) ∈ ℕ0)
106	105	nn0zd 12748	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑑 ∈ ℤ) → ((od‘𝐺)‘𝑦) ∈ ℤ)
107		simplr 781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑑 ∈ ℤ) → 𝑦 ∈ 𝐵)
108	103, 106, 107	3jca 1146	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑑 ∈ ℤ) → (𝑑 ∈ ℤ ∧ ((od‘𝐺)‘𝑦) ∈ ℤ ∧ 𝑦 ∈ 𝐵))
109	16, 18	mulgass 19353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺 ∈ Grp ∧ (𝑑 ∈ ℤ ∧ ((od‘𝐺)‘𝑦) ∈ ℤ ∧ 𝑦 ∈ 𝐵)) → ((𝑑 · ((od‘𝐺)‘𝑦)) ↑ 𝑦) = (𝑑 ↑ (((od‘𝐺)‘𝑦) ↑ 𝑦)))
110	102, 108, 109	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑑 ∈ ℤ) → ((𝑑 · ((od‘𝐺)‘𝑦)) ↑ 𝑦) = (𝑑 ↑ (((od‘𝐺)‘𝑦) ↑ 𝑦)))
111	16, 17, 18, 19	odid 19785	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝐵 → (((od‘𝐺)‘𝑦) ↑ 𝑦) = (0g‘𝐺))
112	107, 111	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑑 ∈ ℤ) → (((od‘𝐺)‘𝑦) ↑ 𝑦) = (0g‘𝐺))
113	112	oveq2d 7462	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑑 ∈ ℤ) → (𝑑 ↑ (((od‘𝐺)‘𝑦) ↑ 𝑦)) = (𝑑 ↑ (0g‘𝐺)))
114	16, 18, 19	mulgz 19344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺 ∈ Grp ∧ 𝑑 ∈ ℤ) → (𝑑 ↑ (0g‘𝐺)) = (0g‘𝐺))
115	102, 103, 114	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑑 ∈ ℤ) → (𝑑 ↑ (0g‘𝐺)) = (0g‘𝐺))
116	113, 115	eqtrd 2798	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑑 ∈ ℤ) → (𝑑 ↑ (((od‘𝐺)‘𝑦) ↑ 𝑦)) = (0g‘𝐺))
117	110, 116	eqtrd 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑑 ∈ ℤ) → ((𝑑 · ((od‘𝐺)‘𝑦)) ↑ 𝑦) = (0g‘𝐺))
118	101, 117	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) ∧ 𝑑 ∈ ℤ) → ((𝑑 · ((od‘𝐺)‘𝑦)) ↑ 𝑦) = (0g‘𝐺))
119	96, 118	eqtrd 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) ∧ 𝑑 ∈ ℤ) → ((𝑑 · 𝑙) ↑ 𝑦) = (0g‘𝐺))
120	119	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) ∧ 𝑑 ∈ ℤ) ∧ (𝑑 · 𝑙) = 𝑁) → ((𝑑 · 𝑙) ↑ 𝑦) = (0g‘𝐺))
121	92, 120	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) ∧ 𝑑 ∈ ℤ) ∧ (𝑑 · 𝑙) = 𝑁) → (𝑁 ↑ 𝑦) = (0g‘𝐺))
122		nfv 1949	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑑(𝑐 · 𝑙) = 𝑁
123		nfv 1949	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑐(𝑑 · 𝑙) = 𝑁
124		oveq1 7453	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑑 → (𝑐 · 𝑙) = (𝑑 · 𝑙))
125	124	eqeq1d 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑑 → ((𝑐 · 𝑙) = 𝑁 ↔ (𝑑 · 𝑙) = 𝑁))
126	122, 123, 125	cbvrexw 3309	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁 ↔ ∃𝑑 ∈ ℤ (𝑑 · 𝑙) = 𝑁)
127	126	bilani 510	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) → ∃𝑑 ∈ ℤ (𝑑 · 𝑙) = 𝑁)
128	127	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) → ∃𝑑 ∈ ℤ (𝑑 · 𝑙) = 𝑁)
129	121, 128	r19.29a 3174	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ∃𝑐 ∈ ℤ (𝑐 · 𝑙) = 𝑁) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) → (𝑁 ↑ 𝑦) = (0g‘𝐺))
130	89, 129	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑙 ∈ (1...𝑁) ∧ 𝑙 ∥ 𝑁)) ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = 𝑙)) → (𝑁 ↑ 𝑦) = (0g‘𝐺))
131	75, 130	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}) → (𝑁 ↑ 𝑦) = (0g‘𝐺))
132	2, 65, 131	elrabd 3650	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}) → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)})
133	63, 132	syl 18	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ∃𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∧ 𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}) → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)})
134		nfv 1949	. . . . . . . . . . . 12 ⊢ Ⅎ𝑙 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}
135		nfv 1949	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}
136		eqeq2 2775	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘𝑥) = 𝑙))
137	136	rabbidv 3423	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙})
138	137	eleq2d 2850	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑙 → (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ↔ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙}))
139	134, 135, 138	cbvrexw 3309	. . . . . . . . . . 11 ⊢ (∃𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ↔ ∃𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙})
140	139	bilani 510	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∃𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) → ∃𝑙 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑙})
141	133, 140	r19.29a 3174	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)})
142	141	ex 418	. . . . . . . 8 ⊢ (𝜑 → (∃𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)}))
143	142	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) → (∃𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)}))
144	58, 143	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)})
145	144	ex 418	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ ∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)}))
146	56, 145	impbid 215	. . . 4 ⊢ (𝜑 → (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)} ↔ 𝑦 ∈ ∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
147	146	eqrdv 2761	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)} = ∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
148	147	fveq2d 6915	. 2 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)}) = (♯‘∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
149		fzfid 14146	. . . 4 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
150		ssrab2 4008	. . . . 5 ⊢ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} ⊆ (1...𝑁)
151	150	a1i 11	. . . 4 ⊢ (𝜑 → {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} ⊆ (1...𝑁))
152	149, 151	ssfid 9291	. . 3 ⊢ (𝜑 → {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} ∈ Fin)
153	32	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) → 𝐵 ∈ Fin)
154		ssrab2 4008	. . . . 5 ⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵
155	154	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
156	153, 155	ssfid 9291	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
157		animorrl 996	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑖 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑘 = 𝑖) → (𝑘 = 𝑖 ∨ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∩ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑖}) = ∅))
158		inrab 4264	. . . . . . . . . . 11 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∩ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑖}) = {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝑥) = 𝑘 ∧ ((od‘𝐺)‘𝑥) = 𝑖)}
159	158	a1i 11	. . . . . . . . . 10 ⊢ (¬ 𝑘 = 𝑖 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∩ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑖}) = {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝑥) = 𝑘 ∧ ((od‘𝐺)‘𝑥) = 𝑖)})
160		rabn0 4342	. . . . . . . . . . . . 13 ⊢ ({𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝑥) = 𝑘 ∧ ((od‘𝐺)‘𝑥) = 𝑖)} ≠ ∅ ↔ ∃𝑥 ∈ 𝐵 (((od‘𝐺)‘𝑥) = 𝑘 ∧ ((od‘𝐺)‘𝑥) = 𝑖))
161	160	biimpi 219	. . . . . . . . . . . 12 ⊢ ({𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝑥) = 𝑘 ∧ ((od‘𝐺)‘𝑥) = 𝑖)} ≠ ∅ → ∃𝑥 ∈ 𝐵 (((od‘𝐺)‘𝑥) = 𝑘 ∧ ((od‘𝐺)‘𝑥) = 𝑖))
162		eqtr2 2784	. . . . . . . . . . . . . 14 ⊢ ((((od‘𝐺)‘𝑤) = 𝑘 ∧ ((od‘𝐺)‘𝑤) = 𝑖) → 𝑘 = 𝑖)
163	162	adantl 487	. . . . . . . . . . . . 13 ⊢ (((∃𝑥 ∈ 𝐵 (((od‘𝐺)‘𝑥) = 𝑘 ∧ ((od‘𝐺)‘𝑥) = 𝑖) ∧ 𝑤 ∈ 𝐵) ∧ (((od‘𝐺)‘𝑤) = 𝑘 ∧ ((od‘𝐺)‘𝑤) = 𝑖)) → 𝑘 = 𝑖)
164		nfv 1949	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑤(((od‘𝐺)‘𝑥) = 𝑘 ∧ ((od‘𝐺)‘𝑥) = 𝑖)
165		nfv 1949	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(((od‘𝐺)‘𝑤) = 𝑘 ∧ ((od‘𝐺)‘𝑤) = 𝑖)
166		fveqeq2 6920	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘𝑤) = 𝑘))
167		fveqeq2 6920	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (((od‘𝐺)‘𝑥) = 𝑖 ↔ ((od‘𝐺)‘𝑤) = 𝑖))
168	166, 167	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → ((((od‘𝐺)‘𝑥) = 𝑘 ∧ ((od‘𝐺)‘𝑥) = 𝑖) ↔ (((od‘𝐺)‘𝑤) = 𝑘 ∧ ((od‘𝐺)‘𝑤) = 𝑖)))
169	164, 165, 168	cbvrexw 3309	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ 𝐵 (((od‘𝐺)‘𝑥) = 𝑘 ∧ ((od‘𝐺)‘𝑥) = 𝑖) ↔ ∃𝑤 ∈ 𝐵 (((od‘𝐺)‘𝑤) = 𝑘 ∧ ((od‘𝐺)‘𝑤) = 𝑖))
170	169	biimpi 219	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ 𝐵 (((od‘𝐺)‘𝑥) = 𝑘 ∧ ((od‘𝐺)‘𝑥) = 𝑖) → ∃𝑤 ∈ 𝐵 (((od‘𝐺)‘𝑤) = 𝑘 ∧ ((od‘𝐺)‘𝑤) = 𝑖))
171	163, 170	r19.29a 3174	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ 𝐵 (((od‘𝐺)‘𝑥) = 𝑘 ∧ ((od‘𝐺)‘𝑥) = 𝑖) → 𝑘 = 𝑖)
172	161, 171	syl 18	. . . . . . . . . . 11 ⊢ ({𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝑥) = 𝑘 ∧ ((od‘𝐺)‘𝑥) = 𝑖)} ≠ ∅ → 𝑘 = 𝑖)
173	172	necon1bi 2987	. . . . . . . . . 10 ⊢ (¬ 𝑘 = 𝑖 → {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝑥) = 𝑘 ∧ ((od‘𝐺)‘𝑥) = 𝑖)} = ∅)
174	159, 173	eqtrd 2798	. . . . . . . . 9 ⊢ (¬ 𝑘 = 𝑖 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∩ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑖}) = ∅)
175	174	adantl 487	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑖 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ ¬ 𝑘 = 𝑖) → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∩ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑖}) = ∅)
176	175	olcd 888	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑖 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ ¬ 𝑘 = 𝑖) → (𝑘 = 𝑖 ∨ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∩ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑖}) = ∅))
177	157, 176	pm2.61dan 825	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) ∧ 𝑖 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) → (𝑘 = 𝑖 ∨ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∩ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑖}) = ∅))
178	177	ralrimiva 3158	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}) → ∀𝑖 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} (𝑘 = 𝑖 ∨ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∩ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑖}) = ∅))
179	178	ralrimiva 3158	. . . 4 ⊢ (𝜑 → ∀𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}∀𝑖 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} (𝑘 = 𝑖 ∨ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∩ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑖}) = ∅))
180		eqeq2 2775	. . . . . 6 ⊢ (𝑘 = 𝑖 → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘𝑥) = 𝑖))
181	180	rabbidv 3423	. . . . 5 ⊢ (𝑘 = 𝑖 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑖})
182	181	disjor 5088	. . . 4 ⊢ (Disj 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ↔ ∀𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁}∀𝑖 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} (𝑘 = 𝑖 ∨ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∩ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑖}) = ∅))
183	179, 182	sylibr 237	. . 3 ⊢ (𝜑 → Disj 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
184	152, 156, 183	hashiun 16021	. 2 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
185	148, 184	eqtr2d 2799	1 ⊢ (𝜑 → Σ𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)}))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  {crab 3416   ⊆ wss 3900   ∩ cin 4092  ∅c0 4281  ∪ ciun 4954  Disj wdisj 5073   class class class wbr 5106  ‘cfv 6561  (class class class)co 7446  Fincfn 9004  1c1 11231   · cmul 11235   ≤ cle 11374  ℕcn 12365  ℕ₀cn0 12636  ℤcz 12723  ...cfz 13669  ♯chash 14504  Σcsu 15885   ∥ cdvds 16454  Basecbs 17419  0_gc0g 17642  Mndcmnd 18955  Grpcgrp 19176  ._gcmg 19309  odcod 19771

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5236  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-inf2 9672  ax-cnex 11286  ax-resscn 11287  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-addrcl 11291  ax-mulcl 11292  ax-mulrcl 11293  ax-mulcom 11294  ax-addass 11295  ax-mulass 11296  ax-distr 11297  ax-i2m1 11298  ax-1ne0 11299  ax-1rid 11300  ax-rnegex 11301  ax-rrecex 11302  ax-cnre 11303  ax-pre-lttri 11304  ax-pre-lttrn 11305  ax-pre-ltadd 11306  ax-pre-mulgt0 11307  ax-pre-sup 11308

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-disj 5074  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-se 5610  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6325  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7403  df-ov 7449  df-oprab 7450  df-mpo 7451  df-om 7905  df-1st 8028  df-2nd 8029  df-frecs 8330  df-wrecs 8361  df-recs 8410  df-rdg 8449  df-1o 8507  df-oadd 8511  df-omul 8512  df-er 8748  df-map 8880  df-en 9005  df-dom 9006  df-sdom 9007  df-fin 9008  df-sup 9464  df-inf 9465  df-oi 9534  df-card 10050  df-acn 10053  df-pnf 11375  df-mnf 11376  df-xr 11377  df-ltxr 11378  df-le 11379  df-sub 11573  df-neg 11574  df-div 12004  df-nn 12366  df-2 12435  df-3 12436  df-n0 12637  df-z 12724  df-uz 12996  df-rp 13151  df-fz 13670  df-fzo 13819  df-fl 13962  df-mod 14040  df-seq 14175  df-exp 14235  df-hash 14505  df-cj 15298  df-re 15299  df-im 15300  df-sqrt 15434  df-abs 15435  df-clim 15687  df-sum 15886  df-dvds 16455  df-0g 17644  df-mgm 18848  df-sgrp 18940  df-mnd 18956  df-grp 19179  df-minusg 19180  df-sbg 19181  df-mulg 19310  df-od 19775

This theorem is used by:  unitscyglem2  43449  unitscyglem4  43451