Description: Degree of the zero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | deg1z.d | ⊢ 𝐷 = ( deg1 ‘ 𝑅 ) | |
deg1z.p | ⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) | ||
deg1z.z | ⊢ 0 = ( 0g ‘ 𝑃 ) | ||
Assertion | deg1z | ⊢ ( 𝑅 ∈ Ring → ( 𝐷 ‘ 0 ) = -∞ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | deg1z.d | ⊢ 𝐷 = ( deg1 ‘ 𝑅 ) | |
2 | deg1z.p | ⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) | |
3 | deg1z.z | ⊢ 0 = ( 0g ‘ 𝑃 ) | |
4 | 1on | ⊢ 1o ∈ On | |
5 | 1 | deg1fval | ⊢ 𝐷 = ( 1o mDeg 𝑅 ) |
6 | eqid | ⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 ) | |
7 | 6 2 3 | ply1mpl0 | ⊢ 0 = ( 0g ‘ ( 1o mPoly 𝑅 ) ) |
8 | 5 6 7 | mdeg0 | ⊢ ( ( 1o ∈ On ∧ 𝑅 ∈ Ring ) → ( 𝐷 ‘ 0 ) = -∞ ) |
9 | 4 8 | mpan | ⊢ ( 𝑅 ∈ Ring → ( 𝐷 ‘ 0 ) = -∞ ) |