This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )