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 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )