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

Metamath Proof Explorer

Theorem dgrid

Description: The degree of the identity function. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Assertion dgrid ( deg ‘ Xp ) = 1

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 ax-1ne0 ⊢ 1 ≠ 0
3 1nn0 ⊢ 1 ∈ ℕ0
4 mptresid ⊢ ( I ↾ ℂ ) = ( 𝑧 ∈ ℂ ↦ 𝑧 )
5 df-idp ⊢ Xp = ( I ↾ ℂ )
6 exp1 ⊢ ( 𝑧 ∈ ℂ → ( 𝑧 ↑ 1 ) = 𝑧 )
7 6 oveq2d ⊢ ( 𝑧 ∈ ℂ → ( 1 · ( 𝑧 ↑ 1 ) ) = ( 1 · 𝑧 ) )
8 mullid ⊢ ( 𝑧 ∈ ℂ → ( 1 · 𝑧 ) = 𝑧 )
9 7 8 eqtrd ⊢ ( 𝑧 ∈ ℂ → ( 1 · ( 𝑧 ↑ 1 ) ) = 𝑧 )
10 9 mpteq2ia ⊢ ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 1 ) ) ) = ( 𝑧 ∈ ℂ ↦ 𝑧 )
11 4 5 10 3eqtr4i ⊢ Xp = ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 1 ) ) )
12 11 dgr1term ⊢ ( ( 1 ∈ ℂ ∧ 1 ≠ 0 ∧ 1 ∈ ℕ0 ) → ( deg ‘ Xp ) = 1 )
13 1 2 3 12 mp3an ⊢ ( deg ‘ Xp ) = 1