# Metamath Proof Explorer

## Theorem fprodexp

Description: Positive integer exponentiation of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fprodexp.kph ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
fprodexp.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
fprodexp.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fprodexp.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
Assertion fprodexp ${⊢}{\phi }\to \prod _{{k}\in {A}}{{B}}^{{N}}={\prod _{{k}\in {A}}{B}}^{{N}}$

### Proof

Step Hyp Ref Expression
1 fprodexp.kph ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
2 fprodexp.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
3 fprodexp.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
4 fprodexp.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
5 prodeq1 ${⊢}{x}=\varnothing \to \prod _{{k}\in {x}}{{B}}^{{N}}=\prod _{{k}\in \varnothing }{{B}}^{{N}}$
6 prodeq1 ${⊢}{x}=\varnothing \to \prod _{{k}\in {x}}{B}=\prod _{{k}\in \varnothing }{B}$
7 6 oveq1d ${⊢}{x}=\varnothing \to {\prod _{{k}\in {x}}{B}}^{{N}}={\prod _{{k}\in \varnothing }{B}}^{{N}}$
8 5 7 eqeq12d ${⊢}{x}=\varnothing \to \left(\prod _{{k}\in {x}}{{B}}^{{N}}={\prod _{{k}\in {x}}{B}}^{{N}}↔\prod _{{k}\in \varnothing }{{B}}^{{N}}={\prod _{{k}\in \varnothing }{B}}^{{N}}\right)$
9 prodeq1 ${⊢}{x}={y}\to \prod _{{k}\in {x}}{{B}}^{{N}}=\prod _{{k}\in {y}}{{B}}^{{N}}$
10 prodeq1 ${⊢}{x}={y}\to \prod _{{k}\in {x}}{B}=\prod _{{k}\in {y}}{B}$
11 10 oveq1d ${⊢}{x}={y}\to {\prod _{{k}\in {x}}{B}}^{{N}}={\prod _{{k}\in {y}}{B}}^{{N}}$
12 9 11 eqeq12d ${⊢}{x}={y}\to \left(\prod _{{k}\in {x}}{{B}}^{{N}}={\prod _{{k}\in {x}}{B}}^{{N}}↔\prod _{{k}\in {y}}{{B}}^{{N}}={\prod _{{k}\in {y}}{B}}^{{N}}\right)$
13 prodeq1 ${⊢}{x}={y}\cup \left\{{z}\right\}\to \prod _{{k}\in {x}}{{B}}^{{N}}=\prod _{{k}\in {y}\cup \left\{{z}\right\}}{{B}}^{{N}}$
14 prodeq1 ${⊢}{x}={y}\cup \left\{{z}\right\}\to \prod _{{k}\in {x}}{B}=\prod _{{k}\in {y}\cup \left\{{z}\right\}}{B}$
15 14 oveq1d ${⊢}{x}={y}\cup \left\{{z}\right\}\to {\prod _{{k}\in {x}}{B}}^{{N}}={\prod _{{k}\in {y}\cup \left\{{z}\right\}}{B}}^{{N}}$
16 13 15 eqeq12d ${⊢}{x}={y}\cup \left\{{z}\right\}\to \left(\prod _{{k}\in {x}}{{B}}^{{N}}={\prod _{{k}\in {x}}{B}}^{{N}}↔\prod _{{k}\in {y}\cup \left\{{z}\right\}}{{B}}^{{N}}={\prod _{{k}\in {y}\cup \left\{{z}\right\}}{B}}^{{N}}\right)$
17 prodeq1 ${⊢}{x}={A}\to \prod _{{k}\in {x}}{{B}}^{{N}}=\prod _{{k}\in {A}}{{B}}^{{N}}$
18 prodeq1 ${⊢}{x}={A}\to \prod _{{k}\in {x}}{B}=\prod _{{k}\in {A}}{B}$
19 18 oveq1d ${⊢}{x}={A}\to {\prod _{{k}\in {x}}{B}}^{{N}}={\prod _{{k}\in {A}}{B}}^{{N}}$
20 17 19 eqeq12d ${⊢}{x}={A}\to \left(\prod _{{k}\in {x}}{{B}}^{{N}}={\prod _{{k}\in {x}}{B}}^{{N}}↔\prod _{{k}\in {A}}{{B}}^{{N}}={\prod _{{k}\in {A}}{B}}^{{N}}\right)$
21 2 nn0zd ${⊢}{\phi }\to {N}\in ℤ$
22 1exp ${⊢}{N}\in ℤ\to {1}^{{N}}=1$
23 21 22 syl ${⊢}{\phi }\to {1}^{{N}}=1$
24 23 eqcomd ${⊢}{\phi }\to 1={1}^{{N}}$
25 prod0 ${⊢}\prod _{{k}\in \varnothing }{{B}}^{{N}}=1$
26 25 a1i ${⊢}{\phi }\to \prod _{{k}\in \varnothing }{{B}}^{{N}}=1$
27 prod0 ${⊢}\prod _{{k}\in \varnothing }{B}=1$
28 27 oveq1i ${⊢}{\prod _{{k}\in \varnothing }{B}}^{{N}}={1}^{{N}}$
29 28 a1i ${⊢}{\phi }\to {\prod _{{k}\in \varnothing }{B}}^{{N}}={1}^{{N}}$
30 24 26 29 3eqtr4d ${⊢}{\phi }\to \prod _{{k}\in \varnothing }{{B}}^{{N}}={\prod _{{k}\in \varnothing }{B}}^{{N}}$
31 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)$
32 1 31 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)$
33 3 adantr ${⊢}\left({\phi }\wedge {y}\subseteq {A}\right)\to {A}\in \mathrm{Fin}$
34 simpr ${⊢}\left({\phi }\wedge {y}\subseteq {A}\right)\to {y}\subseteq {A}$
35 ssfi ${⊢}\left({A}\in \mathrm{Fin}\wedge {y}\subseteq {A}\right)\to {y}\in \mathrm{Fin}$
36 33 34 35 syl2anc ${⊢}\left({\phi }\wedge {y}\subseteq {A}\right)\to {y}\in \mathrm{Fin}$
37 36 adantrr ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to {y}\in \mathrm{Fin}$
38 simpll ${⊢}\left(\left({\phi }\wedge {y}\subseteq {A}\right)\wedge {k}\in {y}\right)\to {\phi }$
39 34 sselda ${⊢}\left(\left({\phi }\wedge {y}\subseteq {A}\right)\wedge {k}\in {y}\right)\to {k}\in {A}$
40 38 39 4 syl2anc ${⊢}\left(\left({\phi }\wedge {y}\subseteq {A}\right)\wedge {k}\in {y}\right)\to {B}\in ℂ$
41 40 adantlrr ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\wedge {k}\in {y}\right)\to {B}\in ℂ$
42 32 37 41 fprodclf ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \prod _{{k}\in {y}}{B}\in ℂ$
43 simpl ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to {\phi }$
44 simprr ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to {z}\in \left({A}\setminus {y}\right)$
45 44 eldifad ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to {z}\in {A}$
46 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
47 1 46 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {z}\in {A}\right)$
48 nfcsb1v
49 48 nfel1
50 47 49 nfim
51 eleq1w ${⊢}{k}={z}\to \left({k}\in {A}↔{z}\in {A}\right)$
52 51 anbi2d ${⊢}{k}={z}\to \left(\left({\phi }\wedge {k}\in {A}\right)↔\left({\phi }\wedge {z}\in {A}\right)\right)$
53 csbeq1a
54 53 eleq1d
55 52 54 imbi12d
56 50 55 4 chvarfv
57 43 45 56 syl2anc
58 2 adantr ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to {N}\in {ℕ}_{0}$
59 mulexp
60 42 57 58 59 syl3anc
61 60 eqcomd
63 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}^$
64 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{N}$
65 48 63 64 nfov
66 44 eldifbd ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to ¬{z}\in {y}$
67 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\subseteq {A}\right)\wedge {k}\in {y}\right)\to {N}\in {ℕ}_{0}$
68 40 67 expcld ${⊢}\left(\left({\phi }\wedge {y}\subseteq {A}\right)\wedge {k}\in {y}\right)\to {{B}}^{{N}}\in ℂ$
69 68 adantlrr ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\wedge {k}\in {y}\right)\to {{B}}^{{N}}\in ℂ$
70 53 oveq1d
71 57 58 expcld
72 32 65 37 44 66 69 70 71 fprodsplitsn
80 62 76 79 3eqtr4d ${⊢}\left(\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\wedge \prod _{{k}\in {y}}{{B}}^{{N}}={\prod _{{k}\in {y}}{B}}^{{N}}\right)\to \prod _{{k}\in {y}\cup \left\{{z}\right\}}{{B}}^{{N}}={\prod _{{k}\in {y}\cup \left\{{z}\right\}}{B}}^{{N}}$
81 80 ex ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left(\prod _{{k}\in {y}}{{B}}^{{N}}={\prod _{{k}\in {y}}{B}}^{{N}}\to \prod _{{k}\in {y}\cup \left\{{z}\right\}}{{B}}^{{N}}={\prod _{{k}\in {y}\cup \left\{{z}\right\}}{B}}^{{N}}\right)$
82 8 12 16 20 30 81 3 findcard2d ${⊢}{\phi }\to \prod _{{k}\in {A}}{{B}}^{{N}}={\prod _{{k}\in {A}}{B}}^{{N}}$