Theorem dvsid

Description: Derivative of the identity function on the real or complex numbers. (Contributed by Steve Rodriguez, 11-Nov-2015)

	Ref	Expression
Assertion	dvsid	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( I ↾ 𝑆 ) ) = ( 𝑆 × { 1 } ) )

Proof

Step	Hyp	Ref	Expression
1		fnresi	⊢ ( I ↾ ℂ ) Fn ℂ
2		rnresi	⊢ ran ( I ↾ ℂ ) = ℂ
3	2	eqimssi	⊢ ran ( I ↾ ℂ ) ⊆ ℂ
4		df-f	⊢ ( ( I ↾ ℂ ) : ℂ ⟶ ℂ ↔ ( ( I ↾ ℂ ) Fn ℂ ∧ ran ( I ↾ ℂ ) ⊆ ℂ ) )
5	1 3 4	mpbir2an	⊢ ( I ↾ ℂ ) : ℂ ⟶ ℂ
6	5	jctr	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 ∈ { ℝ , ℂ } ∧ ( I ↾ ℂ ) : ℂ ⟶ ℂ ) )
7		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
8		dvid	⊢ ( ℂ D ( I ↾ ℂ ) ) = ( ℂ × { 1 } )
9	8	dmeqi	⊢ dom ( ℂ D ( I ↾ ℂ ) ) = dom ( ℂ × { 1 } )
10		1ex	⊢ 1 ∈ V
11	10	fconst	⊢ ( ℂ × { 1 } ) : ℂ ⟶ { 1 }
12	11	fdmi	⊢ dom ( ℂ × { 1 } ) = ℂ
13	9 12	eqtri	⊢ dom ( ℂ D ( I ↾ ℂ ) ) = ℂ
14	7 13	sseqtrrdi	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ dom ( ℂ D ( I ↾ ℂ ) ) )
15		ssid	⊢ ℂ ⊆ ℂ
16	14 15	jctil	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( ℂ ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D ( I ↾ ℂ ) ) ) )
17		dvres3	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ ( I ↾ ℂ ) : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D ( I ↾ ℂ ) ) ) ) → ( 𝑆 D ( ( I ↾ ℂ ) ↾ 𝑆 ) ) = ( ( ℂ D ( I ↾ ℂ ) ) ↾ 𝑆 ) )
18	6 16 17	syl2anc	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( ( I ↾ ℂ ) ↾ 𝑆 ) ) = ( ( ℂ D ( I ↾ ℂ ) ) ↾ 𝑆 ) )
19	7	resabs1d	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( ( I ↾ ℂ ) ↾ 𝑆 ) = ( I ↾ 𝑆 ) )
20	19	oveq2d	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( ( I ↾ ℂ ) ↾ 𝑆 ) ) = ( 𝑆 D ( I ↾ 𝑆 ) ) )
21	8	reseq1i	⊢ ( ( ℂ D ( I ↾ ℂ ) ) ↾ 𝑆 ) = ( ( ℂ × { 1 } ) ↾ 𝑆 )
22		xpssres	⊢ ( 𝑆 ⊆ ℂ → ( ( ℂ × { 1 } ) ↾ 𝑆 ) = ( 𝑆 × { 1 } ) )
23	21 22	syl5eq	⊢ ( 𝑆 ⊆ ℂ → ( ( ℂ D ( I ↾ ℂ ) ) ↾ 𝑆 ) = ( 𝑆 × { 1 } ) )
24	7 23	syl	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( ( ℂ D ( I ↾ ℂ ) ) ↾ 𝑆 ) = ( 𝑆 × { 1 } ) )
25	18 20 24	3eqtr3d	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( I ↾ 𝑆 ) ) = ( 𝑆 × { 1 } ) )