odmod

Description: Reduce the argument of a group multiple by modding out the order of the element. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Mario Carneiro, 6-Sep-2015)

	Ref	Expression
Hypotheses	odcl.1	$⊢ X = {Base}_{G}$
	odcl.2	$⊢ O = od (G)$
	odid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	odid.4	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	odmod	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (N \mod O (A)) \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A$

Proof

Step	Hyp	Ref	Expression
1		odcl.1	$⊢ X = {Base}_{G}$
2		odcl.2	$⊢ O = od (G)$
3		odid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		odid.4	$⊢ \underset{˙}{0} = 0_{G}$
5		simpl3	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to N \in ℤ$
6	5	zred	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to N \in ℝ$
7		simpr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) \in ℕ$
8	7	nnrpd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) \in ℝ^{+}$
9		modval	$⊢ (N \in ℝ \land O (A) \in ℝ^{+}) \to N \mod O (A) = N - O (A) ⌊\frac{N}{O (A)}⌋$
10	6 8 9	syl2anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to N \mod O (A) = N - O (A) ⌊\frac{N}{O (A)}⌋$
11	10	oveq1d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (N \mod O (A)) \underset{˙}{\cdot} A = (N - O (A) ⌊\frac{N}{O (A)}⌋) \underset{˙}{\cdot} A$
12		simpl1	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to G \in Grp$
13	7	nnzd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) \in ℤ$
14	6 7	nndivred	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to \frac{N}{O (A)} \in ℝ$
15	14	flcld	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to ⌊\frac{N}{O (A)}⌋ \in ℤ$
16	13 15	zmulcld	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) ⌊\frac{N}{O (A)}⌋ \in ℤ$
17		simpl2	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to A \in X$
18		eqid	$⊢ -_{G} = -_{G}$
19	1 3 18	mulgsubdir	$⊢ (G \in Grp \land (N \in ℤ \land O (A) ⌊\frac{N}{O (A)}⌋ \in ℤ \land A \in X)) \to (N - O (A) ⌊\frac{N}{O (A)}⌋) \underset{˙}{\cdot} A = (N \underset{˙}{\cdot} A) -_{G} (O (A) ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} A)$
20	12 5 16 17 19	syl13anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (N - O (A) ⌊\frac{N}{O (A)}⌋) \underset{˙}{\cdot} A = (N \underset{˙}{\cdot} A) -_{G} (O (A) ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} A)$
21		nncn	$⊢ O (A) \in ℕ \to O (A) \in ℂ$
22		zcn	$⊢ ⌊\frac{N}{O (A)}⌋ \in ℤ \to ⌊\frac{N}{O (A)}⌋ \in ℂ$
23		mulcom	$⊢ (O (A) \in ℂ \land ⌊\frac{N}{O (A)}⌋ \in ℂ) \to O (A) ⌊\frac{N}{O (A)}⌋ = ⌊\frac{N}{O (A)}⌋ O (A)$
24	21 22 23	syl2an	$⊢ (O (A) \in ℕ \land ⌊\frac{N}{O (A)}⌋ \in ℤ) \to O (A) ⌊\frac{N}{O (A)}⌋ = ⌊\frac{N}{O (A)}⌋ O (A)$
25	7 15 24	syl2anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) ⌊\frac{N}{O (A)}⌋ = ⌊\frac{N}{O (A)}⌋ O (A)$
26	25	oveq1d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} A = ⌊\frac{N}{O (A)}⌋ O (A) \underset{˙}{\cdot} A$
27	1 3	mulgass	$⊢ (G \in Grp \land (⌊\frac{N}{O (A)}⌋ \in ℤ \land O (A) \in ℤ \land A \in X)) \to ⌊\frac{N}{O (A)}⌋ O (A) \underset{˙}{\cdot} A = ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} (O (A) \underset{˙}{\cdot} A)$
28	12 15 13 17 27	syl13anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to ⌊\frac{N}{O (A)}⌋ O (A) \underset{˙}{\cdot} A = ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} (O (A) \underset{˙}{\cdot} A)$
29	1 2 3 4	odid	$⊢ A \in X \to O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$
30	17 29	syl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$
31	30	oveq2d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} (O (A) \underset{˙}{\cdot} A) = ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} \underset{˙}{0}$
32	1 3 4	mulgz	$⊢ (G \in Grp \land ⌊\frac{N}{O (A)}⌋ \in ℤ) \to ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
33	12 15 32	syl2anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
34	31 33	eqtrd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} (O (A) \underset{˙}{\cdot} A) = \underset{˙}{0}$
35	26 28 34	3eqtrd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} A = \underset{˙}{0}$
36	35	oveq2d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (N \underset{˙}{\cdot} A) -_{G} (O (A) ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} A) = (N \underset{˙}{\cdot} A) -_{G} \underset{˙}{0}$
37	1 3	mulgcl	$⊢ (G \in Grp \land N \in ℤ \land A \in X) \to N \underset{˙}{\cdot} A \in X$
38	12 5 17 37	syl3anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to N \underset{˙}{\cdot} A \in X$
39	1 4 18	grpsubid1	$⊢ (G \in Grp \land N \underset{˙}{\cdot} A \in X) \to (N \underset{˙}{\cdot} A) -_{G} \underset{˙}{0} = N \underset{˙}{\cdot} A$
40	12 38 39	syl2anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (N \underset{˙}{\cdot} A) -_{G} \underset{˙}{0} = N \underset{˙}{\cdot} A$
41	36 40	eqtrd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (N \underset{˙}{\cdot} A) -_{G} (O (A) ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} A) = N \underset{˙}{\cdot} A$
42	11 20 41	3eqtrd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (N \mod O (A)) \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A$

Metamath Proof Explorer

Theorem odmod

Proof