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 ∈ ℂ → inv g ⁡ ℂ fld ⁡ X = − X

Proof

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