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	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	odid.4	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	odcong	$⊢ (G \in Grp \land A \in X \land (M \in ℤ \land N \in ℤ)) \to (O (A) ∥ (M - N) \leftrightarrow M \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A)$

Proof

Step	Hyp	Ref	Expression
1		odcl.1	$⊢ X = {Base}_{G}$
2		odcl.2	$⊢ O = od (G)$
3		odid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		odid.4	$⊢ \underset{˙}{0} = 0_{G}$
5		zsubcl	$⊢ (M \in ℤ \land N \in ℤ) \to M - N \in ℤ$
6	1 2 3 4	oddvds	$⊢ (G \in Grp \land A \in X \land M - N \in ℤ) \to (O (A) ∥ (M - N) \leftrightarrow (M - N) \underset{˙}{\cdot} A = \underset{˙}{0})$
7	5 6	syl3an3	$⊢ (G \in Grp \land A \in X \land (M \in ℤ \land N \in ℤ)) \to (O (A) ∥ (M - N) \leftrightarrow (M - N) \underset{˙}{\cdot} A = \underset{˙}{0})$
8		simp1	$⊢ (G \in Grp \land A \in X \land (M \in ℤ \land N \in ℤ)) \to G \in Grp$
9		simp3l	$⊢ (G \in Grp \land A \in X \land (M \in ℤ \land N \in ℤ)) \to M \in ℤ$
10		simp3r	$⊢ (G \in Grp \land A \in X \land (M \in ℤ \land N \in ℤ)) \to N \in ℤ$
11		simp2	$⊢ (G \in Grp \land A \in X \land (M \in ℤ \land N \in ℤ)) \to A \in X$
12		eqid	$⊢ -_{G} = -_{G}$
13	1 3 12	mulgsubdir	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land A \in X)) \to (M - N) \underset{˙}{\cdot} A = (M \underset{˙}{\cdot} A) -_{G} (N \underset{˙}{\cdot} A)$
14	8 9 10 11 13	syl13anc	$⊢ (G \in Grp \land A \in X \land (M \in ℤ \land N \in ℤ)) \to (M - N) \underset{˙}{\cdot} A = (M \underset{˙}{\cdot} A) -_{G} (N \underset{˙}{\cdot} A)$
15	14	eqeq1d	$⊢ (G \in Grp \land A \in X \land (M \in ℤ \land N \in ℤ)) \to ((M - N) \underset{˙}{\cdot} A = \underset{˙}{0} \leftrightarrow (M \underset{˙}{\cdot} A) -_{G} (N \underset{˙}{\cdot} A) = \underset{˙}{0})$
16	1 3	mulgcl	$⊢ (G \in Grp \land M \in ℤ \land A \in X) \to M \underset{˙}{\cdot} A \in X$
17	8 9 11 16	syl3anc	$⊢ (G \in Grp \land A \in X \land (M \in ℤ \land N \in ℤ)) \to M \underset{˙}{\cdot} A \in X$
18	1 3	mulgcl	$⊢ (G \in Grp \land N \in ℤ \land A \in X) \to N \underset{˙}{\cdot} A \in X$
19	8 10 11 18	syl3anc	$⊢ (G \in Grp \land A \in X \land (M \in ℤ \land N \in ℤ)) \to N \underset{˙}{\cdot} A \in X$
20	1 4 12	grpsubeq0	$⊢ (G \in Grp \land M \underset{˙}{\cdot} A \in X \land N \underset{˙}{\cdot} A \in X) \to ((M \underset{˙}{\cdot} A) -_{G} (N \underset{˙}{\cdot} A) = \underset{˙}{0} \leftrightarrow M \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A)$
21	8 17 19 20	syl3anc	$⊢ (G \in Grp \land A \in X \land (M \in ℤ \land N \in ℤ)) \to ((M \underset{˙}{\cdot} A) -_{G} (N \underset{˙}{\cdot} A) = \underset{˙}{0} \leftrightarrow M \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A)$
22	7 15 21	3bitrd	$⊢ (G \in Grp \land A \in X \land (M \in ℤ \land N \in ℤ)) \to (O (A) ∥ (M - N) \leftrightarrow M \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A)$

Metamath Proof Explorer

Theorem odcong

Proof