mulgmodid

Description: Casting out multiples of the identity element leaves the group multiple unchanged. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 30-Aug-2021)

	Ref	Expression
Hypotheses	mulgmodid.b	$⊢ B = {Base}_{G}$
	mulgmodid.o	$⊢ \underset{˙}{0} = 0_{G}$
	mulgmodid.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	mulgmodid	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to (N \mod M) \underset{˙}{\cdot} X = N \underset{˙}{\cdot} X$

Proof

Step	Hyp	Ref	Expression
1		mulgmodid.b	$⊢ B = {Base}_{G}$
2		mulgmodid.o	$⊢ \underset{˙}{0} = 0_{G}$
3		mulgmodid.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		zre	$⊢ N \in ℤ \to N \in ℝ$
5		nnrp	$⊢ M \in ℕ \to M \in ℝ^{+}$
6		modval	$⊢ (N \in ℝ \land M \in ℝ^{+}) \to N \mod M = N - M ⌊\frac{N}{M}⌋$
7	4 5 6	syl2an	$⊢ (N \in ℤ \land M \in ℕ) \to N \mod M = N - M ⌊\frac{N}{M}⌋$
8	7	3ad2ant2	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to N \mod M = N - M ⌊\frac{N}{M}⌋$
9	8	oveq1d	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to (N \mod M) \underset{˙}{\cdot} X = (N - M ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} X$
10		zcn	$⊢ N \in ℤ \to N \in ℂ$
11	10	adantr	$⊢ (N \in ℤ \land M \in ℕ) \to N \in ℂ$
12		nnz	$⊢ M \in ℕ \to M \in ℤ$
13	12	adantl	$⊢ (N \in ℤ \land M \in ℕ) \to M \in ℤ$
14		nnre	$⊢ M \in ℕ \to M \in ℝ$
15		nnne0	$⊢ M \in ℕ \to M \neq 0$
16		redivcl	$⊢ (N \in ℝ \land M \in ℝ \land M \neq 0) \to \frac{N}{M} \in ℝ$
17	4 14 15 16	syl3an	$⊢ (N \in ℤ \land M \in ℕ \land M \in ℕ) \to \frac{N}{M} \in ℝ$
18	17	3anidm23	$⊢ (N \in ℤ \land M \in ℕ) \to \frac{N}{M} \in ℝ$
19	18	flcld	$⊢ (N \in ℤ \land M \in ℕ) \to ⌊\frac{N}{M}⌋ \in ℤ$
20	13 19	zmulcld	$⊢ (N \in ℤ \land M \in ℕ) \to M ⌊\frac{N}{M}⌋ \in ℤ$
21	20	zcnd	$⊢ (N \in ℤ \land M \in ℕ) \to M ⌊\frac{N}{M}⌋ \in ℂ$
22	11 21	negsubd	$⊢ (N \in ℤ \land M \in ℕ) \to N + (- M ⌊\frac{N}{M}⌋) = N - M ⌊\frac{N}{M}⌋$
23	22	3ad2ant2	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to N + (- M ⌊\frac{N}{M}⌋) = N - M ⌊\frac{N}{M}⌋$
24	23	oveq1d	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to (N + (- M ⌊\frac{N}{M}⌋)) \underset{˙}{\cdot} X = (N - M ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} X$
25		simp1	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to G \in Grp$
26		simpl	$⊢ (N \in ℤ \land M \in ℕ) \to N \in ℤ$
27	26	3ad2ant2	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to N \in ℤ$
28	13	3ad2ant2	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to M \in ℤ$
29	19	3ad2ant2	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to ⌊\frac{N}{M}⌋ \in ℤ$
30	28 29	zmulcld	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to M ⌊\frac{N}{M}⌋ \in ℤ$
31	30	znegcld	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to - M ⌊\frac{N}{M}⌋ \in ℤ$
32		simpl	$⊢ (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0}) \to X \in B$
33	32	3ad2ant3	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to X \in B$
34		eqid	$⊢ +_{G} = +_{G}$
35	1 3 34	mulgdir	$⊢ (G \in Grp \land (N \in ℤ \land - M ⌊\frac{N}{M}⌋ \in ℤ \land X \in B)) \to (N + (- M ⌊\frac{N}{M}⌋)) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) +_{G} ((- M ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} X)$
36	25 27 31 33 35	syl13anc	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to (N + (- M ⌊\frac{N}{M}⌋)) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) +_{G} ((- M ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} X)$
37	9 24 36	3eqtr2d	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to (N \mod M) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) +_{G} ((- M ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} X)$
38		nncn	$⊢ M \in ℕ \to M \in ℂ$
39	38	adantl	$⊢ (N \in ℤ \land M \in ℕ) \to M \in ℂ$
40	19	zcnd	$⊢ (N \in ℤ \land M \in ℕ) \to ⌊\frac{N}{M}⌋ \in ℂ$
41	39 40	mulneg2d	$⊢ (N \in ℤ \land M \in ℕ) \to M (- ⌊\frac{N}{M}⌋) = - M ⌊\frac{N}{M}⌋$
42	41	3ad2ant2	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to M (- ⌊\frac{N}{M}⌋) = - M ⌊\frac{N}{M}⌋$
43	42	oveq1d	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to M (- ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} X = (- M ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} X$
44	18	3ad2ant2	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to \frac{N}{M} \in ℝ$
45	44	flcld	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to ⌊\frac{N}{M}⌋ \in ℤ$
46	45	znegcld	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to - ⌊\frac{N}{M}⌋ \in ℤ$
47	1 3	mulgassr	$⊢ (G \in Grp \land (- ⌊\frac{N}{M}⌋ \in ℤ \land M \in ℤ \land X \in B)) \to M (- ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} X = (- ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} (M \underset{˙}{\cdot} X)$
48	25 46 28 33 47	syl13anc	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to M (- ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} X = (- ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} (M \underset{˙}{\cdot} X)$
49		oveq2	$⊢ M \underset{˙}{\cdot} X = \underset{˙}{0} \to (- ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} (M \underset{˙}{\cdot} X) = (- ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} \underset{˙}{0}$
50	49	adantl	$⊢ (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0}) \to (- ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} (M \underset{˙}{\cdot} X) = (- ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} \underset{˙}{0}$
51	50	3ad2ant3	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to (- ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} (M \underset{˙}{\cdot} X) = (- ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} \underset{˙}{0}$
52	1 3 2	mulgz	$⊢ (G \in Grp \land - ⌊\frac{N}{M}⌋ \in ℤ) \to (- ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
53	25 46 52	syl2anc	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to (- ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
54	48 51 53	3eqtrd	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to M (- ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} X = \underset{˙}{0}$
55	43 54	eqtr3d	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to (- M ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} X = \underset{˙}{0}$
56	55	oveq2d	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to (N \underset{˙}{\cdot} X) +_{G} ((- M ⌊\frac{N}{M}⌋) \underset{˙}{\cdot} X) = (N \underset{˙}{\cdot} X) +_{G} \underset{˙}{0}$
57		id	$⊢ G \in Grp \to G \in Grp$
58	1 3	mulgcl	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to N \underset{˙}{\cdot} X \in B$
59	57 26 32 58	syl3an	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to N \underset{˙}{\cdot} X \in B$
60	1 34 2	grprid	$⊢ (G \in Grp \land N \underset{˙}{\cdot} X \in B) \to (N \underset{˙}{\cdot} X) +_{G} \underset{˙}{0} = N \underset{˙}{\cdot} X$
61	25 59 60	syl2anc	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to (N \underset{˙}{\cdot} X) +_{G} \underset{˙}{0} = N \underset{˙}{\cdot} X$
62	37 56 61	3eqtrd	$⊢ (G \in Grp \land (N \in ℤ \land M \in ℕ) \land (X \in B \land M \underset{˙}{\cdot} X = \underset{˙}{0})) \to (N \mod M) \underset{˙}{\cdot} X = N \underset{˙}{\cdot} X$

Metamath Proof Explorer

Theorem mulgmodid

Proof