Theorem qrngneg

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

	Ref	Expression
Hypothesis	qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
Assertion	qrngneg	$$⊢X\in \mathbb{Q}\to {inv}_g\left(Q\right)\left(X\right)=-X$$

Proof

Step	Hyp	Ref	Expression
1		qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
2		qsubdrg	$$⊢\left(\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)$$
3	2	simpli	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
4		subrgsubg	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to \mathbb{Q}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
5	3 4	ax-mp	$$⊢\mathbb{Q}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
6		eqid	$$⊢{inv}_g\left({ℂ}_{\mathrm{fld}}\right)={inv}_g\left({ℂ}_{\mathrm{fld}}\right)$$
7		eqid	$$⊢{inv}_g\left(Q\right)={inv}_g\left(Q\right)$$
8	1 6 7	subginv	$$⊢\left(\mathbb{Q}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge X\in \mathbb{Q}\right)\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(X\right)={inv}_g\left(Q\right)\left(X\right)$$
9	5 8	mpan	$$⊢X\in \mathbb{Q}\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(X\right)={inv}_g\left(Q\right)\left(X\right)$$
10		qcn	$$⊢X\in \mathbb{Q}\to X\in ℂ$$
11		cnfldneg	$$⊢X\in ℂ\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(X\right)=-X$$
12	10 11	syl	$$⊢X\in \mathbb{Q}\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(X\right)=-X$$
13	9 12	eqtr3d	$$⊢X\in \mathbb{Q}\to {inv}_g\left(Q\right)\left(X\right)=-X$$