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		mulid2	⊢ ( 𝑧 ∈ ℂ → ( 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