Theorem subresre

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

	Ref	Expression
Assertion	subresre	⊢ −ℝ = ( − ↾ ( ℝ × ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		resubeqsub	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 −ℝ 𝑦 ) = ( 𝑥 − 𝑦 ) )
2	1	3adant1	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 −ℝ 𝑦 ) = ( 𝑥 − 𝑦 ) )
3		ax-resscn	⊢ ℝ ⊆ ℂ
4	3	a1i	⊢ ( ⊤ → ℝ ⊆ ℂ )
5		resubf	⊢ −ℝ : ( ℝ × ℝ ) ⟶ ℝ
6	5	a1i	⊢ ( ⊤ → −ℝ : ( ℝ × ℝ ) ⟶ ℝ )
7		sn-subf	⊢ − : ( ℂ × ℂ ) ⟶ ℂ
8	7	a1i	⊢ ( ⊤ → − : ( ℂ × ℂ ) ⟶ ℂ )
9	2 4 6 8	oprres	⊢ ( ⊤ → −ℝ = ( − ↾ ( ℝ × ℝ ) ) )
10	9	mptru	⊢ −ℝ = ( − ↾ ( ℝ × ℝ ) )