This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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