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	⊢ { 𝑎 ∈ ( ℕ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 ∪ { -∞ } ) )