Theorem cnfldneg

Description: The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014)

	Ref	Expression
Assertion	cnfldneg	⊢ ( 𝑋 ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ 𝑋 ) = - 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		negid	⊢ ( 𝑋 ∈ ℂ → ( 𝑋 + - 𝑋 ) = 0 )
2		negcl	⊢ ( 𝑋 ∈ ℂ → - 𝑋 ∈ ℂ )
3		cnring	⊢ ℂfld ∈ Ring
4		ringgrp	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Grp )
5	3 4	ax-mp	⊢ ℂfld ∈ Grp
6		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
7		cnfldadd	⊢ + = ( +g ‘ ℂfld )
8		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
9		eqid	⊢ ( invg ‘ ℂfld ) = ( invg ‘ ℂfld )
10	6 7 8 9	grpinvid1	⊢ ( ( ℂfld ∈ Grp ∧ 𝑋 ∈ ℂ ∧ - 𝑋 ∈ ℂ ) → ( ( ( invg ‘ ℂfld ) ‘ 𝑋 ) = - 𝑋 ↔ ( 𝑋 + - 𝑋 ) = 0 ) )
11	5 10	mp3an1	⊢ ( ( 𝑋 ∈ ℂ ∧ - 𝑋 ∈ ℂ ) → ( ( ( invg ‘ ℂfld ) ‘ 𝑋 ) = - 𝑋 ↔ ( 𝑋 + - 𝑋 ) = 0 ) )
12	2 11	mpdan	⊢ ( 𝑋 ∈ ℂ → ( ( ( invg ‘ ℂfld ) ‘ 𝑋 ) = - 𝑋 ↔ ( 𝑋 + - 𝑋 ) = 0 ) )
13	1 12	mpbird	⊢ ( 𝑋 ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ 𝑋 ) = - 𝑋 )