unitscyglem1

	Ref	Expression
Hypotheses	unitscyglem1.1	$⊢ B = {Base}_{G}$
	unitscyglem1.2	$⊢ \underset{˙}{\times} = \cdot_{G}$
	unitscyglem1.3	$⊢ φ \to G \in Grp$
	unitscyglem1.4	$⊢ φ \to B \in Fin$
	unitscyglem1.5	$⊢ φ \to \forall n \in ℕ \|\{x \in B \| n \underset{˙}{\times} x = 0_{G}\}\| \leq n$
	unitscyglem1.6	$⊢ φ \to A \in B$
Assertion	unitscyglem1	$⊢ φ \to \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\| = od (G) (A)$

Proof

Step	Hyp	Ref	Expression
1		unitscyglem1.1	$⊢ B = {Base}_{G}$
2		unitscyglem1.2	$⊢ \underset{˙}{\times} = \cdot_{G}$
3		unitscyglem1.3	$⊢ φ \to G \in Grp$
4		unitscyglem1.4	$⊢ φ \to B \in Fin$
5		unitscyglem1.5	$⊢ φ \to \forall n \in ℕ \|\{x \in B \| n \underset{˙}{\times} x = 0_{G}\}\| \leq n$
6		unitscyglem1.6	$⊢ φ \to A \in B$
7		oveq1	$⊢ n = od (G) (A) \to n \underset{˙}{\times} x = od (G) (A) \underset{˙}{\times} x$
8	7	eqeq1d	$⊢ n = od (G) (A) \to (n \underset{˙}{\times} x = 0_{G} \leftrightarrow od (G) (A) \underset{˙}{\times} x = 0_{G})$
9	8	rabbidv	$⊢ n = od (G) (A) \to \{x \in B \| n \underset{˙}{\times} x = 0_{G}\} = \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}$
10	9	fveq2d	$⊢ n = od (G) (A) \to \|\{x \in B \| n \underset{˙}{\times} x = 0_{G}\}\| = \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\|$
11		id	$⊢ n = od (G) (A) \to n = od (G) (A)$
12	10 11	breq12d	$⊢ n = od (G) (A) \to (\|\{x \in B \| n \underset{˙}{\times} x = 0_{G}\}\| \leq n \leftrightarrow \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\| \leq od (G) (A))$
13		eqid	$⊢ od (G) = od (G)$
14	1 13	odcl2	$⊢ (G \in Grp \land B \in Fin \land A \in B) \to od (G) (A) \in ℕ$
15	3 4 6 14	syl3anc	$⊢ φ \to od (G) (A) \in ℕ$
16	12 5 15	rspcdva	$⊢ φ \to \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\| \leq od (G) (A)$
17		eqid	$⊢ (i \in ℤ ⟼ i \underset{˙}{\times} A) = (i \in ℤ ⟼ i \underset{˙}{\times} A)$
18	1 13 2 17	dfod2	$⊢ (G \in Grp \land A \in B) \to od (G) (A) = if (ran (i \in ℤ ⟼ i \underset{˙}{\times} A) \in Fin, \|ran (i \in ℤ ⟼ i \underset{˙}{\times} A)\|, 0)$
19	3 6 18	syl2anc	$⊢ φ \to od (G) (A) = if (ran (i \in ℤ ⟼ i \underset{˙}{\times} A) \in Fin, \|ran (i \in ℤ ⟼ i \underset{˙}{\times} A)\|, 0)$
20	3	adantr	$⊢ (φ \land i \in ℤ) \to G \in Grp$
21		simpr	$⊢ (φ \land i \in ℤ) \to i \in ℤ$
22	6	adantr	$⊢ (φ \land i \in ℤ) \to A \in B$
23	1 2 20 21 22	mulgcld	$⊢ (φ \land i \in ℤ) \to i \underset{˙}{\times} A \in B$
24	23	fmpttd	$⊢ φ \to (i \in ℤ ⟼ i \underset{˙}{\times} A) : ℤ ⟶ B$
25		frn	$⊢ (i \in ℤ ⟼ i \underset{˙}{\times} A) : ℤ ⟶ B \to ran (i \in ℤ ⟼ i \underset{˙}{\times} A) \subseteq B$
26	24 25	syl	$⊢ φ \to ran (i \in ℤ ⟼ i \underset{˙}{\times} A) \subseteq B$
27	4 26	ssfid	$⊢ φ \to ran (i \in ℤ ⟼ i \underset{˙}{\times} A) \in Fin$
28	27	iftrued	$⊢ φ \to if (ran (i \in ℤ ⟼ i \underset{˙}{\times} A) \in Fin, \|ran (i \in ℤ ⟼ i \underset{˙}{\times} A)\|, 0) = \|ran (i \in ℤ ⟼ i \underset{˙}{\times} A)\|$
29	19 28	eqtrd	$⊢ φ \to od (G) (A) = \|ran (i \in ℤ ⟼ i \underset{˙}{\times} A)\|$
30		eqid	$⊢ \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\} = \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}$
31		fvexd	$⊢ φ \to {Base}_{G} \in V$
32	1 31	eqeltrid	$⊢ φ \to B \in V$
33	30 32	rabexd	$⊢ φ \to \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\} \in V$
34		ovexd	$⊢ (φ \land i \in ℤ) \to i \underset{˙}{\times} A \in V$
35	34	fmpttd	$⊢ φ \to (i \in ℤ ⟼ i \underset{˙}{\times} A) : ℤ ⟶ V$
36	35	ffnd	$⊢ φ \to (i \in ℤ ⟼ i \underset{˙}{\times} A) Fn ℤ$
37		fvelrnb	$⊢ (i \in ℤ ⟼ i \underset{˙}{\times} A) Fn ℤ \to (y \in ran (i \in ℤ ⟼ i \underset{˙}{\times} A) \leftrightarrow \exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y)$
38	36 37	syl	$⊢ φ \to (y \in ran (i \in ℤ ⟼ i \underset{˙}{\times} A) \leftrightarrow \exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y)$
39	38	biimpa	$⊢ (φ \land y \in ran (i \in ℤ ⟼ i \underset{˙}{\times} A)) \to \exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y$
40		id	$⊢ (i \in ℤ ⟼ i \underset{˙}{\times} A) (w) = y \to (i \in ℤ ⟼ i \underset{˙}{\times} A) (w) = y$
41	40	eqcomd	$⊢ (i \in ℤ ⟼ i \underset{˙}{\times} A) (w) = y \to y = (i \in ℤ ⟼ i \underset{˙}{\times} A) (w)$
42	41	adantl	$⊢ (((φ \land \exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y) \land w \in ℤ) \land (i \in ℤ ⟼ i \underset{˙}{\times} A) (w) = y) \to y = (i \in ℤ ⟼ i \underset{˙}{\times} A) (w)$
43		simpll	$⊢ ((φ \land \exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y) \land w \in ℤ) \to φ$
44		simpr	$⊢ ((φ \land \exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y) \land w \in ℤ) \to w \in ℤ$
45	43 44	jca	$⊢ ((φ \land \exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y) \land w \in ℤ) \to (φ \land w \in ℤ)$
46		eqidd	$⊢ (φ \land w \in ℤ) \to (i \in ℤ ⟼ i \underset{˙}{\times} A) = (i \in ℤ ⟼ i \underset{˙}{\times} A)$
47		simpr	$⊢ ((φ \land w \in ℤ) \land i = w) \to i = w$
48	47	oveq1d	$⊢ ((φ \land w \in ℤ) \land i = w) \to i \underset{˙}{\times} A = w \underset{˙}{\times} A$
49		simpr	$⊢ (φ \land w \in ℤ) \to w \in ℤ$
50		ovexd	$⊢ (φ \land w \in ℤ) \to w \underset{˙}{\times} A \in V$
51	46 48 49 50	fvmptd	$⊢ (φ \land w \in ℤ) \to (i \in ℤ ⟼ i \underset{˙}{\times} A) (w) = w \underset{˙}{\times} A$
52		oveq2	$⊢ x = w \underset{˙}{\times} A \to od (G) (A) \underset{˙}{\times} x = od (G) (A) \underset{˙}{\times} (w \underset{˙}{\times} A)$
53	52	eqeq1d	$⊢ x = w \underset{˙}{\times} A \to (od (G) (A) \underset{˙}{\times} x = 0_{G} \leftrightarrow od (G) (A) \underset{˙}{\times} (w \underset{˙}{\times} A) = 0_{G})$
54	3	adantr	$⊢ (φ \land w \in ℤ) \to G \in Grp$
55	6	adantr	$⊢ (φ \land w \in ℤ) \to A \in B$
56	1 2 54 49 55	mulgcld	$⊢ (φ \land w \in ℤ) \to w \underset{˙}{\times} A \in B$
57	15	nnzd	$⊢ φ \to od (G) (A) \in ℤ$
58	57	adantr	$⊢ (φ \land w \in ℤ) \to od (G) (A) \in ℤ$
59	49 58 55	3jca	$⊢ (φ \land w \in ℤ) \to (w \in ℤ \land od (G) (A) \in ℤ \land A \in B)$
60	1 2	mulgass	$⊢ (G \in Grp \land (w \in ℤ \land od (G) (A) \in ℤ \land A \in B)) \to w od (G) (A) \underset{˙}{\times} A = w \underset{˙}{\times} (od (G) (A) \underset{˙}{\times} A)$
61	54 59 60	syl2anc	$⊢ (φ \land w \in ℤ) \to w od (G) (A) \underset{˙}{\times} A = w \underset{˙}{\times} (od (G) (A) \underset{˙}{\times} A)$
62		eqid	$⊢ 0_{G} = 0_{G}$
63	1 13 2 62	odid	$⊢ A \in B \to od (G) (A) \underset{˙}{\times} A = 0_{G}$
64	55 63	syl	$⊢ (φ \land w \in ℤ) \to od (G) (A) \underset{˙}{\times} A = 0_{G}$
65	64	oveq2d	$⊢ (φ \land w \in ℤ) \to w \underset{˙}{\times} (od (G) (A) \underset{˙}{\times} A) = w \underset{˙}{\times} 0_{G}$
66	1 2 62	mulgz	$⊢ (G \in Grp \land w \in ℤ) \to w \underset{˙}{\times} 0_{G} = 0_{G}$
67	3 66	sylan	$⊢ (φ \land w \in ℤ) \to w \underset{˙}{\times} 0_{G} = 0_{G}$
68	65 67	eqtrd	$⊢ (φ \land w \in ℤ) \to w \underset{˙}{\times} (od (G) (A) \underset{˙}{\times} A) = 0_{G}$
69	61 68	eqtr2d	$⊢ (φ \land w \in ℤ) \to 0_{G} = w od (G) (A) \underset{˙}{\times} A$
70	59	simp2d	$⊢ (φ \land w \in ℤ) \to od (G) (A) \in ℤ$
71	70 49 55	3jca	$⊢ (φ \land w \in ℤ) \to (od (G) (A) \in ℤ \land w \in ℤ \land A \in B)$
72	1 2	mulgassr	$⊢ (G \in Grp \land (od (G) (A) \in ℤ \land w \in ℤ \land A \in B)) \to w od (G) (A) \underset{˙}{\times} A = od (G) (A) \underset{˙}{\times} (w \underset{˙}{\times} A)$
73	54 71 72	syl2anc	$⊢ (φ \land w \in ℤ) \to w od (G) (A) \underset{˙}{\times} A = od (G) (A) \underset{˙}{\times} (w \underset{˙}{\times} A)$
74	69 73	eqtr2d	$⊢ (φ \land w \in ℤ) \to od (G) (A) \underset{˙}{\times} (w \underset{˙}{\times} A) = 0_{G}$
75	53 56 74	elrabd	$⊢ (φ \land w \in ℤ) \to w \underset{˙}{\times} A \in \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}$
76	51 75	eqeltrd	$⊢ (φ \land w \in ℤ) \to (i \in ℤ ⟼ i \underset{˙}{\times} A) (w) \in \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}$
77	45 76	syl	$⊢ ((φ \land \exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y) \land w \in ℤ) \to (i \in ℤ ⟼ i \underset{˙}{\times} A) (w) \in \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}$
78	77	adantr	$⊢ (((φ \land \exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y) \land w \in ℤ) \land (i \in ℤ ⟼ i \underset{˙}{\times} A) (w) = y) \to (i \in ℤ ⟼ i \underset{˙}{\times} A) (w) \in \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}$
79	42 78	eqeltrd	$⊢ (((φ \land \exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y) \land w \in ℤ) \land (i \in ℤ ⟼ i \underset{˙}{\times} A) (w) = y) \to y \in \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}$
80		nfv	$⊢ Ⅎ w (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y$
81		nfv	$⊢ Ⅎ z (i \in ℤ ⟼ i \underset{˙}{\times} A) (w) = y$
82		fveqeq2	$⊢ z = w \to ((i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y \leftrightarrow (i \in ℤ ⟼ i \underset{˙}{\times} A) (w) = y)$
83	80 81 82	cbvrexw	$⊢ \exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y \leftrightarrow \exists w \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (w) = y$
84	83	bilani	$⊢ (φ \land \exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y) \to \exists w \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (w) = y$
85	79 84	r19.29a	$⊢ (φ \land \exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y) \to y \in \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}$
86	85	ex	$⊢ φ \to (\exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y \to y \in \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\})$
87	86	adantr	$⊢ (φ \land y \in ran (i \in ℤ ⟼ i \underset{˙}{\times} A)) \to (\exists z \in ℤ (i \in ℤ ⟼ i \underset{˙}{\times} A) (z) = y \to y \in \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\})$
88	39 87	mpd	$⊢ (φ \land y \in ran (i \in ℤ ⟼ i \underset{˙}{\times} A)) \to y \in \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}$
89	88	ex	$⊢ φ \to (y \in ran (i \in ℤ ⟼ i \underset{˙}{\times} A) \to y \in \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\})$
90	89	ssrdv	$⊢ φ \to ran (i \in ℤ ⟼ i \underset{˙}{\times} A) \subseteq \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}$
91		hashss	$⊢ (\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\} \in V \land ran (i \in ℤ ⟼ i \underset{˙}{\times} A) \subseteq \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}) \to \|ran (i \in ℤ ⟼ i \underset{˙}{\times} A)\| \leq \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\|$
92	33 90 91	syl2anc	$⊢ φ \to \|ran (i \in ℤ ⟼ i \underset{˙}{\times} A)\| \leq \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\|$
93	29 92	eqbrtrd	$⊢ φ \to od (G) (A) \leq \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\|$
94	16 93	jca	$⊢ φ \to (\|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\| \leq od (G) (A) \land od (G) (A) \leq \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\|)$
95		ssrab2	$⊢ \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\} \subseteq B$
96	95	a1i	$⊢ φ \to \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\} \subseteq B$
97	4 96	ssfid	$⊢ φ \to \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\} \in Fin$
98		hashcl	$⊢ \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\} \in Fin \to \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\| \in ℕ_{0}$
99	97 98	syl	$⊢ φ \to \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\| \in ℕ_{0}$
100	99	nn0red	$⊢ φ \to \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\| \in ℝ$
101	15	nnred	$⊢ φ \to od (G) (A) \in ℝ$
102	100 101	letri3d	$⊢ φ \to (\|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\| = od (G) (A) \leftrightarrow (\|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\| \leq od (G) (A) \land od (G) (A) \leq \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\|))$
103	94 102	mpbird	$⊢ φ \to \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\| = od (G) (A)$

Metamath Proof Explorer

Theorem unitscyglem1

Proof