Theorem subresre

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

	Ref	Expression
Assertion	subresre	|- -R = ( - |` ( RR X. RR ) )

Proof

Step	Hyp	Ref	Expression
1		resubeqsub	|- ( ( x e. RR /\ y e. RR ) -> ( x -R y ) = ( x - y ) )
2	1	3adant1	|- ( ( T. /\ x e. RR /\ y e. RR ) -> ( x -R y ) = ( x - y ) )
3		ax-resscn	|- RR C_ CC
4	3	a1i	|- ( T. -> RR C_ CC )
5		resubf	|- -R : ( RR X. RR ) --> RR
6	5	a1i	|- ( T. -> -R : ( RR X. RR ) --> RR )
7		sn-subf	|- - : ( CC X. CC ) --> CC
8	7	a1i	|- ( T. -> - : ( CC X. CC ) --> CC )
9	2 4 6 8	oprres	|- ( T. -> -R = ( - |` ( RR X. RR ) ) )
10	9	mptru	|- -R = ( - |` ( RR X. RR ) )