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 
|- O = ( od ` G )
odinv.2 
|- I = ( invg ` G )
odinv.3 
|- X = ( Base ` G )
Assertion odinv 
|- ( ( G e. Grp /\ A e. X ) -> ( O ` ( I ` A ) ) = ( O ` A ) )

Proof

Step Hyp Ref Expression
1 odinv.1 
 |-  O = ( od ` G )
2 odinv.2 
 |-  I = ( invg ` G )
3 odinv.3 
 |-  X = ( Base ` G )
4 neg1z 
 |-  -u 1 e. ZZ
5 eqid 
 |-  ( .g ` G ) = ( .g ` G )
6 3 1 5 odmulg 
 |-  ( ( G e. Grp /\ A e. X /\ -u 1 e. ZZ ) -> ( O ` A ) = ( ( -u 1 gcd ( O ` A ) ) x. ( O ` ( -u 1 ( .g ` G ) A ) ) ) )
7 4 6 mp3an3 
 |-  ( ( G e. Grp /\ A e. X ) -> ( O ` A ) = ( ( -u 1 gcd ( O ` A ) ) x. ( O ` ( -u 1 ( .g ` G ) A ) ) ) )
8 3 1 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
9 8 adantl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( O ` A ) e. NN0 )
10 9 nn0zd 
 |-  ( ( G e. Grp /\ A e. X ) -> ( O ` A ) e. ZZ )
11 gcdcom 
 |-  ( ( -u 1 e. ZZ /\ ( O ` A ) e. ZZ ) -> ( -u 1 gcd ( O ` A ) ) = ( ( O ` A ) gcd -u 1 ) )
12 4 10 11 sylancr 
 |-  ( ( G e. Grp /\ A e. X ) -> ( -u 1 gcd ( O ` A ) ) = ( ( O ` A ) gcd -u 1 ) )
13 1z 
 |-  1 e. ZZ
14 gcdneg 
 |-  ( ( ( O ` A ) e. ZZ /\ 1 e. ZZ ) -> ( ( O ` A ) gcd -u 1 ) = ( ( O ` A ) gcd 1 ) )
15 10 13 14 sylancl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) gcd -u 1 ) = ( ( O ` A ) gcd 1 ) )
16 gcd1 
 |-  ( ( O ` A ) e. ZZ -> ( ( O ` A ) gcd 1 ) = 1 )
17 10 16 syl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) gcd 1 ) = 1 )
18 12 15 17 3eqtrd 
 |-  ( ( G e. Grp /\ A e. X ) -> ( -u 1 gcd ( O ` A ) ) = 1 )
19 3 5 2 mulgm1 
 |-  ( ( G e. Grp /\ A e. X ) -> ( -u 1 ( .g ` G ) A ) = ( I ` A ) )
20 19 fveq2d 
 |-  ( ( G e. Grp /\ A e. X ) -> ( O ` ( -u 1 ( .g ` G ) A ) ) = ( O ` ( I ` A ) ) )
21 18 20 oveq12d 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( -u 1 gcd ( O ` A ) ) x. ( O ` ( -u 1 ( .g ` G ) A ) ) ) = ( 1 x. ( O ` ( I ` A ) ) ) )
22 3 2 grpinvcl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( I ` A ) e. X )
23 3 1 odcl 
 |-  ( ( I ` A ) e. X -> ( O ` ( I ` A ) ) e. NN0 )
24 22 23 syl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( O ` ( I ` A ) ) e. NN0 )
25 24 nn0cnd 
 |-  ( ( G e. Grp /\ A e. X ) -> ( O ` ( I ` A ) ) e. CC )
26 25 mulid2d 
 |-  ( ( G e. Grp /\ A e. X ) -> ( 1 x. ( O ` ( I ` A ) ) ) = ( O ` ( I ` A ) ) )
27 7 21 26 3eqtrrd 
 |-  ( ( G e. Grp /\ A e. X ) -> ( O ` ( I ` A ) ) = ( O ` A ) )