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 𝑄 = ( ℂflds ℚ )
Assertion qrngneg ( 𝑋 ∈ ℚ → ( ( invg𝑄 ) ‘ 𝑋 ) = - 𝑋 )

Proof

Step Hyp Ref Expression
1 qrng.q 𝑄 = ( ℂflds ℚ )
2 qsubdrg ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂflds ℚ ) ∈ DivRing )
3 2 simpli ℚ ∈ ( SubRing ‘ ℂfld )
4 subrgsubg ( ℚ ∈ ( SubRing ‘ ℂfld ) → ℚ ∈ ( SubGrp ‘ ℂfld ) )
5 3 4 ax-mp ℚ ∈ ( SubGrp ‘ ℂfld )
6 eqid ( invg ‘ ℂfld ) = ( invg ‘ ℂfld )
7 eqid ( invg𝑄 ) = ( invg𝑄 )
8 1 6 7 subginv ( ( ℚ ∈ ( SubGrp ‘ ℂfld ) ∧ 𝑋 ∈ ℚ ) → ( ( invg ‘ ℂfld ) ‘ 𝑋 ) = ( ( invg𝑄 ) ‘ 𝑋 ) )
9 5 8 mpan ( 𝑋 ∈ ℚ → ( ( invg ‘ ℂfld ) ‘ 𝑋 ) = ( ( invg𝑄 ) ‘ 𝑋 ) )
10 qcn ( 𝑋 ∈ ℚ → 𝑋 ∈ ℂ )
11 cnfldneg ( 𝑋 ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ 𝑋 ) = - 𝑋 )
12 10 11 syl ( 𝑋 ∈ ℚ → ( ( invg ‘ ℂfld ) ‘ 𝑋 ) = - 𝑋 )
13 9 12 eqtr3d ( 𝑋 ∈ ℚ → ( ( invg𝑄 ) ‘ 𝑋 ) = - 𝑋 )