odinv

Description: The order of the inverse of a group element. (Contributed by Mario Carneiro, 20-Oct-2015)

	Ref	Expression
Hypotheses	odinv.1	$⊢ O = od (G)$
	odinv.2	$⊢ I = {inv}_{g} (G)$
	odinv.3	$⊢ X = {Base}_{G}$
Assertion	odinv	$⊢ (G \in Grp \land A \in X) \to O (I (A)) = O (A)$

Proof

Step	Hyp	Ref	Expression
1		odinv.1	$⊢ O = od (G)$
2		odinv.2	$⊢ I = {inv}_{g} (G)$
3		odinv.3	$⊢ X = {Base}_{G}$
4		neg1z	$⊢ - 1 \in ℤ$
5		eqid	$⊢ \cdot_{G} = \cdot_{G}$
6	3 1 5	odmulg	$⊢ (G \in Grp \land A \in X \land - 1 \in ℤ) \to O (A) = (-1 \gcd O (A)) O (-1 \cdot_{G} A)$
7	4 6	mp3an3	$⊢ (G \in Grp \land A \in X) \to O (A) = (-1 \gcd O (A)) O (-1 \cdot_{G} A)$
8	3 1	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
9	8	adantl	$⊢ (G \in Grp \land A \in X) \to O (A) \in ℕ_{0}$
10	9	nn0zd	$⊢ (G \in Grp \land A \in X) \to O (A) \in ℤ$
11		gcdcom	$⊢ (- 1 \in ℤ \land O (A) \in ℤ) \to -1 \gcd O (A) = O (A) \gcd -1$
12	4 10 11	sylancr	$⊢ (G \in Grp \land A \in X) \to -1 \gcd O (A) = O (A) \gcd -1$
13		1z	$⊢ 1 \in ℤ$
14		gcdneg	$⊢ (O (A) \in ℤ \land 1 \in ℤ) \to O (A) \gcd -1 = O (A) \gcd 1$
15	10 13 14	sylancl	$⊢ (G \in Grp \land A \in X) \to O (A) \gcd -1 = O (A) \gcd 1$
16		gcd1	$⊢ O (A) \in ℤ \to O (A) \gcd 1 = 1$
17	10 16	syl	$⊢ (G \in Grp \land A \in X) \to O (A) \gcd 1 = 1$
18	12 15 17	3eqtrd	$⊢ (G \in Grp \land A \in X) \to -1 \gcd O (A) = 1$
19	3 5 2	mulgm1	$⊢ (G \in Grp \land A \in X) \to -1 \cdot_{G} A = I (A)$
20	19	fveq2d	$⊢ (G \in Grp \land A \in X) \to O (-1 \cdot_{G} A) = O (I (A))$
21	18 20	oveq12d	$⊢ (G \in Grp \land A \in X) \to (-1 \gcd O (A)) O (-1 \cdot_{G} A) = 1 O (I (A))$
22	3 2	grpinvcl	$⊢ (G \in Grp \land A \in X) \to I (A) \in X$
23	3 1	odcl	$⊢ I (A) \in X \to O (I (A)) \in ℕ_{0}$
24	22 23	syl	$⊢ (G \in Grp \land A \in X) \to O (I (A)) \in ℕ_{0}$
25	24	nn0cnd	$⊢ (G \in Grp \land A \in X) \to O (I (A)) \in ℂ$
26	25	mullidd	$⊢ (G \in Grp \land A \in X) \to 1 O (I (A)) = O (I (A))$
27	7 21 26	3eqtrrd	$⊢ (G \in Grp \land A \in X) \to O (I (A)) = O (A)$

Metamath Proof Explorer

Theorem odinv

Proof