Theorem resdvopclptsd

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

	Ref	Expression
Hypotheses	resdvopclptsd.1	⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ 𝐴 ) ) = ( 𝑥 ∈ ℂ ↦ 𝐵 ) )
	resdvopclptsd.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐴 ∈ ℂ )
	resdvopclptsd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐵 ∈ ℂ )
Assertion	resdvopclptsd	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 0 (,) 1 ) ↦ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		resdvopclptsd.1	⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ 𝐴 ) ) = ( 𝑥 ∈ ℂ ↦ 𝐵 ) )
2		resdvopclptsd.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐴 ∈ ℂ )
3		resdvopclptsd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐵 ∈ ℂ )
4		eqid	⊢ ( 𝑥 ∈ ℂ ↦ 𝐴 ) = ( 𝑥 ∈ ℂ ↦ 𝐴 )
5		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
6		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
7	4 2 1 3 5 6	dvmptresicc	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 0 (,) 1 ) ↦ 𝐵 ) )