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