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