Theorem 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	⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
	reprval.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	reprval.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
	hashreprin.b	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	hashreprin.1	⊢ ( 𝜑 → 𝐵 ⊆ ℕ )
Assertion	hashreprin	⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ) = Σ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )

Proof

Step	Hyp	Ref	Expression
1		reprval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
2		reprval.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		reprval.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
4		hashreprin.b	⊢ ( 𝜑 → 𝐵 ∈ Fin )
5		hashreprin.1	⊢ ( 𝜑 → 𝐵 ⊆ ℕ )
6	5 2 3 4	reprfi	⊢ ( 𝜑 → ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∈ Fin )
7		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
8	7	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 )
9	5 2 3 8	reprss	⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ⊆ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) )
10	6 9	ssfid	⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ∈ Fin )
11		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
12		fsumconst	⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) 1 = ( ( ♯ ‘ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ) · 1 ) )
13	10 11 12	syl2anc	⊢ ( 𝜑 → Σ 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) 1 = ( ( ♯ ‘ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ) · 1 ) )
14	11	ralrimivw	⊢ ( 𝜑 → ∀ 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) 1 ∈ ℂ )
15	6	olcd	⊢ ( 𝜑 → ( ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∈ Fin ) )
16		sumss2	⊢ ( ( ( ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ⊆ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ∀ 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) 1 ∈ ℂ ) ∧ ( ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∈ Fin ) ) → Σ 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) 1 = Σ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) if ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) , 1 , 0 ) )
17	9 14 15 16	syl21anc	⊢ ( 𝜑 → Σ 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) 1 = Σ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) if ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) , 1 , 0 ) )
18	5 2 3	reprinrn	⊢ ( 𝜑 → ( 𝑐 ∈ ( ( 𝐵 ∩ 𝐴 ) ( repr ‘ 𝑆 ) 𝑀 ) ↔ ( 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ran 𝑐 ⊆ 𝐴 ) ) )
19		incom	⊢ ( 𝐵 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 )
20	19	oveq1i	⊢ ( ( 𝐵 ∩ 𝐴 ) ( repr ‘ 𝑆 ) 𝑀 ) = ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 )
21	20	eleq2i	⊢ ( 𝑐 ∈ ( ( 𝐵 ∩ 𝐴 ) ( repr ‘ 𝑆 ) 𝑀 ) ↔ 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) )
22	21	bibi1i	⊢ ( ( 𝑐 ∈ ( ( 𝐵 ∩ 𝐴 ) ( repr ‘ 𝑆 ) 𝑀 ) ↔ ( 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ran 𝑐 ⊆ 𝐴 ) ) ↔ ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ↔ ( 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ran 𝑐 ⊆ 𝐴 ) ) )
23	22	imbi2i	⊢ ( ( 𝜑 → ( 𝑐 ∈ ( ( 𝐵 ∩ 𝐴 ) ( repr ‘ 𝑆 ) 𝑀 ) ↔ ( 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ran 𝑐 ⊆ 𝐴 ) ) ) ↔ ( 𝜑 → ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ↔ ( 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ran 𝑐 ⊆ 𝐴 ) ) ) )
24	18 23	mpbi	⊢ ( 𝜑 → ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ↔ ( 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∧ ran 𝑐 ⊆ 𝐴 ) ) )
25	24	baibd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) → ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ↔ ran 𝑐 ⊆ 𝐴 ) )
26	25	ifbid	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) → if ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) , 1 , 0 ) = if ( ran 𝑐 ⊆ 𝐴 , 1 , 0 ) )
27		nnex	⊢ ℕ ∈ V
28	27	a1i	⊢ ( 𝜑 → ℕ ∈ V )
29	28	ralrimivw	⊢ ( 𝜑 → ∀ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ℕ ∈ V )
30	29	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) → ℕ ∈ V )
31		fzofi	⊢ ( 0 ..^ 𝑆 ) ∈ Fin
32	31	a1i	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) → ( 0 ..^ 𝑆 ) ∈ Fin )
33	1	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝐴 ⊆ ℕ )
34	5	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝐵 ⊆ ℕ )
35	2	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝑀 ∈ ℤ )
36	3	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝑆 ∈ ℕ0 )
37		simpr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) )
38	34 35 36 37	reprf	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐵 )
39	38 34	fssd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ ℕ )
40	30 32 33 39	prodindf	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐 ‘ 𝑎 ) ) = if ( ran 𝑐 ⊆ 𝐴 , 1 , 0 ) )
41	26 40	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ) → if ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) , 1 , 0 ) = ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
42	41	sumeq2dv	⊢ ( 𝜑 → Σ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) if ( 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) , 1 , 0 ) = Σ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
43	17 42	eqtrd	⊢ ( 𝜑 → Σ 𝑐 ∈ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) 1 = Σ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
44		hashcl	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ∈ Fin → ( ♯ ‘ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ) ∈ ℕ0 )
45	10 44	syl	⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ) ∈ ℕ0 )
46	45	nn0cnd	⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ) ∈ ℂ )
47	46	mulridd	⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ) · 1 ) = ( ♯ ‘ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ) )
48	13 43 47	3eqtr3rd	⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ) = Σ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )