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 = ( 0_g ‘ 𝐺 )
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 = ( 0_g ‘ 𝐺 )
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 ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 𝑁 · 𝐴 ) )

Metamath Proof Explorer

Theorem odmod

Proof