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