This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulgnegneg

Description: The inverse of a negative group multiple is the positive group multiple. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 30-Aug-2021)

Ref Expression
Hypotheses mulgnncl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgnncl.t ⊢ · = ( .g ‘ 𝐺 )
mulgneg.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion mulgnegneg ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )

Proof

Step Hyp Ref Expression
1 mulgnncl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgnncl.t ⊢ · = ( .g ‘ 𝐺 )
3 mulgneg.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
4 1 2 3 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )
5 4 fveq2d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) = ( 𝐼 ‘ ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) ) )
6 simp1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → 𝐺 ∈ Grp )
7 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
8 1 3 grpinvinv ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) ) = ( 𝑁 · 𝑋 ) )
9 6 7 8 syl2anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) ) = ( 𝑁 · 𝑋 ) )
10 5 9 eqtrd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )