mdegleb

Description: Property of being of limited degree. (Contributed by Stefan O'Rear, 19-Mar-2015)

	Ref	Expression
Hypotheses	mdegval.d	$⊢ D = I mDeg R$
	mdegval.p	$⊢ P = I mPoly R$
	mdegval.b	$⊢ B = {Base}_{P}$
	mdegval.z	$⊢ \underset{˙}{0} = 0_{R}$
	mdegval.a	$⊢ A = \{m \in ({ℕ_{0}}^{I}) \| m^{-1} [ℕ] \in Fin\}$
	mdegval.h	$⊢ H = (h \in A ⟼ \sum_{ℂ_{fld}} h)$
Assertion	mdegleb	$⊢ (F \in B \land G \in ℝ^{*}) \to (D (F) \leq G \leftrightarrow \forall x \in A (G < H (x) \to F (x) = \underset{˙}{0}))$

Proof

Step	Hyp	Ref	Expression
1		mdegval.d	$⊢ D = I mDeg R$
2		mdegval.p	$⊢ P = I mPoly R$
3		mdegval.b	$⊢ B = {Base}_{P}$
4		mdegval.z	$⊢ \underset{˙}{0} = 0_{R}$
5		mdegval.a	$⊢ A = \{m \in ({ℕ_{0}}^{I}) \| m^{-1} [ℕ] \in Fin\}$
6		mdegval.h	$⊢ H = (h \in A ⟼ \sum_{ℂ_{fld}} h)$
7	1 2 3 4 5 6	mdegval	$⊢ F \in B \to D (F) = sup (H [F supp \underset{˙}{0}] ℝ^{*} <)$
8	7	adantr	$⊢ (F \in B \land G \in ℝ^{}) \to D (F) = sup (H [F supp \underset{˙}{0}] ℝ^{} <)$
9	8	breq1d	$⊢ (F \in B \land G \in ℝ^{}) \to (D (F) \leq G \leftrightarrow sup (H [F supp \underset{˙}{0}] ℝ^{} <) \leq G)$
10		imassrn	$⊢ H [F supp \underset{˙}{0}] \subseteq ran H$
11	5 6	tdeglem1	$⊢ H : A ⟶ ℕ_{0}$
12	11	a1i	$⊢ (F \in B \land G \in ℝ^{*}) \to H : A ⟶ ℕ_{0}$
13	12	frnd	$⊢ (F \in B \land G \in ℝ^{*}) \to ran H \subseteq ℕ_{0}$
14		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
15		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
16	14 15	sstri	$⊢ ℕ_{0} \subseteq ℝ^{*}$
17	13 16	sstrdi	$⊢ (F \in B \land G \in ℝ^{}) \to ran H \subseteq ℝ^{}$
18	10 17	sstrid	$⊢ (F \in B \land G \in ℝ^{}) \to H [F supp \underset{˙}{0}] \subseteq ℝ^{}$
19		supxrleub	$⊢ (H [F supp \underset{˙}{0}] \subseteq ℝ^{} \land G \in ℝ^{}) \to (sup (H [F supp \underset{˙}{0}] ℝ^{*} <) \leq G \leftrightarrow \forall y \in H [F supp \underset{˙}{0}] y \leq G)$
20	18 19	sylancom	$⊢ (F \in B \land G \in ℝ^{}) \to (sup (H [F supp \underset{˙}{0}] ℝ^{} <) \leq G \leftrightarrow \forall y \in H [F supp \underset{˙}{0}] y \leq G)$
21	12	ffnd	$⊢ (F \in B \land G \in ℝ^{*}) \to H Fn A$
22		suppssdm	$⊢ F supp \underset{˙}{0} \subseteq dom F$
23		eqid	$⊢ {Base}_{R} = {Base}_{R}$
24		simpl	$⊢ (F \in B \land G \in ℝ^{*}) \to F \in B$
25	2 23 3 5 24	mplelf	$⊢ (F \in B \land G \in ℝ^{*}) \to F : A ⟶ {Base}_{R}$
26	22 25	fssdm	$⊢ (F \in B \land G \in ℝ^{*}) \to F supp \underset{˙}{0} \subseteq A$
27		breq1	$⊢ y = H (x) \to (y \leq G \leftrightarrow H (x) \leq G)$
28	27	ralima	$⊢ (H Fn A \land F supp \underset{˙}{0} \subseteq A) \to (\forall y \in H [F supp \underset{˙}{0}] y \leq G \leftrightarrow \forall x \in {supp}_{\underset{˙}{0}} (F) H (x) \leq G)$
29	21 26 28	syl2anc	$⊢ (F \in B \land G \in ℝ^{*}) \to (\forall y \in H [F supp \underset{˙}{0}] y \leq G \leftrightarrow \forall x \in {supp}_{\underset{˙}{0}} (F) H (x) \leq G)$
30	25	ffnd	$⊢ (F \in B \land G \in ℝ^{*}) \to F Fn A$
31	4	fvexi	$⊢ \underset{˙}{0} \in V$
32	31	a1i	$⊢ (F \in B \land G \in ℝ^{*}) \to \underset{˙}{0} \in V$
33		elsuppfng	$⊢ (F Fn A \land F \in B \land \underset{˙}{0} \in V) \to (x \in {supp}_{\underset{˙}{0}} (F) \leftrightarrow (x \in A \land F (x) \neq \underset{˙}{0}))$
34	30 24 32 33	syl3anc	$⊢ (F \in B \land G \in ℝ^{*}) \to (x \in {supp}_{\underset{˙}{0}} (F) \leftrightarrow (x \in A \land F (x) \neq \underset{˙}{0}))$
35		fvex	$⊢ F (x) \in V$
36	35	biantrur	$⊢ F (x) \neq \underset{˙}{0} \leftrightarrow (F (x) \in V \land F (x) \neq \underset{˙}{0})$
37		eldifsn	$⊢ F (x) \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (F (x) \in V \land F (x) \neq \underset{˙}{0})$
38	36 37	bitr4i	$⊢ F (x) \neq \underset{˙}{0} \leftrightarrow F (x) \in (V ∖ \{\underset{˙}{0}\})$
39	38	anbi2i	$⊢ (x \in A \land F (x) \neq \underset{˙}{0}) \leftrightarrow (x \in A \land F (x) \in (V ∖ \{\underset{˙}{0}\}))$
40	34 39	bitrdi	$⊢ (F \in B \land G \in ℝ^{*}) \to (x \in {supp}_{\underset{˙}{0}} (F) \leftrightarrow (x \in A \land F (x) \in (V ∖ \{\underset{˙}{0}\})))$
41	40	imbi1d	$⊢ (F \in B \land G \in ℝ^{*}) \to ((x \in {supp}_{\underset{˙}{0}} (F) \to H (x) \leq G) \leftrightarrow ((x \in A \land F (x) \in (V ∖ \{\underset{˙}{0}\})) \to H (x) \leq G))$
42		impexp	$⊢ ((x \in A \land F (x) \in (V ∖ \{\underset{˙}{0}\})) \to H (x) \leq G) \leftrightarrow (x \in A \to (F (x) \in (V ∖ \{\underset{˙}{0}\}) \to H (x) \leq G))$
43		con34b	$⊢ (F (x) \in (V ∖ \{\underset{˙}{0}\}) \to H (x) \leq G) \leftrightarrow (\neg H (x) \leq G \to \neg F (x) \in (V ∖ \{\underset{˙}{0}\}))$
44		simplr	$⊢ ((F \in B \land G \in ℝ^{}) \land x \in A) \to G \in ℝ^{}$
45	12	ffvelrnda	$⊢ ((F \in B \land G \in ℝ^{*}) \land x \in A) \to H (x) \in ℕ_{0}$
46	16 45	sselid	$⊢ ((F \in B \land G \in ℝ^{}) \land x \in A) \to H (x) \in ℝ^{}$
47		xrltnle	$⊢ (G \in ℝ^{} \land H (x) \in ℝ^{}) \to (G < H (x) \leftrightarrow \neg H (x) \leq G)$
48	44 46 47	syl2anc	$⊢ ((F \in B \land G \in ℝ^{*}) \land x \in A) \to (G < H (x) \leftrightarrow \neg H (x) \leq G)$
49	48	bicomd	$⊢ ((F \in B \land G \in ℝ^{*}) \land x \in A) \to (\neg H (x) \leq G \leftrightarrow G < H (x))$
50		ianor	$⊢ \neg (F (x) \in V \land F (x) \neq \underset{˙}{0}) \leftrightarrow (\neg F (x) \in V \lor \neg F (x) \neq \underset{˙}{0})$
51	50 37	xchnxbir	$⊢ \neg F (x) \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (\neg F (x) \in V \lor \neg F (x) \neq \underset{˙}{0})$
52		orcom	$⊢ (\neg F (x) \in V \lor \neg F (x) \neq \underset{˙}{0}) \leftrightarrow (\neg F (x) \neq \underset{˙}{0} \lor \neg F (x) \in V)$
53	35	notnoti	$⊢ \neg \neg F (x) \in V$
54	53	biorfi	$⊢ \neg F (x) \neq \underset{˙}{0} \leftrightarrow (\neg F (x) \neq \underset{˙}{0} \lor \neg F (x) \in V)$
55		nne	$⊢ \neg F (x) \neq \underset{˙}{0} \leftrightarrow F (x) = \underset{˙}{0}$
56	52 54 55	3bitr2i	$⊢ (\neg F (x) \in V \lor \neg F (x) \neq \underset{˙}{0}) \leftrightarrow F (x) = \underset{˙}{0}$
57	56	a1i	$⊢ ((F \in B \land G \in ℝ^{*}) \land x \in A) \to ((\neg F (x) \in V \lor \neg F (x) \neq \underset{˙}{0}) \leftrightarrow F (x) = \underset{˙}{0})$
58	51 57	syl5bb	$⊢ ((F \in B \land G \in ℝ^{*}) \land x \in A) \to (\neg F (x) \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow F (x) = \underset{˙}{0})$
59	49 58	imbi12d	$⊢ ((F \in B \land G \in ℝ^{*}) \land x \in A) \to ((\neg H (x) \leq G \to \neg F (x) \in (V ∖ \{\underset{˙}{0}\})) \leftrightarrow (G < H (x) \to F (x) = \underset{˙}{0}))$
60	43 59	syl5bb	$⊢ ((F \in B \land G \in ℝ^{*}) \land x \in A) \to ((F (x) \in (V ∖ \{\underset{˙}{0}\}) \to H (x) \leq G) \leftrightarrow (G < H (x) \to F (x) = \underset{˙}{0}))$
61	60	pm5.74da	$⊢ (F \in B \land G \in ℝ^{*}) \to ((x \in A \to (F (x) \in (V ∖ \{\underset{˙}{0}\}) \to H (x) \leq G)) \leftrightarrow (x \in A \to (G < H (x) \to F (x) = \underset{˙}{0})))$
62	42 61	syl5bb	$⊢ (F \in B \land G \in ℝ^{*}) \to (((x \in A \land F (x) \in (V ∖ \{\underset{˙}{0}\})) \to H (x) \leq G) \leftrightarrow (x \in A \to (G < H (x) \to F (x) = \underset{˙}{0})))$
63	41 62	bitrd	$⊢ (F \in B \land G \in ℝ^{*}) \to ((x \in {supp}_{\underset{˙}{0}} (F) \to H (x) \leq G) \leftrightarrow (x \in A \to (G < H (x) \to F (x) = \underset{˙}{0})))$
64	63	ralbidv2	$⊢ (F \in B \land G \in ℝ^{*}) \to (\forall x \in {supp}_{\underset{˙}{0}} (F) H (x) \leq G \leftrightarrow \forall x \in A (G < H (x) \to F (x) = \underset{˙}{0}))$
65	29 64	bitrd	$⊢ (F \in B \land G \in ℝ^{*}) \to (\forall y \in H [F supp \underset{˙}{0}] y \leq G \leftrightarrow \forall x \in A (G < H (x) \to F (x) = \underset{˙}{0}))$
66	9 20 65	3bitrd	$⊢ (F \in B \land G \in ℝ^{*}) \to (D (F) \leq G \leftrightarrow \forall x \in A (G < H (x) \to F (x) = \underset{˙}{0}))$

Metamath Proof Explorer

Theorem mdegleb

Proof