Theorem resdvopclptsd

Description: Restrict derivative on unit interval. (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypotheses	resdvopclptsd.1	|- ( ph -> ( CC _D ( x e. CC |-> A ) ) = ( x e. CC |-> B ) )
	resdvopclptsd.2	|- ( ( ph /\ x e. CC ) -> A e. CC )
	resdvopclptsd.3	|- ( ( ph /\ x e. CC ) -> B e. CC )
Assertion	resdvopclptsd	|- ( ph -> ( RR _D ( x e. ( 0 [,] 1 ) |-> A ) ) = ( x e. ( 0 (,) 1 ) |-> B ) )

Proof

Step	Hyp	Ref	Expression
1		resdvopclptsd.1	|- ( ph -> ( CC _D ( x e. CC |-> A ) ) = ( x e. CC |-> B ) )
2		resdvopclptsd.2	|- ( ( ph /\ x e. CC ) -> A e. CC )
3		resdvopclptsd.3	|- ( ( ph /\ x e. CC ) -> B e. CC )
4		eqid	|- ( x e. CC |-> A ) = ( x e. CC |-> A )
5		0red	|- ( ph -> 0 e. RR )
6		1red	|- ( ph -> 1 e. RR )
7	4 2 1 3 5 6	dvmptresicc	|- ( ph -> ( RR _D ( x e. ( 0 [,] 1 ) |-> A ) ) = ( x e. ( 0 (,) 1 ) |-> B ) )