---

Step * 2 1 of Lemma l_sum-mapfilter


1. T : Type
2. u : T
3. v : T List
4. ∀[P:T ⟶ 𝔹]. ∀[f:{x:T| (x ∈ v) ∧ (↑(P x))}  ⟶ ℤ].
     (l_sum(map(f;filter(P;v))) = Σ(if P v[i] then f v[i] else 0 fi  | i < ||v||) ∈ ℤ)
5. P : T ⟶ 𝔹
6. ∀[f:{x:T| (x ∈ v) ∧ (↑(P x))}  ⟶ ℤ]
     (l_sum(map(f;filter(P;v))) = Σ(if P v[i] then f v[i] else 0 fi  | i < ||v||) ∈ ℤ)
7. f : {x:T| (x ∈ [u / v]) ∧ (↑(P x))}  ⟶ ℤ
8. l_sum(map(f;filter(P;v))) = Σ(if P v[i] then f v[i] else 0 fi  | i < ||v||) ∈ ℤ
⊢ l_sum(map(f;if P u then [u / filter(P;v)] else filter(P;v) fi ))
= Σ(if P [u / v][i] then f [u / v][i] else 0 fi  | i < ||v|| + 1)
∈ ℤ
BY
{ ((InstLemma `sum_split` [⌜||v|| + 1⌝;⌜λ2i.if P [u / v][i] then f [u / v][i] else 0 fi ⌝;⌜1⌝]⋅
    THENA Try (Complete (Auto))
    )
   THEN Try ((HypSubst' (-1) 0 THEN Thin (-1)))
   ) }

1
1. T : Type
2. u : T
3. v : T List
4. ∀[P:T ⟶ 𝔹]. ∀[f:{x:T| (x ∈ v) ∧ (↑(P x))}  ⟶ ℤ].
     (l_sum(map(f;filter(P;v))) = Σ(if P v[i] then f v[i] else 0 fi  | i < ||v||) ∈ ℤ)
5. P : T ⟶ 𝔹
6. ∀[f:{x:T| (x ∈ v) ∧ (↑(P x))}  ⟶ ℤ]
     (l_sum(map(f;filter(P;v))) = Σ(if P v[i] then f v[i] else 0 fi  | i < ||v||) ∈ ℤ)
7. f : {x:T| (x ∈ [u / v]) ∧ (↑(P x))}  ⟶ ℤ
8. l_sum(map(f;filter(P;v))) = Σ(if P v[i] then f v[i] else 0 fi  | i < ||v||) ∈ ℤ
⊢ l_sum(map(f;if P u then [u / filter(P;v)] else filter(P;v) fi ))
= (Σ(if P [u / v][x] then f [u / v][x] else 0 fi  | x < 1)
  + Σ(if P [u / v][x + 1] then f [u / v][x + 1] else 0 fi  | x < (||v|| + 1) - 1))
∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{x:T|  (x  \mmember{}  v)  \mwedge{}  (\muparrow{}(P  x))\}    {}\mrightarrow{}  \mBbbZ{}].
          (l\_sum(map(f;filter(P;v)))  =  \mSigma{}(if  P  v[i]  then  f  v[i]  else  0  fi    |  i  <  ||v||))
5.  P  :  T  {}\mrightarrow{}  \mBbbB{}
6.  \mforall{}[f:\{x:T|  (x  \mmember{}  v)  \mwedge{}  (\muparrow{}(P  x))\}    {}\mrightarrow{}  \mBbbZ{}]
          (l\_sum(map(f;filter(P;v)))  =  \mSigma{}(if  P  v[i]  then  f  v[i]  else  0  fi    |  i  <  ||v||))
7.  f  :  \{x:T|  (x  \mmember{}  [u  /  v])  \mwedge{}  (\muparrow{}(P  x))\}    {}\mrightarrow{}  \mBbbZ{}
8.  l\_sum(map(f;filter(P;v)))  =  \mSigma{}(if  P  v[i]  then  f  v[i]  else  0  fi    |  i  <  ||v||)
\mvdash{}  l\_sum(map(f;if  P  u  then  [u  /  filter(P;v)]  else  filter(P;v)  fi  ))
=  \mSigma{}(if  P  [u  /  v][i]  then  f  [u  /  v][i]  else  0  fi    |  i  <  ||v||  +  1)


By

---

Latex:
((InstLemma  `sum\_split`  [\mkleeneopen{}||v||  +  1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.if  P  [u  /  v][i]  then  f  [u  /  v][i]  else  0  fi  \mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}
    THENA  Try  (Complete  (Auto))
    )
  THEN  Try  ((HypSubst'  (-1)  0  THEN  Thin  (-1)))
  )

---

Home Index