fta1

Description: The easy direction of the Fundamental Theorem of Algebra: A nonzero polynomial has at most deg ( F ) roots. (Contributed by Mario Carneiro, 26-Jul-2014)

		Ref	Expression
	Hypothesis	fta1.1	$⊢ R = F^{-1} [\{0\}]$
	Assertion	fta1	$⊢ (F \in Poly (S) \land F \neq 0_{𝑝}) \to (R \in Fin \land \|R\| \leq \deg (F))$

Proof

Step	Hyp	Ref	Expression
1		fta1.1	$⊢ R = F^{-1} [\{0\}]$
2		eqid	$⊢ \deg (F) = \deg (F)$
3		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
4	3	adantr	$⊢ (F \in Poly (S) \land F \neq 0_{𝑝}) \to \deg (F) \in ℕ_{0}$
5		eqeq2	$⊢ x = 0 \to (\deg (f) = x \leftrightarrow \deg (f) = 0)$
6	5	imbi1d	$⊢ x = 0 \to ((\deg (f) = x \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \leftrightarrow (\deg (f) = 0 \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
7	6	ralbidv	$⊢ x = 0 \to (\forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = x \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \leftrightarrow \forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = 0 \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
8		eqeq2	$⊢ x = d \to (\deg (f) = x \leftrightarrow \deg (f) = d)$
9	8	imbi1d	$⊢ x = d \to ((\deg (f) = x \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \leftrightarrow (\deg (f) = d \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
10	9	ralbidv	$⊢ x = d \to (\forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = x \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \leftrightarrow \forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = d \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
11		eqeq2	$⊢ x = d + 1 \to (\deg (f) = x \leftrightarrow \deg (f) = d + 1)$
12	11	imbi1d	$⊢ x = d + 1 \to ((\deg (f) = x \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \leftrightarrow (\deg (f) = d + 1 \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
13	12	ralbidv	$⊢ x = d + 1 \to (\forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = x \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \leftrightarrow \forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = d + 1 \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
14		eqeq2	$⊢ x = \deg (F) \to (\deg (f) = x \leftrightarrow \deg (f) = \deg (F))$
15	14	imbi1d	$⊢ x = \deg (F) \to ((\deg (f) = x \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \leftrightarrow (\deg (f) = \deg (F) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
16	15	ralbidv	$⊢ x = \deg (F) \to (\forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = x \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \leftrightarrow \forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = \deg (F) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
17		eldifsni	$⊢ f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \to f \neq 0_{𝑝}$
18	17	adantr	$⊢ (f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \to f \neq 0_{𝑝}$
19		simplr	$⊢ ((f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \land x \in f^{-1} [\{0\}]) \to \deg (f) = 0$
20		eldifi	$⊢ f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \to f \in Poly (ℂ)$
21	20	ad2antrr	$⊢ ((f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \land x \in f^{-1} [\{0\}]) \to f \in Poly (ℂ)$
22		0dgrb	$⊢ f \in Poly (ℂ) \to (\deg (f) = 0 \leftrightarrow f = ℂ \times \{f (0)\})$
23	21 22	syl	$⊢ ((f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \land x \in f^{-1} [\{0\}]) \to (\deg (f) = 0 \leftrightarrow f = ℂ \times \{f (0)\})$
24	19 23	mpbid	$⊢ ((f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \land x \in f^{-1} [\{0\}]) \to f = ℂ \times \{f (0)\}$
25	24	fveq1d	$⊢ ((f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \land x \in f^{-1} [\{0\}]) \to f (x) = (ℂ \times \{f (0)\}) (x)$
26	20	adantr	$⊢ (f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \to f \in Poly (ℂ)$
27		plyf	$⊢ f \in Poly (ℂ) \to f : ℂ ⟶ ℂ$
28		ffn	$⊢ f : ℂ ⟶ ℂ \to f Fn ℂ$
29		fniniseg	$⊢ f Fn ℂ \to (x \in f^{-1} [\{0\}] \leftrightarrow (x \in ℂ \land f (x) = 0))$
30	26 27 28 29	4syl	$⊢ (f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \to (x \in f^{-1} [\{0\}] \leftrightarrow (x \in ℂ \land f (x) = 0))$
31	30	biimpa	$⊢ ((f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \land x \in f^{-1} [\{0\}]) \to (x \in ℂ \land f (x) = 0)$
32	31	simprd	$⊢ ((f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \land x \in f^{-1} [\{0\}]) \to f (x) = 0$
33	31	simpld	$⊢ ((f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \land x \in f^{-1} [\{0\}]) \to x \in ℂ$
34		fvex	$⊢ f (0) \in V$
35	34	fvconst2	$⊢ x \in ℂ \to (ℂ \times \{f (0)\}) (x) = f (0)$
36	33 35	syl	$⊢ ((f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \land x \in f^{-1} [\{0\}]) \to (ℂ \times \{f (0)\}) (x) = f (0)$
37	25 32 36	3eqtr3rd	$⊢ ((f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \land x \in f^{-1} [\{0\}]) \to f (0) = 0$
38	37	sneqd	$⊢ ((f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \land x \in f^{-1} [\{0\}]) \to \{f (0)\} = \{0\}$
39	38	xpeq2d	$⊢ ((f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \land x \in f^{-1} [\{0\}]) \to ℂ \times \{f (0)\} = ℂ \times \{0\}$
40	24 39	eqtrd	$⊢ ((f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \land x \in f^{-1} [\{0\}]) \to f = ℂ \times \{0\}$
41		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
42	40 41	syl6eqr	$⊢ ((f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \land x \in f^{-1} [\{0\}]) \to f = 0_{𝑝}$
43	42	ex	$⊢ (f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \to (x \in f^{-1} [\{0\}] \to f = 0_{𝑝})$
44	43	necon3ad	$⊢ (f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \to (f \neq 0_{𝑝} \to \neg x \in f^{-1} [\{0\}])$
45	18 44	mpd	$⊢ (f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \to \neg x \in f^{-1} [\{0\}]$
46	45	eq0rdv	$⊢ (f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \land \deg (f) = 0) \to f^{-1} [\{0\}] = \emptyset$
47	46	ex	$⊢ f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \to (\deg (f) = 0 \to f^{-1} [\{0\}] = \emptyset)$
48		dgrcl	$⊢ f \in Poly (ℂ) \to \deg (f) \in ℕ_{0}$
49		nn0ge0	$⊢ \deg (f) \in ℕ_{0} \to 0 \leq \deg (f)$
50	20 48 49	3syl	$⊢ f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \to 0 \leq \deg (f)$
51		id	$⊢ f^{-1} [\{0\}] = \emptyset \to f^{-1} [\{0\}] = \emptyset$
52		0fin	$⊢ \emptyset \in Fin$
53	51 52	eqeltrdi	$⊢ f^{-1} [\{0\}] = \emptyset \to f^{-1} [\{0\}] \in Fin$
54	53	biantrurd	$⊢ f^{-1} [\{0\}] = \emptyset \to (\|f^{-1} [\{0\}]\| \leq \deg (f) \leftrightarrow (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f)))$
55		fveq2	$⊢ f^{-1} [\{0\}] = \emptyset \to \|f^{-1} [\{0\}]\| = \|\emptyset\|$
56		hash0	$⊢ \|\emptyset\| = 0$
57	55 56	syl6eq	$⊢ f^{-1} [\{0\}] = \emptyset \to \|f^{-1} [\{0\}]\| = 0$
58	57	breq1d	$⊢ f^{-1} [\{0\}] = \emptyset \to (\|f^{-1} [\{0\}]\| \leq \deg (f) \leftrightarrow 0 \leq \deg (f))$
59	54 58	bitr3d	$⊢ f^{-1} [\{0\}] = \emptyset \to ((f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f)) \leftrightarrow 0 \leq \deg (f))$
60	50 59	syl5ibrcom	$⊢ f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \to (f^{-1} [\{0\}] = \emptyset \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f)))$
61	47 60	syld	$⊢ f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \to (\deg (f) = 0 \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f)))$
62	61	rgen	$⊢ \forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = 0 \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f)))$
63		fveqeq2	$⊢ f = g \to (\deg (f) = d \leftrightarrow \deg (g) = d)$
64		cnveq	$⊢ f = g \to f^{-1} = g^{-1}$
65	64	imaeq1d	$⊢ f = g \to f^{-1} [\{0\}] = g^{-1} [\{0\}]$
66	65	eleq1d	$⊢ f = g \to (f^{-1} [\{0\}] \in Fin \leftrightarrow g^{-1} [\{0\}] \in Fin)$
67	65	fveq2d	$⊢ f = g \to \|f^{-1} [\{0\}]\| = \|g^{-1} [\{0\}]\|$
68		fveq2	$⊢ f = g \to \deg (f) = \deg (g)$
69	67 68	breq12d	$⊢ f = g \to (\|f^{-1} [\{0\}]\| \leq \deg (f) \leftrightarrow \|g^{-1} [\{0\}]\| \leq \deg (g))$
70	66 69	anbi12d	$⊢ f = g \to ((f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f)) \leftrightarrow (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g)))$
71	63 70	imbi12d	$⊢ f = g \to ((\deg (f) = d \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \leftrightarrow (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))))$
72	71	cbvralvw	$⊢ \forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = d \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \leftrightarrow \forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g)))$
73	50	ad2antlr	$⊢ ((d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \land \deg (f) = d + 1) \to 0 \leq \deg (f)$
74	73 59	syl5ibrcom	$⊢ ((d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \land \deg (f) = d + 1) \to (f^{-1} [\{0\}] = \emptyset \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f)))$
75	74	a1dd	$⊢ ((d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \land \deg (f) = d + 1) \to (f^{-1} [\{0\}] = \emptyset \to (\forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
76		n0	$⊢ f^{-1} [\{0\}] \neq \emptyset \leftrightarrow \exists x x \in f^{-1} [\{0\}]$
77		eqid	$⊢ f^{-1} [\{0\}] = f^{-1} [\{0\}]$
78		simplll	$⊢ (((d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \land \deg (f) = d + 1) \land (x \in f^{-1} [\{0\}] \land \forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))))) \to d \in ℕ_{0}$
79		simpllr	$⊢ (((d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \land \deg (f) = d + 1) \land (x \in f^{-1} [\{0\}] \land \forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))))) \to f \in (Poly (ℂ) ∖ \{0_{𝑝}\})$
80		simplr	$⊢ (((d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \land \deg (f) = d + 1) \land (x \in f^{-1} [\{0\}] \land \forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))))) \to \deg (f) = d + 1$
81		simprl	$⊢ (((d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \land \deg (f) = d + 1) \land (x \in f^{-1} [\{0\}] \land \forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))))) \to x \in f^{-1} [\{0\}]$
82		simprr	$⊢ (((d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \land \deg (f) = d + 1) \land (x \in f^{-1} [\{0\}] \land \forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))))) \to \forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g)))$
83	77 78 79 80 81 82	fta1lem	$⊢ (((d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \land \deg (f) = d + 1) \land (x \in f^{-1} [\{0\}] \land \forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))))) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))$
84	83	exp32	$⊢ ((d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \land \deg (f) = d + 1) \to (x \in f^{-1} [\{0\}] \to (\forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
85	84	exlimdv	$⊢ ((d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \land \deg (f) = d + 1) \to (\exists x x \in f^{-1} [\{0\}] \to (\forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
86	76 85	syl5bi	$⊢ ((d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \land \deg (f) = d + 1) \to (f^{-1} [\{0\}] \neq \emptyset \to (\forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
87	75 86	pm2.61dne	$⊢ ((d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \land \deg (f) = d + 1) \to (\forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f)))$
88	87	ex	$⊢ (d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \to (\deg (f) = d + 1 \to (\forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
89	88	com23	$⊢ (d \in ℕ_{0} \land f \in (Poly (ℂ) ∖ \{0_{𝑝}\})) \to (\forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))) \to (\deg (f) = d + 1 \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
90	89	ralrimdva	$⊢ d \in ℕ_{0} \to (\forall g \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (g) = d \to (g^{-1} [\{0\}] \in Fin \land \|g^{-1} [\{0\}]\| \leq \deg (g))) \to \forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = d + 1 \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
91	72 90	syl5bi	$⊢ d \in ℕ_{0} \to (\forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = d \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \to \forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = d + 1 \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))))$
92	7 10 13 16 62 91	nn0ind	$⊢ \deg (F) \in ℕ_{0} \to \forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = \deg (F) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f)))$
93	4 92	syl	$⊢ (F \in Poly (S) \land F \neq 0_{𝑝}) \to \forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = \deg (F) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f)))$
94		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
95	94	sseli	$⊢ F \in Poly (S) \to F \in Poly (ℂ)$
96		eldifsn	$⊢ F \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \leftrightarrow (F \in Poly (ℂ) \land F \neq 0_{𝑝})$
97		fveqeq2	$⊢ f = F \to (\deg (f) = \deg (F) \leftrightarrow \deg (F) = \deg (F))$
98		cnveq	$⊢ f = F \to f^{-1} = F^{-1}$
99	98	imaeq1d	$⊢ f = F \to f^{-1} [\{0\}] = F^{-1} [\{0\}]$
100	99 1	syl6eqr	$⊢ f = F \to f^{-1} [\{0\}] = R$
101	100	eleq1d	$⊢ f = F \to (f^{-1} [\{0\}] \in Fin \leftrightarrow R \in Fin)$
102	100	fveq2d	$⊢ f = F \to \|f^{-1} [\{0\}]\| = \|R\|$
103		fveq2	$⊢ f = F \to \deg (f) = \deg (F)$
104	102 103	breq12d	$⊢ f = F \to (\|f^{-1} [\{0\}]\| \leq \deg (f) \leftrightarrow \|R\| \leq \deg (F))$
105	101 104	anbi12d	$⊢ f = F \to ((f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f)) \leftrightarrow (R \in Fin \land \|R\| \leq \deg (F)))$
106	97 105	imbi12d	$⊢ f = F \to ((\deg (f) = \deg (F) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \leftrightarrow (\deg (F) = \deg (F) \to (R \in Fin \land \|R\| \leq \deg (F))))$
107	106	rspcv	$⊢ F \in (Poly (ℂ) ∖ \{0_{𝑝}\}) \to (\forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = \deg (F) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \to (\deg (F) = \deg (F) \to (R \in Fin \land \|R\| \leq \deg (F))))$
108	96 107	sylbir	$⊢ (F \in Poly (ℂ) \land F \neq 0_{𝑝}) \to (\forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = \deg (F) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \to (\deg (F) = \deg (F) \to (R \in Fin \land \|R\| \leq \deg (F))))$
109	95 108	sylan	$⊢ (F \in Poly (S) \land F \neq 0_{𝑝}) \to (\forall f \in (Poly (ℂ) ∖ \{0_{𝑝}\}) (\deg (f) = \deg (F) \to (f^{-1} [\{0\}] \in Fin \land \|f^{-1} [\{0\}]\| \leq \deg (f))) \to (\deg (F) = \deg (F) \to (R \in Fin \land \|R\| \leq \deg (F))))$
110	93 109	mpd	$⊢ (F \in Poly (S) \land F \neq 0_{𝑝}) \to (\deg (F) = \deg (F) \to (R \in Fin \land \|R\| \leq \deg (F)))$
111	2 110	mpi	$⊢ (F \in Poly (S) \land F \neq 0_{𝑝}) \to (R \in Fin \land \|R\| \leq \deg (F))$

Metamath Proof Explorer

Theorem fta1

Proof