Theorem dvid

Description: Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Assertion	dvid	⊢ ( ℂ D ( I ↾ ℂ ) ) = ( ℂ × { 1 } )

Proof

Step	Hyp	Ref	Expression
1		f1oi	⊢ ( I ↾ ℂ ) : ℂ –1-1-onto→ ℂ
2		f1of	⊢ ( ( I ↾ ℂ ) : ℂ –1-1-onto→ ℂ → ( I ↾ ℂ ) : ℂ ⟶ ℂ )
3	1 2	mp1i	⊢ ( ⊤ → ( I ↾ ℂ ) : ℂ ⟶ ℂ )
4		simp2	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) → 𝑧 ∈ ℂ )
5		simp1	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) → 𝑥 ∈ ℂ )
6	4 5	subcld	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) → ( 𝑧 − 𝑥 ) ∈ ℂ )
7		simp3	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) → 𝑧 ≠ 𝑥 )
8	4 5 7	subne0d	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) → ( 𝑧 − 𝑥 ) ≠ 0 )
9		fvresi	⊢ ( 𝑧 ∈ ℂ → ( ( I ↾ ℂ ) ‘ 𝑧 ) = 𝑧 )
10		fvresi	⊢ ( 𝑥 ∈ ℂ → ( ( I ↾ ℂ ) ‘ 𝑥 ) = 𝑥 )
11	9 10	oveqan12rd	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( ( I ↾ ℂ ) ‘ 𝑧 ) − ( ( I ↾ ℂ ) ‘ 𝑥 ) ) = ( 𝑧 − 𝑥 ) )
12	11	3adant3	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) → ( ( ( I ↾ ℂ ) ‘ 𝑧 ) − ( ( I ↾ ℂ ) ‘ 𝑥 ) ) = ( 𝑧 − 𝑥 ) )
13	6 8 12	diveq1bd	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) → ( ( ( ( I ↾ ℂ ) ‘ 𝑧 ) − ( ( I ↾ ℂ ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) = 1 )
14	13	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → ( ( ( ( I ↾ ℂ ) ‘ 𝑧 ) − ( ( I ↾ ℂ ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) = 1 )
15		ax-1cn	⊢ 1 ∈ ℂ
16	3 14 15	dvidlem	⊢ ( ⊤ → ( ℂ D ( I ↾ ℂ ) ) = ( ℂ × { 1 } ) )
17	16	mptru	⊢ ( ℂ D ( I ↾ ℂ ) ) = ( ℂ × { 1 } )