This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ ( 𝐼 ‘ 𝐴 ) ) = ( 𝑂 ‘ 𝐴 ) ) |
| 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 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ ( 𝐼 ‘ 𝐴 ) ) = ( 𝑂 ‘ 𝐴 ) ) |