Theorem odcong

Description: If two multipliers are congruent relative to the base point's order, the corresponding multiples are the same. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	odcl.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
	odcl.2	⊢ 𝑂 = ( od ‘ 𝐺 )
	odid.3	⊢ · = ( .g ‘ 𝐺 )
	odid.4	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	odcong	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) ↔ ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		odcl.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		odcl.2	⊢ 𝑂 = ( od ‘ 𝐺 )
3		odid.3	⊢ · = ( .g ‘ 𝐺 )
4		odid.4	⊢ 0 = ( 0g ‘ 𝐺 )
5		zsubcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 − 𝑁 ) ∈ ℤ )
6	1 2 3 4	oddvds	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 − 𝑁 ) ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) ↔ ( ( 𝑀 − 𝑁 ) · 𝐴 ) = 0 ) )
7	5 6	syl3an3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) ↔ ( ( 𝑀 − 𝑁 ) · 𝐴 ) = 0 ) )
8		simp1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝐺 ∈ Grp )
9		simp3l	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑀 ∈ ℤ )
10		simp3r	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
11		simp2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝐴 ∈ 𝑋 )
12		eqid	⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
13	1 3 12	mulgsubdir	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑀 − 𝑁 ) · 𝐴 ) = ( ( 𝑀 · 𝐴 ) ( -g ‘ 𝐺 ) ( 𝑁 · 𝐴 ) ) )
14	8 9 10 11 13	syl13anc	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑀 − 𝑁 ) · 𝐴 ) = ( ( 𝑀 · 𝐴 ) ( -g ‘ 𝐺 ) ( 𝑁 · 𝐴 ) ) )
15	14	eqeq1d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( ( 𝑀 − 𝑁 ) · 𝐴 ) = 0 ↔ ( ( 𝑀 · 𝐴 ) ( -g ‘ 𝐺 ) ( 𝑁 · 𝐴 ) ) = 0 ) )
16	1 3	mulgcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑀 · 𝐴 ) ∈ 𝑋 )
17	8 9 11 16	syl3anc	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀 · 𝐴 ) ∈ 𝑋 )
18	1 3	mulgcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 · 𝐴 ) ∈ 𝑋 )
19	8 10 11 18	syl3anc	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑁 · 𝐴 ) ∈ 𝑋 )
20	1 4 12	grpsubeq0	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 · 𝐴 ) ∈ 𝑋 ∧ ( 𝑁 · 𝐴 ) ∈ 𝑋 ) → ( ( ( 𝑀 · 𝐴 ) ( -g ‘ 𝐺 ) ( 𝑁 · 𝐴 ) ) = 0 ↔ ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) )
21	8 17 19 20	syl3anc	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( ( 𝑀 · 𝐴 ) ( -g ‘ 𝐺 ) ( 𝑁 · 𝐴 ) ) = 0 ↔ ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) )
22	7 15 21	3bitrd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) ↔ ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) )