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 ⊢ N = deg ⁡ F
plycj.2 ⊢ G = * ∘ F ∘ *
plycj.3 ⊢ φ ∧ x ∈ S → x ‾ ∈ S
plycj.4 ⊢ φ → F ∈ Poly ⁡ S
Assertion plycj ⊢ φ → G ∈ Poly ⁡ S

Proof

Step Hyp Ref Expression
1 plycj.1 ⊢ N = deg ⁡ F
2 plycj.2 ⊢ G = * ∘ F ∘ *
3 plycj.3 ⊢ φ ∧ x ∈ S → x ‾ ∈ S
4 plycj.4 ⊢ φ → F ∈ Poly ⁡ S
5 eqid ⊢ coeff ⁡ F = coeff ⁡ F
6 1 2 5 plycjlem ⊢ F ∈ Poly ⁡ S → G = z ∈ ℂ ⟼ ∑ k = 0 N * ∘ coeff ⁡ F ⁡ k ⁢ z k
7 4 6 syl ⊢ φ → G = z ∈ ℂ ⟼ ∑ k = 0 N * ∘ coeff ⁡ F ⁡ k ⁢ z k
8 plybss ⊢ F ∈ Poly ⁡ S → S ⊆ ℂ
9 4 8 syl ⊢ φ → S ⊆ ℂ
10 0cnd ⊢ φ → 0 ∈ ℂ
11 10 snssd ⊢ φ → 0 ⊆ ℂ
12 9 11 unssd ⊢ φ → S ∪ 0 ⊆ ℂ
13 dgrcl ⊢ F ∈ Poly ⁡ S → deg ⁡ F ∈ ℕ 0
14 4 13 syl ⊢ φ → deg ⁡ F ∈ ℕ 0
15 1 14 eqeltrid ⊢ φ → N ∈ ℕ 0
16 5 coef ⊢ F ∈ Poly ⁡ S → coeff ⁡ F : ℕ 0 ⟶ S ∪ 0
17 4 16 syl ⊢ φ → coeff ⁡ F : ℕ 0 ⟶ S ∪ 0
18 elfznn0 ⊢ k ∈ 0 … N → k ∈ ℕ 0
19 fvco3 ⊢ coeff ⁡ F : ℕ 0 ⟶ S ∪ 0 ∧ k ∈ ℕ 0 → * ∘ coeff ⁡ F ⁡ k = coeff ⁡ F ⁡ k ‾
20 17 18 19 syl2an ⊢ φ ∧ k ∈ 0 … N → * ∘ coeff ⁡ F ⁡ k = coeff ⁡ F ⁡ k ‾
21 ffvelrn ⊢ coeff ⁡ F : ℕ 0 ⟶ S ∪ 0 ∧ k ∈ ℕ 0 → coeff ⁡ F ⁡ k ∈ S ∪ 0
22 17 18 21 syl2an ⊢ φ ∧ k ∈ 0 … N → coeff ⁡ F ⁡ k ∈ S ∪ 0
23 3 ralrimiva ⊢ φ → ∀ x ∈ S x ‾ ∈ S
24 fveq2 ⊢ x = coeff ⁡ F ⁡ k → x ‾ = coeff ⁡ F ⁡ k ‾
25 24 eleq1d ⊢ x = coeff ⁡ F ⁡ k → x ‾ ∈ S ↔ coeff ⁡ F ⁡ k ‾ ∈ S
26 25 rspccv ⊢ ∀ x ∈ S x ‾ ∈ S → coeff ⁡ F ⁡ k ∈ S → coeff ⁡ F ⁡ k ‾ ∈ S
27 23 26 syl ⊢ φ → coeff ⁡ F ⁡ k ∈ S → coeff ⁡ F ⁡ k ‾ ∈ S
28 elsni ⊢ coeff ⁡ F ⁡ k ∈ 0 → coeff ⁡ F ⁡ k = 0
29 28 fveq2d ⊢ coeff ⁡ F ⁡ k ∈ 0 → coeff ⁡ F ⁡ k ‾ = 0 ‾
30 cj0 ⊢ 0 ‾ = 0
31 29 30 eqtrdi ⊢ coeff ⁡ F ⁡ k ∈ 0 → coeff ⁡ F ⁡ k ‾ = 0
32 fvex ⊢ coeff ⁡ F ⁡ k ‾ ∈ V
33 32 elsn ⊢ coeff ⁡ F ⁡ k ‾ ∈ 0 ↔ coeff ⁡ F ⁡ k ‾ = 0
34 31 33 sylibr ⊢ coeff ⁡ F ⁡ k ∈ 0 → coeff ⁡ F ⁡ k ‾ ∈ 0
35 34 a1i ⊢ φ → coeff ⁡ F ⁡ k ∈ 0 → coeff ⁡ F ⁡ k ‾ ∈ 0
36 27 35 orim12d ⊢ φ → coeff ⁡ F ⁡ k ∈ S ∨ coeff ⁡ F ⁡ k ∈ 0 → coeff ⁡ F ⁡ k ‾ ∈ S ∨ coeff ⁡ F ⁡ k ‾ ∈ 0
37 elun ⊢ coeff ⁡ F ⁡ k ∈ S ∪ 0 ↔ coeff ⁡ F ⁡ k ∈ S ∨ coeff ⁡ F ⁡ k ∈ 0
38 elun ⊢ coeff ⁡ F ⁡ k ‾ ∈ S ∪ 0 ↔ coeff ⁡ F ⁡ k ‾ ∈ S ∨ coeff ⁡ F ⁡ k ‾ ∈ 0
39 36 37 38 3imtr4g ⊢ φ → coeff ⁡ F ⁡ k ∈ S ∪ 0 → coeff ⁡ F ⁡ k ‾ ∈ S ∪ 0
40 39 adantr ⊢ φ ∧ k ∈ 0 … N → coeff ⁡ F ⁡ k ∈ S ∪ 0 → coeff ⁡ F ⁡ k ‾ ∈ S ∪ 0
41 22 40 mpd ⊢ φ ∧ k ∈ 0 … N → coeff ⁡ F ⁡ k ‾ ∈ S ∪ 0
42 20 41 eqeltrd ⊢ φ ∧ k ∈ 0 … N → * ∘ coeff ⁡ F ⁡ k ∈ S ∪ 0
43 12 15 42 elplyd ⊢ φ → z ∈ ℂ ⟼ ∑ k = 0 N * ∘ coeff ⁡ F ⁡ k ⁢ z k ∈ Poly ⁡ S ∪ 0
44 7 43 eqeltrd ⊢ φ → G ∈ Poly ⁡ S ∪ 0
45 plyun0 ⊢ Poly ⁡ S ∪ 0 = Poly ⁡ S
46 44 45 eleqtrdi ⊢ φ → G ∈ Poly ⁡ S