Theorem dgrid

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

	Ref	Expression
Assertion	dgrid	$$⊢\mathrm{deg}\left(X^p\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		ax-1ne0	$$⊢1\ne 0$$
3		1nn0	$$⊢1\in {\mathbb{N}}_0$$
4		mptresid	$$⊢{\mathrm{I}\upharpoonright }_{ℂ}=\left(z\in ℂ⟼z\right)$$
5		df-idp	$$⊢X^p={\mathrm{I}\upharpoonright }_{ℂ}$$
6		exp1	$$⊢z\in ℂ\to z^1=z$$
7	6	oveq2d	$$⊢z\in ℂ\to 1z^1=1z$$
8		mullid	$$⊢z\in ℂ\to 1z=z$$
9	7 8	eqtrd	$$⊢z\in ℂ\to 1z^1=z$$
10	9	mpteq2ia	$$⊢\left(z\in ℂ⟼1z^1\right)=\left(z\in ℂ⟼z\right)$$
11	4 5 10	3eqtr4i	$$⊢X^p=\left(z\in ℂ⟼1z^1\right)$$
12	11	dgr1term	$$⊢\left(1\in ℂ\wedge 1\ne 0\wedge 1\in {\mathbb{N}}_0\right)\to \mathrm{deg}\left(X^p\right)=1$$
13	1 2 3 12	mp3an	$$⊢\mathrm{deg}\left(X^p\right)=1$$