plyremlem

Description: Closure of a linear factor. (Contributed by Mario Carneiro, 26-Jul-2014)

		Ref	Expression
	Hypothesis	plyrem.1	$⊢ G = X^{p} -_{f} (ℂ \times \{A\})$
	Assertion	plyremlem	$⊢ A \in ℂ \to (G \in Poly (ℂ) \land \deg (G) = 1 \land G^{-1} [\{0\}] = \{A\})$

Proof

Step	Hyp	Ref	Expression
1		plyrem.1	$⊢ G = X^{p} -_{f} (ℂ \times \{A\})$
2		ssid	$⊢ ℂ \subseteq ℂ$
3		ax-1cn	$⊢ 1 \in ℂ$
4		plyid	$⊢ (ℂ \subseteq ℂ \land 1 \in ℂ) \to X^{p} \in Poly (ℂ)$
5	2 3 4	mp2an	$⊢ X^{p} \in Poly (ℂ)$
6		plyconst	$⊢ (ℂ \subseteq ℂ \land A \in ℂ) \to ℂ \times \{A\} \in Poly (ℂ)$
7	2 6	mpan	$⊢ A \in ℂ \to ℂ \times \{A\} \in Poly (ℂ)$
8		plysubcl	$⊢ (X^{p} \in Poly (ℂ) \land ℂ \times \{A\} \in Poly (ℂ)) \to X^{p} -_{f} (ℂ \times \{A\}) \in Poly (ℂ)$
9	5 7 8	sylancr	$⊢ A \in ℂ \to X^{p} -_{f} (ℂ \times \{A\}) \in Poly (ℂ)$
10	1 9	eqeltrid	$⊢ A \in ℂ \to G \in Poly (ℂ)$
11		negcl	$⊢ A \in ℂ \to - A \in ℂ$
12		addcom	$⊢ (- A \in ℂ \land z \in ℂ) \to - A + z = z + (- A)$
13	11 12	sylan	$⊢ (A \in ℂ \land z \in ℂ) \to - A + z = z + (- A)$
14		negsub	$⊢ (z \in ℂ \land A \in ℂ) \to z + (- A) = z - A$
15	14	ancoms	$⊢ (A \in ℂ \land z \in ℂ) \to z + (- A) = z - A$
16	13 15	eqtrd	$⊢ (A \in ℂ \land z \in ℂ) \to - A + z = z - A$
17	16	mpteq2dva	$⊢ A \in ℂ \to (z \in ℂ ⟼ - A + z) = (z \in ℂ ⟼ z - A)$
18		cnex	$⊢ ℂ \in V$
19	18	a1i	$⊢ A \in ℂ \to ℂ \in V$
20		negex	$⊢ - A \in V$
21	20	a1i	$⊢ (A \in ℂ \land z \in ℂ) \to - A \in V$
22		simpr	$⊢ (A \in ℂ \land z \in ℂ) \to z \in ℂ$
23		fconstmpt	$⊢ ℂ \times \{- A\} = (z \in ℂ ⟼ - A)$
24	23	a1i	$⊢ A \in ℂ \to ℂ \times \{- A\} = (z \in ℂ ⟼ - A)$
25		df-idp	$⊢ X^{p} = {I ↾}_{ℂ}$
26		mptresid	$⊢ {I ↾}_{ℂ} = (z \in ℂ ⟼ z)$
27	25 26	eqtri	$⊢ X^{p} = (z \in ℂ ⟼ z)$
28	27	a1i	$⊢ A \in ℂ \to X^{p} = (z \in ℂ ⟼ z)$
29	19 21 22 24 28	offval2	$⊢ A \in ℂ \to (ℂ \times \{- A\}) +_{f} X^{p} = (z \in ℂ ⟼ - A + z)$
30		simpl	$⊢ (A \in ℂ \land z \in ℂ) \to A \in ℂ$
31		fconstmpt	$⊢ ℂ \times \{A\} = (z \in ℂ ⟼ A)$
32	31	a1i	$⊢ A \in ℂ \to ℂ \times \{A\} = (z \in ℂ ⟼ A)$
33	19 22 30 28 32	offval2	$⊢ A \in ℂ \to X^{p} -_{f} (ℂ \times \{A\}) = (z \in ℂ ⟼ z - A)$
34	17 29 33	3eqtr4d	$⊢ A \in ℂ \to (ℂ \times \{- A\}) +_{f} X^{p} = X^{p} -_{f} (ℂ \times \{A\})$
35	34 1	eqtr4di	$⊢ A \in ℂ \to (ℂ \times \{- A\}) +_{f} X^{p} = G$
36	35	fveq2d	$⊢ A \in ℂ \to \deg ((ℂ \times \{- A\}) +_{f} X^{p}) = \deg (G)$
37		plyconst	$⊢ (ℂ \subseteq ℂ \land - A \in ℂ) \to ℂ \times \{- A\} \in Poly (ℂ)$
38	2 11 37	sylancr	$⊢ A \in ℂ \to ℂ \times \{- A\} \in Poly (ℂ)$
39	5	a1i	$⊢ A \in ℂ \to X^{p} \in Poly (ℂ)$
40		0dgr	$⊢ - A \in ℂ \to \deg (ℂ \times \{- A\}) = 0$
41	11 40	syl	$⊢ A \in ℂ \to \deg (ℂ \times \{- A\}) = 0$
42		0lt1	$⊢ 0 < 1$
43	41 42	eqbrtrdi	$⊢ A \in ℂ \to \deg (ℂ \times \{- A\}) < 1$
44		eqid	$⊢ \deg (ℂ \times \{- A\}) = \deg (ℂ \times \{- A\})$
45		dgrid	$⊢ \deg (X^{p}) = 1$
46	45	eqcomi	$⊢ 1 = \deg (X^{p})$
47	44 46	dgradd2	$⊢ (ℂ \times \{- A\} \in Poly (ℂ) \land X^{p} \in Poly (ℂ) \land \deg (ℂ \times \{- A\}) < 1) \to \deg ((ℂ \times \{- A\}) +_{f} X^{p}) = 1$
48	38 39 43 47	syl3anc	$⊢ A \in ℂ \to \deg ((ℂ \times \{- A\}) +_{f} X^{p}) = 1$
49	36 48	eqtr3d	$⊢ A \in ℂ \to \deg (G) = 1$
50	1 33	eqtrid	$⊢ A \in ℂ \to G = (z \in ℂ ⟼ z - A)$
51	50	fveq1d	$⊢ A \in ℂ \to G (z) = (z \in ℂ ⟼ z - A) (z)$
52	51	adantr	$⊢ (A \in ℂ \land z \in ℂ) \to G (z) = (z \in ℂ ⟼ z - A) (z)$
53		ovex	$⊢ z - A \in V$
54		eqid	$⊢ (z \in ℂ ⟼ z - A) = (z \in ℂ ⟼ z - A)$
55	54	fvmpt2	$⊢ (z \in ℂ \land z - A \in V) \to (z \in ℂ ⟼ z - A) (z) = z - A$
56	22 53 55	sylancl	$⊢ (A \in ℂ \land z \in ℂ) \to (z \in ℂ ⟼ z - A) (z) = z - A$
57	52 56	eqtrd	$⊢ (A \in ℂ \land z \in ℂ) \to G (z) = z - A$
58	57	eqeq1d	$⊢ (A \in ℂ \land z \in ℂ) \to (G (z) = 0 \leftrightarrow z - A = 0)$
59		subeq0	$⊢ (z \in ℂ \land A \in ℂ) \to (z - A = 0 \leftrightarrow z = A)$
60	59	ancoms	$⊢ (A \in ℂ \land z \in ℂ) \to (z - A = 0 \leftrightarrow z = A)$
61	58 60	bitrd	$⊢ (A \in ℂ \land z \in ℂ) \to (G (z) = 0 \leftrightarrow z = A)$
62	61	pm5.32da	$⊢ A \in ℂ \to ((z \in ℂ \land G (z) = 0) \leftrightarrow (z \in ℂ \land z = A))$
63		plyf	$⊢ G \in Poly (ℂ) \to G : ℂ ⟶ ℂ$
64		ffn	$⊢ G : ℂ ⟶ ℂ \to G Fn ℂ$
65		fniniseg	$⊢ G Fn ℂ \to (z \in G^{-1} [\{0\}] \leftrightarrow (z \in ℂ \land G (z) = 0))$
66	10 63 64 65	4syl	$⊢ A \in ℂ \to (z \in G^{-1} [\{0\}] \leftrightarrow (z \in ℂ \land G (z) = 0))$
67		eleq1a	$⊢ A \in ℂ \to (z = A \to z \in ℂ)$
68	67	pm4.71rd	$⊢ A \in ℂ \to (z = A \leftrightarrow (z \in ℂ \land z = A))$
69	62 66 68	3bitr4d	$⊢ A \in ℂ \to (z \in G^{-1} [\{0\}] \leftrightarrow z = A)$
70		velsn	$⊢ z \in \{A\} \leftrightarrow z = A$
71	69 70	bitr4di	$⊢ A \in ℂ \to (z \in G^{-1} [\{0\}] \leftrightarrow z \in \{A\})$
72	71	eqrdv	$⊢ A \in ℂ \to G^{-1} [\{0\}] = \{A\}$
73	10 49 72	3jca	$⊢ A \in ℂ \to (G \in Poly (ℂ) \land \deg (G) = 1 \land G^{-1} [\{0\}] = \{A\})$

Metamath Proof Explorer

Theorem plyremlem

Proof