Metamath Proof Explorer

Theorem odmulgid

Description: A relationship between the order of a multiple and the order of the basepoint. (Contributed by Stefan O'Rear, 6-Sep-2015)

		Ref	Expression
	Hypotheses	odmulgid.1	$⊢ X = {Base}_{G}$
		odmulgid.2	$⊢ O = od (G)$
		odmulgid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	Assertion	odmulgid	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land K \in ℤ) \to (O (N \underset{˙}{\cdot} A) ∥ K \leftrightarrow O (A) ∥ K \cdot N)$

Proof

Step	Hyp	Ref	Expression
1		odmulgid.1	$⊢ X = {Base}_{G}$
2		odmulgid.2	$⊢ O = od (G)$
3		odmulgid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		simpl1	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land K \in ℤ) \to G \in Grp$
5		simpr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land K \in ℤ) \to K \in ℤ$
6		simpl3	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land K \in ℤ) \to N \in ℤ$
7		simpl2	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land K \in ℤ) \to A \in X$
8	1 3	mulgass	$⊢ (G \in Grp \land (K \in ℤ \land N \in ℤ \land A \in X)) \to K \cdot N \underset{˙}{\cdot} A = K \underset{˙}{\cdot} (N \underset{˙}{\cdot} A)$
9	4 5 6 7 8	syl13anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land K \in ℤ) \to K \cdot N \underset{˙}{\cdot} A = K \underset{˙}{\cdot} (N \underset{˙}{\cdot} A)$
10	9	eqeq1d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land K \in ℤ) \to (K \cdot N \underset{˙}{\cdot} A = 0_{G} \leftrightarrow K \underset{˙}{\cdot} (N \underset{˙}{\cdot} A) = 0_{G})$
11	5 6	zmulcld	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land K \in ℤ) \to K \cdot N \in ℤ$
12		eqid	$⊢ 0_{G} = 0_{G}$
13	1 2 3 12	oddvds	$⊢ (G \in Grp \land A \in X \land K \cdot N \in ℤ) \to (O (A) ∥ K \cdot N \leftrightarrow K \cdot N \underset{˙}{\cdot} A = 0_{G})$
14	4 7 11 13	syl3anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land K \in ℤ) \to (O (A) ∥ K \cdot N \leftrightarrow K \cdot N \underset{˙}{\cdot} A = 0_{G})$
15	1 3	mulgcl	$⊢ (G \in Grp \land N \in ℤ \land A \in X) \to N \underset{˙}{\cdot} A \in X$
16	4 6 7 15	syl3anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land K \in ℤ) \to N \underset{˙}{\cdot} A \in X$
17	1 2 3 12	oddvds	$⊢ (G \in Grp \land N \underset{˙}{\cdot} A \in X \land K \in ℤ) \to (O (N \underset{˙}{\cdot} A) ∥ K \leftrightarrow K \underset{˙}{\cdot} (N \underset{˙}{\cdot} A) = 0_{G})$
18	4 16 5 17	syl3anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land K \in ℤ) \to (O (N \underset{˙}{\cdot} A) ∥ K \leftrightarrow K \underset{˙}{\cdot} (N \underset{˙}{\cdot} A) = 0_{G})$
19	10 14 18	3bitr4rd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land K \in ℤ) \to (O (N \underset{˙}{\cdot} A) ∥ K \leftrightarrow O (A) ∥ K \cdot N)$