Metamath Proof Explorer

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 mulid2d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 1 · ( 𝑂 ‘ ( 𝐼 ‘ 𝐴 ) ) ) = ( 𝑂 ‘ ( 𝐼 ‘ 𝐴 ) ) )
27 7 21 26 3eqtrrd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ ( 𝐼 ‘ 𝐴 ) ) = ( 𝑂 ‘ 𝐴 ) )