Step |
Hyp |
Ref |
Expression |
1 |
|
mdegcl.d |
⊢ 𝐷 = ( 𝐼 mDeg 𝑅 ) |
2 |
|
mdegcl.p |
⊢ 𝑃 = ( 𝐼 mPoly 𝑅 ) |
3 |
|
mdegcl.b |
⊢ 𝐵 = ( Base ‘ 𝑃 ) |
4 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
5 |
|
eqid |
⊢ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } = { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } |
6 |
|
eqid |
⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) |
7 |
1 2 3 4 5 6
|
mdegval |
⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) = sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) ) |
8 |
|
supeq1 |
⊢ ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) = ∅ → sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) = sup ( ∅ , ℝ* , < ) ) |
9 |
8
|
eleq1d |
⊢ ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) = ∅ → ( sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) ∈ ( ℕ0 ∪ { -∞ } ) ↔ sup ( ∅ , ℝ* , < ) ∈ ( ℕ0 ∪ { -∞ } ) ) ) |
10 |
|
imassrn |
⊢ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ⊆ ran ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) |
11 |
5 6
|
tdeglem1 |
⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ℕ0 |
12 |
|
frn |
⊢ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ℕ0 → ran ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ⊆ ℕ0 ) |
13 |
11 12
|
mp1i |
⊢ ( 𝐹 ∈ 𝐵 → ran ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ⊆ ℕ0 ) |
14 |
10 13
|
sstrid |
⊢ ( 𝐹 ∈ 𝐵 → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ⊆ ℕ0 ) |
15 |
14
|
adantr |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ≠ ∅ ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ⊆ ℕ0 ) |
16 |
|
ssun1 |
⊢ ℕ0 ⊆ ( ℕ0 ∪ { -∞ } ) |
17 |
15 16
|
sstrdi |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ≠ ∅ ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ⊆ ( ℕ0 ∪ { -∞ } ) ) |
18 |
|
ffun |
⊢ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ℕ0 → Fun ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ) |
19 |
11 18
|
mp1i |
⊢ ( 𝐹 ∈ 𝐵 → Fun ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ) |
20 |
|
id |
⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ 𝐵 ) |
21 |
|
reldmmpl |
⊢ Rel dom mPoly |
22 |
21 2 3
|
elbasov |
⊢ ( 𝐹 ∈ 𝐵 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) |
23 |
22
|
simprd |
⊢ ( 𝐹 ∈ 𝐵 → 𝑅 ∈ V ) |
24 |
2 3 4 20 23
|
mplelsfi |
⊢ ( 𝐹 ∈ 𝐵 → 𝐹 finSupp ( 0g ‘ 𝑅 ) ) |
25 |
24
|
fsuppimpd |
⊢ ( 𝐹 ∈ 𝐵 → ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ∈ Fin ) |
26 |
|
imafi |
⊢ ( ( Fun ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ∧ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ∈ Fin ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ∈ Fin ) |
27 |
19 25 26
|
syl2anc |
⊢ ( 𝐹 ∈ 𝐵 → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ∈ Fin ) |
28 |
27
|
adantr |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ≠ ∅ ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ∈ Fin ) |
29 |
|
simpr |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ≠ ∅ ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ≠ ∅ ) |
30 |
|
nn0ssre |
⊢ ℕ0 ⊆ ℝ |
31 |
|
ressxr |
⊢ ℝ ⊆ ℝ* |
32 |
30 31
|
sstri |
⊢ ℕ0 ⊆ ℝ* |
33 |
15 32
|
sstrdi |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ≠ ∅ ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ⊆ ℝ* ) |
34 |
|
xrltso |
⊢ < Or ℝ* |
35 |
|
fisupcl |
⊢ ( ( < Or ℝ* ∧ ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ∈ Fin ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ≠ ∅ ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ⊆ ℝ* ) ) → sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) ∈ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) |
36 |
34 35
|
mpan |
⊢ ( ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ∈ Fin ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ≠ ∅ ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ⊆ ℝ* ) → sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) ∈ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) |
37 |
28 29 33 36
|
syl3anc |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ≠ ∅ ) → sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) ∈ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) |
38 |
17 37
|
sseldd |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ≠ ∅ ) → sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) ∈ ( ℕ0 ∪ { -∞ } ) ) |
39 |
|
xrsup0 |
⊢ sup ( ∅ , ℝ* , < ) = -∞ |
40 |
|
ssun2 |
⊢ { -∞ } ⊆ ( ℕ0 ∪ { -∞ } ) |
41 |
|
mnfxr |
⊢ -∞ ∈ ℝ* |
42 |
41
|
elexi |
⊢ -∞ ∈ V |
43 |
42
|
snid |
⊢ -∞ ∈ { -∞ } |
44 |
40 43
|
sselii |
⊢ -∞ ∈ ( ℕ0 ∪ { -∞ } ) |
45 |
39 44
|
eqeltri |
⊢ sup ( ∅ , ℝ* , < ) ∈ ( ℕ0 ∪ { -∞ } ) |
46 |
45
|
a1i |
⊢ ( 𝐹 ∈ 𝐵 → sup ( ∅ , ℝ* , < ) ∈ ( ℕ0 ∪ { -∞ } ) ) |
47 |
9 38 46
|
pm2.61ne |
⊢ ( 𝐹 ∈ 𝐵 → sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) ∈ ( ℕ0 ∪ { -∞ } ) ) |
48 |
7 47
|
eqeltrd |
⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ( ℕ0 ∪ { -∞ } ) ) |