odval2

Description: A non-conditional definition of the group order. (Contributed by Stefan O'Rear, 6-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	odval2	$⊢ (G \in Grp \land A \in X) \to O (A) = (ι x \in ℕ_{0} \| \forall y \in ℕ_{0} (x ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}))$

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	1 2	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
6	5	adantl	$⊢ (G \in Grp \land A \in X) \to O (A) \in ℕ_{0}$
7	1 2 3 4	odeq	$⊢ (G \in Grp \land A \in X \land x \in ℕ_{0}) \to (x = O (A) \leftrightarrow \forall y \in ℕ_{0} (x ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}))$
8	7	3expa	$⊢ ((G \in Grp \land A \in X) \land x \in ℕ_{0}) \to (x = O (A) \leftrightarrow \forall y \in ℕ_{0} (x ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}))$
9	8	bicomd	$⊢ ((G \in Grp \land A \in X) \land x \in ℕ_{0}) \to (\forall y \in ℕ_{0} (x ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}) \leftrightarrow x = O (A))$
10	6 9	riota5	$⊢ (G \in Grp \land A \in X) \to (ι x \in ℕ_{0} \| \forall y \in ℕ_{0} (x ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) = O (A)$
11	10	eqcomd	$⊢ (G \in Grp \land A \in X) \to O (A) = (ι x \in ℕ_{0} \| \forall y \in ℕ_{0} (x ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}))$

Metamath Proof Explorer