Metamath Proof Explorer

Theorem mdegldg

Description: A nonzero polynomial has some coefficient which witnesses its degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses mdegval.d ⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
mdegval.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mdegval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
mdegval.z ⊢ 0 = ( 0g ‘ 𝑅 )
mdegval.a ⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ Fin }
mdegval.h ⊢ 𝐻 = ( ℎ ∈ 𝐴 ↦ ( ℂfld Σg ℎ ) )
mdegldg.y ⊢ 𝑌 = ( 0g ‘ 𝑃 )
Assertion mdegldg ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ∃ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ( 𝐻 ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 mdegval.d ⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
2 mdegval.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3 mdegval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 mdegval.z ⊢ 0 = ( 0g ‘ 𝑅 )
5 mdegval.a ⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ Fin }
6 mdegval.h ⊢ 𝐻 = ( ℎ ∈ 𝐴 ↦ ( ℂfld Σg ℎ ) )
7 mdegldg.y ⊢ 𝑌 = ( 0g ‘ 𝑃 )
8 1 2 3 4 5 6 mdegval ⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) = sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) )
9 8 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( 𝐷 ‘ 𝐹 ) = sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) )
10 5 6 tdeglem1 ⊢ 𝐻 : 𝐴 ⟶ ℕ0
11 10 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → 𝐻 : 𝐴 ⟶ ℕ0 )
12 11 ffund ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → Fun 𝐻 )
13 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → 𝐹 ∈ 𝐵 )
14 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → 𝑅 ∈ Ring )
15 2 3 4 13 14 mplelsfi ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → 𝐹 finSupp 0 )
16 15 fsuppimpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( 𝐹 supp 0 ) ∈ Fin )
17 imafi ⊢ ( ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ∈ Fin ) → ( 𝐻 “ ( 𝐹 supp 0 ) ) ∈ Fin )
18 12 16 17 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( 𝐻 “ ( 𝐹 supp 0 ) ) ∈ Fin )
19 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → 𝐹 ≠ 𝑌 )
20 2 3 mplrcl ⊢ ( 𝐹 ∈ 𝐵 → 𝐼 ∈ V )
21 20 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → 𝐼 ∈ V )
22 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
23 22 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → 𝑅 ∈ Grp )
24 2 5 4 7 21 23 mpl0 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → 𝑌 = ( 𝐴 × { 0 } ) )
25 19 24 neeqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → 𝐹 ≠ ( 𝐴 × { 0 } ) )
26 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
27 2 26 3 5 13 mplelf ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → 𝐹 : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
28 27 ffnd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → 𝐹 Fn 𝐴 )
29 4 fvexi ⊢ 0 ∈ V
30 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
31 5 30 rabex2 ⊢ 𝐴 ∈ V
32 fnsuppeq0 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 supp 0 ) = ∅ ↔ 𝐹 = ( 𝐴 × { 0 } ) ) )
33 31 32 mp3an2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 0 ∈ V ) → ( ( 𝐹 supp 0 ) = ∅ ↔ 𝐹 = ( 𝐴 × { 0 } ) ) )
34 28 29 33 sylancl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( ( 𝐹 supp 0 ) = ∅ ↔ 𝐹 = ( 𝐴 × { 0 } ) ) )
35 34 necon3bid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( ( 𝐹 supp 0 ) ≠ ∅ ↔ 𝐹 ≠ ( 𝐴 × { 0 } ) ) )
36 25 35 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( 𝐹 supp 0 ) ≠ ∅ )
37 11 ffnd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → 𝐻 Fn 𝐴 )
38 suppssdm ⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
39 38 27 fssdm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( 𝐹 supp 0 ) ⊆ 𝐴 )
40 fnimaeq0 ⊢ ( ( 𝐻 Fn 𝐴 ∧ ( 𝐹 supp 0 ) ⊆ 𝐴 ) → ( ( 𝐻 “ ( 𝐹 supp 0 ) ) = ∅ ↔ ( 𝐹 supp 0 ) = ∅ ) )
41 37 39 40 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( ( 𝐻 “ ( 𝐹 supp 0 ) ) = ∅ ↔ ( 𝐹 supp 0 ) = ∅ ) )
42 41 necon3bid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( ( 𝐻 “ ( 𝐹 supp 0 ) ) ≠ ∅ ↔ ( 𝐹 supp 0 ) ≠ ∅ ) )
43 36 42 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( 𝐻 “ ( 𝐹 supp 0 ) ) ≠ ∅ )
44 imassrn ⊢ ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ran 𝐻
45 11 frnd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ran 𝐻 ⊆ ℕ0 )
46 44 45 sstrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ℕ0 )
47 nn0ssre ⊢ ℕ0 ⊆ ℝ
48 ressxr ⊢ ℝ ⊆ ℝ*
49 47 48 sstri ⊢ ℕ0 ⊆ ℝ*
50 46 49 sstrdi ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ℝ* )
51 xrltso ⊢ < Or ℝ*
52 fisupcl ⊢ ( ( < Or ℝ* ∧ ( ( 𝐻 “ ( 𝐹 supp 0 ) ) ∈ Fin ∧ ( 𝐻 “ ( 𝐹 supp 0 ) ) ≠ ∅ ∧ ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ℝ* ) ) → sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) )
53 51 52 mpan ⊢ ( ( ( 𝐻 “ ( 𝐹 supp 0 ) ) ∈ Fin ∧ ( 𝐻 “ ( 𝐹 supp 0 ) ) ≠ ∅ ∧ ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ℝ* ) → sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) )
54 18 43 50 53 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) )
55 9 54 eqeltrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( 𝐷 ‘ 𝐹 ) ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) )
56 37 39 fvelimabd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) ↔ ∃ 𝑥 ∈ ( 𝐹 supp 0 ) ( 𝐻 ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) ) )
57 rexsupp ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V ) → ( ∃ 𝑥 ∈ ( 𝐹 supp 0 ) ( 𝐻 ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) ↔ ∃ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ( 𝐻 ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) ) ) )
58 31 29 57 mp3an23 ⊢ ( 𝐹 Fn 𝐴 → ( ∃ 𝑥 ∈ ( 𝐹 supp 0 ) ( 𝐻 ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) ↔ ∃ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ( 𝐻 ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) ) ) )
59 28 58 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( ∃ 𝑥 ∈ ( 𝐹 supp 0 ) ( 𝐻 ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) ↔ ∃ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ( 𝐻 ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) ) ) )
60 56 59 bitrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ( 𝐻 ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) ) ) )
61 55 60 mpbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌 ) → ∃ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ( 𝐻 ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) ) )