Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgmodid.o ⊢ 0 = ( 0g ‘ 𝐺 )
mulgmodid.t ⊢ · = ( .g ‘ 𝐺 )
Assertion mulgmodid ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( ( 𝑁 mod 𝑀 ) · 𝑋 ) = ( 𝑁 · 𝑋 ) )

Proof

Step Hyp Ref Expression
1 mulgmodid.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgmodid.o ⊢ 0 = ( 0g ‘ 𝐺 )
3 mulgmodid.t ⊢ · = ( .g ‘ 𝐺 )
4 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
5 nnrp ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ+ )
6 modval ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝑁 mod 𝑀 ) = ( 𝑁 − ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ) )
7 4 5 6 syl2an ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 mod 𝑀 ) = ( 𝑁 − ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ) )
8 7 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( 𝑁 mod 𝑀 ) = ( 𝑁 − ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ) )
9 8 oveq1d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( ( 𝑁 mod 𝑀 ) · 𝑋 ) = ( ( 𝑁 − ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ) · 𝑋 ) )
10 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
11 10 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 𝑁 ∈ ℂ )
12 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
13 12 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℤ )
14 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
15 nnne0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ≠ 0 )
16 redivcl ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑀 ≠ 0 ) → ( 𝑁 / 𝑀 ) ∈ ℝ )
17 4 14 15 16 syl3an ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 / 𝑀 ) ∈ ℝ )
18 17 3anidm23 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 / 𝑀 ) ∈ ℝ )
19 18 flcld ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ∈ ℤ )
20 13 19 zmulcld ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ∈ ℤ )
21 20 zcnd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ∈ ℂ )
22 11 21 negsubd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 + - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ) = ( 𝑁 − ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ) )
23 22 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( 𝑁 + - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ) = ( 𝑁 − ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ) )
24 23 oveq1d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( ( 𝑁 + - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ) · 𝑋 ) = ( ( 𝑁 − ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ) · 𝑋 ) )
25 simp1 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → 𝐺 ∈ Grp )
26 simpl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 𝑁 ∈ ℤ )
27 26 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → 𝑁 ∈ ℤ )
28 13 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → 𝑀 ∈ ℤ )
29 19 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ∈ ℤ )
30 28 29 zmulcld ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ∈ ℤ )
31 30 znegcld ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ∈ ℤ )
32 simpl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) → 𝑋 ∈ 𝐵 )
33 32 3ad2ant3 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → 𝑋 ∈ 𝐵 )
34 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
35 1 3 34 mulgdir ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑁 + - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) ( +g ‘ 𝐺 ) ( - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) · 𝑋 ) ) )
36 25 27 31 33 35 syl13anc ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( ( 𝑁 + - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) ( +g ‘ 𝐺 ) ( - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) · 𝑋 ) ) )
37 9 24 36 3eqtr2d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( ( 𝑁 mod 𝑀 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) ( +g ‘ 𝐺 ) ( - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) · 𝑋 ) ) )
38 nncn ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
39 38 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℂ )
40 19 zcnd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ∈ ℂ )
41 39 40 mulneg2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝑀 · - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) = - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) )
42 41 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( 𝑀 · - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) = - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) )
43 42 oveq1d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( ( 𝑀 · - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) · 𝑋 ) = ( - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) · 𝑋 ) )
44 18 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( 𝑁 / 𝑀 ) ∈ ℝ )
45 44 flcld ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ∈ ℤ )
46 45 znegcld ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ∈ ℤ )
47 1 3 mulgassr ⊢ ( ( 𝐺 ∈ Grp ∧ ( - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 · - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) · 𝑋 ) = ( - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) · ( 𝑀 · 𝑋 ) ) )
48 25 46 28 33 47 syl13anc ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( ( 𝑀 · - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) · 𝑋 ) = ( - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) · ( 𝑀 · 𝑋 ) ) )
49 oveq2 ⊢ ( ( 𝑀 · 𝑋 ) = 0 → ( - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) · ( 𝑀 · 𝑋 ) ) = ( - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) · 0 ) )
50 49 adantl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) → ( - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) · ( 𝑀 · 𝑋 ) ) = ( - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) · 0 ) )
51 50 3ad2ant3 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) · ( 𝑀 · 𝑋 ) ) = ( - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) · 0 ) )
52 1 3 2 mulgz ⊢ ( ( 𝐺 ∈ Grp ∧ - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ∈ ℤ ) → ( - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) · 0 ) = 0 )
53 25 46 52 syl2anc ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) · 0 ) = 0 )
54 48 51 53 3eqtrd ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( ( 𝑀 · - ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) · 𝑋 ) = 0 )
55 43 54 eqtr3d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) · 𝑋 ) = 0 )
56 55 oveq2d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( ( 𝑁 · 𝑋 ) ( +g ‘ 𝐺 ) ( - ( 𝑀 · ( ⌊ ‘ ( 𝑁 / 𝑀 ) ) ) · 𝑋 ) ) = ( ( 𝑁 · 𝑋 ) ( +g ‘ 𝐺 ) 0 ) )
57 id ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Grp )
58 1 3 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
59 57 26 32 58 syl3an ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
60 1 34 2 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( ( 𝑁 · 𝑋 ) ( +g ‘ 𝐺 ) 0 ) = ( 𝑁 · 𝑋 ) )
61 25 59 60 syl2anc ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( ( 𝑁 · 𝑋 ) ( +g ‘ 𝐺 ) 0 ) = ( 𝑁 · 𝑋 ) )
62 37 56 61 3eqtrd ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) = 0 ) ) → ( ( 𝑁 mod 𝑀 ) · 𝑋 ) = ( 𝑁 · 𝑋 ) )