Theorem qrngneg

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

	Ref	Expression
Hypothesis	qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
Assertion	qrngneg	⊢ ( 𝑋 ∈ ℚ → ( ( invg ‘ 𝑄 ) ‘ 𝑋 ) = - 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
2		qsubdrg	⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ 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 ‘ 𝑄 ) ‘ 𝑋 ) = - 𝑋 )