Metamath Proof Explorer

Theorem plycj

Description: The double conjugation of a polynomial is a polynomial. (The single conjugation is not because our definition of polynomial includes only holomorphic functions, i.e. no dependence on ( *z ) independently of z .) (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses plycj.1 ⊢ 𝑁 = ( deg ‘ 𝐹 )
plycj.2 ⊢ 𝐺 = ( ( ∗ ∘ 𝐹 ) ∘ ∗ )
plycj.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ∗ ‘ 𝑥 ) ∈ 𝑆 )
plycj.4 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
Assertion plycj ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 plycj.1 ⊢ 𝑁 = ( deg ‘ 𝐹 )
2 plycj.2 ⊢ 𝐺 = ( ( ∗ ∘ 𝐹 ) ∘ ∗ )
3 plycj.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ∗ ‘ 𝑥 ) ∈ 𝑆 )
4 plycj.4 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
5 eqid ⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
6 1 2 5 plycjlem ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ∗ ∘ ( coeff ‘ 𝐹 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
7 4 6 syl ⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ∗ ∘ ( coeff ‘ 𝐹 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
8 plybss ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ )
9 4 8 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
10 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
11 10 snssd ⊢ ( 𝜑 → { 0 } ⊆ ℂ )
12 9 11 unssd ⊢ ( 𝜑 → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
13 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
14 4 13 syl ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℕ0 )
15 1 14 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
16 5 coef ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
17 4 16 syl ⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
18 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
19 fvco3 ⊢ ( ( ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ∗ ∘ ( coeff ‘ 𝐹 ) ) ‘ 𝑘 ) = ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) )
20 17 18 19 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ∗ ∘ ( coeff ‘ 𝐹 ) ) ‘ 𝑘 ) = ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) )
21 ffvelrn ⊢ ( ( ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) )
22 17 18 21 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) )
23 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( ∗ ‘ 𝑥 ) ∈ 𝑆 )
24 fveq2 ⊢ ( 𝑥 = ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) → ( ∗ ‘ 𝑥 ) = ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) )
25 24 eleq1d ⊢ ( 𝑥 = ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) → ( ( ∗ ‘ 𝑥 ) ∈ 𝑆 ↔ ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ 𝑆 ) )
26 25 rspccv ⊢ ( ∀ 𝑥 ∈ 𝑆 ( ∗ ‘ 𝑥 ) ∈ 𝑆 → ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑆 → ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ 𝑆 ) )
27 23 26 syl ⊢ ( 𝜑 → ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑆 → ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ 𝑆 ) )
28 elsni ⊢ ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ { 0 } → ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) = 0 )
29 28 fveq2d ⊢ ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ { 0 } → ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) = ( ∗ ‘ 0 ) )
30 cj0 ⊢ ( ∗ ‘ 0 ) = 0
31 29 30 eqtrdi ⊢ ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ { 0 } → ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) = 0 )
32 fvex ⊢ ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ V
33 32 elsn ⊢ ( ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ { 0 } ↔ ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) = 0 )
34 31 33 sylibr ⊢ ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ { 0 } → ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ { 0 } )
35 34 a1i ⊢ ( 𝜑 → ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ { 0 } → ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ { 0 } ) )
36 27 35 orim12d ⊢ ( 𝜑 → ( ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑆 ∨ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ { 0 } ) → ( ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ 𝑆 ∨ ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ { 0 } ) ) )
37 elun ⊢ ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) ↔ ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑆 ∨ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ { 0 } ) )
38 elun ⊢ ( ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ ( 𝑆 ∪ { 0 } ) ↔ ( ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ 𝑆 ∨ ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ { 0 } ) )
39 36 37 38 3imtr4g ⊢ ( 𝜑 → ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) → ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ ( 𝑆 ∪ { 0 } ) ) )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) → ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ ( 𝑆 ∪ { 0 } ) ) )
41 22 40 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ∗ ‘ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ ( 𝑆 ∪ { 0 } ) )
42 20 41 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ∗ ∘ ( coeff ‘ 𝐹 ) ) ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) )
43 12 15 42 elplyd ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ∗ ∘ ( coeff ‘ 𝐹 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) )
44 7 43 eqeltrd ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) )
45 plyun0 ⊢ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) = ( Poly ‘ 𝑆 )
46 44 45 eleqtrdi ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )