mdegldg

Description: A nonzero polynomial has some coefficient which witnesses its degree. (Contributed by Stefan O'Rear, 23-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)$
	mdegldg.y	$⊢ Y = 0_{P}$
Assertion	mdegldg	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to \exists x \in A (F (x) \neq \underset{˙}{0} \land H (x) = D (F))$

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		mdegldg.y	$⊢ Y = 0_{P}$
8	1 2 3 4 5 6	mdegval	$⊢ F \in B \to D (F) = sup (H [F supp \underset{˙}{0}] ℝ^{*} <)$
9	8	3ad2ant2	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to D (F) = sup (H [F supp \underset{˙}{0}] ℝ^{*} <)$
10	5 6	tdeglem1	$⊢ H : A ⟶ ℕ_{0}$
11	10	a1i	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to H : A ⟶ ℕ_{0}$
12	11	ffund	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to Fun H$
13		simp2	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to F \in B$
14	2 3 4 13	mplelsfi	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to {finSupp}_{\underset{˙}{0}} (F)$
15	14	fsuppimpd	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to F supp \underset{˙}{0} \in Fin$
16		imafi	$⊢ (Fun H \land F supp \underset{˙}{0} \in Fin) \to H [F supp \underset{˙}{0}] \in Fin$
17	12 15 16	syl2anc	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to H [F supp \underset{˙}{0}] \in Fin$
18		simp3	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to F \neq Y$
19	2 3	mplrcl	$⊢ F \in B \to I \in V$
20	19	3ad2ant2	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to I \in V$
21		ringgrp	$⊢ R \in Ring \to R \in Grp$
22	21	3ad2ant1	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to R \in Grp$
23	2 5 4 7 20 22	mpl0	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to Y = A \times \{\underset{˙}{0}\}$
24	18 23	neeqtrd	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to F \neq A \times \{\underset{˙}{0}\}$
25		eqid	$⊢ {Base}_{R} = {Base}_{R}$
26	2 25 3 5 13	mplelf	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to F : A ⟶ {Base}_{R}$
27	26	ffnd	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to F Fn A$
28	4	fvexi	$⊢ \underset{˙}{0} \in V$
29		ovex	$⊢ {ℕ_{0}}^{I} \in V$
30	5 29	rabex2	$⊢ A \in V$
31		fnsuppeq0	$⊢ (F Fn A \land A \in V \land \underset{˙}{0} \in V) \to (F supp \underset{˙}{0} = \emptyset \leftrightarrow F = A \times \{\underset{˙}{0}\})$
32	30 31	mp3an2	$⊢ (F Fn A \land \underset{˙}{0} \in V) \to (F supp \underset{˙}{0} = \emptyset \leftrightarrow F = A \times \{\underset{˙}{0}\})$
33	27 28 32	sylancl	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to (F supp \underset{˙}{0} = \emptyset \leftrightarrow F = A \times \{\underset{˙}{0}\})$
34	33	necon3bid	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to (F supp \underset{˙}{0} \neq \emptyset \leftrightarrow F \neq A \times \{\underset{˙}{0}\})$
35	24 34	mpbird	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to F supp \underset{˙}{0} \neq \emptyset$
36	11	ffnd	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to H Fn A$
37		suppssdm	$⊢ F supp \underset{˙}{0} \subseteq dom F$
38	37 26	fssdm	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to F supp \underset{˙}{0} \subseteq A$
39		fnimaeq0	$⊢ (H Fn A \land F supp \underset{˙}{0} \subseteq A) \to (H [F supp \underset{˙}{0}] = \emptyset \leftrightarrow F supp \underset{˙}{0} = \emptyset)$
40	36 38 39	syl2anc	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to (H [F supp \underset{˙}{0}] = \emptyset \leftrightarrow F supp \underset{˙}{0} = \emptyset)$
41	40	necon3bid	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to (H [F supp \underset{˙}{0}] \neq \emptyset \leftrightarrow F supp \underset{˙}{0} \neq \emptyset)$
42	35 41	mpbird	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to H [F supp \underset{˙}{0}] \neq \emptyset$
43		imassrn	$⊢ H [F supp \underset{˙}{0}] \subseteq ran H$
44	11	frnd	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to ran H \subseteq ℕ_{0}$
45	43 44	sstrid	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to H [F supp \underset{˙}{0}] \subseteq ℕ_{0}$
46		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
47		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
48	46 47	sstri	$⊢ ℕ_{0} \subseteq ℝ^{*}$
49	45 48	sstrdi	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to H [F supp \underset{˙}{0}] \subseteq ℝ^{*}$
50		xrltso	$⊢ < Or ℝ^{*}$
51		fisupcl	$⊢ (< Or ℝ^{} \land (H [F supp \underset{˙}{0}] \in Fin \land H [F supp \underset{˙}{0}] \neq \emptyset \land H [F supp \underset{˙}{0}] \subseteq ℝ^{})) \to sup (H [F supp \underset{˙}{0}] ℝ^{*} <) \in H [F supp \underset{˙}{0}]$
52	50 51	mpan	$⊢ (H [F supp \underset{˙}{0}] \in Fin \land H [F supp \underset{˙}{0}] \neq \emptyset \land H [F supp \underset{˙}{0}] \subseteq ℝ^{}) \to sup (H [F supp \underset{˙}{0}] ℝ^{} <) \in H [F supp \underset{˙}{0}]$
53	17 42 49 52	syl3anc	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to sup (H [F supp \underset{˙}{0}] ℝ^{*} <) \in H [F supp \underset{˙}{0}]$
54	9 53	eqeltrd	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to D (F) \in H [F supp \underset{˙}{0}]$
55	36 38	fvelimabd	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to (D (F) \in H [F supp \underset{˙}{0}] \leftrightarrow \exists x \in {supp}_{\underset{˙}{0}} (F) H (x) = D (F))$
56		rexsupp	$⊢ (F Fn A \land A \in V \land \underset{˙}{0} \in V) \to (\exists x \in {supp}_{\underset{˙}{0}} (F) H (x) = D (F) \leftrightarrow \exists x \in A (F (x) \neq \underset{˙}{0} \land H (x) = D (F)))$
57	30 28 56	mp3an23	$⊢ F Fn A \to (\exists x \in {supp}_{\underset{˙}{0}} (F) H (x) = D (F) \leftrightarrow \exists x \in A (F (x) \neq \underset{˙}{0} \land H (x) = D (F)))$
58	27 57	syl	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to (\exists x \in {supp}_{\underset{˙}{0}} (F) H (x) = D (F) \leftrightarrow \exists x \in A (F (x) \neq \underset{˙}{0} \land H (x) = D (F)))$
59	55 58	bitrd	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to (D (F) \in H [F supp \underset{˙}{0}] \leftrightarrow \exists x \in A (F (x) \neq \underset{˙}{0} \land H (x) = D (F)))$
60	54 59	mpbid	$⊢ (R \in Ring \land F \in B \land F \neq Y) \to \exists x \in A (F (x) \neq \underset{˙}{0} \land H (x) = D (F))$

Metamath Proof Explorer

Theorem mdegldg

Proof