Metamath Proof Explorer


Theorem plymullem

Description: Lemma for plymul . (Contributed by Mario Carneiro, 21-Jul-2014)

Ref Expression
Hypotheses plyadd.1 φFPolyS
plyadd.2 φGPolyS
plyadd.3 φxSySx+yS
plyadd.m φM0
plyadd.n φN0
plyadd.a φAS00
plyadd.b φBS00
plyadd.a2 φAM+1=0
plyadd.b2 φBN+1=0
plyadd.f φF=zk=0MAkzk
plyadd.g φG=zk=0NBkzk
plymul.x φxSySxyS
Assertion plymullem φF×fGPolyS

Proof

Step Hyp Ref Expression
1 plyadd.1 φFPolyS
2 plyadd.2 φGPolyS
3 plyadd.3 φxSySx+yS
4 plyadd.m φM0
5 plyadd.n φN0
6 plyadd.a φAS00
7 plyadd.b φBS00
8 plyadd.a2 φAM+1=0
9 plyadd.b2 φBN+1=0
10 plyadd.f φF=zk=0MAkzk
11 plyadd.g φG=zk=0NBkzk
12 plymul.x φxSySxyS
13 plybss FPolySS
14 1 13 syl φS
15 0cnd φ0
16 15 snssd φ0
17 14 16 unssd φS0
18 cnex V
19 ssexg S0VS0V
20 17 18 19 sylancl φS0V
21 nn0ex 0V
22 elmapg S0V0VAS00A:0S0
23 20 21 22 sylancl φAS00A:0S0
24 6 23 mpbid φA:0S0
25 24 17 fssd φA:0
26 elmapg S0V0VBS00B:0S0
27 20 21 26 sylancl φBS00B:0S0
28 7 27 mpbid φB:0S0
29 28 17 fssd φB:0
30 1 2 4 5 25 29 8 9 10 11 plymullem1 φF×fG=zn=0M+Nk=0nAkBnkzn
31 4 5 nn0addcld φM+N0
32 eqid S0=S0
33 14 32 3 un0addcl φxS0yS0x+yS0
34 fzfid φ0nFin
35 elfznn0 k0nk0
36 ffvelrn A:0S0k0AkS0
37 24 35 36 syl2an φk0nAkS0
38 fznn0sub k0nnk0
39 ffvelrn B:0S0nk0BnkS0
40 28 38 39 syl2an φk0nBnkS0
41 37 40 jca φk0nAkS0BnkS0
42 14 32 12 un0mulcl φxS0yS0xyS0
43 42 caovclg φAkS0BnkS0AkBnkS0
44 41 43 syldan φk0nAkBnkS0
45 ssun2 0S0
46 c0ex 0V
47 46 snss 0S00S0
48 45 47 mpbir 0S0
49 48 a1i φ0S0
50 17 33 34 44 49 fsumcllem φk=0nAkBnkS0
51 50 adantr φn0M+Nk=0nAkBnkS0
52 17 31 51 elplyd φzn=0M+Nk=0nAkBnkznPolyS0
53 30 52 eqeltrd φF×fGPolyS0
54 plyun0 PolyS0=PolyS
55 53 54 eleqtrdi φF×fGPolyS