Metamath Proof Explorer

Theorem qrngneg

Description: The additive inverse in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypothesis qrng.q 
|- Q = ( CCfld |`s QQ )
Assertion qrngneg 
|- ( X e. QQ -> ( ( invg ` Q ) ` X ) = -u X )

Proof

Step Hyp Ref Expression
1 qrng.q 
 |-  Q = ( CCfld |`s QQ )
2 qsubdrg 
 |-  ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing )
3 2 simpli 
 |-  QQ e. ( SubRing ` CCfld )
4 subrgsubg 
 |-  ( QQ e. ( SubRing ` CCfld ) -> QQ e. ( SubGrp ` CCfld ) )
5 3 4 ax-mp 
 |-  QQ e. ( SubGrp ` CCfld )
6 eqid 
 |-  ( invg ` CCfld ) = ( invg ` CCfld )
7 eqid 
 |-  ( invg ` Q ) = ( invg ` Q )
8 1 6 7 subginv 
 |-  ( ( QQ e. ( SubGrp ` CCfld ) /\ X e. QQ ) -> ( ( invg ` CCfld ) ` X ) = ( ( invg ` Q ) ` X ) )
9 5 8 mpan 
 |-  ( X e. QQ -> ( ( invg ` CCfld ) ` X ) = ( ( invg ` Q ) ` X ) )
10 qcn 
 |-  ( X e. QQ -> X e. CC )
11 cnfldneg 
 |-  ( X e. CC -> ( ( invg ` CCfld ) ` X ) = -u X )
12 10 11 syl 
 |-  ( X e. QQ -> ( ( invg ` CCfld ) ` X ) = -u X )
13 9 12 eqtr3d 
 |-  ( X e. QQ -> ( ( invg ` Q ) ` X ) = -u X )