Theorem resubgval

Description: Subtraction in the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019)

	Ref	Expression
Hypothesis	resubgval.m	$$⊢\underset{\dot{}}{-}={-}_{{ℝ}_{\mathrm{fld}}}$$
Assertion	resubgval	$$⊢\left(X\in ℝ\wedge Y\in ℝ\right)\to X-Y=X\underset{\dot{}}{-}Y$$

Proof

Step	Hyp	Ref	Expression
1		resubgval.m	$$⊢\underset{\dot{}}{-}={-}_{{ℝ}_{\mathrm{fld}}}$$
2		resubdrg	$$⊢\left(ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\right)$$
3	2	simpli	$$⊢ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
4		subrgsubg	$$⊢ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to ℝ\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
5	3 4	ax-mp	$$⊢ℝ\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
6		cnfldsub	$$⊢-={-}_{{ℂ}_{\mathrm{fld}}}$$
7		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
8	6 7 1	subgsub	$$⊢\left(ℝ\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge X\in ℝ\wedge Y\in ℝ\right)\to X-Y=X\underset{\dot{}}{-}Y$$
9	5 8	mp3an1	$$⊢\left(X\in ℝ\wedge Y\in ℝ\right)\to X-Y=X\underset{\dot{}}{-}Y$$