resubgval

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

		Ref	Expression
	Hypothesis	resubgval.m	$⊢ \underset{˙}{-} = -_{ℝ_{fld}}$
	Assertion	resubgval	$⊢ (X \in ℝ \land Y \in ℝ) \to X - Y = X \underset{˙}{-} Y$

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

Metamath Proof Explorer