mdegle0

Description: A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	mdegaddle.y	$⊢ Y = I mPoly R$
	mdegaddle.d	$⊢ D = I mDeg R$
	mdegaddle.i	$⊢ φ \to I \in V$
	mdegaddle.r	$⊢ φ \to R \in Ring$
	mdegle0.b	$⊢ B = {Base}_{Y}$
	mdegle0.a	$⊢ A = algSc (Y)$
	mdegle0.f	$⊢ φ \to F \in B$
Assertion	mdegle0	$⊢ φ \to (D (F) \leq 0 \leftrightarrow F = A (F (I \times \{0\})))$

Proof

Step	Hyp	Ref	Expression
1		mdegaddle.y	$⊢ Y = I mPoly R$
2		mdegaddle.d	$⊢ D = I mDeg R$
3		mdegaddle.i	$⊢ φ \to I \in V$
4		mdegaddle.r	$⊢ φ \to R \in Ring$
5		mdegle0.b	$⊢ B = {Base}_{Y}$
6		mdegle0.a	$⊢ A = algSc (Y)$
7		mdegle0.f	$⊢ φ \to F \in B$
8		0xr	$⊢ 0 \in ℝ^{*}$
9		eqid	$⊢ 0_{R} = 0_{R}$
10		eqid	$⊢ \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} = \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}$
11		eqid	$⊢ (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) = (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b)$
12	2 1 5 9 10 11	mdegleb	$⊢ (F \in B \land 0 \in ℝ^{*}) \to (D (F) \leq 0 \leftrightarrow \forall x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} (0 < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \to F (x) = 0_{R}))$
13	7 8 12	sylancl	$⊢ φ \to (D (F) \leq 0 \leftrightarrow \forall x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} (0 < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \to F (x) = 0_{R}))$
14	10 11	tdeglem1	$⊢ I \in V \to (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) : \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟶ ℕ_{0}$
15	3 14	syl	$⊢ φ \to (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) : \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟶ ℕ_{0}$
16	15	ffvelrnda	$⊢ (φ \land x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}) \to (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \in ℕ_{0}$
17		nn0re	$⊢ (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \in ℕ_{0} \to (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \in ℝ$
18		nn0ge0	$⊢ (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \in ℕ_{0} \to 0 \leq (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x)$
19	17 18	jca	$⊢ (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \in ℕ_{0} \to ((b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \in ℝ \land 0 \leq (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x))$
20		ne0gt0	$⊢ ((b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \in ℝ \land 0 \leq (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x)) \to ((b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \neq 0 \leftrightarrow 0 < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x))$
21	16 19 20	3syl	$⊢ (φ \land x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}) \to ((b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \neq 0 \leftrightarrow 0 < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x))$
22	10 11	tdeglem4	$⊢ (I \in V \land x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}) \to ((b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) = 0 \leftrightarrow x = I \times \{0\})$
23	3 22	sylan	$⊢ (φ \land x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}) \to ((b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) = 0 \leftrightarrow x = I \times \{0\})$
24	23	necon3abid	$⊢ (φ \land x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}) \to ((b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \neq 0 \leftrightarrow \neg x = I \times \{0\})$
25	21 24	bitr3d	$⊢ (φ \land x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}) \to (0 < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \leftrightarrow \neg x = I \times \{0\})$
26	25	imbi1d	$⊢ (φ \land x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}) \to ((0 < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \to F (x) = 0_{R}) \leftrightarrow (\neg x = I \times \{0\} \to F (x) = 0_{R}))$
27		eqeq2	$⊢ F (I \times \{0\}) = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}) \to (F (x) = F (I \times \{0\}) \leftrightarrow F (x) = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}))$
28	27	bibi1d	$⊢ F (I \times \{0\}) = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}) \to ((F (x) = F (I \times \{0\}) \leftrightarrow (\neg x = I \times \{0\} \to F (x) = 0_{R})) \leftrightarrow (F (x) = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}) \leftrightarrow (\neg x = I \times \{0\} \to F (x) = 0_{R})))$
29		eqeq2	$⊢ 0_{R} = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}) \to (F (x) = 0_{R} \leftrightarrow F (x) = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}))$
30	29	bibi1d	$⊢ 0_{R} = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}) \to ((F (x) = 0_{R} \leftrightarrow (\neg x = I \times \{0\} \to F (x) = 0_{R})) \leftrightarrow (F (x) = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}) \leftrightarrow (\neg x = I \times \{0\} \to F (x) = 0_{R})))$
31		fveq2	$⊢ x = I \times \{0\} \to F (x) = F (I \times \{0\})$
32		pm2.24	$⊢ x = I \times \{0\} \to (\neg x = I \times \{0\} \to F (x) = 0_{R})$
33	31 32	2thd	$⊢ x = I \times \{0\} \to (F (x) = F (I \times \{0\}) \leftrightarrow (\neg x = I \times \{0\} \to F (x) = 0_{R}))$
34	33	adantl	$⊢ (φ \land x = I \times \{0\}) \to (F (x) = F (I \times \{0\}) \leftrightarrow (\neg x = I \times \{0\} \to F (x) = 0_{R}))$
35		biimt	$⊢ \neg x = I \times \{0\} \to (F (x) = 0_{R} \leftrightarrow (\neg x = I \times \{0\} \to F (x) = 0_{R}))$
36	35	adantl	$⊢ (φ \land \neg x = I \times \{0\}) \to (F (x) = 0_{R} \leftrightarrow (\neg x = I \times \{0\} \to F (x) = 0_{R}))$
37	28 30 34 36	ifbothda	$⊢ φ \to (F (x) = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}) \leftrightarrow (\neg x = I \times \{0\} \to F (x) = 0_{R}))$
38	37	adantr	$⊢ (φ \land x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}) \to (F (x) = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}) \leftrightarrow (\neg x = I \times \{0\} \to F (x) = 0_{R}))$
39	26 38	bitr4d	$⊢ (φ \land x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}) \to ((0 < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \to F (x) = 0_{R}) \leftrightarrow F (x) = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}))$
40	39	ralbidva	$⊢ φ \to (\forall x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} (0 < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \to F (x) = 0_{R}) \leftrightarrow \forall x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} F (x) = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}))$
41		eqid	$⊢ {Base}_{R} = {Base}_{R}$
42	1 41 5 10 7	mplelf	$⊢ φ \to F : \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
43	42	feqmptd	$⊢ φ \to F = (x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ F (x))$
44	10	psrbag0	$⊢ I \in V \to I \times \{0\} \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}$
45	3 44	syl	$⊢ φ \to I \times \{0\} \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}$
46	42 45	ffvelrnd	$⊢ φ \to F (I \times \{0\}) \in {Base}_{R}$
47	1 10 9 41 6 3 4 46	mplascl	$⊢ φ \to A (F (I \times \{0\})) = (x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}))$
48	43 47	eqeq12d	$⊢ φ \to (F = A (F (I \times \{0\})) \leftrightarrow (x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ F (x)) = (x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ if (x = I \times \{0\}, F (I \times \{0\}), 0_{R})))$
49		fvex	$⊢ F (x) \in V$
50	49	rgenw	$⊢ \forall x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} F (x) \in V$
51		mpteqb	$⊢ \forall x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} F (x) \in V \to ((x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ F (x)) = (x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ if (x = I \times \{0\}, F (I \times \{0\}), 0_{R})) \leftrightarrow \forall x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} F (x) = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}))$
52	50 51	mp1i	$⊢ φ \to ((x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ F (x)) = (x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ if (x = I \times \{0\}, F (I \times \{0\}), 0_{R})) \leftrightarrow \forall x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} F (x) = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}))$
53	48 52	bitrd	$⊢ φ \to (F = A (F (I \times \{0\})) \leftrightarrow \forall x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} F (x) = if (x = I \times \{0\}, F (I \times \{0\}), 0_{R}))$
54	40 53	bitr4d	$⊢ φ \to (\forall x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} (0 < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \to F (x) = 0_{R}) \leftrightarrow F = A (F (I \times \{0\})))$
55	13 54	bitrd	$⊢ φ \to (D (F) \leq 0 \leftrightarrow F = A (F (I \times \{0\})))$

Metamath Proof Explorer

Theorem mdegle0

Proof