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 ⊢ φ → A ⊆ ℕ
reprval.m ⊢ φ → M ∈ ℤ
reprval.s ⊢ φ → S ∈ ℕ 0
hashreprin.b ⊢ φ → B ∈ Fin
hashreprin.1 ⊢ φ → B ⊆ ℕ
Assertion hashreprin ⊢ φ → A ∩ B repr ⁡ S M = ∑ c ∈ B repr ⁡ S M ∏ a ∈ 0 ..^ S 𝟙 ℕ ⁡ A ⁡ c ⁡ a

Proof

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