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	2 3	mplrcl	$⊢ F \in B \to I \in V$
12	11	adantr	$⊢ (F \in B \land G \in ℝ^{*}) \to I \in V$
13	5 6	tdeglem1	$⊢ I \in V \to H : A ⟶ ℕ_{0}$
14	12 13	syl	$⊢ (F \in B \land G \in ℝ^{*}) \to H : A ⟶ ℕ_{0}$
15	14	frnd	$⊢ (F \in B \land G \in ℝ^{*}) \to ran H \subseteq ℕ_{0}$
16		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
17		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
18	16 17	sstri	$⊢ ℕ_{0} \subseteq ℝ^{*}$
19	15 18	sstrdi	$⊢ (F \in B \land G \in ℝ^{}) \to ran H \subseteq ℝ^{}$
20	10 19	sstrid	$⊢ (F \in B \land G \in ℝ^{}) \to H [F supp \underset{˙}{0}] \subseteq ℝ^{}$
21		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)$
22	20 21	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)$
23	14	ffnd	$⊢ (F \in B \land G \in ℝ^{*}) \to H Fn A$
24		suppssdm	$⊢ F supp \underset{˙}{0} \subseteq dom F$
25		eqid	$⊢ {Base}_{R} = {Base}_{R}$
26		simpl	$⊢ (F \in B \land G \in ℝ^{*}) \to F \in B$
27	2 25 3 5 26	mplelf	$⊢ (F \in B \land G \in ℝ^{*}) \to F : A ⟶ {Base}_{R}$
28	24 27	fssdm	$⊢ (F \in B \land G \in ℝ^{*}) \to F supp \underset{˙}{0} \subseteq A$
29		breq1	$⊢ y = H (x) \to (y \leq G \leftrightarrow H (x) \leq G)$
30	29	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)$
31	23 28 30	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)$
32	27	ffnd	$⊢ (F \in B \land G \in ℝ^{*}) \to F Fn A$
33		ovex	$⊢ {ℕ_{0}}^{I} \in V$
34	33	rabex	$⊢ \{m \in ({ℕ_{0}}^{I}) \| m^{-1} [ℕ] \in Fin\} \in V$
35	34	a1i	$⊢ (F \in B \land G \in ℝ^{*}) \to \{m \in ({ℕ_{0}}^{I}) \| m^{-1} [ℕ] \in Fin\} \in V$
36	5 35	eqeltrid	$⊢ (F \in B \land G \in ℝ^{*}) \to A \in V$
37	4	fvexi	$⊢ \underset{˙}{0} \in V$
38	37	a1i	$⊢ (F \in B \land G \in ℝ^{*}) \to \underset{˙}{0} \in V$
39		elsuppfn	$⊢ (F Fn A \land A \in V \land \underset{˙}{0} \in V) \to (x \in {supp}_{\underset{˙}{0}} (F) \leftrightarrow (x \in A \land F (x) \neq \underset{˙}{0}))$
40		fvex	$⊢ F (x) \in V$
41	40	biantrur	$⊢ F (x) \neq \underset{˙}{0} \leftrightarrow (F (x) \in V \land F (x) \neq \underset{˙}{0})$
42		eldifsn	$⊢ F (x) \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (F (x) \in V \land F (x) \neq \underset{˙}{0})$
43	41 42	bitr4i	$⊢ F (x) \neq \underset{˙}{0} \leftrightarrow F (x) \in (V ∖ \{\underset{˙}{0}\})$
44	43	a1i	$⊢ (F Fn A \land A \in V \land \underset{˙}{0} \in V) \to (F (x) \neq \underset{˙}{0} \leftrightarrow F (x) \in (V ∖ \{\underset{˙}{0}\}))$
45	44	anbi2d	$⊢ (F Fn A \land A \in V \land \underset{˙}{0} \in V) \to ((x \in A \land F (x) \neq \underset{˙}{0}) \leftrightarrow (x \in A \land F (x) \in (V ∖ \{\underset{˙}{0}\})))$
46	39 45	bitrd	$⊢ (F Fn A \land A \in V \land \underset{˙}{0} \in V) \to (x \in {supp}_{\underset{˙}{0}} (F) \leftrightarrow (x \in A \land F (x) \in (V ∖ \{\underset{˙}{0}\})))$
47	32 36 38 46	syl3anc	$⊢ (F \in B \land G \in ℝ^{*}) \to (x \in {supp}_{\underset{˙}{0}} (F) \leftrightarrow (x \in A \land F (x) \in (V ∖ \{\underset{˙}{0}\})))$
48	47	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))$
49		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))$
50		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}\}))$
51		simplr	$⊢ ((F \in B \land G \in ℝ^{}) \land x \in A) \to G \in ℝ^{}$
52	14	ffvelrnda	$⊢ ((F \in B \land G \in ℝ^{*}) \land x \in A) \to H (x) \in ℕ_{0}$
53	18 52	sseldi	$⊢ ((F \in B \land G \in ℝ^{}) \land x \in A) \to H (x) \in ℝ^{}$
54		xrltnle	$⊢ (G \in ℝ^{} \land H (x) \in ℝ^{}) \to (G < H (x) \leftrightarrow \neg H (x) \leq G)$
55	51 53 54	syl2anc	$⊢ ((F \in B \land G \in ℝ^{*}) \land x \in A) \to (G < H (x) \leftrightarrow \neg H (x) \leq G)$
56	55	bicomd	$⊢ ((F \in B \land G \in ℝ^{*}) \land x \in A) \to (\neg H (x) \leq G \leftrightarrow G < H (x))$
57		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})$
58	57 42	xchnxbir	$⊢ \neg F (x) \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (\neg F (x) \in V \lor \neg F (x) \neq \underset{˙}{0})$
59		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)$
60	40	notnoti	$⊢ \neg \neg F (x) \in V$
61	60	biorfi	$⊢ \neg F (x) \neq \underset{˙}{0} \leftrightarrow (\neg F (x) \neq \underset{˙}{0} \lor \neg F (x) \in V)$
62		nne	$⊢ \neg F (x) \neq \underset{˙}{0} \leftrightarrow F (x) = \underset{˙}{0}$
63	59 61 62	3bitr2i	$⊢ (\neg F (x) \in V \lor \neg F (x) \neq \underset{˙}{0}) \leftrightarrow F (x) = \underset{˙}{0}$
64	63	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})$
65	58 64	syl5bb	$⊢ ((F \in B \land G \in ℝ^{*}) \land x \in A) \to (\neg F (x) \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow F (x) = \underset{˙}{0})$
66	56 65	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}))$
67	50 66	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}))$
68	67	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})))$
69	49 68	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})))$
70	48 69	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})))$
71	70	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}))$
72	31 71	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}))$
73	9 22 72	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