Metamath Proof Explorer


Theorem coemul

Description: A coefficient of a product of polynomials. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses coefv0.1 A=coeffF
coeadd.2 B=coeffG
Assertion coemul FPolySGPolySN0coeffF×fGN=k=0NAkBNk

Proof

Step Hyp Ref Expression
1 coefv0.1 A=coeffF
2 coeadd.2 B=coeffG
3 eqid degF=degF
4 eqid degG=degG
5 1 2 3 4 coemullem FPolySGPolyScoeffF×fG=n0k=0nAkBnkdegF×fGdegF+degG
6 5 simpld FPolySGPolyScoeffF×fG=n0k=0nAkBnk
7 6 fveq1d FPolySGPolyScoeffF×fGN=n0k=0nAkBnkN
8 oveq2 n=N0n=0N
9 fvoveq1 n=NBnk=BNk
10 9 oveq2d n=NAkBnk=AkBNk
11 10 adantr n=Nk0nAkBnk=AkBNk
12 8 11 sumeq12dv n=Nk=0nAkBnk=k=0NAkBNk
13 eqid n0k=0nAkBnk=n0k=0nAkBnk
14 sumex k=0NAkBNkV
15 12 13 14 fvmpt N0n0k=0nAkBnkN=k=0NAkBNk
16 7 15 sylan9eq FPolySGPolySN0coeffF×fGN=k=0NAkBNk
17 16 3impa FPolySGPolySN0coeffF×fGN=k=0NAkBNk