fincygsubgodd

Description: Calculate the order of a subgroup of a finite cyclic group. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	fincygsubgodd.1	$⊢ B = {Base}_{G}$
	fincygsubgodd.2	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	fincygsubgodd.3	$⊢ D = \frac{\|B\|}{C}$
	fincygsubgodd.4	$⊢ F = (n \in ℤ ⟼ n \underset{˙}{\cdot} A)$
	fincygsubgodd.5	$⊢ H = (n \in ℤ ⟼ n \underset{˙}{\cdot} (C \underset{˙}{\cdot} A))$
	fincygsubgodd.6	$⊢ φ \to G \in Grp$
	fincygsubgodd.7	$⊢ φ \to A \in B$
	fincygsubgodd.8	$⊢ φ \to ran F = B$
	fincygsubgodd.9	$⊢ φ \to C ∥ \|B\|$
	fincygsubgodd.10	$⊢ φ \to B \in Fin$
	fincygsubgodd.11	$⊢ φ \to C \in ℕ$
Assertion	fincygsubgodd	$⊢ φ \to \|ran H\| = D$

Proof

Step	Hyp	Ref	Expression
1		fincygsubgodd.1	$⊢ B = {Base}_{G}$
2		fincygsubgodd.2	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		fincygsubgodd.3	$⊢ D = \frac{\|B\|}{C}$
4		fincygsubgodd.4	$⊢ F = (n \in ℤ ⟼ n \underset{˙}{\cdot} A)$
5		fincygsubgodd.5	$⊢ H = (n \in ℤ ⟼ n \underset{˙}{\cdot} (C \underset{˙}{\cdot} A))$
6		fincygsubgodd.6	$⊢ φ \to G \in Grp$
7		fincygsubgodd.7	$⊢ φ \to A \in B$
8		fincygsubgodd.8	$⊢ φ \to ran F = B$
9		fincygsubgodd.9	$⊢ φ \to C ∥ \|B\|$
10		fincygsubgodd.10	$⊢ φ \to B \in Fin$
11		fincygsubgodd.11	$⊢ φ \to C \in ℕ$
12		eqid	$⊢ od (G) = od (G)$
13	4	rneqi	$⊢ ran F = ran (n \in ℤ ⟼ n \underset{˙}{\cdot} A)$
14	8 13	eqtr3di	$⊢ φ \to B = ran (n \in ℤ ⟼ n \underset{˙}{\cdot} A)$
15	1 2 12 6 7 14	cycsubggenodd	$⊢ φ \to od (G) (A) = if (B \in Fin, \|B\|, 0)$
16	10	iftrued	$⊢ φ \to if (B \in Fin, \|B\|, 0) = \|B\|$
17	15 16	eqtrd	$⊢ φ \to od (G) (A) = \|B\|$
18	17	oveq1d	$⊢ φ \to \frac{od (G) (A)}{C} = \frac{\|B\|}{C}$
19	11	nnzd	$⊢ φ \to C \in ℤ$
20	1 12 2	odmulg	$⊢ (G \in Grp \land A \in B \land C \in ℤ) \to od (G) (A) = (C \gcd od (G) (A)) od (G) (C \underset{˙}{\cdot} A)$
21	6 7 19 20	syl3anc	$⊢ φ \to od (G) (A) = (C \gcd od (G) (A)) od (G) (C \underset{˙}{\cdot} A)$
22	1 12	odcl	$⊢ A \in B \to od (G) (A) \in ℕ_{0}$
23		nn0z	$⊢ od (G) (A) \in ℕ_{0} \to od (G) (A) \in ℤ$
24	7 22 23	3syl	$⊢ φ \to od (G) (A) \in ℤ$
25	9 17	breqtrrd	$⊢ φ \to C ∥ od (G) (A)$
26	11 24 25	dvdsgcdidd	$⊢ φ \to C \gcd od (G) (A) = C$
27	26	oveq1d	$⊢ φ \to (C \gcd od (G) (A)) od (G) (C \underset{˙}{\cdot} A) = C od (G) (C \underset{˙}{\cdot} A)$
28	21 27	eqtrd	$⊢ φ \to od (G) (A) = C od (G) (C \underset{˙}{\cdot} A)$
29	1 12 7	odcld	$⊢ φ \to od (G) (A) \in ℕ_{0}$
30	29	nn0cnd	$⊢ φ \to od (G) (A) \in ℂ$
31	1 2 6 19 7	mulgcld	$⊢ φ \to C \underset{˙}{\cdot} A \in B$
32	1 12 31	odcld	$⊢ φ \to od (G) (C \underset{˙}{\cdot} A) \in ℕ_{0}$
33	32	nn0cnd	$⊢ φ \to od (G) (C \underset{˙}{\cdot} A) \in ℂ$
34	19	zcnd	$⊢ φ \to C \in ℂ$
35	11	nnne0d	$⊢ φ \to C \neq 0$
36	30 33 34 35	divmul2d	$⊢ φ \to (\frac{od (G) (A)}{C} = od (G) (C \underset{˙}{\cdot} A) \leftrightarrow od (G) (A) = C od (G) (C \underset{˙}{\cdot} A))$
37	28 36	mpbird	$⊢ φ \to \frac{od (G) (A)}{C} = od (G) (C \underset{˙}{\cdot} A)$
38	18 37	eqtr3d	$⊢ φ \to \frac{\|B\|}{C} = od (G) (C \underset{˙}{\cdot} A)$
39	3 38	eqtrid	$⊢ φ \to D = od (G) (C \underset{˙}{\cdot} A)$
40	5	rneqi	$⊢ ran H = ran (n \in ℤ ⟼ n \underset{˙}{\cdot} (C \underset{˙}{\cdot} A))$
41	40	a1i	$⊢ φ \to ran H = ran (n \in ℤ ⟼ n \underset{˙}{\cdot} (C \underset{˙}{\cdot} A))$
42	1 2 12 6 31 41	cycsubggenodd	$⊢ φ \to od (G) (C \underset{˙}{\cdot} A) = if (ran H \in Fin, \|ran H\|, 0)$
43	39 42	eqtrd	$⊢ φ \to D = if (ran H \in Fin, \|ran H\|, 0)$
44		iffalse	$⊢ \neg ran H \in Fin \to if (ran H \in Fin, \|ran H\|, 0) = 0$
45	43 44	sylan9eq	$⊢ (φ \land \neg ran H \in Fin) \to D = 0$
46	3	a1i	$⊢ φ \to D = \frac{\|B\|}{C}$
47		hashcl	$⊢ B \in Fin \to \|B\| \in ℕ_{0}$
48		nn0cn	$⊢ \|B\| \in ℕ_{0} \to \|B\| \in ℂ$
49	10 47 48	3syl	$⊢ φ \to \|B\| \in ℂ$
50	7 10	hashelne0d	$⊢ φ \to \neg \|B\| = 0$
51	50	neqned	$⊢ φ \to \|B\| \neq 0$
52	49 34 51 35	divne0d	$⊢ φ \to \frac{\|B\|}{C} \neq 0$
53	46 52	eqnetrd	$⊢ φ \to D \neq 0$
54	53	neneqd	$⊢ φ \to \neg D = 0$
55	54	adantr	$⊢ (φ \land \neg ran H \in Fin) \to \neg D = 0$
56	45 55	condan	$⊢ φ \to ran H \in Fin$
57	56	iftrued	$⊢ φ \to if (ran H \in Fin, \|ran H\|, 0) = \|ran H\|$
58	39 42 57	3eqtrrd	$⊢ φ \to \|ran H\| = D$

Metamath Proof Explorer

Theorem fincygsubgodd

Proof