# Metamath Proof Explorer

## Theorem fprodmul

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

Ref Expression
Hypotheses fprodmul.1 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fprodmul.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
fprodmul.3 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in ℂ$
Assertion fprodmul ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}{C}=\prod _{{k}\in {A}}{B}\prod _{{k}\in {A}}{C}$

### Proof

Step Hyp Ref Expression
1 fprodmul.1 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
2 fprodmul.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
3 fprodmul.3 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in ℂ$
4 1t1e1 ${⊢}1\cdot 1=1$
5 prod0 ${⊢}\prod _{{k}\in \varnothing }{B}=1$
6 prod0 ${⊢}\prod _{{k}\in \varnothing }{C}=1$
7 5 6 oveq12i ${⊢}\prod _{{k}\in \varnothing }{B}\prod _{{k}\in \varnothing }{C}=1\cdot 1$
8 prod0 ${⊢}\prod _{{k}\in \varnothing }{B}{C}=1$
9 4 7 8 3eqtr4ri ${⊢}\prod _{{k}\in \varnothing }{B}{C}=\prod _{{k}\in \varnothing }{B}\prod _{{k}\in \varnothing }{C}$
10 prodeq1 ${⊢}{A}=\varnothing \to \prod _{{k}\in {A}}{B}{C}=\prod _{{k}\in \varnothing }{B}{C}$
11 prodeq1 ${⊢}{A}=\varnothing \to \prod _{{k}\in {A}}{B}=\prod _{{k}\in \varnothing }{B}$
12 prodeq1 ${⊢}{A}=\varnothing \to \prod _{{k}\in {A}}{C}=\prod _{{k}\in \varnothing }{C}$
13 11 12 oveq12d ${⊢}{A}=\varnothing \to \prod _{{k}\in {A}}{B}\prod _{{k}\in {A}}{C}=\prod _{{k}\in \varnothing }{B}\prod _{{k}\in \varnothing }{C}$
14 9 10 13 3eqtr4a ${⊢}{A}=\varnothing \to \prod _{{k}\in {A}}{B}{C}=\prod _{{k}\in {A}}{B}\prod _{{k}\in {A}}{C}$
15 14 a1i ${⊢}{\phi }\to \left({A}=\varnothing \to \prod _{{k}\in {A}}{B}{C}=\prod _{{k}\in {A}}{B}\prod _{{k}\in {A}}{C}\right)$
16 simprl ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left|{A}\right|\in ℕ$
17 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
18 16 17 eleqtrdi ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left|{A}\right|\in {ℤ}_{\ge 1}$
19 2 fmpttd ${⊢}{\phi }\to \left({k}\in {A}⟼{B}\right):{A}⟶ℂ$
20 19 adantr ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left({k}\in {A}⟼{B}\right):{A}⟶ℂ$
21 f1of ${⊢}{f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\to {f}:\left(1\dots \left|{A}\right|\right)⟶{A}$
22 21 ad2antll ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to {f}:\left(1\dots \left|{A}\right|\right)⟶{A}$
23 fco ${⊢}\left(\left({k}\in {A}⟼{B}\right):{A}⟶ℂ\wedge {f}:\left(1\dots \left|{A}\right|\right)⟶{A}\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right):\left(1\dots \left|{A}\right|\right)⟶ℂ$
24 20 22 23 syl2anc ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right):\left(1\dots \left|{A}\right|\right)⟶ℂ$
25 24 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\left({n}\right)\in ℂ$
26 3 fmpttd ${⊢}{\phi }\to \left({k}\in {A}⟼{C}\right):{A}⟶ℂ$
27 26 adantr ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left({k}\in {A}⟼{C}\right):{A}⟶ℂ$
28 fco ${⊢}\left(\left({k}\in {A}⟼{C}\right):{A}⟶ℂ\wedge {f}:\left(1\dots \left|{A}\right|\right)⟶{A}\right)\to \left(\left({k}\in {A}⟼{C}\right)\circ {f}\right):\left(1\dots \left|{A}\right|\right)⟶ℂ$
29 27 22 28 syl2anc ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left(\left({k}\in {A}⟼{C}\right)\circ {f}\right):\left(1\dots \left|{A}\right|\right)⟶ℂ$
30 29 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\left({n}\right)\in ℂ$
31 22 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to {f}\left({n}\right)\in {A}$
32 simpr ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {k}\in {A}$
33 2 3 mulcld ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}{C}\in ℂ$
34 eqid ${⊢}\left({k}\in {A}⟼{B}{C}\right)=\left({k}\in {A}⟼{B}{C}\right)$
35 34 fvmpt2 ${⊢}\left({k}\in {A}\wedge {B}{C}\in ℂ\right)\to \left({k}\in {A}⟼{B}{C}\right)\left({k}\right)={B}{C}$
36 32 33 35 syl2anc ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {A}⟼{B}{C}\right)\left({k}\right)={B}{C}$
37 eqid ${⊢}\left({k}\in {A}⟼{B}\right)=\left({k}\in {A}⟼{B}\right)$
38 37 fvmpt2 ${⊢}\left({k}\in {A}\wedge {B}\in ℂ\right)\to \left({k}\in {A}⟼{B}\right)\left({k}\right)={B}$
39 32 2 38 syl2anc ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {A}⟼{B}\right)\left({k}\right)={B}$
40 eqid ${⊢}\left({k}\in {A}⟼{C}\right)=\left({k}\in {A}⟼{C}\right)$
41 40 fvmpt2 ${⊢}\left({k}\in {A}\wedge {C}\in ℂ\right)\to \left({k}\in {A}⟼{C}\right)\left({k}\right)={C}$
42 32 3 41 syl2anc ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {A}⟼{C}\right)\left({k}\right)={C}$
43 39 42 oveq12d ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {A}⟼{B}\right)\left({k}\right)\left({k}\in {A}⟼{C}\right)\left({k}\right)={B}{C}$
44 36 43 eqtr4d ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {A}⟼{B}{C}\right)\left({k}\right)=\left({k}\in {A}⟼{B}\right)\left({k}\right)\left({k}\in {A}⟼{C}\right)\left({k}\right)$
45 44 ralrimiva ${⊢}{\phi }\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}{C}\right)\left({k}\right)=\left({k}\in {A}⟼{B}\right)\left({k}\right)\left({k}\in {A}⟼{C}\right)\left({k}\right)$
46 45 ad2antrr ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}{C}\right)\left({k}\right)=\left({k}\in {A}⟼{B}\right)\left({k}\right)\left({k}\in {A}⟼{C}\right)\left({k}\right)$
47 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}{C}\right)\left({f}\left({n}\right)\right)$
48 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)$
49 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}×$
50 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
51 48 49 50 nfov ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
52 47 51 nfeq ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}{C}\right)\left({f}\left({n}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
53 fveq2 ${⊢}{k}={f}\left({n}\right)\to \left({k}\in {A}⟼{B}{C}\right)\left({k}\right)=\left({k}\in {A}⟼{B}{C}\right)\left({f}\left({n}\right)\right)$
54 fveq2 ${⊢}{k}={f}\left({n}\right)\to \left({k}\in {A}⟼{B}\right)\left({k}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)$
55 fveq2 ${⊢}{k}={f}\left({n}\right)\to \left({k}\in {A}⟼{C}\right)\left({k}\right)=\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
56 54 55 oveq12d ${⊢}{k}={f}\left({n}\right)\to \left({k}\in {A}⟼{B}\right)\left({k}\right)\left({k}\in {A}⟼{C}\right)\left({k}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
57 53 56 eqeq12d ${⊢}{k}={f}\left({n}\right)\to \left(\left({k}\in {A}⟼{B}{C}\right)\left({k}\right)=\left({k}\in {A}⟼{B}\right)\left({k}\right)\left({k}\in {A}⟼{C}\right)\left({k}\right)↔\left({k}\in {A}⟼{B}{C}\right)\left({f}\left({n}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)\right)$
58 52 57 rspc ${⊢}{f}\left({n}\right)\in {A}\to \left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}{C}\right)\left({k}\right)=\left({k}\in {A}⟼{B}\right)\left({k}\right)\left({k}\in {A}⟼{C}\right)\left({k}\right)\to \left({k}\in {A}⟼{B}{C}\right)\left({f}\left({n}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)\right)$
59 31 46 58 sylc ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left({k}\in {A}⟼{B}{C}\right)\left({f}\left({n}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
60 fvco3 ${⊢}\left({f}:\left(1\dots \left|{A}\right|\right)⟶{A}\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}{C}\right)\circ {f}\right)\left({n}\right)=\left({k}\in {A}⟼{B}{C}\right)\left({f}\left({n}\right)\right)$
61 22 60 sylan ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}{C}\right)\circ {f}\right)\left({n}\right)=\left({k}\in {A}⟼{B}{C}\right)\left({f}\left({n}\right)\right)$
62 fvco3 ${⊢}\left({f}:\left(1\dots \left|{A}\right|\right)⟶{A}\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)$
63 22 62 sylan ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)$
64 fvco3 ${⊢}\left({f}:\left(1\dots \left|{A}\right|\right)⟶{A}\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\left({n}\right)=\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
65 22 64 sylan ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\left({n}\right)=\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
66 63 65 oveq12d ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\left({n}\right)\left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
67 59 61 66 3eqtr4d ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}{C}\right)\circ {f}\right)\left({n}\right)=\left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\left({n}\right)\left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\left({n}\right)$
68 18 25 30 67 prodfmul ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to seq1\left(×,\left(\left({k}\in {A}⟼{B}{C}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)=seq1\left(×,\left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)seq1\left(×,\left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)$
69 fveq2 ${⊢}{m}={f}\left({n}\right)\to \left({k}\in {A}⟼{B}{C}\right)\left({m}\right)=\left({k}\in {A}⟼{B}{C}\right)\left({f}\left({n}\right)\right)$
70 simprr ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}$
71 33 fmpttd ${⊢}{\phi }\to \left({k}\in {A}⟼{B}{C}\right):{A}⟶ℂ$
72 71 adantr ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left({k}\in {A}⟼{B}{C}\right):{A}⟶ℂ$
73 72 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {m}\in {A}\right)\to \left({k}\in {A}⟼{B}{C}\right)\left({m}\right)\in ℂ$
74 69 16 70 73 61 fprod ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \prod _{{m}\in {A}}\left({k}\in {A}⟼{B}{C}\right)\left({m}\right)=seq1\left(×,\left(\left({k}\in {A}⟼{B}{C}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)$
75 fveq2 ${⊢}{m}={f}\left({n}\right)\to \left({k}\in {A}⟼{B}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)$
76 20 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {m}\in {A}\right)\to \left({k}\in {A}⟼{B}\right)\left({m}\right)\in ℂ$
77 75 16 70 76 63 fprod ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \prod _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)=seq1\left(×,\left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)$
78 fveq2 ${⊢}{m}={f}\left({n}\right)\to \left({k}\in {A}⟼{C}\right)\left({m}\right)=\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
79 27 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {m}\in {A}\right)\to \left({k}\in {A}⟼{C}\right)\left({m}\right)\in ℂ$
80 78 16 70 79 65 fprod ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \prod _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)=seq1\left(×,\left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)$
81 77 80 oveq12d ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \prod _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)\prod _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)=seq1\left(×,\left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)seq1\left(×,\left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)$
82 68 74 81 3eqtr4d ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \prod _{{m}\in {A}}\left({k}\in {A}⟼{B}{C}\right)\left({m}\right)=\prod _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)\prod _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)$
83 prodfc ${⊢}\prod _{{m}\in {A}}\left({k}\in {A}⟼{B}{C}\right)\left({m}\right)=\prod _{{k}\in {A}}{B}{C}$
84 prodfc ${⊢}\prod _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)=\prod _{{k}\in {A}}{B}$
85 prodfc ${⊢}\prod _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)=\prod _{{k}\in {A}}{C}$
86 84 85 oveq12i ${⊢}\prod _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)\prod _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)=\prod _{{k}\in {A}}{B}\prod _{{k}\in {A}}{C}$
87 82 83 86 3eqtr3g ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \prod _{{k}\in {A}}{B}{C}=\prod _{{k}\in {A}}{B}\prod _{{k}\in {A}}{C}$
88 87 expr ${⊢}\left({\phi }\wedge \left|{A}\right|\in ℕ\right)\to \left({f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\to \prod _{{k}\in {A}}{B}{C}=\prod _{{k}\in {A}}{B}\prod _{{k}\in {A}}{C}\right)$
89 88 exlimdv ${⊢}\left({\phi }\wedge \left|{A}\right|\in ℕ\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\to \prod _{{k}\in {A}}{B}{C}=\prod _{{k}\in {A}}{B}\prod _{{k}\in {A}}{C}\right)$
90 89 expimpd ${⊢}{\phi }\to \left(\left(\left|{A}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\to \prod _{{k}\in {A}}{B}{C}=\prod _{{k}\in {A}}{B}\prod _{{k}\in {A}}{C}\right)$
91 fz1f1o ${⊢}{A}\in \mathrm{Fin}\to \left({A}=\varnothing \vee \left(\left|{A}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)$
92 1 91 syl ${⊢}{\phi }\to \left({A}=\varnothing \vee \left(\left|{A}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)$
93 15 90 92 mpjaod ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}{C}=\prod _{{k}\in {A}}{B}\prod _{{k}\in {A}}{C}$