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 ⊢ 𝐺 = ( ( ∗ ∘ 𝐹 ) ∘ ∗ )
plycj.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ∗ ‘ 𝑥 ) ∈ 𝑆 )
plycj.4 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
Assertion plycj ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )

Proof

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