Metamath Proof Explorer


Theorem prodfmul

Description: The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017)

Ref Expression
Hypotheses prodfmul.1 φNM
prodfmul.2 φkMNFk
prodfmul.3 φkMNGk
prodfmul.4 φkMNHk=FkGk
Assertion prodfmul φseqM×HN=seqM×FNseqM×GN

Proof

Step Hyp Ref Expression
1 prodfmul.1 φNM
2 prodfmul.2 φkMNFk
3 prodfmul.3 φkMNGk
4 prodfmul.4 φkMNHk=FkGk
5 mulcl xyxy
6 5 adantl φxyxy
7 mulcom xyxy=yx
8 7 adantl φxyxy=yx
9 mulass xyzxyz=xyz
10 9 adantl φxyzxyz=xyz
11 6 8 10 1 2 3 4 seqcaopr φseqM×HN=seqM×FNseqM×GN