Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
plyconz.g ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
plyconz.1 ⊢ ( 𝜑 → 𝐹 ≠ 0𝑝 )
plyconz.2 ⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ≠ 0 )
Assertion plyconz ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ≠ 0𝑝 )

Proof

Step Hyp Ref Expression
1 plyconz.f ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
2 plyconz.g ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
3 plyconz.1 ⊢ ( 𝜑 → 𝐹 ≠ 0𝑝 )
4 plyconz.2 ⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ≠ 0 )
5 2 4 rnplynfin ⊢ ( 𝜑 → ¬ ran 𝐺 ∈ Fin )
6 eqid ⊢ ( ◡ 𝐹 “ { 0 } ) = ( ◡ 𝐹 “ { 0 } )
7 6 fta1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) → ( ( ◡ 𝐹 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ 𝐹 “ { 0 } ) ) ≤ ( deg ‘ 𝐹 ) ) )
8 1 3 7 syl2anc ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ 𝐹 “ { 0 } ) ) ≤ ( deg ‘ 𝐹 ) ) )
9 8 simpld ⊢ ( 𝜑 → ( ◡ 𝐹 “ { 0 } ) ∈ Fin )
10 9 adantr ⊢ ( ( 𝜑 ∧ ran 𝐺 ⊆ ( ◡ 𝐹 “ { 0 } ) ) → ( ◡ 𝐹 “ { 0 } ) ∈ Fin )
11 simpr ⊢ ( ( 𝜑 ∧ ran 𝐺 ⊆ ( ◡ 𝐹 “ { 0 } ) ) → ran 𝐺 ⊆ ( ◡ 𝐹 “ { 0 } ) )
12 10 11 ssfid ⊢ ( ( 𝜑 ∧ ran 𝐺 ⊆ ( ◡ 𝐹 “ { 0 } ) ) → ran 𝐺 ∈ Fin )
13 5 12 mtand ⊢ ( 𝜑 → ¬ ran 𝐺 ⊆ ( ◡ 𝐹 “ { 0 } ) )
14 plyf ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 : ℂ ⟶ ℂ )
15 2 14 syl ⊢ ( 𝜑 → 𝐺 : ℂ ⟶ ℂ )
16 15 frnd ⊢ ( 𝜑 → ran 𝐺 ⊆ ℂ )
17 16 sseld ⊢ ( 𝜑 → ( 𝑧 ∈ ran 𝐺 → 𝑧 ∈ ℂ ) )
18 fveqeq2 ⊢ ( 𝑦 = 𝑧 → ( ( 𝐹 ‘ 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑧 ) = 0 ) )
19 18 rspcv ⊢ ( 𝑧 ∈ ran 𝐺 → ( ∀ 𝑦 ∈ ran 𝐺 ( 𝐹 ‘ 𝑦 ) = 0 → ( 𝐹 ‘ 𝑧 ) = 0 ) )
20 19 com12 ⊢ ( ∀ 𝑦 ∈ ran 𝐺 ( 𝐹 ‘ 𝑦 ) = 0 → ( 𝑧 ∈ ran 𝐺 → ( 𝐹 ‘ 𝑧 ) = 0 ) )
21 17 20 anim12ii ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran 𝐺 ( 𝐹 ‘ 𝑦 ) = 0 ) → ( 𝑧 ∈ ran 𝐺 → ( 𝑧 ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) = 0 ) ) )
22 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
23 1 22 syl ⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
24 23 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℂ )
25 24 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran 𝐺 ( 𝐹 ‘ 𝑦 ) = 0 ) → 𝐹 Fn ℂ )
26 fniniseg ⊢ ( 𝐹 Fn ℂ → ( 𝑧 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑧 ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) = 0 ) ) )
27 25 26 syl ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran 𝐺 ( 𝐹 ‘ 𝑦 ) = 0 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑧 ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) = 0 ) ) )
28 21 27 sylibrd ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran 𝐺 ( 𝐹 ‘ 𝑦 ) = 0 ) → ( 𝑧 ∈ ran 𝐺 → 𝑧 ∈ ( ◡ 𝐹 “ { 0 } ) ) )
29 28 ssrdv ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran 𝐺 ( 𝐹 ‘ 𝑦 ) = 0 ) → ran 𝐺 ⊆ ( ◡ 𝐹 “ { 0 } ) )
30 13 29 mtand ⊢ ( 𝜑 → ¬ ∀ 𝑦 ∈ ran 𝐺 ( 𝐹 ‘ 𝑦 ) = 0 )
31 df-ne ⊢ ( ( 𝐹 ‘ 𝑦 ) ≠ 0 ↔ ¬ ( 𝐹 ‘ 𝑦 ) = 0 )
32 31 rexbii ⊢ ( ∃ 𝑦 ∈ ran 𝐺 ( 𝐹 ‘ 𝑦 ) ≠ 0 ↔ ∃ 𝑦 ∈ ran 𝐺 ¬ ( 𝐹 ‘ 𝑦 ) = 0 )
33 rexnal ⊢ ( ∃ 𝑦 ∈ ran 𝐺 ¬ ( 𝐹 ‘ 𝑦 ) = 0 ↔ ¬ ∀ 𝑦 ∈ ran 𝐺 ( 𝐹 ‘ 𝑦 ) = 0 )
34 32 33 bitri ⊢ ( ∃ 𝑦 ∈ ran 𝐺 ( 𝐹 ‘ 𝑦 ) ≠ 0 ↔ ¬ ∀ 𝑦 ∈ ran 𝐺 ( 𝐹 ‘ 𝑦 ) = 0 )
35 30 34 sylibr ⊢ ( 𝜑 → ∃ 𝑦 ∈ ran 𝐺 ( 𝐹 ‘ 𝑦 ) ≠ 0 )
36 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐺 ‘ 𝑥 ) ∈ V )
37 15 ffnd ⊢ ( 𝜑 → 𝐺 Fn ℂ )
38 fvelrnb ⊢ ( 𝐺 Fn ℂ → ( 𝑦 ∈ ran 𝐺 ↔ ∃ 𝑥 ∈ ℂ ( 𝐺 ‘ 𝑥 ) = 𝑦 ) )
39 eqcom ⊢ ( ( 𝐺 ‘ 𝑥 ) = 𝑦 ↔ 𝑦 = ( 𝐺 ‘ 𝑥 ) )
40 39 rexbii ⊢ ( ∃ 𝑥 ∈ ℂ ( 𝐺 ‘ 𝑥 ) = 𝑦 ↔ ∃ 𝑥 ∈ ℂ 𝑦 = ( 𝐺 ‘ 𝑥 ) )
41 38 40 bitrdi ⊢ ( 𝐺 Fn ℂ → ( 𝑦 ∈ ran 𝐺 ↔ ∃ 𝑥 ∈ ℂ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) )
42 37 41 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝐺 ↔ ∃ 𝑥 ∈ ℂ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) )
43 fveq2 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
44 43 neeq1d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) ≠ 0 ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ≠ 0 ) )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑦 ) ≠ 0 ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ≠ 0 ) )
46 36 42 45 rexxfr2d ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ran 𝐺 ( 𝐹 ‘ 𝑦 ) ≠ 0 ↔ ∃ 𝑥 ∈ ℂ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ≠ 0 ) )
47 35 46 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℂ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ≠ 0 )
48 15 ffund ⊢ ( 𝜑 → Fun 𝐺 )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → Fun 𝐺 )
50 15 fdmd ⊢ ( 𝜑 → dom 𝐺 = ℂ )
51 50 eqimsscd ⊢ ( 𝜑 → ℂ ⊆ dom 𝐺 )
52 51 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ dom 𝐺 )
53 eqid ⊢ ( 𝐹 ∘ 𝐺 ) = ( 𝐹 ∘ 𝐺 )
54 49 52 53 fvcod ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
55 54 neeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ≠ 0 ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ≠ 0 ) )
56 55 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℂ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ≠ 0 ↔ ∃ 𝑥 ∈ ℂ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ≠ 0 ) )
57 47 56 mpbird ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℂ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ≠ 0 )
58 ne0p ⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ≠ 0 ) → ( 𝐹 ∘ 𝐺 ) ≠ 0𝑝 )
59 58 rexlimiva ⊢ ( ∃ 𝑥 ∈ ℂ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ≠ 0 → ( 𝐹 ∘ 𝐺 ) ≠ 0𝑝 )
60 57 59 syl ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ≠ 0𝑝 )