fprodcl2lem

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

	Ref	Expression
Hypotheses	fprodcllem.1	$⊢ φ \to S \subseteq ℂ$
	fprodcllem.2	$⊢ (φ \land (x \in S \land y \in S)) \to x y \in S$
	fprodcllem.3	$⊢ φ \to A \in Fin$
	fprodcllem.4	$⊢ (φ \land k \in A) \to B \in S$
	fprodcl2lem.5	$⊢ φ \to A \neq \emptyset$
Assertion	fprodcl2lem	$⊢ φ \to \prod_{k \in A} B \in S$

Proof

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		fprodcl2lem.5	$⊢ φ \to A \neq \emptyset$
6	5	a1d	$⊢ φ \to (\neg \prod_{k \in A} B \in S \to A \neq \emptyset)$
7	6	necon4bd	$⊢ φ \to (A = \emptyset \to \prod_{k \in A} B \in S)$
8		prodfc	$⊢ \prod_{m \in A} (k \in A ⟼ B) (m) = \prod_{k \in A} B$
9		fveq2	$⊢ m = f (x) \to (k \in A ⟼ B) (m) = (k \in A ⟼ B) (f (x))$
10		simprl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℕ$
11		simprr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
12	1	adantr	$⊢ (φ \land k \in A) \to S \subseteq ℂ$
13	12 4	sseldd	$⊢ (φ \land k \in A) \to B \in ℂ$
14	13	fmpttd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ ℂ$
15	14	ffvelcdmda	$⊢ (φ \land m \in A) \to (k \in A ⟼ B) (m) \in ℂ$
16	15	adantlr	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ B) (m) \in ℂ$
17		f1of	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) ⟶ A$
18	17	ad2antll	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) ⟶ A$
19		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land x \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (x) = (k \in A ⟼ B) (f (x))$
20	18 19	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (x) = (k \in A ⟼ B) (f (x))$
21	9 10 11 16 20	fprod	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{m \in A} (k \in A ⟼ B) (m) = seq 1 (\times ((k \in A ⟼ B) \circ f)) (\|A\|)$
22	8 21	eqtr3id	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{k \in A} B = seq 1 (\times ((k \in A ⟼ B) \circ f)) (\|A\|)$
23		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
24	10 23	eleqtrdi	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℤ_{\geq 1}$
25	4	fmpttd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ S$
26		fco	$⊢ ((k \in A ⟼ B) : A ⟶ S \land f : (1 \dots \|A\|) ⟶ A) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ S$
27	25 18 26	syl2an2r	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ S$
28	27	ffvelcdmda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (x) \in S$
29	2	adantlr	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land (x \in S \land y \in S)) \to x y \in S$
30	24 28 29	seqcl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to seq 1 (\times ((k \in A ⟼ B) \circ f)) (\|A\|) \in S$
31	22 30	eqeltrd	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{k \in A} B \in S$
32	31	expr	$⊢ (φ \land \|A\| \in ℕ) \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \prod_{k \in A} B \in S)$
33	32	exlimdv	$⊢ (φ \land \|A\| \in ℕ) \to (\exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \prod_{k \in A} B \in S)$
34	33	expimpd	$⊢ φ \to ((\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \prod_{k \in A} B \in S)$
35		fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
36	3 35	syl	$⊢ φ \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
37	7 34 36	mpjaod	$⊢ φ \to \prod_{k \in A} B \in S$

Metamath Proof Explorer

Theorem fprodcl2lem

Proof