plyconz

Description: The composition of a nonzero and a nonconstant polynomial is a nonzero polynomial. (Contributed by SN, 30-Aug-2026)

	Ref	Expression
Hypotheses	plyconz.f	$⊢ φ \to F \in Poly (S)$
	plyconz.g	$⊢ φ \to G \in Poly (S)$
	plyconz.1	$⊢ φ \to F \neq 0_{𝑝}$
	plyconz.2	$⊢ φ \to \deg (G) \neq 0$
Assertion	plyconz	$⊢ φ \to F \circ G \neq 0_{𝑝}$

Proof

Step	Hyp	Ref	Expression
1		plyconz.f	$⊢ φ \to F \in Poly (S)$
2		plyconz.g	$⊢ φ \to G \in Poly (S)$
3		plyconz.1	$⊢ φ \to F \neq 0_{𝑝}$
4		plyconz.2	$⊢ φ \to \deg (G) \neq 0$
5	2 4	rnplynfin	$⊢ φ \to \neg ran G \in Fin$
6		eqid	$⊢ F^{-1} [\{0\}] = F^{-1} [\{0\}]$
7	6	fta1	$⊢ (F \in Poly (S) \land F \neq 0_{𝑝}) \to (F^{-1} [\{0\}] \in Fin \land \|F^{-1} [\{0\}]\| \leq \deg (F))$
8	1 3 7	syl2anc	$⊢ φ \to (F^{-1} [\{0\}] \in Fin \land \|F^{-1} [\{0\}]\| \leq \deg (F))$
9	8	simpld	$⊢ φ \to F^{-1} [\{0\}] \in Fin$
10	9	adantr	$⊢ (φ \land ran G \subseteq F^{-1} [\{0\}]) \to F^{-1} [\{0\}] \in Fin$
11		simpr	$⊢ (φ \land ran G \subseteq F^{-1} [\{0\}]) \to ran G \subseteq F^{-1} [\{0\}]$
12	10 11	ssfid	$⊢ (φ \land ran G \subseteq F^{-1} [\{0\}]) \to ran G \in Fin$
13	5 12	mtand	$⊢ φ \to \neg ran G \subseteq F^{-1} [\{0\}]$
14		plyf	$⊢ G \in Poly (S) \to G : ℂ ⟶ ℂ$
15	2 14	syl	$⊢ φ \to G : ℂ ⟶ ℂ$
16	15	frnd	$⊢ φ \to ran G \subseteq ℂ$
17	16	sseld	$⊢ φ \to (z \in ran G \to z \in ℂ)$
18		fveqeq2	$⊢ y = z \to (F (y) = 0 \leftrightarrow F (z) = 0)$
19	18	rspcv	$⊢ z \in ran G \to (\forall y \in ran G F (y) = 0 \to F (z) = 0)$
20	19	com12	$⊢ \forall y \in ran G F (y) = 0 \to (z \in ran G \to F (z) = 0)$
21	17 20	anim12ii	$⊢ (φ \land \forall y \in ran G F (y) = 0) \to (z \in ran G \to (z \in ℂ \land F (z) = 0))$
22		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
23	1 22	syl	$⊢ φ \to F : ℂ ⟶ ℂ$
24	23	ffnd	$⊢ φ \to F Fn ℂ$
25	24	adantr	$⊢ (φ \land \forall y \in ran G F (y) = 0) \to F Fn ℂ$
26		fniniseg	$⊢ F Fn ℂ \to (z \in F^{-1} [\{0\}] \leftrightarrow (z \in ℂ \land F (z) = 0))$
27	25 26	syl	$⊢ (φ \land \forall y \in ran G F (y) = 0) \to (z \in F^{-1} [\{0\}] \leftrightarrow (z \in ℂ \land F (z) = 0))$
28	21 27	sylibrd	$⊢ (φ \land \forall y \in ran G F (y) = 0) \to (z \in ran G \to z \in F^{-1} [\{0\}])$
29	28	ssrdv	$⊢ (φ \land \forall y \in ran G F (y) = 0) \to ran G \subseteq F^{-1} [\{0\}]$
30	13 29	mtand	$⊢ φ \to \neg \forall y \in ran G F (y) = 0$
31		df-ne	$⊢ F (y) \neq 0 \leftrightarrow \neg F (y) = 0$
32	31	rexbii	$⊢ \exists y \in ran G F (y) \neq 0 \leftrightarrow \exists y \in ran G \neg F (y) = 0$
33		rexnal	$⊢ \exists y \in ran G \neg F (y) = 0 \leftrightarrow \neg \forall y \in ran G F (y) = 0$
34	32 33	bitri	$⊢ \exists y \in ran G F (y) \neq 0 \leftrightarrow \neg \forall y \in ran G F (y) = 0$
35	30 34	sylibr	$⊢ φ \to \exists y \in ran G F (y) \neq 0$
36		fvexd	$⊢ (φ \land x \in ℂ) \to G (x) \in V$
37	15	ffnd	$⊢ φ \to G Fn ℂ$
38		fvelrnb	$⊢ G Fn ℂ \to (y \in ran G \leftrightarrow \exists x \in ℂ G (x) = y)$
39		eqcom	$⊢ G (x) = y \leftrightarrow y = G (x)$
40	39	rexbii	$⊢ \exists x \in ℂ G (x) = y \leftrightarrow \exists x \in ℂ y = G (x)$
41	38 40	bitrdi	$⊢ G Fn ℂ \to (y \in ran G \leftrightarrow \exists x \in ℂ y = G (x))$
42	37 41	syl	$⊢ φ \to (y \in ran G \leftrightarrow \exists x \in ℂ y = G (x))$
43		fveq2	$⊢ y = G (x) \to F (y) = F (G (x))$
44	43	neeq1d	$⊢ y = G (x) \to (F (y) \neq 0 \leftrightarrow F (G (x)) \neq 0)$
45	44	adantl	$⊢ (φ \land y = G (x)) \to (F (y) \neq 0 \leftrightarrow F (G (x)) \neq 0)$
46	36 42 45	rexxfr2d	$⊢ φ \to (\exists y \in ran G F (y) \neq 0 \leftrightarrow \exists x \in ℂ F (G (x)) \neq 0)$
47	35 46	mpbid	$⊢ φ \to \exists x \in ℂ F (G (x)) \neq 0$
48	15	ffund	$⊢ φ \to Fun G$
49	48	adantr	$⊢ (φ \land x \in ℂ) \to Fun G$
50	15	fdmd	$⊢ φ \to dom G = ℂ$
51	50	eqimsscd	$⊢ φ \to ℂ \subseteq dom G$
52	51	sselda	$⊢ (φ \land x \in ℂ) \to x \in dom G$
53		eqid	$⊢ F \circ G = F \circ G$
54	49 52 53	fvcod	$⊢ (φ \land x \in ℂ) \to (F \circ G) (x) = F (G (x))$
55	54	neeq1d	$⊢ (φ \land x \in ℂ) \to ((F \circ G) (x) \neq 0 \leftrightarrow F (G (x)) \neq 0)$
56	55	rexbidva	$⊢ φ \to (\exists x \in ℂ (F \circ G) (x) \neq 0 \leftrightarrow \exists x \in ℂ F (G (x)) \neq 0)$
57	47 56	mpbird	$⊢ φ \to \exists x \in ℂ (F \circ G) (x) \neq 0$
58		ne0p	$⊢ (x \in ℂ \land (F \circ G) (x) \neq 0) \to F \circ G \neq 0_{𝑝}$
59	58	rexlimiva	$⊢ \exists x \in ℂ (F \circ G) (x) \neq 0 \to F \circ G \neq 0_{𝑝}$
60	57 59	syl	$⊢ φ \to F \circ G \neq 0_{𝑝}$

Metamath Proof Explorer

Theorem plyconz

Proof