| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mdegval.d | . 2
⊢ 𝐷 = (𝐼 mDeg 𝑅) | 
| 2 |  | oveq12 7441 | . . . . . . . . 9
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑖 mPoly 𝑟) = (𝐼 mPoly 𝑅)) | 
| 3 |  | mdegval.p | . . . . . . . . 9
⊢ 𝑃 = (𝐼 mPoly 𝑅) | 
| 4 | 2, 3 | eqtr4di 2794 | . . . . . . . 8
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑖 mPoly 𝑟) = 𝑃) | 
| 5 | 4 | fveq2d 6909 | . . . . . . 7
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (Base‘(𝑖 mPoly 𝑟)) = (Base‘𝑃)) | 
| 6 |  | mdegval.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝑃) | 
| 7 | 5, 6 | eqtr4di 2794 | . . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (Base‘(𝑖 mPoly 𝑟)) = 𝐵) | 
| 8 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) | 
| 9 |  | mdegval.z | . . . . . . . . . . . 12
⊢  0 =
(0g‘𝑅) | 
| 10 | 8, 9 | eqtr4di 2794 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) | 
| 11 | 10 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (𝑓 supp (0g‘𝑟)) = (𝑓 supp 0 )) | 
| 12 | 11 | mpteq1d 5236 | . . . . . . . . 9
⊢ (𝑟 = 𝑅 → (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)) = (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ))) | 
| 13 | 12 | rneqd 5948 | . . . . . . . 8
⊢ (𝑟 = 𝑅 → ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)) = ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ))) | 
| 14 | 13 | supeq1d 9487 | . . . . . . 7
⊢ (𝑟 = 𝑅 → sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)), ℝ*, < ) = sup(ran
(ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)), ℝ*, <
)) | 
| 15 | 14 | adantl 481 | . . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)), ℝ*, < ) = sup(ran
(ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)), ℝ*, <
)) | 
| 16 | 7, 15 | mpteq12dv 5232 | . . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)), ℝ*, < )) = (𝑓 ∈ 𝐵 ↦ sup(ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)), ℝ*, <
))) | 
| 17 |  | df-mdeg 26095 | . . . . 5
⊢  mDeg =
(𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)), ℝ*, <
))) | 
| 18 | 6 | fvexi 6919 | . . . . . 6
⊢ 𝐵 ∈ V | 
| 19 | 18 | mptex 7244 | . . . . 5
⊢ (𝑓 ∈ 𝐵 ↦ sup(ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)), ℝ*, < )) ∈
V | 
| 20 | 16, 17, 19 | ovmpoa 7589 | . . . 4
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mDeg 𝑅) = (𝑓 ∈ 𝐵 ↦ sup(ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)), ℝ*, <
))) | 
| 21 |  | mdegval.h | . . . . . . . . . 10
⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld
Σg ℎ)) | 
| 22 | 21 | reseq1i 5992 | . . . . . . . . 9
⊢ (𝐻 ↾ (𝑓 supp 0 )) = ((ℎ ∈ 𝐴 ↦ (ℂfld
Σg ℎ)) ↾ (𝑓 supp 0 )) | 
| 23 |  | suppssdm 8203 | . . . . . . . . . . 11
⊢ (𝑓 supp 0 ) ⊆ dom 𝑓 | 
| 24 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 25 |  | mdegval.a | . . . . . . . . . . . 12
⊢ 𝐴 = {𝑚 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑚 “ ℕ) ∈
Fin} | 
| 26 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → 𝑓 ∈ 𝐵) | 
| 27 | 3, 24, 6, 25, 26 | mplelf 22019 | . . . . . . . . . . 11
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → 𝑓:𝐴⟶(Base‘𝑅)) | 
| 28 | 23, 27 | fssdm 6754 | . . . . . . . . . 10
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → (𝑓 supp 0 ) ⊆ 𝐴) | 
| 29 | 28 | resmptd 6057 | . . . . . . . . 9
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → ((ℎ ∈ 𝐴 ↦ (ℂfld
Σg ℎ)) ↾ (𝑓 supp 0 )) = (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ))) | 
| 30 | 22, 29 | eqtr2id 2789 | . . . . . . . 8
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)) = (𝐻 ↾ (𝑓 supp 0 ))) | 
| 31 | 30 | rneqd 5948 | . . . . . . 7
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)) = ran (𝐻 ↾ (𝑓 supp 0 ))) | 
| 32 |  | df-ima 5697 | . . . . . . 7
⊢ (𝐻 “ (𝑓 supp 0 )) = ran (𝐻 ↾ (𝑓 supp 0 )) | 
| 33 | 31, 32 | eqtr4di 2794 | . . . . . 6
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)) = (𝐻 “ (𝑓 supp 0 ))) | 
| 34 | 33 | supeq1d 9487 | . . . . 5
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → sup(ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)), ℝ*, < ) = sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< )) | 
| 35 | 34 | mpteq2dva 5241 | . . . 4
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝑓 ∈ 𝐵 ↦ sup(ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)), ℝ*, < )) = (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< ))) | 
| 36 | 20, 35 | eqtrd 2776 | . . 3
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mDeg 𝑅) = (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< ))) | 
| 37 |  | reldmmdeg 26097 | . . . . . 6
⊢ Rel dom
mDeg | 
| 38 | 37 | ovprc 7470 | . . . . 5
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mDeg 𝑅) = ∅) | 
| 39 |  | mpt0 6709 | . . . . 5
⊢ (𝑓 ∈ ∅ ↦
sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< )) = ∅ | 
| 40 | 38, 39 | eqtr4di 2794 | . . . 4
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mDeg 𝑅) = (𝑓 ∈ ∅ ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< ))) | 
| 41 |  | reldmmpl 22009 | . . . . . . . . 9
⊢ Rel dom
mPoly | 
| 42 | 41 | ovprc 7470 | . . . . . . . 8
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mPoly 𝑅) = ∅) | 
| 43 | 3, 42 | eqtrid 2788 | . . . . . . 7
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑃 = ∅) | 
| 44 | 43 | fveq2d 6909 | . . . . . 6
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) →
(Base‘𝑃) =
(Base‘∅)) | 
| 45 |  | base0 17253 | . . . . . 6
⊢ ∅ =
(Base‘∅) | 
| 46 | 44, 6, 45 | 3eqtr4g 2801 | . . . . 5
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝐵 = ∅) | 
| 47 | 46 | mpteq1d 5236 | . . . 4
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< )) = (𝑓 ∈ ∅
↦ sup((𝐻 “
(𝑓 supp 0 )), ℝ*,
< ))) | 
| 48 | 40, 47 | eqtr4d 2779 | . . 3
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mDeg 𝑅) = (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< ))) | 
| 49 | 36, 48 | pm2.61i 182 | . 2
⊢ (𝐼 mDeg 𝑅) = (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< )) | 
| 50 | 1, 49 | eqtri 2764 | 1
⊢ 𝐷 = (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< )) |