| 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 | 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 | ⊢ ( ℕ0  ↑m  𝐼 )  ∈  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   ∧  ( 𝐻 ‘ 𝑥 )  =  ( 𝐷 ‘ 𝐹 ) ) ) |