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 𝐴 = { 𝑚 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑚 “ ℕ ) ∈ 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 𝐴 = { 𝑚 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑚 “ ℕ ) ∈ 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 2 3 4 13 mplelsfi ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → 𝐹 finSupp 0 )
15 14 fsuppimpd ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( 𝐹 supp 0 ) ∈ Fin )
16 imafi ( ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ∈ Fin ) → ( 𝐻 “ ( 𝐹 supp 0 ) ) ∈ Fin )
17 12 15 16 syl2anc ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( 𝐻 “ ( 𝐹 supp 0 ) ) ∈ Fin )
18 simp3 ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → 𝐹𝑌 )
19 2 3 mplrcl ( 𝐹𝐵𝐼 ∈ V )
20 19 3ad2ant2 ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → 𝐼 ∈ V )
21 ringgrp ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
22 21 3ad2ant1 ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → 𝑅 ∈ Grp )
23 2 5 4 7 20 22 mpl0 ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → 𝑌 = ( 𝐴 × { 0 } ) )
24 18 23 neeqtrd ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → 𝐹 ≠ ( 𝐴 × { 0 } ) )
25 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
26 2 25 3 5 13 mplelf ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → 𝐹 : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
27 26 ffnd ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → 𝐹 Fn 𝐴 )
28 4 fvexi 0 ∈ V
29 ovex ( ℕ0m 𝐼 ) ∈ V
30 5 29 rabex2 𝐴 ∈ V
31 fnsuppeq0 ( ( 𝐹 Fn 𝐴𝐴 ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 supp 0 ) = ∅ ↔ 𝐹 = ( 𝐴 × { 0 } ) ) )
32 30 31 mp3an2 ( ( 𝐹 Fn 𝐴0 ∈ V ) → ( ( 𝐹 supp 0 ) = ∅ ↔ 𝐹 = ( 𝐴 × { 0 } ) ) )
33 27 28 32 sylancl ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( ( 𝐹 supp 0 ) = ∅ ↔ 𝐹 = ( 𝐴 × { 0 } ) ) )
34 33 necon3bid ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( ( 𝐹 supp 0 ) ≠ ∅ ↔ 𝐹 ≠ ( 𝐴 × { 0 } ) ) )
35 24 34 mpbird ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( 𝐹 supp 0 ) ≠ ∅ )
36 11 ffnd ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → 𝐻 Fn 𝐴 )
37 suppssdm ( 𝐹 supp 0 ) ⊆ dom 𝐹
38 37 26 fssdm ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( 𝐹 supp 0 ) ⊆ 𝐴 )
39 fnimaeq0 ( ( 𝐻 Fn 𝐴 ∧ ( 𝐹 supp 0 ) ⊆ 𝐴 ) → ( ( 𝐻 “ ( 𝐹 supp 0 ) ) = ∅ ↔ ( 𝐹 supp 0 ) = ∅ ) )
40 36 38 39 syl2anc ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( ( 𝐻 “ ( 𝐹 supp 0 ) ) = ∅ ↔ ( 𝐹 supp 0 ) = ∅ ) )
41 40 necon3bid ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( ( 𝐻 “ ( 𝐹 supp 0 ) ) ≠ ∅ ↔ ( 𝐹 supp 0 ) ≠ ∅ ) )
42 35 41 mpbird ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( 𝐻 “ ( 𝐹 supp 0 ) ) ≠ ∅ )
43 imassrn ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ran 𝐻
44 11 frnd ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ran 𝐻 ⊆ ℕ0 )
45 43 44 sstrid ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ℕ0 )
46 nn0ssre 0 ⊆ ℝ
47 ressxr ℝ ⊆ ℝ*
48 46 47 sstri 0 ⊆ ℝ*
49 45 48 sstrdi ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ℝ* )
50 xrltso < Or ℝ*
51 fisupcl ( ( < Or ℝ* ∧ ( ( 𝐻 “ ( 𝐹 supp 0 ) ) ∈ Fin ∧ ( 𝐻 “ ( 𝐹 supp 0 ) ) ≠ ∅ ∧ ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ℝ* ) ) → sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) )
52 50 51 mpan ( ( ( 𝐻 “ ( 𝐹 supp 0 ) ) ∈ Fin ∧ ( 𝐻 “ ( 𝐹 supp 0 ) ) ≠ ∅ ∧ ( 𝐻 “ ( 𝐹 supp 0 ) ) ⊆ ℝ* ) → sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) )
53 17 42 49 52 syl3anc ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ* , < ) ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) )
54 9 53 eqeltrd ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( 𝐷𝐹 ) ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) )
55 36 38 fvelimabd ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( ( 𝐷𝐹 ) ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) ↔ ∃ 𝑥 ∈ ( 𝐹 supp 0 ) ( 𝐻𝑥 ) = ( 𝐷𝐹 ) ) )
56 rexsupp ( ( 𝐹 Fn 𝐴𝐴 ∈ V ∧ 0 ∈ V ) → ( ∃ 𝑥 ∈ ( 𝐹 supp 0 ) ( 𝐻𝑥 ) = ( 𝐷𝐹 ) ↔ ∃ 𝑥𝐴 ( ( 𝐹𝑥 ) ≠ 0 ∧ ( 𝐻𝑥 ) = ( 𝐷𝐹 ) ) ) )
57 30 28 56 mp3an23 ( 𝐹 Fn 𝐴 → ( ∃ 𝑥 ∈ ( 𝐹 supp 0 ) ( 𝐻𝑥 ) = ( 𝐷𝐹 ) ↔ ∃ 𝑥𝐴 ( ( 𝐹𝑥 ) ≠ 0 ∧ ( 𝐻𝑥 ) = ( 𝐷𝐹 ) ) ) )
58 27 57 syl ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( ∃ 𝑥 ∈ ( 𝐹 supp 0 ) ( 𝐻𝑥 ) = ( 𝐷𝐹 ) ↔ ∃ 𝑥𝐴 ( ( 𝐹𝑥 ) ≠ 0 ∧ ( 𝐻𝑥 ) = ( 𝐷𝐹 ) ) ) )
59 55 58 bitrd ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ( ( 𝐷𝐹 ) ∈ ( 𝐻 “ ( 𝐹 supp 0 ) ) ↔ ∃ 𝑥𝐴 ( ( 𝐹𝑥 ) ≠ 0 ∧ ( 𝐻𝑥 ) = ( 𝐷𝐹 ) ) ) )
60 54 59 mpbid ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹𝑌 ) → ∃ 𝑥𝐴 ( ( 𝐹𝑥 ) ≠ 0 ∧ ( 𝐻𝑥 ) = ( 𝐷𝐹 ) ) )