Theorem mncn0

Description: A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014)

	Ref	Expression
Assertion	mncn0	⊢ ( 𝑃 ∈ ( Monic ‘ 𝑆 ) → 𝑃 ≠ 0𝑝 )

Proof

Step	Hyp	Ref	Expression
1		mnccoe	⊢ ( 𝑃 ∈ ( Monic ‘ 𝑆 ) → ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = 1 )
2		coe0	⊢ ( coeff ‘ 0𝑝 ) = ( ℕ0 × { 0 } )
3	2	fveq1i	⊢ ( ( coeff ‘ 0𝑝 ) ‘ ( deg ‘ 0𝑝 ) ) = ( ( ℕ0 × { 0 } ) ‘ ( deg ‘ 0𝑝 ) )
4		dgr0	⊢ ( deg ‘ 0𝑝 ) = 0
5		0nn0	⊢ 0 ∈ ℕ0
6	4 5	eqeltri	⊢ ( deg ‘ 0𝑝 ) ∈ ℕ0
7		c0ex	⊢ 0 ∈ V
8	7	fvconst2	⊢ ( ( deg ‘ 0𝑝 ) ∈ ℕ0 → ( ( ℕ0 × { 0 } ) ‘ ( deg ‘ 0𝑝 ) ) = 0 )
9	6 8	ax-mp	⊢ ( ( ℕ0 × { 0 } ) ‘ ( deg ‘ 0𝑝 ) ) = 0
10	3 9	eqtri	⊢ ( ( coeff ‘ 0𝑝 ) ‘ ( deg ‘ 0𝑝 ) ) = 0
11		0ne1	⊢ 0 ≠ 1
12	10 11	eqnetri	⊢ ( ( coeff ‘ 0𝑝 ) ‘ ( deg ‘ 0𝑝 ) ) ≠ 1
13		fveq2	⊢ ( 𝑃 = 0𝑝 → ( coeff ‘ 𝑃 ) = ( coeff ‘ 0𝑝 ) )
14		fveq2	⊢ ( 𝑃 = 0𝑝 → ( deg ‘ 𝑃 ) = ( deg ‘ 0𝑝 ) )
15	13 14	fveq12d	⊢ ( 𝑃 = 0𝑝 → ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = ( ( coeff ‘ 0𝑝 ) ‘ ( deg ‘ 0𝑝 ) ) )
16	15	neeq1d	⊢ ( 𝑃 = 0𝑝 → ( ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) ≠ 1 ↔ ( ( coeff ‘ 0𝑝 ) ‘ ( deg ‘ 0𝑝 ) ) ≠ 1 ) )
17	12 16	mpbiri	⊢ ( 𝑃 = 0𝑝 → ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) ≠ 1 )
18	17	necon2i	⊢ ( ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = 1 → 𝑃 ≠ 0𝑝 )
19	1 18	syl	⊢ ( 𝑃 ∈ ( Monic ‘ 𝑆 ) → 𝑃 ≠ 0𝑝 )