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 ⊢ X = Base G
odcl.2 ⊢ O = od ⁡ G
odid.3 ⊢ · ˙ = ⋅ G
odid.4 ⊢ 0 ˙ = 0 G
Assertion odcong ⊢ G ∈ Grp ∧ A ∈ X ∧ M ∈ ℤ ∧ N ∈ ℤ → O ⁡ A ∥ M − N ↔ M · ˙ A = N · ˙ A

Proof

Step Hyp Ref Expression
1 odcl.1 ⊢ X = Base G
2 odcl.2 ⊢ O = od ⁡ G
3 odid.3 ⊢ · ˙ = ⋅ G
4 odid.4 ⊢ 0 ˙ = 0 G
5 zsubcl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M − N ∈ ℤ
6 1 2 3 4 oddvds ⊢ G ∈ Grp ∧ A ∈ X ∧ M − N ∈ ℤ → O ⁡ A ∥ M − N ↔ M − N · ˙ A = 0 ˙
7 5 6 syl3an3 ⊢ G ∈ Grp ∧ A ∈ X ∧ M ∈ ℤ ∧ N ∈ ℤ → O ⁡ A ∥ M − N ↔ M − N · ˙ A = 0 ˙
8 simp1 ⊢ G ∈ Grp ∧ A ∈ X ∧ M ∈ ℤ ∧ N ∈ ℤ → G ∈ Grp
9 simp3l ⊢ G ∈ Grp ∧ A ∈ X ∧ M ∈ ℤ ∧ N ∈ ℤ → M ∈ ℤ
10 simp3r ⊢ G ∈ Grp ∧ A ∈ X ∧ M ∈ ℤ ∧ N ∈ ℤ → N ∈ ℤ
11 simp2 ⊢ G ∈ Grp ∧ A ∈ X ∧ M ∈ ℤ ∧ N ∈ ℤ → A ∈ X
12 eqid ⊢ - G = - G
13 1 3 12 mulgsubdir ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ A ∈ X → M − N · ˙ A = M · ˙ A - G N · ˙ A
14 8 9 10 11 13 syl13anc ⊢ G ∈ Grp ∧ A ∈ X ∧ M ∈ ℤ ∧ N ∈ ℤ → M − N · ˙ A = M · ˙ A - G N · ˙ A
15 14 eqeq1d ⊢ G ∈ Grp ∧ A ∈ X ∧ M ∈ ℤ ∧ N ∈ ℤ → M − N · ˙ A = 0 ˙ ↔ M · ˙ A - G N · ˙ A = 0 ˙
16 1 3 mulgcl ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ A ∈ X → M · ˙ A ∈ X
17 8 9 11 16 syl3anc ⊢ G ∈ Grp ∧ A ∈ X ∧ M ∈ ℤ ∧ N ∈ ℤ → M · ˙ A ∈ X
18 1 3 mulgcl ⊢ G ∈ Grp ∧ N ∈ ℤ ∧ A ∈ X → N · ˙ A ∈ X
19 8 10 11 18 syl3anc ⊢ G ∈ Grp ∧ A ∈ X ∧ M ∈ ℤ ∧ N ∈ ℤ → N · ˙ A ∈ X
20 1 4 12 grpsubeq0 ⊢ G ∈ Grp ∧ M · ˙ A ∈ X ∧ N · ˙ A ∈ X → M · ˙ A - G N · ˙ A = 0 ˙ ↔ M · ˙ A = N · ˙ A
21 8 17 19 20 syl3anc ⊢ G ∈ Grp ∧ A ∈ X ∧ M ∈ ℤ ∧ N ∈ ℤ → M · ˙ A - G N · ˙ A = 0 ˙ ↔ M · ˙ A = N · ˙ A
22 7 15 21 3bitrd ⊢ G ∈ Grp ∧ A ∈ X ∧ M ∈ ℤ ∧ N ∈ ℤ → O ⁡ A ∥ M − N ↔ M · ˙ A = N · ˙ A