hashreprin

Description: Express a sum of representations over an intersection using a product of the indicator function. (Contributed by Thierry Arnoux, 11-Dec-2021)

	Ref	Expression
Hypotheses	reprval.a	$⊢ φ \to A \subseteq ℕ$
	reprval.m	$⊢ φ \to M \in ℤ$
	reprval.s	$⊢ φ \to S \in ℕ_{0}$
	hashreprin.b	$⊢ φ \to B \in Fin$
	hashreprin.1	$⊢ φ \to B \subseteq ℕ$
Assertion	hashreprin	$⊢ φ \to \|(A \cap B) repr (S) M\| = \sum_{c \in B repr (S) M} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$

Proof

Step	Hyp	Ref	Expression
1		reprval.a	$⊢ φ \to A \subseteq ℕ$
2		reprval.m	$⊢ φ \to M \in ℤ$
3		reprval.s	$⊢ φ \to S \in ℕ_{0}$
4		hashreprin.b	$⊢ φ \to B \in Fin$
5		hashreprin.1	$⊢ φ \to B \subseteq ℕ$
6	5 2 3 4	reprfi	$⊢ φ \to B repr (S) M \in Fin$
7		inss2	$⊢ A \cap B \subseteq B$
8	7	a1i	$⊢ φ \to A \cap B \subseteq B$
9	5 2 3 8	reprss	$⊢ φ \to (A \cap B) repr (S) M \subseteq B repr (S) M$
10	6 9	ssfid	$⊢ φ \to (A \cap B) repr (S) M \in Fin$
11		1cnd	$⊢ φ \to 1 \in ℂ$
12		fsumconst	$⊢ ((A \cap B) repr (S) M \in Fin \land 1 \in ℂ) \to \sum_{c \in (A \cap B) repr (S) M} 1 = \|(A \cap B) repr (S) M\| \cdot 1$
13	10 11 12	syl2anc	$⊢ φ \to \sum_{c \in (A \cap B) repr (S) M} 1 = \|(A \cap B) repr (S) M\| \cdot 1$
14	11	ralrimivw	$⊢ φ \to \forall c \in ((A \cap B) repr (S) M) 1 \in ℂ$
15	6	olcd	$⊢ φ \to (B repr (S) M \subseteq ℤ_{\geq 0} \lor B repr (S) M \in Fin)$
16		sumss2	$⊢ (((A \cap B) repr (S) M \subseteq B repr (S) M \land \forall c \in ((A \cap B) repr (S) M) 1 \in ℂ) \land (B repr (S) M \subseteq ℤ_{\geq 0} \lor B repr (S) M \in Fin)) \to \sum_{c \in (A \cap B) repr (S) M} 1 = \sum_{c \in B repr (S) M} if (c \in ((A \cap B) repr (S) M), 1, 0)$
17	9 14 15 16	syl21anc	$⊢ φ \to \sum_{c \in (A \cap B) repr (S) M} 1 = \sum_{c \in B repr (S) M} if (c \in ((A \cap B) repr (S) M), 1, 0)$
18	5 2 3	reprinrn	$⊢ φ \to (c \in ((B \cap A) repr (S) M) \leftrightarrow (c \in (B repr (S) M) \land ran c \subseteq A))$
19		incom	$⊢ B \cap A = A \cap B$
20	19	oveq1i	$⊢ (B \cap A) repr (S) M = (A \cap B) repr (S) M$
21	20	eleq2i	$⊢ c \in ((B \cap A) repr (S) M) \leftrightarrow c \in ((A \cap B) repr (S) M)$
22	21	bibi1i	$⊢ (c \in ((B \cap A) repr (S) M) \leftrightarrow (c \in (B repr (S) M) \land ran c \subseteq A)) \leftrightarrow (c \in ((A \cap B) repr (S) M) \leftrightarrow (c \in (B repr (S) M) \land ran c \subseteq A))$
23	22	imbi2i	$⊢ (φ \to (c \in ((B \cap A) repr (S) M) \leftrightarrow (c \in (B repr (S) M) \land ran c \subseteq A))) \leftrightarrow (φ \to (c \in ((A \cap B) repr (S) M) \leftrightarrow (c \in (B repr (S) M) \land ran c \subseteq A)))$
24	18 23	mpbi	$⊢ φ \to (c \in ((A \cap B) repr (S) M) \leftrightarrow (c \in (B repr (S) M) \land ran c \subseteq A))$
25	24	baibd	$⊢ (φ \land c \in (B repr (S) M)) \to (c \in ((A \cap B) repr (S) M) \leftrightarrow ran c \subseteq A)$
26	25	ifbid	$⊢ (φ \land c \in (B repr (S) M)) \to if (c \in ((A \cap B) repr (S) M), 1, 0) = if (ran c \subseteq A, 1, 0)$
27		nnex	$⊢ ℕ \in V$
28	27	a1i	$⊢ φ \to ℕ \in V$
29	28	ralrimivw	$⊢ φ \to \forall c \in (B repr (S) M) ℕ \in V$
30	29	r19.21bi	$⊢ (φ \land c \in (B repr (S) M)) \to ℕ \in V$
31		fzofi	$⊢ (0 ..^S) \in Fin$
32	31	a1i	$⊢ (φ \land c \in (B repr (S) M)) \to (0 ..^S) \in Fin$
33	1	adantr	$⊢ (φ \land c \in (B repr (S) M)) \to A \subseteq ℕ$
34	5	adantr	$⊢ (φ \land c \in (B repr (S) M)) \to B \subseteq ℕ$
35	2	adantr	$⊢ (φ \land c \in (B repr (S) M)) \to M \in ℤ$
36	3	adantr	$⊢ (φ \land c \in (B repr (S) M)) \to S \in ℕ_{0}$
37		simpr	$⊢ (φ \land c \in (B repr (S) M)) \to c \in (B repr (S) M)$
38	34 35 36 37	reprf	$⊢ (φ \land c \in (B repr (S) M)) \to c : (0 ..^S) ⟶ B$
39	38 34	fssd	$⊢ (φ \land c \in (B repr (S) M)) \to c : (0 ..^S) ⟶ ℕ$
40	30 32 33 39	prodindf	$⊢ (φ \land c \in (B repr (S) M)) \to \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a)) = if (ran c \subseteq A, 1, 0)$
41	26 40	eqtr4d	$⊢ (φ \land c \in (B repr (S) M)) \to if (c \in ((A \cap B) repr (S) M), 1, 0) = \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$
42	41	sumeq2dv	$⊢ φ \to \sum_{c \in B repr (S) M} if (c \in ((A \cap B) repr (S) M), 1, 0) = \sum_{c \in B repr (S) M} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$
43	17 42	eqtrd	$⊢ φ \to \sum_{c \in (A \cap B) repr (S) M} 1 = \sum_{c \in B repr (S) M} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$
44		hashcl	$⊢ (A \cap B) repr (S) M \in Fin \to \|(A \cap B) repr (S) M\| \in ℕ_{0}$
45	10 44	syl	$⊢ φ \to \|(A \cap B) repr (S) M\| \in ℕ_{0}$
46	45	nn0cnd	$⊢ φ \to \|(A \cap B) repr (S) M\| \in ℂ$
47	46	mulridd	$⊢ φ \to \|(A \cap B) repr (S) M\| \cdot 1 = \|(A \cap B) repr (S) M\|$
48	13 43 47	3eqtr3rd	$⊢ φ \to \|(A \cap B) repr (S) M\| = \sum_{c \in B repr (S) M} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$

Metamath Proof Explorer

Theorem hashreprin

Proof