plyexmo

Description: An infinite set of values can be extended to a polynomial in at most one way. (Contributed by Stefan O'Rear, 14-Nov-2014)

		Ref	Expression
	Assertion	plyexmo	$⊢ (D \subseteq ℂ \land \neg D \in Fin) \to \exists^{*} p (p \in Poly (S) \land {p ↾}_{D} = F)$

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to \neg D \in Fin$
2		simpll	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to D \subseteq ℂ$
3	2	sseld	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to (b \in D \to b \in ℂ)$
4		simprll	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to p \in Poly (ℂ)$
5		plyf	$⊢ p \in Poly (ℂ) \to p : ℂ ⟶ ℂ$
6	4 5	syl	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to p : ℂ ⟶ ℂ$
7	6	ffnd	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to p Fn ℂ$
8	7	adantr	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land b \in D) \to p Fn ℂ$
9		simprrl	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to a \in Poly (ℂ)$
10		plyf	$⊢ a \in Poly (ℂ) \to a : ℂ ⟶ ℂ$
11	9 10	syl	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to a : ℂ ⟶ ℂ$
12	11	ffnd	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to a Fn ℂ$
13	12	adantr	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land b \in D) \to a Fn ℂ$
14		cnex	$⊢ ℂ \in V$
15	14	a1i	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land b \in D) \to ℂ \in V$
16	2	sselda	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land b \in D) \to b \in ℂ$
17		fnfvof	$⊢ ((p Fn ℂ \land a Fn ℂ) \land (ℂ \in V \land b \in ℂ)) \to (p -_{f} a) (b) = p (b) - a (b)$
18	8 13 15 16 17	syl22anc	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land b \in D) \to (p -_{f} a) (b) = p (b) - a (b)$
19	6	adantr	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land b \in D) \to p : ℂ ⟶ ℂ$
20	19 16	ffvelrnd	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land b \in D) \to p (b) \in ℂ$
21		simprlr	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to {p ↾}_{D} = F$
22		simprrr	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to {a ↾}_{D} = F$
23	21 22	eqtr4d	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to {p ↾}_{D} = {a ↾}_{D}$
24	23	adantr	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land b \in D) \to {p ↾}_{D} = {a ↾}_{D}$
25	24	fveq1d	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land b \in D) \to ({p ↾}_{D}) (b) = ({a ↾}_{D}) (b)$
26		fvres	$⊢ b \in D \to ({p ↾}_{D}) (b) = p (b)$
27	26	adantl	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land b \in D) \to ({p ↾}_{D}) (b) = p (b)$
28		fvres	$⊢ b \in D \to ({a ↾}_{D}) (b) = a (b)$
29	28	adantl	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land b \in D) \to ({a ↾}_{D}) (b) = a (b)$
30	25 27 29	3eqtr3d	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land b \in D) \to p (b) = a (b)$
31	20 30	subeq0bd	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land b \in D) \to p (b) - a (b) = 0$
32	18 31	eqtrd	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land b \in D) \to (p -_{f} a) (b) = 0$
33	32	ex	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to (b \in D \to (p -_{f} a) (b) = 0)$
34	3 33	jcad	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to (b \in D \to (b \in ℂ \land (p -_{f} a) (b) = 0))$
35		plysubcl	$⊢ (p \in Poly (ℂ) \land a \in Poly (ℂ)) \to p -_{f} a \in Poly (ℂ)$
36	4 9 35	syl2anc	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to p -_{f} a \in Poly (ℂ)$
37		plyf	$⊢ p -_{f} a \in Poly (ℂ) \to (p -_{f} a) : ℂ ⟶ ℂ$
38		ffn	$⊢ (p -_{f} a) : ℂ ⟶ ℂ \to (p -_{f} a) Fn ℂ$
39		fniniseg	$⊢ (p -_{f} a) Fn ℂ \to (b \in {(p -_{f} a)}^{-1} [\{0\}] \leftrightarrow (b \in ℂ \land (p -_{f} a) (b) = 0))$
40	36 37 38 39	4syl	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to (b \in {(p -_{f} a)}^{-1} [\{0\}] \leftrightarrow (b \in ℂ \land (p -_{f} a) (b) = 0))$
41	34 40	sylibrd	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to (b \in D \to b \in {(p -_{f} a)}^{-1} [\{0\}])$
42	41	ssrdv	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to D \subseteq {(p -_{f} a)}^{-1} [\{0\}]$
43		ssfi	$⊢ ({(p -_{f} a)}^{-1} [\{0\}] \in Fin \land D \subseteq {(p -_{f} a)}^{-1} [\{0\}]) \to D \in Fin$
44	43	expcom	$⊢ D \subseteq {(p -_{f} a)}^{-1} [\{0\}] \to ({(p -_{f} a)}^{-1} [\{0\}] \in Fin \to D \in Fin)$
45	42 44	syl	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to ({(p -_{f} a)}^{-1} [\{0\}] \in Fin \to D \in Fin)$
46	1 45	mtod	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to \neg {(p -_{f} a)}^{-1} [\{0\}] \in Fin$
47		neqne	$⊢ \neg p -_{f} a = 0_{𝑝} \to p -_{f} a \neq 0_{𝑝}$
48		eqid	$⊢ {(p -_{f} a)}^{-1} [\{0\}] = {(p -_{f} a)}^{-1} [\{0\}]$
49	48	fta1	$⊢ (p -_{f} a \in Poly (ℂ) \land p -_{f} a \neq 0_{𝑝}) \to ({(p -_{f} a)}^{-1} [\{0\}] \in Fin \land \|{(p -_{f} a)}^{-1} [\{0\}]\| \leq \deg (p -_{f} a))$
50	36 47 49	syl2an	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land \neg p -_{f} a = 0_{𝑝}) \to ({(p -_{f} a)}^{-1} [\{0\}] \in Fin \land \|{(p -_{f} a)}^{-1} [\{0\}]\| \leq \deg (p -_{f} a))$
51	50	simpld	$⊢ (((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \land \neg p -_{f} a = 0_{𝑝}) \to {(p -_{f} a)}^{-1} [\{0\}] \in Fin$
52	51	ex	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to (\neg p -_{f} a = 0_{𝑝} \to {(p -_{f} a)}^{-1} [\{0\}] \in Fin)$
53	46 52	mt3d	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to p -_{f} a = 0_{𝑝}$
54		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
55	53 54	syl6eq	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to p -_{f} a = ℂ \times \{0\}$
56		ofsubeq0	$⊢ (ℂ \in V \land p : ℂ ⟶ ℂ \land a : ℂ ⟶ ℂ) \to (p -_{f} a = ℂ \times \{0\} \leftrightarrow p = a)$
57	14 6 11 56	mp3an2i	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to (p -_{f} a = ℂ \times \{0\} \leftrightarrow p = a)$
58	55 57	mpbid	$⊢ ((D \subseteq ℂ \land \neg D \in Fin) \land ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F))) \to p = a$
59	58	ex	$⊢ (D \subseteq ℂ \land \neg D \in Fin) \to (((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F)) \to p = a)$
60	59	alrimivv	$⊢ (D \subseteq ℂ \land \neg D \in Fin) \to \forall p \forall a (((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F)) \to p = a)$
61		eleq1w	$⊢ p = a \to (p \in Poly (ℂ) \leftrightarrow a \in Poly (ℂ))$
62		reseq1	$⊢ p = a \to {p ↾}_{D} = {a ↾}_{D}$
63	62	eqeq1d	$⊢ p = a \to ({p ↾}_{D} = F \leftrightarrow {a ↾}_{D} = F)$
64	61 63	anbi12d	$⊢ p = a \to ((p \in Poly (ℂ) \land {p ↾}_{D} = F) \leftrightarrow (a \in Poly (ℂ) \land {a ↾}_{D} = F))$
65	64	mo4	$⊢ \exists^{*} p (p \in Poly (ℂ) \land {p ↾}_{D} = F) \leftrightarrow \forall p \forall a (((p \in Poly (ℂ) \land {p ↾}_{D} = F) \land (a \in Poly (ℂ) \land {a ↾}_{D} = F)) \to p = a)$
66	60 65	sylibr	$⊢ (D \subseteq ℂ \land \neg D \in Fin) \to \exists^{*} p (p \in Poly (ℂ) \land {p ↾}_{D} = F)$
67		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
68	67	sseli	$⊢ p \in Poly (S) \to p \in Poly (ℂ)$
69	68	anim1i	$⊢ (p \in Poly (S) \land {p ↾}_{D} = F) \to (p \in Poly (ℂ) \land {p ↾}_{D} = F)$
70	69	moimi	$⊢ \exists^{} p (p \in Poly (ℂ) \land {p ↾}_{D} = F) \to \exists^{} p (p \in Poly (S) \land {p ↾}_{D} = F)$
71	66 70	syl	$⊢ (D \subseteq ℂ \land \neg D \in Fin) \to \exists^{*} p (p \in Poly (S) \land {p ↾}_{D} = F)$

Metamath Proof Explorer

Theorem plyexmo

Proof