Theorem odinv

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

	Ref	Expression
Hypotheses	odinv.1	⊢ 𝑂 = ( od ‘ 𝐺 )
	odinv.2	⊢ 𝐼 = ( invg ‘ 𝐺 )
	odinv.3	⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion	odinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ ( 𝐼 ‘ 𝐴 ) ) = ( 𝑂 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		odinv.1	⊢ 𝑂 = ( od ‘ 𝐺 )
2		odinv.2	⊢ 𝐼 = ( invg ‘ 𝐺 )
3		odinv.3	⊢ 𝑋 = ( Base ‘ 𝐺 )
4		neg1z	⊢ - 1 ∈ ℤ
5		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
6	3 1 5	odmulg	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ - 1 ∈ ℤ ) → ( 𝑂 ‘ 𝐴 ) = ( ( - 1 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( - 1 ( .g ‘ 𝐺 ) 𝐴 ) ) ) )
7	4 6	mp3an3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) = ( ( - 1 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( - 1 ( .g ‘ 𝐺 ) 𝐴 ) ) ) )
8	3 1	odcl	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
9	8	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
10	9	nn0zd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
11		gcdcom	⊢ ( ( - 1 ∈ ℤ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℤ ) → ( - 1 gcd ( 𝑂 ‘ 𝐴 ) ) = ( ( 𝑂 ‘ 𝐴 ) gcd - 1 ) )
12	4 10 11	sylancr	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( - 1 gcd ( 𝑂 ‘ 𝐴 ) ) = ( ( 𝑂 ‘ 𝐴 ) gcd - 1 ) )
13		1z	⊢ 1 ∈ ℤ
14		gcdneg	⊢ ( ( ( 𝑂 ‘ 𝐴 ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) gcd - 1 ) = ( ( 𝑂 ‘ 𝐴 ) gcd 1 ) )
15	10 13 14	sylancl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) gcd - 1 ) = ( ( 𝑂 ‘ 𝐴 ) gcd 1 ) )
16		gcd1	⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℤ → ( ( 𝑂 ‘ 𝐴 ) gcd 1 ) = 1 )
17	10 16	syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) gcd 1 ) = 1 )
18	12 15 17	3eqtrd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( - 1 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 )
19	3 5 2	mulgm1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( - 1 ( .g ‘ 𝐺 ) 𝐴 ) = ( 𝐼 ‘ 𝐴 ) )
20	19	fveq2d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ ( - 1 ( .g ‘ 𝐺 ) 𝐴 ) ) = ( 𝑂 ‘ ( 𝐼 ‘ 𝐴 ) ) )
21	18 20	oveq12d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( - 1 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( - 1 ( .g ‘ 𝐺 ) 𝐴 ) ) ) = ( 1 · ( 𝑂 ‘ ( 𝐼 ‘ 𝐴 ) ) ) )
22	3 2	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐼 ‘ 𝐴 ) ∈ 𝑋 )
23	3 1	odcl	⊢ ( ( 𝐼 ‘ 𝐴 ) ∈ 𝑋 → ( 𝑂 ‘ ( 𝐼 ‘ 𝐴 ) ) ∈ ℕ0 )
24	22 23	syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ ( 𝐼 ‘ 𝐴 ) ) ∈ ℕ0 )
25	24	nn0cnd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ ( 𝐼 ‘ 𝐴 ) ) ∈ ℂ )
26	25	mullidd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 1 · ( 𝑂 ‘ ( 𝐼 ‘ 𝐴 ) ) ) = ( 𝑂 ‘ ( 𝐼 ‘ 𝐴 ) ) )
27	7 21 26	3eqtrrd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ ( 𝐼 ‘ 𝐴 ) ) = ( 𝑂 ‘ 𝐴 ) )