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 
|- ( X e. CC -> ( ( invg ` CCfld ) ` X ) = -u X )

Proof

Step Hyp Ref Expression
1 negid 
 |-  ( X e. CC -> ( X + -u X ) = 0 )
2 negcl 
 |-  ( X e. CC -> -u X e. CC )
3 cnring 
 |-  CCfld e. Ring
4 ringgrp 
 |-  ( CCfld e. Ring -> CCfld e. Grp )
5 3 4 ax-mp 
 |-  CCfld e. Grp
6 cnfldbas 
 |-  CC = ( Base ` CCfld )
7 cnfldadd 
 |-  + = ( +g ` CCfld )
8 cnfld0 
 |-  0 = ( 0g ` CCfld )
9 eqid 
 |-  ( invg ` CCfld ) = ( invg ` CCfld )
10 6 7 8 9 grpinvid1 
 |-  ( ( CCfld e. Grp /\ X e. CC /\ -u X e. CC ) -> ( ( ( invg ` CCfld ) ` X ) = -u X <-> ( X + -u X ) = 0 ) )
11 5 10 mp3an1 
 |-  ( ( X e. CC /\ -u X e. CC ) -> ( ( ( invg ` CCfld ) ` X ) = -u X <-> ( X + -u X ) = 0 ) )
12 2 11 mpdan 
 |-  ( X e. CC -> ( ( ( invg ` CCfld ) ` X ) = -u X <-> ( X + -u X ) = 0 ) )
13 1 12 mpbird 
 |-  ( X e. CC -> ( ( invg ` CCfld ) ` X ) = -u X )