Theorem deg1ldgn

Description: An index at which a polynomial is zero, cannot be its degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	deg1z.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1z.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1z.z	⊢ 0 = ( 0g ‘ 𝑃 )
	deg1nn0cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	deg1ldg.y	⊢ 𝑌 = ( 0g ‘ 𝑅 )
	deg1ldg.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
	deg1ldgn.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	deg1ldgn.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	deg1ldgn.x	⊢ ( 𝜑 → 𝑋 ∈ ℕ0 )
	deg1ldgn.e	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = 𝑌 )
Assertion	deg1ldgn	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≠ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		deg1z.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1z.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1z.z	⊢ 0 = ( 0g ‘ 𝑃 )
4		deg1nn0cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		deg1ldg.y	⊢ 𝑌 = ( 0g ‘ 𝑅 )
6		deg1ldg.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
7		deg1ldgn.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		deg1ldgn.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9		deg1ldgn.x	⊢ ( 𝜑 → 𝑋 ∈ ℕ0 )
10		deg1ldgn.e	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = 𝑌 )
11		fveq2	⊢ ( ( 𝐷 ‘ 𝐹 ) = 𝑋 → ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) = ( 𝐴 ‘ 𝑋 ) )
12	11	adantl	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 𝑋 ) → ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) = ( 𝐴 ‘ 𝑋 ) )
13	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 𝑋 ) → 𝑅 ∈ Ring )
14	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 𝑋 ) → 𝐹 ∈ 𝐵 )
15		eleq1a	⊢ ( 𝑋 ∈ ℕ0 → ( ( 𝐷 ‘ 𝐹 ) = 𝑋 → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) )
16	9 15	syl	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) = 𝑋 → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) )
17	16	imp	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 𝑋 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
18	1 2 3 4	deg1nn0clb	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( 𝐹 ≠ 0 ↔ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) )
19	7 8 18	syl2anc	⊢ ( 𝜑 → ( 𝐹 ≠ 0 ↔ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) )
20	19	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 𝑋 ) → ( 𝐹 ≠ 0 ↔ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) )
21	17 20	mpbird	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 𝑋 ) → 𝐹 ≠ 0 )
22	1 2 3 4 5 6	deg1ldg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ 𝑌 )
23	13 14 21 22	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 𝑋 ) → ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ 𝑌 )
24	12 23	eqnetrrd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = 𝑋 ) → ( 𝐴 ‘ 𝑋 ) ≠ 𝑌 )
25	24	ex	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) = 𝑋 → ( 𝐴 ‘ 𝑋 ) ≠ 𝑌 ) )
26	25	necon2d	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑋 ) = 𝑌 → ( 𝐷 ‘ 𝐹 ) ≠ 𝑋 ) )
27	10 26	mpd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≠ 𝑋 )