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