Step | Hyp | Ref
| Expression |
1 | | mdegval.d |
. 2
⊢ 𝐷 = (𝐼 mDeg 𝑅) |
2 | | oveq12 6558 |
. . . . . . . . 9
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑖 mPoly 𝑟) = (𝐼 mPoly 𝑅)) |
3 | | mdegval.p |
. . . . . . . . 9
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
4 | 2, 3 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑖 mPoly 𝑟) = 𝑃) |
5 | 4 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (Base‘(𝑖 mPoly 𝑟)) = (Base‘𝑃)) |
6 | | mdegval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑃) |
7 | 5, 6 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (Base‘(𝑖 mPoly 𝑟)) = 𝐵) |
8 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
9 | | mdegval.z |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝑅) |
10 | 8, 9 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) |
11 | 10 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (𝑓 supp (0g‘𝑟)) = (𝑓 supp 0 )) |
12 | 11 | mpteq1d 4666 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)) = (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ))) |
13 | 12 | rneqd 5274 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)) = ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ))) |
14 | 13 | supeq1d 8235 |
. . . . . . 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 4663 |
. . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)), ℝ*, < )) = (𝑓 ∈ 𝐵 ↦ sup(ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)), ℝ*, <
))) |
17 | | df-mdeg 23619 |
. . . . 5
⊢ mDeg =
(𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)), ℝ*, <
))) |
18 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝑃)
∈ V |
19 | 6, 18 | eqeltri 2684 |
. . . . . 6
⊢ 𝐵 ∈ V |
20 | 19 | mptex 6390 |
. . . . 5
⊢ (𝑓 ∈ 𝐵 ↦ sup(ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)), ℝ*, < )) ∈
V |
21 | 16, 17, 20 | ovmpt2a 6689 |
. . . 4
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mDeg 𝑅) = (𝑓 ∈ 𝐵 ↦ sup(ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)), ℝ*, <
))) |
22 | | mdegval.h |
. . . . . . . . . 10
⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld
Σg ℎ)) |
23 | 22 | reseq1i 5313 |
. . . . . . . . 9
⊢ (𝐻 ↾ (𝑓 supp 0 )) = ((ℎ ∈ 𝐴 ↦ (ℂfld
Σg ℎ)) ↾ (𝑓 supp 0 )) |
24 | | suppssdm 7195 |
. . . . . . . . . . 11
⊢ (𝑓 supp 0 ) ⊆ dom 𝑓 |
25 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑅) =
(Base‘𝑅) |
26 | | mdegval.a |
. . . . . . . . . . . . 13
⊢ 𝐴 = {𝑚 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑚 “ ℕ) ∈
Fin} |
27 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → 𝑓 ∈ 𝐵) |
28 | 3, 25, 6, 26, 27 | mplelf 19254 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → 𝑓:𝐴⟶(Base‘𝑅)) |
29 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴⟶(Base‘𝑅) → dom 𝑓 = 𝐴) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → dom 𝑓 = 𝐴) |
31 | 24, 30 | syl5sseq 3616 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → (𝑓 supp 0 ) ⊆ 𝐴) |
32 | 31 | resmptd 5371 |
. . . . . . . . 9
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → ((ℎ ∈ 𝐴 ↦ (ℂfld
Σg ℎ)) ↾ (𝑓 supp 0 )) = (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ))) |
33 | 23, 32 | syl5req 2657 |
. . . . . . . 8
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)) = (𝐻 ↾ (𝑓 supp 0 ))) |
34 | 33 | rneqd 5274 |
. . . . . . 7
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)) = ran (𝐻 ↾ (𝑓 supp 0 ))) |
35 | | df-ima 5051 |
. . . . . . 7
⊢ (𝐻 “ (𝑓 supp 0 )) = ran (𝐻 ↾ (𝑓 supp 0 )) |
36 | 34, 35 | syl6eqr 2662 |
. . . . . 6
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)) = (𝐻 “ (𝑓 supp 0 ))) |
37 | 36 | supeq1d 8235 |
. . . . 5
⊢ (((𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑓 ∈ 𝐵) → sup(ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)), ℝ*, < ) = sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< )) |
38 | 37 | mpteq2dva 4672 |
. . . 4
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝑓 ∈ 𝐵 ↦ sup(ran (ℎ ∈ (𝑓 supp 0 ) ↦
(ℂfld Σg ℎ)), ℝ*, < )) = (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< ))) |
39 | 21, 38 | eqtrd 2644 |
. . 3
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mDeg 𝑅) = (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< ))) |
40 | | reldmmdeg 23621 |
. . . . . 6
⊢ Rel dom
mDeg |
41 | 40 | ovprc 6581 |
. . . . 5
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mDeg 𝑅) = ∅) |
42 | | mpt0 5934 |
. . . . 5
⊢ (𝑓 ∈ ∅ ↦
sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< )) = ∅ |
43 | 41, 42 | syl6eqr 2662 |
. . . 4
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mDeg 𝑅) = (𝑓 ∈ ∅ ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< ))) |
44 | | reldmmpl 19248 |
. . . . . . . . 9
⊢ Rel dom
mPoly |
45 | 44 | ovprc 6581 |
. . . . . . . 8
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mPoly 𝑅) = ∅) |
46 | 3, 45 | syl5eq 2656 |
. . . . . . 7
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑃 = ∅) |
47 | 46 | fveq2d 6107 |
. . . . . 6
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) →
(Base‘𝑃) =
(Base‘∅)) |
48 | | base0 15740 |
. . . . . 6
⊢ ∅ =
(Base‘∅) |
49 | 47, 6, 48 | 3eqtr4g 2669 |
. . . . 5
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝐵 = ∅) |
50 | 49 | mpteq1d 4666 |
. . . 4
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< )) = (𝑓 ∈ ∅
↦ sup((𝐻 “
(𝑓 supp 0 )), ℝ*,
< ))) |
51 | 43, 50 | eqtr4d 2647 |
. . 3
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mDeg 𝑅) = (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< ))) |
52 | 39, 51 | pm2.61i 175 |
. 2
⊢ (𝐼 mDeg 𝑅) = (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< )) |
53 | 1, 52 | eqtri 2632 |
1
⊢ 𝐷 = (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*,
< )) |