This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
odid.3 ⊢ · = ( .g ‘ 𝐺 )
odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion odmod ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 𝑁 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 odcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odid.3 ⊢ · = ( .g ‘ 𝐺 )
4 odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
5 simpl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑁 ∈ ℤ )
6 5 zred ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑁 ∈ ℝ )
7 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
8 7 nnrpd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℝ+ )
9 modval ⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑁 − ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) ) )
10 6 8 9 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑁 − ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) ) )
11 10 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 − ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) ) · 𝐴 ) )
12 simpl1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝐺 ∈ Grp )
13 7 nnzd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
14 6 7 nndivred ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ∈ ℝ )
15 14 flcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ∈ ℤ )
16 13 15 zmulcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) ∈ ℤ )
17 simpl2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝐴 ∈ 𝑋 )
18 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
19 1 3 18 mulgsubdir ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑁 − ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) ) · 𝐴 ) = ( ( 𝑁 · 𝐴 ) ( -g ‘ 𝐺 ) ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) · 𝐴 ) ) )
20 12 5 16 17 19 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 − ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) ) · 𝐴 ) = ( ( 𝑁 · 𝐴 ) ( -g ‘ 𝐺 ) ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) · 𝐴 ) ) )
21 nncn ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( 𝑂 ‘ 𝐴 ) ∈ ℂ )
22 zcn ⊢ ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ∈ ℤ → ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ∈ ℂ )
23 mulcom ⊢ ( ( ( 𝑂 ‘ 𝐴 ) ∈ ℂ ∧ ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ∈ ℂ ) → ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) = ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( 𝑂 ‘ 𝐴 ) ) )
24 21 22 23 syl2an ⊢ ( ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∧ ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) = ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( 𝑂 ‘ 𝐴 ) ) )
25 7 15 24 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) = ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( 𝑂 ‘ 𝐴 ) ) )
26 25 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) · 𝐴 ) = ( ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) )
27 1 3 mulgass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ∈ ℤ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ) )
28 12 15 13 17 27 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ) )
29 1 2 3 4 odid ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 )
30 17 29 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 )
31 30 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ) = ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · 0 ) )
32 1 3 4 mulgz ⊢ ( ( 𝐺 ∈ Grp ∧ ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ∈ ℤ ) → ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · 0 ) = 0 )
33 12 15 32 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · 0 ) = 0 )
34 31 33 eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ) = 0 )
35 26 28 34 3eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) · 𝐴 ) = 0 )
36 35 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 · 𝐴 ) ( -g ‘ 𝐺 ) ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) · 𝐴 ) ) = ( ( 𝑁 · 𝐴 ) ( -g ‘ 𝐺 ) 0 ) )
37 1 3 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 · 𝐴 ) ∈ 𝑋 )
38 12 5 17 37 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 · 𝐴 ) ∈ 𝑋 )
39 1 4 18 grpsubid1 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 · 𝐴 ) ∈ 𝑋 ) → ( ( 𝑁 · 𝐴 ) ( -g ‘ 𝐺 ) 0 ) = ( 𝑁 · 𝐴 ) )
40 12 38 39 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 · 𝐴 ) ( -g ‘ 𝐺 ) 0 ) = ( 𝑁 · 𝐴 ) )
41 36 40 eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 · 𝐴 ) ( -g ‘ 𝐺 ) ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) · 𝐴 ) ) = ( 𝑁 · 𝐴 ) )
42 11 20 41 3eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 𝑁 · 𝐴 ) )