subresre

Description: Subtraction restricted to the reals. (Contributed by SN, 5-May-2024)

		Ref	Expression
	Assertion	subresre	$⊢ -_{ℝ} = {- ↾}_{ℝ^{2}}$

Step	Hyp	Ref	Expression
1		resubeqsub	$⊢ (x \in ℝ \land y \in ℝ) \to x -_{ℝ} y = x - y$
2	1	3adant1	$⊢ (⊤ \land x \in ℝ \land y \in ℝ) \to x -_{ℝ} y = x - y$
3		ax-resscn	$⊢ ℝ \subseteq ℂ$
4	3	a1i	$⊢ ⊤ \to ℝ \subseteq ℂ$
5		resubf	$⊢ -_{ℝ} : ℝ^{2} ⟶ ℝ$
6	5	a1i	$⊢ ⊤ \to -_{ℝ} : ℝ^{2} ⟶ ℝ$
7		sn-subf	$⊢ - : ℂ \times ℂ ⟶ ℂ$
8	7	a1i	$⊢ ⊤ \to - : ℂ \times ℂ ⟶ ℂ$
9	2 4 6 8	oprres	$⊢ ⊤ \to -_{ℝ} = {- ↾}_{ℝ^{2}}$
10	9	mptru	$⊢ -_{ℝ} = {- ↾}_{ℝ^{2}}$

Metamath Proof Explorer