Theorem mulgm1

Description: Group multiple (exponentiation) operation at negative one. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by Mario Carneiro, 20-Dec-2014)

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

Proof

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