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 ⁡ X p = 1

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 ax-1ne0 ⊢ 1 ≠ 0
3 1nn0 ⊢ 1 ∈ ℕ 0
4 mptresid ⊢ I ↾ ℂ = z ∈ ℂ ⟼ z
5 df-idp ⊢ X p = I ↾ ℂ
6 exp1 ⊢ z ∈ ℂ → z 1 = z
7 6 oveq2d ⊢ z ∈ ℂ → 1 ⁢ z 1 = 1 ⁢ z
8 mullid ⊢ z ∈ ℂ → 1 ⁢ z = z
9 7 8 eqtrd ⊢ z ∈ ℂ → 1 ⁢ z 1 = z
10 9 mpteq2ia ⊢ z ∈ ℂ ⟼ 1 ⁢ z 1 = z ∈ ℂ ⟼ z
11 4 5 10 3eqtr4i ⊢ X p = z ∈ ℂ ⟼ 1 ⁢ z 1
12 11 dgr1term ⊢ 1 ∈ ℂ ∧ 1 ≠ 0 ∧ 1 ∈ ℕ 0 → deg ⁡ X p = 1
13 1 2 3 12 mp3an ⊢ deg ⁡ X p = 1