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	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ( ℕ₀ ∪ { -∞ } ) )

Proof

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

Metamath Proof Explorer

Theorem mdegcl

Proof