dgrlem

Description: Lemma for dgrcl and similar theorems. (Contributed by Mario Carneiro, 22-Jul-2014)

		Ref	Expression
	Hypothesis	dgrval.1	$⊢ A = coeff (F)$
	Assertion	dgrlem	$⊢ F \in Poly (S) \to (A : ℕ_{0} ⟶ S \cup \{0\} \land \exists n \in ℤ \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n)$

Proof

Step	Hyp	Ref	Expression
1		dgrval.1	$⊢ A = coeff (F)$
2		elply2	$⊢ F \in Poly (S) \leftrightarrow (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})))$
3	2	simprbi	$⊢ F \in Poly (S) \to \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
4		simplrr	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to a \in ({(S \cup \{0\})}^{ℕ_{0}})$
5		simpll	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to F \in Poly (S)$
6		plybss	$⊢ F \in Poly (S) \to S \subseteq ℂ$
7	5 6	syl	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to S \subseteq ℂ$
8		0cnd	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to 0 \in ℂ$
9	8	snssd	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to \{0\} \subseteq ℂ$
10	7 9	unssd	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to S \cup \{0\} \subseteq ℂ$
11		cnex	$⊢ ℂ \in V$
12		ssexg	$⊢ (S \cup \{0\} \subseteq ℂ \land ℂ \in V) \to S \cup \{0\} \in V$
13	10 11 12	sylancl	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to S \cup \{0\} \in V$
14		nn0ex	$⊢ ℕ_{0} \in V$
15		elmapg	$⊢ (S \cup \{0\} \in V \land ℕ_{0} \in V) \to (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \leftrightarrow a : ℕ_{0} ⟶ S \cup \{0\})$
16	13 14 15	sylancl	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \leftrightarrow a : ℕ_{0} ⟶ S \cup \{0\})$
17	4 16	mpbid	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to a : ℕ_{0} ⟶ S \cup \{0\}$
18		simplrl	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to n \in ℕ_{0}$
19	17 10	fssd	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to a : ℕ_{0} ⟶ ℂ$
20		simprl	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to a [ℤ_{\geq (n + 1)}] = \{0\}$
21		simprr	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})$
22	5 18 19 20 21	coeeq	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to coeff (F) = a$
23	1 22	eqtr2id	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to a = A$
24	23	feq1d	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to (a : ℕ_{0} ⟶ S \cup \{0\} \leftrightarrow A : ℕ_{0} ⟶ S \cup \{0\})$
25	17 24	mpbid	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to A : ℕ_{0} ⟶ S \cup \{0\}$
26	25	ex	$⊢ (F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \to A : ℕ_{0} ⟶ S \cup \{0\})$
27	26	rexlimdvva	$⊢ F \in Poly (S) \to (\exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \to A : ℕ_{0} ⟶ S \cup \{0\})$
28	3 27	mpd	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ S \cup \{0\}$
29		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
30		ffn	$⊢ a : ℕ_{0} ⟶ ℂ \to a Fn ℕ_{0}$
31		elpreima	$⊢ a Fn ℕ_{0} \to (x \in a^{-1} [ℂ ∖ \{0\}] \leftrightarrow (x \in ℕ_{0} \land a (x) \in (ℂ ∖ \{0\})))$
32	19 30 31	3syl	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to (x \in a^{-1} [ℂ ∖ \{0\}] \leftrightarrow (x \in ℕ_{0} \land a (x) \in (ℂ ∖ \{0\})))$
33	32	biimpa	$⊢ (((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \land x \in a^{-1} [ℂ ∖ \{0\}]) \to (x \in ℕ_{0} \land a (x) \in (ℂ ∖ \{0\}))$
34		eldifsni	$⊢ a (x) \in (ℂ ∖ \{0\}) \to a (x) \neq 0$
35	33 34	simpl2im	$⊢ (((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \land x \in a^{-1} [ℂ ∖ \{0\}]) \to a (x) \neq 0$
36	33	simpld	$⊢ (((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \land x \in a^{-1} [ℂ ∖ \{0\}]) \to x \in ℕ_{0}$
37		plyco0	$⊢ (n \in ℕ_{0} \land a : ℕ_{0} ⟶ ℂ) \to (a [ℤ_{\geq (n + 1)}] = \{0\} \leftrightarrow \forall x \in ℕ_{0} (a (x) \neq 0 \to x \leq n))$
38	18 19 37	syl2anc	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to (a [ℤ_{\geq (n + 1)}] = \{0\} \leftrightarrow \forall x \in ℕ_{0} (a (x) \neq 0 \to x \leq n))$
39	20 38	mpbid	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to \forall x \in ℕ_{0} (a (x) \neq 0 \to x \leq n)$
40	39	r19.21bi	$⊢ (((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \land x \in ℕ_{0}) \to (a (x) \neq 0 \to x \leq n)$
41	36 40	syldan	$⊢ (((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \land x \in a^{-1} [ℂ ∖ \{0\}]) \to (a (x) \neq 0 \to x \leq n)$
42	35 41	mpd	$⊢ (((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \land x \in a^{-1} [ℂ ∖ \{0\}]) \to x \leq n$
43	42	ralrimiva	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to \forall x \in a^{-1} [ℂ ∖ \{0\}] x \leq n$
44	23	cnveqd	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to a^{-1} = A^{-1}$
45	44	imaeq1d	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to a^{-1} [ℂ ∖ \{0\}] = A^{-1} [ℂ ∖ \{0\}]$
46	45	raleqdv	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to (\forall x \in a^{-1} [ℂ ∖ \{0\}] x \leq n \leftrightarrow \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n)$
47	43 46	mpbid	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n$
48	47	ex	$⊢ (F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \to \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n)$
49	48	expr	$⊢ (F \in Poly (S) \land n \in ℕ_{0}) \to (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \to ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \to \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n))$
50	49	rexlimdv	$⊢ (F \in Poly (S) \land n \in ℕ_{0}) \to (\exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \to \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n)$
51	50	reximdva	$⊢ F \in Poly (S) \to (\exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \to \exists n \in ℕ_{0} \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n)$
52	3 51	mpd	$⊢ F \in Poly (S) \to \exists n \in ℕ_{0} \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n$
53		ssrexv	$⊢ ℕ_{0} \subseteq ℤ \to (\exists n \in ℕ_{0} \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n \to \exists n \in ℤ \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n)$
54	29 52 53	mpsyl	$⊢ F \in Poly (S) \to \exists n \in ℤ \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n$
55	28 54	jca	$⊢ F \in Poly (S) \to (A : ℕ_{0} ⟶ S \cup \{0\} \land \exists n \in ℤ \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n)$

Metamath Proof Explorer

Theorem dgrlem

Proof