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

Metamath Proof Explorer

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