# Metamath Proof Explorer

## Theorem fprodcllem

Description: Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017)

Ref Expression
Hypotheses fprodcllem.1 ${⊢}{\phi }\to {S}\subseteq ℂ$
fprodcllem.2 ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{y}\in {S}$
fprodcllem.3 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fprodcllem.4 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in {S}$
fprodcllem.5 ${⊢}{\phi }\to 1\in {S}$
Assertion fprodcllem ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}\in {S}$

### Proof

Step Hyp Ref Expression
1 fprodcllem.1 ${⊢}{\phi }\to {S}\subseteq ℂ$
2 fprodcllem.2 ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{y}\in {S}$
3 fprodcllem.3 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
4 fprodcllem.4 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in {S}$
5 fprodcllem.5 ${⊢}{\phi }\to 1\in {S}$
6 prodeq1 ${⊢}{A}=\varnothing \to \prod _{{k}\in {A}}{B}=\prod _{{k}\in \varnothing }{B}$
7 prod0 ${⊢}\prod _{{k}\in \varnothing }{B}=1$
8 6 7 syl6eq ${⊢}{A}=\varnothing \to \prod _{{k}\in {A}}{B}=1$
9 8 adantl ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to \prod _{{k}\in {A}}{B}=1$
10 5 adantr ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to 1\in {S}$
11 9 10 eqeltrd ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to \prod _{{k}\in {A}}{B}\in {S}$
12 1 adantr ${⊢}\left({\phi }\wedge {A}\ne \varnothing \right)\to {S}\subseteq ℂ$
13 2 adantlr ${⊢}\left(\left({\phi }\wedge {A}\ne \varnothing \right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{y}\in {S}$
14 3 adantr ${⊢}\left({\phi }\wedge {A}\ne \varnothing \right)\to {A}\in \mathrm{Fin}$
15 4 adantlr ${⊢}\left(\left({\phi }\wedge {A}\ne \varnothing \right)\wedge {k}\in {A}\right)\to {B}\in {S}$
16 simpr ${⊢}\left({\phi }\wedge {A}\ne \varnothing \right)\to {A}\ne \varnothing$
17 12 13 14 15 16 fprodcl2lem ${⊢}\left({\phi }\wedge {A}\ne \varnothing \right)\to \prod _{{k}\in {A}}{B}\in {S}$
18 11 17 pm2.61dane ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}\in {S}$