Metamath Proof Explorer

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 mulid1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ) · 1 ) = ( ♯ ‘ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ) )
48 13 43 47 3eqtr3rd ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝐴 ∩ 𝐵 ) ( repr ‘ 𝑆 ) 𝑀 ) ) = Σ 𝑐 ∈ ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )