---

Step * 1 1 1 1 of Lemma rng_prod_plus


1. r : CRng
2. n : ℤ
3. 0 < n
4. F : ℕn ⟶ |r|
5. G : ℕn ⟶ |r|
6. ∀[f:(ℕn ⟶ ℕ2) ⟶ |r|]. ∀[as:(ℕn ⟶ ℕ2) List].
     (Σ{r} x ∈ as. f[x]
     = (Σ{r} x ∈ filter(λ2p.(p (n - 1) =z 0);as). f[x] +r Σ{r} x ∈ filter(λa.(¬b(a (n - 1) =z 0));as). f[x])
     ∈ |r|)
7. filter(λ2p.(p (n - 1) =z 0);functions-list(n;2)) ∈ (ℕn ⟶ ℕ2) List
⊢ Σ{r} p ∈ functions-list(n - 1;2). ((Π(r) 0 ≤ i < n - 1. if (p i =z 0) then F[i] else G[i] fi ) * F[n - 1])
= Σ{r} p ∈ filter(λ2p.(p (n - 1) =z 0);functions-list(n;2)). ((Π(r) 0 
                                                                    ≤ i 
                                                                    < n - 1
                                                                if (p i =z 0) then F[i] else G[i] fi ) 
                                                              * 
                                                              F[n - 1])
∈ |r|
BY
{ ((InstLemma `rng_lsum_map` [⌜r⌝;⌜ℕn - 1 ⟶ ℕ2⌝;⌜ℕn ⟶ ℕ2⌝;⌜λf,i. if (i =z n - 1) then 0 else f i fi ⌝;⌜λ2p.(Π(r) 0 
                                                                                                               ≤ i 
                                                                                                               < n - 1
                                                                                                           if (p i =z 0)
                                                                                                           then F[i]
                                                                                                           else G[i]
                                                                                                           fi ) 
                                                                                                         * 
                                                                                                         F[n - 1]⌝;
    ⌜functions-list(n - 1;2)⌝]⋅
    THENA Auto
    )
   THEN Reduce -1
   THEN Symmetry
   THEN NthHypEq (-1)
   THEN (EqCDA
         THENL [((Assert map(λf,i. if (i =z n - 1) then 0 else f i fi ;functions-list(n - 1;2)) ∈ (ℕn ⟶ ℕ2) List BY
                        Auto)
                 THEN (BLemma `rng_lsum_functionality_wrt_permutation` THENA Auto)
                 THEN ThinVar `r')
               ; (RepeatFor 3 (EqCDA) THEN AutoSplit)]
   )) }

1
1. n : ℤ
2. 0 < n
3. filter(λ2p.(p (n - 1) =z 0);functions-list(n;2)) ∈ (ℕn ⟶ ℕ2) List
4. map(λf,i. if (i =z n - 1) then 0 else f i fi ;functions-list(n - 1;2)) ∈ (ℕn ⟶ ℕ2) List
⊢ permutation(ℕn ⟶ ℕ2;filter(λ2p.(p (n - 1) =z 0);functions-list(n;2));
              map(λf,i. if (i =z n - 1) then 0 else f i fi ;functions-list(n - 1;2)))

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  F  :  \mBbbN{}n  {}\mrightarrow{}  |r|
5.  G  :  \mBbbN{}n  {}\mrightarrow{}  |r|
6.  \mforall{}[f:(\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}2)  {}\mrightarrow{}  |r|].  \mforall{}[as:(\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}2)  List].
          (\mSigma{}\{r\}  x  \mmember{}  as.  f[x]
          =  (\mSigma{}\{r\}  x  \mmember{}  filter(\mlambda{}\msubtwo{}p.(p  (n  -  1)  =\msubz{}  0);as).  f[x] 
                +r 
                \mSigma{}\{r\}  x  \mmember{}  filter(\mlambda{}a.(\mneg{}\msubb{}(a  (n  -  1)  =\msubz{}  0));as).  f[x]))
7.  filter(\mlambda{}\msubtwo{}p.(p  (n  -  1)  =\msubz{}  0);functions-list(n;2))  \mmember{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}2)  List
\mvdash{}  \mSigma{}\{r\}  p  \mmember{}  functions-list(n  -  1;2).  ((\mPi{}(r)  0 
                                                                                      \mleq{}  i 
                                                                                      <  n  -  1
                                                                              if  (p  i  =\msubz{}  0)  then  F[i]  else  G[i]  fi  ) 
                                                                          * 
                                                                          F[n  -  1])
=  \mSigma{}\{r\}  p  \mmember{}  filter(\mlambda{}\msubtwo{}p.(p  (n  -  1)  =\msubz{}  0);functions-list(n;2)).  ((\mPi{}(r)  0 
                                                                                                                                        \mleq{}  i 
                                                                                                                                        <  n  -  1
                                                                                                                                if  (p  i  =\msubz{}  0)
                                                                                                                                then  F[i]
                                                                                                                                else  G[i]
                                                                                                                                fi  ) 
                                                                                                                            * 
                                                                                                                            F[n  -  1])


By

---

Latex:
((InstLemma  `rng\_lsum\_map`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}\mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbN{}2\mkleeneclose{};\mkleeneopen{}\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}2\mkleeneclose{};\mkleeneopen{}\mlambda{}f,i.  if  (i  =\msubz{}  n  -  1)  then  0  else  f  i  fi  \000C\mkleeneclose{};
    \mkleeneopen{}\mlambda{}\msubtwo{}p.(\mPi{}(r)  0  \mleq{}  i  <  n  -  1.  if  (p  i  =\msubz{}  0)  then  F[i]  else  G[i]  fi  )  *  F[n  -  1]\mkleeneclose{};
    \mkleeneopen{}functions-list(n  -  1;2)\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  Reduce  -1
  THEN  Symmetry
  THEN  NthHypEq  (-1)
  THEN  (EqCDA
              THENL  [((Assert  map(\mlambda{}f,i.  if  (i  =\msubz{}  n  -  1)  then  0  else  f  i  fi  ;functions-list(n  -  1;2))  \mmember{}  (\mBbbN{}n
                                              {}\mrightarrow{}  \mBbbN{}2)  List  BY
                                            Auto)
                              THEN  (BLemma  `rng\_lsum\_functionality\_wrt\_permutation`  THENA  Auto)
                              THEN  ThinVar  `r')
                          ;  (RepeatFor  3  (EqCDA)  THEN  AutoSplit)]
  ))

---

Home Index