prodindf

Description: The product of indicators is one if and only if all values are in the set. (Contributed by Thierry Arnoux, 11-Dec-2021)

	Ref	Expression
Hypotheses	prodindf.1	$⊢ φ \to O \in V$
	prodindf.2	$⊢ φ \to A \in Fin$
	prodindf.3	$⊢ φ \to B \subseteq O$
	prodindf.4	$⊢ φ \to F : A ⟶ O$
Assertion	prodindf	$⊢ φ \to \prod_{k \in A} 𝟙_{O} (B) (F (k)) = if (ran F \subseteq B, 1, 0)$

Proof

Step	Hyp	Ref	Expression
1		prodindf.1	$⊢ φ \to O \in V$
2		prodindf.2	$⊢ φ \to A \in Fin$
3		prodindf.3	$⊢ φ \to B \subseteq O$
4		prodindf.4	$⊢ φ \to F : A ⟶ O$
5		2fveq3	$⊢ k = l \to 𝟙_{O} (B) (F (k)) = 𝟙_{O} (B) (F (l))$
6		indf	$⊢ (O \in V \land B \subseteq O) \to 𝟙_{O} (B) : O ⟶ \{0, 1\}$
7	1 3 6	syl2anc	$⊢ φ \to 𝟙_{O} (B) : O ⟶ \{0, 1\}$
8	7	adantr	$⊢ (φ \land k \in A) \to 𝟙_{O} (B) : O ⟶ \{0, 1\}$
9	4	ffvelcdmda	$⊢ (φ \land k \in A) \to F (k) \in O$
10	8 9	ffvelcdmd	$⊢ (φ \land k \in A) \to 𝟙_{O} (B) (F (k)) \in \{0, 1\}$
11	5 2 10	fprodex01	$⊢ φ \to \prod_{k \in A} 𝟙_{O} (B) (F (k)) = if (\forall l \in A 𝟙_{O} (B) (F (l)) = 1, 1, 0)$
12		2fveq3	$⊢ l = k \to 𝟙_{O} (B) (F (l)) = 𝟙_{O} (B) (F (k))$
13	12	eqeq1d	$⊢ l = k \to (𝟙_{O} (B) (F (l)) = 1 \leftrightarrow 𝟙_{O} (B) (F (k)) = 1)$
14	13	cbvralvw	$⊢ \forall l \in A 𝟙_{O} (B) (F (l)) = 1 \leftrightarrow \forall k \in A 𝟙_{O} (B) (F (k)) = 1$
15	14	a1i	$⊢ φ \to (\forall l \in A 𝟙_{O} (B) (F (l)) = 1 \leftrightarrow \forall k \in A 𝟙_{O} (B) (F (k)) = 1)$
16	15	ifbid	$⊢ φ \to if (\forall l \in A 𝟙_{O} (B) (F (l)) = 1, 1, 0) = if (\forall k \in A 𝟙_{O} (B) (F (k)) = 1, 1, 0)$
17		eqid	$⊢ (k \in A ⟼ F (k)) = (k \in A ⟼ F (k))$
18	17	rnmptss	$⊢ \forall k \in A F (k) \in B \to ran (k \in A ⟼ F (k)) \subseteq B$
19		nfv	$⊢ Ⅎ k φ$
20		nfmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ F (k))$
21	20	nfrn	$⊢ \underline{Ⅎ} k ran (k \in A ⟼ F (k))$
22		nfcv	$⊢ \underline{Ⅎ} k B$
23	21 22	nfss	$⊢ Ⅎ k ran (k \in A ⟼ F (k)) \subseteq B$
24	19 23	nfan	$⊢ Ⅎ k (φ \land ran (k \in A ⟼ F (k)) \subseteq B)$
25		simplr	$⊢ ((φ \land ran (k \in A ⟼ F (k)) \subseteq B) \land k \in A) \to ran (k \in A ⟼ F (k)) \subseteq B$
26	4	feqmptd	$⊢ φ \to F = (k \in A ⟼ F (k))$
27		eqidd	$⊢ φ \to k = k$
28	26 27	fveq12d	$⊢ φ \to F (k) = (k \in A ⟼ F (k)) (k)$
29	28	ralrimivw	$⊢ φ \to \forall k \in A F (k) = (k \in A ⟼ F (k)) (k)$
30	29	r19.21bi	$⊢ (φ \land k \in A) \to F (k) = (k \in A ⟼ F (k)) (k)$
31	4	ffnd	$⊢ φ \to F Fn A$
32	26	fneq1d	$⊢ φ \to (F Fn A \leftrightarrow (k \in A ⟼ F (k)) Fn A)$
33	31 32	mpbid	$⊢ φ \to (k \in A ⟼ F (k)) Fn A$
34	33	adantr	$⊢ (φ \land k \in A) \to (k \in A ⟼ F (k)) Fn A$
35		simpr	$⊢ (φ \land k \in A) \to k \in A$
36		fnfvelrn	$⊢ ((k \in A ⟼ F (k)) Fn A \land k \in A) \to (k \in A ⟼ F (k)) (k) \in ran (k \in A ⟼ F (k))$
37	34 35 36	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ F (k)) (k) \in ran (k \in A ⟼ F (k))$
38	30 37	eqeltrd	$⊢ (φ \land k \in A) \to F (k) \in ran (k \in A ⟼ F (k))$
39	38	adantlr	$⊢ ((φ \land ran (k \in A ⟼ F (k)) \subseteq B) \land k \in A) \to F (k) \in ran (k \in A ⟼ F (k))$
40	25 39	sseldd	$⊢ ((φ \land ran (k \in A ⟼ F (k)) \subseteq B) \land k \in A) \to F (k) \in B$
41	40	ex	$⊢ (φ \land ran (k \in A ⟼ F (k)) \subseteq B) \to (k \in A \to F (k) \in B)$
42	24 41	ralrimi	$⊢ (φ \land ran (k \in A ⟼ F (k)) \subseteq B) \to \forall k \in A F (k) \in B$
43	42	ex	$⊢ φ \to (ran (k \in A ⟼ F (k)) \subseteq B \to \forall k \in A F (k) \in B)$
44	18 43	impbid2	$⊢ φ \to (\forall k \in A F (k) \in B \leftrightarrow ran (k \in A ⟼ F (k)) \subseteq B)$
45	1	adantr	$⊢ (φ \land k \in A) \to O \in V$
46	3	adantr	$⊢ (φ \land k \in A) \to B \subseteq O$
47		ind1a	$⊢ (O \in V \land B \subseteq O \land F (k) \in O) \to (𝟙_{O} (B) (F (k)) = 1 \leftrightarrow F (k) \in B)$
48	45 46 9 47	syl3anc	$⊢ (φ \land k \in A) \to (𝟙_{O} (B) (F (k)) = 1 \leftrightarrow F (k) \in B)$
49	48	ralbidva	$⊢ φ \to (\forall k \in A 𝟙_{O} (B) (F (k)) = 1 \leftrightarrow \forall k \in A F (k) \in B)$
50	26	rneqd	$⊢ φ \to ran F = ran (k \in A ⟼ F (k))$
51	50	sseq1d	$⊢ φ \to (ran F \subseteq B \leftrightarrow ran (k \in A ⟼ F (k)) \subseteq B)$
52	44 49 51	3bitr4d	$⊢ φ \to (\forall k \in A 𝟙_{O} (B) (F (k)) = 1 \leftrightarrow ran F \subseteq B)$
53	52	ifbid	$⊢ φ \to if (\forall k \in A 𝟙_{O} (B) (F (k)) = 1, 1, 0) = if (ran F \subseteq B, 1, 0)$
54	11 16 53	3eqtrd	$⊢ φ \to \prod_{k \in A} 𝟙_{O} (B) (F (k)) = if (ran F \subseteq B, 1, 0)$

Metamath Proof Explorer

Theorem prodindf

Proof