Theorem subresre

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

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

Proof

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