Description: The coefficient function of a sum is the sum of coefficients. (Contributed by Mario Carneiro, 24-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | coefv0.1 | ⊢ 𝐴 = ( coeff ‘ 𝐹 ) | |
coeadd.2 | ⊢ 𝐵 = ( coeff ‘ 𝐺 ) | ||
Assertion | coeadd | ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( 𝐴 ∘f + 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coefv0.1 | ⊢ 𝐴 = ( coeff ‘ 𝐹 ) | |
2 | coeadd.2 | ⊢ 𝐵 = ( coeff ‘ 𝐺 ) | |
3 | eqid | ⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 ) | |
4 | eqid | ⊢ ( deg ‘ 𝐺 ) = ( deg ‘ 𝐺 ) | |
5 | 1 2 3 4 | coeaddlem | ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( 𝐴 ∘f + 𝐵 ) ∧ ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ if ( ( deg ‘ 𝐹 ) ≤ ( deg ‘ 𝐺 ) , ( deg ‘ 𝐺 ) , ( deg ‘ 𝐹 ) ) ) ) |
6 | 5 | simpld | ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( 𝐴 ∘f + 𝐵 ) ) |