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

Metamath Proof Explorer

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 ) ‘ 𝑋 ) = - 𝑋 )