fprodcllem

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

Step	Hyp	Ref	Expression
1		fprodcllem.1	$⊢ φ \to S \subseteq ℂ$
2		fprodcllem.2	$⊢ (φ \land (x \in S \land y \in S)) \to x y \in S$
3		fprodcllem.3	$⊢ φ \to A \in Fin$
4		fprodcllem.4	$⊢ (φ \land k \in A) \to B \in S$
5		fprodcllem.5	$⊢ φ \to 1 \in S$
6		prodeq1	$⊢ A = \emptyset \to \prod_{k \in A} B = \prod_{k \in \emptyset} B$
7		prod0	$⊢ \prod_{k \in \emptyset} B = 1$
8	6 7	eqtrdi	$⊢ A = \emptyset \to \prod_{k \in A} B = 1$
9	8	adantl	$⊢ (φ \land A = \emptyset) \to \prod_{k \in A} B = 1$
10	5	adantr	$⊢ (φ \land A = \emptyset) \to 1 \in S$
11	9 10	eqeltrd	$⊢ (φ \land A = \emptyset) \to \prod_{k \in A} B \in S$
12	1	adantr	$⊢ (φ \land A \neq \emptyset) \to S \subseteq ℂ$
13	2	adantlr	$⊢ ((φ \land A \neq \emptyset) \land (x \in S \land y \in S)) \to x y \in S$
14	3	adantr	$⊢ (φ \land A \neq \emptyset) \to A \in Fin$
15	4	adantlr	$⊢ ((φ \land A \neq \emptyset) \land k \in A) \to B \in S$
16		simpr	$⊢ (φ \land A \neq \emptyset) \to A \neq \emptyset$
17	12 13 14 15 16	fprodcl2lem	$⊢ (φ \land A \neq \emptyset) \to \prod_{k \in A} B \in S$
18	11 17	pm2.61dane	$⊢ φ \to \prod_{k \in A} B \in S$

Metamath Proof Explorer