Metamath Proof Explorer


Theorem mdegcl

Description: Sharp closure for multivariate polynomials. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses mdegcl.d 𝐷 = ( 𝐼 mDeg 𝑅 )
mdegcl.p 𝑃 = ( 𝐼 mPoly 𝑅 )
mdegcl.b 𝐵 = ( Base ‘ 𝑃 )
Assertion mdegcl ( 𝐹𝐵 → ( 𝐷𝐹 ) ∈ ( ℕ0 ∪ { -∞ } ) )

Proof

Step Hyp Ref Expression
1 mdegcl.d 𝐷 = ( 𝐼 mDeg 𝑅 )
2 mdegcl.p 𝑃 = ( 𝐼 mPoly 𝑅 )
3 mdegcl.b 𝐵 = ( Base ‘ 𝑃 )
4 eqid ( 0g𝑅 ) = ( 0g𝑅 )
5 eqid { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } = { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin }
6 eqid ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) )
7 1 2 3 4 5 6 mdegval ( 𝐹𝐵 → ( 𝐷𝐹 ) = sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) , ℝ* , < ) )
8 supeq1 ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) = ∅ → sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) , ℝ* , < ) = sup ( ∅ , ℝ* , < ) )
9 8 eleq1d ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) = ∅ → ( sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) , ℝ* , < ) ∈ ( ℕ0 ∪ { -∞ } ) ↔ sup ( ∅ , ℝ* , < ) ∈ ( ℕ0 ∪ { -∞ } ) ) )
10 imassrn ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ⊆ ran ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) )
11 5 6 tdeglem1 ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) : { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ⟶ ℕ0
12 frn ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) : { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ⟶ ℕ0 → ran ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ⊆ ℕ0 )
13 11 12 mp1i ( 𝐹𝐵 → ran ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ⊆ ℕ0 )
14 10 13 sstrid ( 𝐹𝐵 → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ⊆ ℕ0 )
15 14 adantr ( ( 𝐹𝐵 ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ≠ ∅ ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ⊆ ℕ0 )
16 ssun1 0 ⊆ ( ℕ0 ∪ { -∞ } )
17 15 16 sstrdi ( ( 𝐹𝐵 ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ≠ ∅ ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ⊆ ( ℕ0 ∪ { -∞ } ) )
18 ffun ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) : { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ⟶ ℕ0 → Fun ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) )
19 11 18 mp1i ( 𝐹𝐵 → Fun ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ 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 ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ∧ ( 𝐹 supp ( 0g𝑅 ) ) ∈ Fin ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ∈ Fin )
27 19 25 26 syl2anc ( 𝐹𝐵 → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ∈ Fin )
28 27 adantr ( ( 𝐹𝐵 ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ≠ ∅ ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ∈ Fin )
29 simpr ( ( 𝐹𝐵 ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ≠ ∅ ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ≠ ∅ )
30 nn0ssre 0 ⊆ ℝ
31 ressxr ℝ ⊆ ℝ*
32 30 31 sstri 0 ⊆ ℝ*
33 15 32 sstrdi ( ( 𝐹𝐵 ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ≠ ∅ ) → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ⊆ ℝ* )
34 xrltso < Or ℝ*
35 fisupcl ( ( < Or ℝ* ∧ ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ∈ Fin ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ≠ ∅ ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ⊆ ℝ* ) ) → sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) , ℝ* , < ) ∈ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) )
36 34 35 mpan ( ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ∈ Fin ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ≠ ∅ ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ⊆ ℝ* ) → sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) , ℝ* , < ) ∈ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) )
37 28 29 33 36 syl3anc ( ( 𝐹𝐵 ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ≠ ∅ ) → sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) , ℝ* , < ) ∈ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) )
38 17 37 sseldd ( ( 𝐹𝐵 ∧ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) ≠ ∅ ) → sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ 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 ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝐹 supp ( 0g𝑅 ) ) ) , ℝ* , < ) ∈ ( ℕ0 ∪ { -∞ } ) )
48 7 47 eqeltrd ( 𝐹𝐵 → ( 𝐷𝐹 ) ∈ ( ℕ0 ∪ { -∞ } ) )