This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem plysub

Description: The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014)

Ref Expression
Hypotheses plyadd.1 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
plyadd.2 ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
plyadd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
plymul.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
plysub.5 ⊢ ( 𝜑 → - 1 ∈ 𝑆 )
Assertion plysub ( 𝜑 → ( 𝐹 ∘f − 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 plyadd.1 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
2 plyadd.2 ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
3 plyadd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
4 plymul.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
5 plysub.5 ⊢ ( 𝜑 → - 1 ∈ 𝑆 )
6 cnex ⊢ ℂ ∈ V
7 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
8 1 7 syl ⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
9 plyf ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 : ℂ ⟶ ℂ )
10 2 9 syl ⊢ ( 𝜑 → 𝐺 : ℂ ⟶ ℂ )
11 ofnegsub ⊢ ( ( ℂ ∈ V ∧ 𝐹 : ℂ ⟶ ℂ ∧ 𝐺 : ℂ ⟶ ℂ ) → ( 𝐹 ∘f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹 ∘f − 𝐺 ) )
12 6 8 10 11 mp3an2i ⊢ ( 𝜑 → ( 𝐹 ∘f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹 ∘f − 𝐺 ) )
13 plybss ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ )
14 1 13 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
15 plyconst ⊢ ( ( 𝑆 ⊆ ℂ ∧ - 1 ∈ 𝑆 ) → ( ℂ × { - 1 } ) ∈ ( Poly ‘ 𝑆 ) )
16 14 5 15 syl2anc ⊢ ( 𝜑 → ( ℂ × { - 1 } ) ∈ ( Poly ‘ 𝑆 ) )
17 16 2 3 4 plymul ⊢ ( 𝜑 → ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )
18 1 17 3 plyadd ⊢ ( 𝜑 → ( 𝐹 ∘f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) ∈ ( Poly ‘ 𝑆 ) )
19 12 18 eqeltrrd ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )