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 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ 𝐾 ↔ ( 𝑂 ‘ 𝐴 ) ∥ ( 𝐾 · 𝑁 ) ) )