Metamath Proof Explorer


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 ( 𝜑 → ( 𝐷𝐹 ) ≠ 𝑋 )