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

Metamath Proof Explorer

Theorem odmulgid

Description: A relationship between the order of a multiple and the order of the basepoint. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses odmulgid.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odmulgid.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
odmulgid.3 ⊢ · = ( .g ‘ 𝐺 )
Assertion odmulgid ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ 𝐾 ↔ ( 𝑂 ‘ 𝐴 ) ∥ ( 𝐾 · 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 odmulgid.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odmulgid.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odmulgid.3 ⊢ · = ( .g ‘ 𝐺 )
4 simpl1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → 𝐺 ∈ Grp )
5 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℤ )
6 simpl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → 𝑁 ∈ ℤ )
7 simpl2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → 𝐴 ∈ 𝑋 )
8 1 3 mulgass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝐾 · 𝑁 ) · 𝐴 ) = ( 𝐾 · ( 𝑁 · 𝐴 ) ) )
9 4 5 6 7 8 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · 𝑁 ) · 𝐴 ) = ( 𝐾 · ( 𝑁 · 𝐴 ) ) )
10 9 eqeq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝐾 · 𝑁 ) · 𝐴 ) = ( 0g ‘ 𝐺 ) ↔ ( 𝐾 · ( 𝑁 · 𝐴 ) ) = ( 0g ‘ 𝐺 ) ) )
11 5 6 zmulcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 · 𝑁 ) ∈ ℤ )
12 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
13 1 2 3 12 oddvds ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝐾 · 𝑁 ) ↔ ( ( 𝐾 · 𝑁 ) · 𝐴 ) = ( 0g ‘ 𝐺 ) ) )
14 4 7 11 13 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝐾 · 𝑁 ) ↔ ( ( 𝐾 · 𝑁 ) · 𝐴 ) = ( 0g ‘ 𝐺 ) ) )
15 1 3 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 · 𝐴 ) ∈ 𝑋 )
16 4 6 7 15 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → ( 𝑁 · 𝐴 ) ∈ 𝑋 )
17 1 2 3 12 oddvds ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 · 𝐴 ) ∈ 𝑋 ∧ 𝐾 ∈ ℤ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ 𝐾 ↔ ( 𝐾 · ( 𝑁 · 𝐴 ) ) = ( 0g ‘ 𝐺 ) ) )
18 4 16 5 17 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ 𝐾 ↔ ( 𝐾 · ( 𝑁 · 𝐴 ) ) = ( 0g ‘ 𝐺 ) ) )
19 10 14 18 3bitr4rd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ 𝐾 ↔ ( 𝑂 ‘ 𝐴 ) ∥ ( 𝐾 · 𝑁 ) ) )