This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem odid

Description: Any element to the power of its order is the identity. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised 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	odid	$⊢ A \in X \to O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$

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		oveq1	$⊢ O (A) = 0 \to O (A) \underset{˙}{\cdot} A = 0 \underset{˙}{\cdot} A$
6	1 4 3	mulg0	$⊢ A \in X \to 0 \underset{˙}{\cdot} A = \underset{˙}{0}$
7	5 6	sylan9eqr	$⊢ (A \in X \land O (A) = 0) \to O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$
8	7	adantrr	$⊢ (A \in X \land (O (A) = 0 \land \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} = \emptyset)) \to O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$
9		oveq1	$⊢ y = O (A) \to y \underset{˙}{\cdot} A = O (A) \underset{˙}{\cdot} A$
10	9	eqeq1d	$⊢ y = O (A) \to (y \underset{˙}{\cdot} A = \underset{˙}{0} \leftrightarrow O (A) \underset{˙}{\cdot} A = \underset{˙}{0})$
11	10	elrab	$⊢ O (A) \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \leftrightarrow (O (A) \in ℕ \land O (A) \underset{˙}{\cdot} A = \underset{˙}{0})$
12	11	simprbi	$⊢ O (A) \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \to O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$
13	12	adantl	$⊢ (A \in X \land O (A) \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\}) \to O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$
14		eqid	$⊢ \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} = \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\}$
15	1 3 4 2 14	odlem1	$⊢ A \in X \to ((O (A) = 0 \land \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} = \emptyset) \lor O (A) \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\})$
16	8 13 15	mpjaodan	$⊢ A \in X \to O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$