grpods

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

	Ref	Expression
Hypotheses	grpods.1	$⊢ B = {Base}_{G}$
	grpods.2	$⊢ \underset{˙}{\times} = \cdot_{G}$
	grpods.3	$⊢ φ \to G \in Grp$
	grpods.4	$⊢ φ \to B \in Fin$
	grpods.5	$⊢ φ \to N \in ℕ$
Assertion	grpods	$⊢ φ \to \sum_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \|\{x \in B \| od (G) (x) = k\}\| = \|\{x \in B \| N \underset{˙}{\times} x = 0_{G}\}\|$

Proof

Step	Hyp	Ref	Expression
1		grpods.1	$⊢ B = {Base}_{G}$
2		grpods.2	$⊢ \underset{˙}{\times} = \cdot_{G}$
3		grpods.3	$⊢ φ \to G \in Grp$
4		grpods.4	$⊢ φ \to B \in Fin$
5		grpods.5	$⊢ φ \to N \in ℕ$
6		oveq2	$⊢ x = y \to N \underset{˙}{\times} x = N \underset{˙}{\times} y$
7	6	eqeq1d	$⊢ x = y \to (N \underset{˙}{\times} x = 0_{G} \leftrightarrow N \underset{˙}{\times} y = 0_{G})$
8	7	elrab	$⊢ y \in \{x \in B \| N \underset{˙}{\times} x = 0_{G}\} \leftrightarrow (y \in B \land N \underset{˙}{\times} y = 0_{G})$
9	8	biimpi	$⊢ y \in \{x \in B \| N \underset{˙}{\times} x = 0_{G}\} \to (y \in B \land N \underset{˙}{\times} y = 0_{G})$
10	9	adantl	$⊢ (φ \land y \in \{x \in B \| N \underset{˙}{\times} x = 0_{G}\}) \to (y \in B \land N \underset{˙}{\times} y = 0_{G})$
11		simpl	$⊢ (φ \land (y \in B \land N \underset{˙}{\times} y = 0_{G})) \to φ$
12		simprl	$⊢ (φ \land (y \in B \land N \underset{˙}{\times} y = 0_{G})) \to y \in B$
13	11 12	jca	$⊢ (φ \land (y \in B \land N \underset{˙}{\times} y = 0_{G})) \to (φ \land y \in B)$
14		simprr	$⊢ (φ \land (y \in B \land N \underset{˙}{\times} y = 0_{G})) \to N \underset{˙}{\times} y = 0_{G}$
15	11 3	syl	$⊢ (φ \land (y \in B \land N \underset{˙}{\times} y = 0_{G})) \to G \in Grp$
16		grpmnd	$⊢ G \in Grp \to G \in Mnd$
17	15 16	syl	$⊢ (φ \land (y \in B \land N \underset{˙}{\times} y = 0_{G})) \to G \in Mnd$
18	11 5	syl	$⊢ (φ \land (y \in B \land N \underset{˙}{\times} y = 0_{G})) \to N \in ℕ$
19	18	nnnn0d	$⊢ (φ \land (y \in B \land N \underset{˙}{\times} y = 0_{G})) \to N \in ℕ_{0}$
20		eqid	$⊢ od (G) = od (G)$
21		eqid	$⊢ 0_{G} = 0_{G}$
22	1 20 2 21	oddvdsnn0	$⊢ (G \in Mnd \land y \in B \land N \in ℕ_{0}) \to (od (G) (y) ∥ N \leftrightarrow N \underset{˙}{\times} y = 0_{G})$
23	17 12 19 22	syl3anc	$⊢ (φ \land (y \in B \land N \underset{˙}{\times} y = 0_{G})) \to (od (G) (y) ∥ N \leftrightarrow N \underset{˙}{\times} y = 0_{G})$
24	14 23	mpbird	$⊢ (φ \land (y \in B \land N \underset{˙}{\times} y = 0_{G})) \to od (G) (y) ∥ N$
25	13 24	jca	$⊢ (φ \land (y \in B \land N \underset{˙}{\times} y = 0_{G})) \to ((φ \land y \in B) \land od (G) (y) ∥ N)$
26		breq1	$⊢ m = od (G) (y) \to (m ∥ N \leftrightarrow od (G) (y) ∥ N)$
27		1zzd	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to 1 \in ℤ$
28	5	ad2antrr	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to N \in ℕ$
29	28	nnzd	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to N \in ℤ$
30		dvdszrcl	$⊢ od (G) (y) ∥ N \to (od (G) (y) \in ℤ \land N \in ℤ)$
31	30	simpld	$⊢ od (G) (y) ∥ N \to od (G) (y) \in ℤ$
32	31	adantl	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to od (G) (y) \in ℤ$
33	3	ad2antrr	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to G \in Grp$
34	4	ad2antrr	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to B \in Fin$
35		simplr	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to y \in B$
36	1 20	odcl2	$⊢ (G \in Grp \land B \in Fin \land y \in B) \to od (G) (y) \in ℕ$
37	33 34 35 36	syl3anc	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to od (G) (y) \in ℕ$
38	37	nnge1d	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to 1 \leq od (G) (y)$
39	32 28	jca	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to (od (G) (y) \in ℤ \land N \in ℕ)$
40		simpr	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to od (G) (y) ∥ N$
41		dvdsle	$⊢ (od (G) (y) \in ℤ \land N \in ℕ) \to (od (G) (y) ∥ N \to od (G) (y) \leq N)$
42	41	imp	$⊢ ((od (G) (y) \in ℤ \land N \in ℕ) \land od (G) (y) ∥ N) \to od (G) (y) \leq N$
43	39 40 42	syl2anc	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to od (G) (y) \leq N$
44	27 29 32 38 43	elfzd	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to od (G) (y) \in (1 \dots N)$
45	26 44 40	elrabd	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to od (G) (y) \in \{m \in (1 \dots N) \| m ∥ N\}$
46		fveqeq2	$⊢ x = y \to (od (G) (x) = od (G) (y) \leftrightarrow od (G) (y) = od (G) (y))$
47		eqidd	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to od (G) (y) = od (G) (y)$
48	46 35 47	elrabd	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to y \in \{x \in B \| od (G) (x) = od (G) (y)\}$
49		eqeq2	$⊢ k = od (G) (y) \to (od (G) (x) = k \leftrightarrow od (G) (x) = od (G) (y))$
50	49	rabbidv	$⊢ k = od (G) (y) \to \{x \in B \| od (G) (x) = k\} = \{x \in B \| od (G) (x) = od (G) (y)\}$
51	50	eliuni	$⊢ (od (G) (y) \in \{m \in (1 \dots N) \| m ∥ N\} \land y \in \{x \in B \| od (G) (x) = od (G) (y)\}) \to y \in ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\}$
52	45 48 51	syl2anc	$⊢ ((φ \land y \in B) \land od (G) (y) ∥ N) \to y \in ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\}$
53	25 52	syl	$⊢ (φ \land (y \in B \land N \underset{˙}{\times} y = 0_{G})) \to y \in ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\}$
54	53	ex	$⊢ φ \to ((y \in B \land N \underset{˙}{\times} y = 0_{G}) \to y \in ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\})$
55	54	adantr	$⊢ (φ \land y \in \{x \in B \| N \underset{˙}{\times} x = 0_{G}\}) \to ((y \in B \land N \underset{˙}{\times} y = 0_{G}) \to y \in ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\})$
56	10 55	mpd	$⊢ (φ \land y \in \{x \in B \| N \underset{˙}{\times} x = 0_{G}\}) \to y \in ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\}$
57	56	ex	$⊢ φ \to (y \in \{x \in B \| N \underset{˙}{\times} x = 0_{G}\} \to y \in ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\})$
58		eliun	$⊢ y \in ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\} \leftrightarrow \exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\}$
59	58	biimpi	$⊢ y \in ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\} \to \exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\}$
60	59	adantl	$⊢ (φ \land y \in ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\}) \to \exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\}$
61		simplll	$⊢ (((φ \land \exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\}) \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\}) \to φ$
62		simplr	$⊢ (((φ \land \exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\}) \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\}) \to l \in \{m \in (1 \dots N) \| m ∥ N\}$
63	61 62	jca	$⊢ (((φ \land \exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\}) \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\}) \to (φ \land l \in \{m \in (1 \dots N) \| m ∥ N\})$
64		simpr	$⊢ (((φ \land \exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\}) \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\}) \to y \in \{x \in B \| od (G) (x) = l\}$
65	63 64	jca	$⊢ (((φ \land \exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\}) \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\}) \to ((φ \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\})$
66		elrabi	$⊢ y \in \{x \in B \| od (G) (x) = l\} \to y \in B$
67	66	adantl	$⊢ ((φ \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\}) \to y \in B$
68		simpll	$⊢ ((φ \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\}) \to φ$
69		breq1	$⊢ m = l \to (m ∥ N \leftrightarrow l ∥ N)$
70	69	elrab	$⊢ l \in \{m \in (1 \dots N) \| m ∥ N\} \leftrightarrow (l \in (1 \dots N) \land l ∥ N)$
71	70	biimpi	$⊢ l \in \{m \in (1 \dots N) \| m ∥ N\} \to (l \in (1 \dots N) \land l ∥ N)$
72	71	adantl	$⊢ (φ \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \to (l \in (1 \dots N) \land l ∥ N)$
73	72	adantr	$⊢ ((φ \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\}) \to (l \in (1 \dots N) \land l ∥ N)$
74	68 73	jca	$⊢ ((φ \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\}) \to (φ \land (l \in (1 \dots N) \land l ∥ N))$
75		fveqeq2	$⊢ x = y \to (od (G) (x) = l \leftrightarrow od (G) (y) = l)$
76	75	elrab	$⊢ y \in \{x \in B \| od (G) (x) = l\} \leftrightarrow (y \in B \land od (G) (y) = l)$
77	76	biimpi	$⊢ y \in \{x \in B \| od (G) (x) = l\} \to (y \in B \land od (G) (y) = l)$
78	77	adantl	$⊢ ((φ \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\}) \to (y \in B \land od (G) (y) = l)$
79	74 78	jca	$⊢ ((φ \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\}) \to ((φ \land (l \in (1 \dots N) \land l ∥ N)) \land (y \in B \land od (G) (y) = l))$
80		simpll	$⊢ ((φ \land (l \in (1 \dots N) \land l ∥ N)) \land (y \in B \land od (G) (y) = l)) \to φ$
81		simprr	$⊢ (φ \land (l \in (1 \dots N) \land l ∥ N)) \to l ∥ N$
82		elfzelz	$⊢ l \in (1 \dots N) \to l \in ℤ$
83	82	adantr	$⊢ (l \in (1 \dots N) \land l ∥ N) \to l \in ℤ$
84	83	adantl	$⊢ (φ \land (l \in (1 \dots N) \land l ∥ N)) \to l \in ℤ$
85	5	adantr	$⊢ (φ \land (l \in (1 \dots N) \land l ∥ N)) \to N \in ℕ$
86	85	nnzd	$⊢ (φ \land (l \in (1 \dots N) \land l ∥ N)) \to N \in ℤ$
87		divides	$⊢ (l \in ℤ \land N \in ℤ) \to (l ∥ N \leftrightarrow \exists c \in ℤ c l = N)$
88	84 86 87	syl2anc	$⊢ (φ \land (l \in (1 \dots N) \land l ∥ N)) \to (l ∥ N \leftrightarrow \exists c \in ℤ c l = N)$
89	81 88	mpbid	$⊢ (φ \land (l \in (1 \dots N) \land l ∥ N)) \to \exists c \in ℤ c l = N$
90	89	adantr	$⊢ ((φ \land (l \in (1 \dots N) \land l ∥ N)) \land (y \in B \land od (G) (y) = l)) \to \exists c \in ℤ c l = N$
91	80 90	jca	$⊢ ((φ \land (l \in (1 \dots N) \land l ∥ N)) \land (y \in B \land od (G) (y) = l)) \to (φ \land \exists c \in ℤ c l = N)$
92		simpr	$⊢ ((φ \land (l \in (1 \dots N) \land l ∥ N)) \land (y \in B \land od (G) (y) = l)) \to (y \in B \land od (G) (y) = l)$
93	91 92	jca	$⊢ ((φ \land (l \in (1 \dots N) \land l ∥ N)) \land (y \in B \land od (G) (y) = l)) \to ((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l))$
94		oveq1	$⊢ d l = N \to d l \underset{˙}{\times} y = N \underset{˙}{\times} y$
95	94	eqcomd	$⊢ d l = N \to N \underset{˙}{\times} y = d l \underset{˙}{\times} y$
96	95	adantl	$⊢ ((((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \land d \in ℤ) \land d l = N) \to N \underset{˙}{\times} y = d l \underset{˙}{\times} y$
97		simplrr	$⊢ (((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \land d \in ℤ) \to od (G) (y) = l$
98	97	oveq2d	$⊢ (((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \land d \in ℤ) \to d od (G) (y) = d l$
99	98	eqcomd	$⊢ (((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \land d \in ℤ) \to d l = d od (G) (y)$
100	99	oveq1d	$⊢ (((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \land d \in ℤ) \to d l \underset{˙}{\times} y = d od (G) (y) \underset{˙}{\times} y$
101		simplll	$⊢ (((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \land d \in ℤ) \to φ$
102		simplrl	$⊢ (((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \land d \in ℤ) \to y \in B$
103	101 102	jca	$⊢ (((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \land d \in ℤ) \to (φ \land y \in B)$
104		simpr	$⊢ (((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \land d \in ℤ) \to d \in ℤ$
105	103 104	jca	$⊢ (((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \land d \in ℤ) \to ((φ \land y \in B) \land d \in ℤ)$
106	3	ad2antrr	$⊢ ((φ \land y \in B) \land d \in ℤ) \to G \in Grp$
107		simpr	$⊢ ((φ \land y \in B) \land d \in ℤ) \to d \in ℤ$
108	1 20	odcl	$⊢ y \in B \to od (G) (y) \in ℕ_{0}$
109	108	ad2antlr	$⊢ ((φ \land y \in B) \land d \in ℤ) \to od (G) (y) \in ℕ_{0}$
110	109	nn0zd	$⊢ ((φ \land y \in B) \land d \in ℤ) \to od (G) (y) \in ℤ$
111		simplr	$⊢ ((φ \land y \in B) \land d \in ℤ) \to y \in B$
112	107 110 111	3jca	$⊢ ((φ \land y \in B) \land d \in ℤ) \to (d \in ℤ \land od (G) (y) \in ℤ \land y \in B)$
113	1 2	mulgass	$⊢ (G \in Grp \land (d \in ℤ \land od (G) (y) \in ℤ \land y \in B)) \to d od (G) (y) \underset{˙}{\times} y = d \underset{˙}{\times} (od (G) (y) \underset{˙}{\times} y)$
114	106 112 113	syl2anc	$⊢ ((φ \land y \in B) \land d \in ℤ) \to d od (G) (y) \underset{˙}{\times} y = d \underset{˙}{\times} (od (G) (y) \underset{˙}{\times} y)$
115	1 20 2 21	odid	$⊢ y \in B \to od (G) (y) \underset{˙}{\times} y = 0_{G}$
116	111 115	syl	$⊢ ((φ \land y \in B) \land d \in ℤ) \to od (G) (y) \underset{˙}{\times} y = 0_{G}$
117	116	oveq2d	$⊢ ((φ \land y \in B) \land d \in ℤ) \to d \underset{˙}{\times} (od (G) (y) \underset{˙}{\times} y) = d \underset{˙}{\times} 0_{G}$
118	1 2 21	mulgz	$⊢ (G \in Grp \land d \in ℤ) \to d \underset{˙}{\times} 0_{G} = 0_{G}$
119	106 107 118	syl2anc	$⊢ ((φ \land y \in B) \land d \in ℤ) \to d \underset{˙}{\times} 0_{G} = 0_{G}$
120	117 119	eqtrd	$⊢ ((φ \land y \in B) \land d \in ℤ) \to d \underset{˙}{\times} (od (G) (y) \underset{˙}{\times} y) = 0_{G}$
121	114 120	eqtrd	$⊢ ((φ \land y \in B) \land d \in ℤ) \to d od (G) (y) \underset{˙}{\times} y = 0_{G}$
122	105 121	syl	$⊢ (((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \land d \in ℤ) \to d od (G) (y) \underset{˙}{\times} y = 0_{G}$
123	100 122	eqtrd	$⊢ (((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \land d \in ℤ) \to d l \underset{˙}{\times} y = 0_{G}$
124	123	adantr	$⊢ ((((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \land d \in ℤ) \land d l = N) \to d l \underset{˙}{\times} y = 0_{G}$
125	96 124	eqtrd	$⊢ ((((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \land d \in ℤ) \land d l = N) \to N \underset{˙}{\times} y = 0_{G}$
126		nfv	$⊢ Ⅎ d c l = N$
127		nfv	$⊢ Ⅎ c d l = N$
128		oveq1	$⊢ c = d \to c l = d l$
129	128	eqeq1d	$⊢ c = d \to (c l = N \leftrightarrow d l = N)$
130	126 127 129	cbvrexw	$⊢ \exists c \in ℤ c l = N \leftrightarrow \exists d \in ℤ d l = N$
131	130	biimpi	$⊢ \exists c \in ℤ c l = N \to \exists d \in ℤ d l = N$
132	131	adantl	$⊢ (φ \land \exists c \in ℤ c l = N) \to \exists d \in ℤ d l = N$
133	132	adantr	$⊢ ((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \to \exists d \in ℤ d l = N$
134	125 133	r19.29a	$⊢ ((φ \land \exists c \in ℤ c l = N) \land (y \in B \land od (G) (y) = l)) \to N \underset{˙}{\times} y = 0_{G}$
135	93 134	syl	$⊢ ((φ \land (l \in (1 \dots N) \land l ∥ N)) \land (y \in B \land od (G) (y) = l)) \to N \underset{˙}{\times} y = 0_{G}$
136	79 135	syl	$⊢ ((φ \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\}) \to N \underset{˙}{\times} y = 0_{G}$
137	7 67 136	elrabd	$⊢ ((φ \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\}) \to y \in \{x \in B \| N \underset{˙}{\times} x = 0_{G}\}$
138	65 137	syl	$⊢ (((φ \land \exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\}) \land l \in \{m \in (1 \dots N) \| m ∥ N\}) \land y \in \{x \in B \| od (G) (x) = l\}) \to y \in \{x \in B \| N \underset{˙}{\times} x = 0_{G}\}$
139		nfv	$⊢ Ⅎ l y \in \{x \in B \| od (G) (x) = k\}$
140		nfv	$⊢ Ⅎ k y \in \{x \in B \| od (G) (x) = l\}$
141		eqeq2	$⊢ k = l \to (od (G) (x) = k \leftrightarrow od (G) (x) = l)$
142	141	rabbidv	$⊢ k = l \to \{x \in B \| od (G) (x) = k\} = \{x \in B \| od (G) (x) = l\}$
143	142	eleq2d	$⊢ k = l \to (y \in \{x \in B \| od (G) (x) = k\} \leftrightarrow y \in \{x \in B \| od (G) (x) = l\})$
144	139 140 143	cbvrexw	$⊢ \exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\} \leftrightarrow \exists l \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = l\}$
145	144	biimpi	$⊢ \exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\} \to \exists l \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = l\}$
146	145	adantl	$⊢ (φ \land \exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\}) \to \exists l \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = l\}$
147	138 146	r19.29a	$⊢ (φ \land \exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\}) \to y \in \{x \in B \| N \underset{˙}{\times} x = 0_{G}\}$
148	147	ex	$⊢ φ \to (\exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\} \to y \in \{x \in B \| N \underset{˙}{\times} x = 0_{G}\})$
149	148	adantr	$⊢ (φ \land y \in ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\}) \to (\exists k \in \{m \in (1 \dots N) \| m ∥ N\} y \in \{x \in B \| od (G) (x) = k\} \to y \in \{x \in B \| N \underset{˙}{\times} x = 0_{G}\})$
150	60 149	mpd	$⊢ (φ \land y \in ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\}) \to y \in \{x \in B \| N \underset{˙}{\times} x = 0_{G}\}$
151	150	ex	$⊢ φ \to (y \in ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\} \to y \in \{x \in B \| N \underset{˙}{\times} x = 0_{G}\})$
152	57 151	impbid	$⊢ φ \to (y \in \{x \in B \| N \underset{˙}{\times} x = 0_{G}\} \leftrightarrow y \in ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\})$
153	152	eqrdv	$⊢ φ \to \{x \in B \| N \underset{˙}{\times} x = 0_{G}\} = ⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\}$
154	153	fveq2d	$⊢ φ \to \|\{x \in B \| N \underset{˙}{\times} x = 0_{G}\}\| = \|⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\}\|$
155		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
156		ssrab2	$⊢ \{m \in (1 \dots N) \| m ∥ N\} \subseteq (1 \dots N)$
157	156	a1i	$⊢ φ \to \{m \in (1 \dots N) \| m ∥ N\} \subseteq (1 \dots N)$
158	155 157	ssfid	$⊢ φ \to \{m \in (1 \dots N) \| m ∥ N\} \in Fin$
159	4	adantr	$⊢ (φ \land k \in \{m \in (1 \dots N) \| m ∥ N\}) \to B \in Fin$
160		ssrab2	$⊢ \{x \in B \| od (G) (x) = k\} \subseteq B$
161	160	a1i	$⊢ (φ \land k \in \{m \in (1 \dots N) \| m ∥ N\}) \to \{x \in B \| od (G) (x) = k\} \subseteq B$
162	159 161	ssfid	$⊢ (φ \land k \in \{m \in (1 \dots N) \| m ∥ N\}) \to \{x \in B \| od (G) (x) = k\} \in Fin$
163		animorrl	$⊢ (((φ \land k \in \{m \in (1 \dots N) \| m ∥ N\}) \land i \in \{m \in (1 \dots N) \| m ∥ N\}) \land k = i) \to (k = i \lor \{x \in B \| od (G) (x) = k\} \cap \{x \in B \| od (G) (x) = i\} = \emptyset)$
164		inrab	$⊢ \{x \in B \| od (G) (x) = k\} \cap \{x \in B \| od (G) (x) = i\} = \{x \in B \| (od (G) (x) = k \land od (G) (x) = i)\}$
165	164	a1i	$⊢ \neg k = i \to \{x \in B \| od (G) (x) = k\} \cap \{x \in B \| od (G) (x) = i\} = \{x \in B \| (od (G) (x) = k \land od (G) (x) = i)\}$
166		rabn0	$⊢ \{x \in B \| (od (G) (x) = k \land od (G) (x) = i)\} \neq \emptyset \leftrightarrow \exists x \in B (od (G) (x) = k \land od (G) (x) = i)$
167	166	biimpi	$⊢ \{x \in B \| (od (G) (x) = k \land od (G) (x) = i)\} \neq \emptyset \to \exists x \in B (od (G) (x) = k \land od (G) (x) = i)$
168		eqtr2	$⊢ (od (G) (w) = k \land od (G) (w) = i) \to k = i$
169	168	adantl	$⊢ ((\exists x \in B (od (G) (x) = k \land od (G) (x) = i) \land w \in B) \land (od (G) (w) = k \land od (G) (w) = i)) \to k = i$
170		nfv	$⊢ Ⅎ w (od (G) (x) = k \land od (G) (x) = i)$
171		nfv	$⊢ Ⅎ x (od (G) (w) = k \land od (G) (w) = i)$
172		fveqeq2	$⊢ x = w \to (od (G) (x) = k \leftrightarrow od (G) (w) = k)$
173		fveqeq2	$⊢ x = w \to (od (G) (x) = i \leftrightarrow od (G) (w) = i)$
174	172 173	anbi12d	$⊢ x = w \to ((od (G) (x) = k \land od (G) (x) = i) \leftrightarrow (od (G) (w) = k \land od (G) (w) = i))$
175	170 171 174	cbvrexw	$⊢ \exists x \in B (od (G) (x) = k \land od (G) (x) = i) \leftrightarrow \exists w \in B (od (G) (w) = k \land od (G) (w) = i)$
176	175	biimpi	$⊢ \exists x \in B (od (G) (x) = k \land od (G) (x) = i) \to \exists w \in B (od (G) (w) = k \land od (G) (w) = i)$
177	169 176	r19.29a	$⊢ \exists x \in B (od (G) (x) = k \land od (G) (x) = i) \to k = i$
178	167 177	syl	$⊢ \{x \in B \| (od (G) (x) = k \land od (G) (x) = i)\} \neq \emptyset \to k = i$
179	178	necon1bi	$⊢ \neg k = i \to \{x \in B \| (od (G) (x) = k \land od (G) (x) = i)\} = \emptyset$
180	165 179	eqtrd	$⊢ \neg k = i \to \{x \in B \| od (G) (x) = k\} \cap \{x \in B \| od (G) (x) = i\} = \emptyset$
181	180	adantl	$⊢ (((φ \land k \in \{m \in (1 \dots N) \| m ∥ N\}) \land i \in \{m \in (1 \dots N) \| m ∥ N\}) \land \neg k = i) \to \{x \in B \| od (G) (x) = k\} \cap \{x \in B \| od (G) (x) = i\} = \emptyset$
182	181	olcd	$⊢ (((φ \land k \in \{m \in (1 \dots N) \| m ∥ N\}) \land i \in \{m \in (1 \dots N) \| m ∥ N\}) \land \neg k = i) \to (k = i \lor \{x \in B \| od (G) (x) = k\} \cap \{x \in B \| od (G) (x) = i\} = \emptyset)$
183	163 182	pm2.61dan	$⊢ ((φ \land k \in \{m \in (1 \dots N) \| m ∥ N\}) \land i \in \{m \in (1 \dots N) \| m ∥ N\}) \to (k = i \lor \{x \in B \| od (G) (x) = k\} \cap \{x \in B \| od (G) (x) = i\} = \emptyset)$
184	183	ralrimiva	$⊢ (φ \land k \in \{m \in (1 \dots N) \| m ∥ N\}) \to \forall i \in \{m \in (1 \dots N) \| m ∥ N\} (k = i \lor \{x \in B \| od (G) (x) = k\} \cap \{x \in B \| od (G) (x) = i\} = \emptyset)$
185	184	ralrimiva	$⊢ φ \to \forall k \in \{m \in (1 \dots N) \| m ∥ N\} \forall i \in \{m \in (1 \dots N) \| m ∥ N\} (k = i \lor \{x \in B \| od (G) (x) = k\} \cap \{x \in B \| od (G) (x) = i\} = \emptyset)$
186		eqeq2	$⊢ k = i \to (od (G) (x) = k \leftrightarrow od (G) (x) = i)$
187	186	rabbidv	$⊢ k = i \to \{x \in B \| od (G) (x) = k\} = \{x \in B \| od (G) (x) = i\}$
188	187	disjor	$⊢ \underset{k \in \{m \in (1 \dots N) \| m ∥ N\}}{Disj} \{x \in B \| od (G) (x) = k\} \leftrightarrow \forall k \in \{m \in (1 \dots N) \| m ∥ N\} \forall i \in \{m \in (1 \dots N) \| m ∥ N\} (k = i \lor \{x \in B \| od (G) (x) = k\} \cap \{x \in B \| od (G) (x) = i\} = \emptyset)$
189	185 188	sylibr	$⊢ φ \to \underset{k \in \{m \in (1 \dots N) \| m ∥ N\}}{Disj} \{x \in B \| od (G) (x) = k\}$
190	158 162 189	hashiun	$⊢ φ \to \|⋃_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \{x \in B \| od (G) (x) = k\}\| = \sum_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \|\{x \in B \| od (G) (x) = k\}\|$
191	154 190	eqtr2d	$⊢ φ \to \sum_{k \in \{m \in (1 \dots N) \| m ∥ N\}} \|\{x \in B \| od (G) (x) = k\}\| = \|\{x \in B \| N \underset{˙}{\times} x = 0_{G}\}\|$

Metamath Proof Explorer

Theorem grpods

Proof