---

Step * 1 of Lemma vs-lift-neg-bfs


1. K : CRng
2. S : Type
3. fs : basic-formal-sum(K;S)
4. vs : VectorSpace(K)
5. f : S ⟶ Point(vs)
⊢ Σ{let k,s = let k,s = p in <-K k, s> in k * f s | p ∈ fs} = Σ{-K 1 * let k,s = p in k * f s | p ∈ fs} ∈ Point(vs)
BY
{ (EqCDA THEN D -1 THEN Reduce 0 THEN (RWO "vs-mul-mul" 0 THEN Auto) THEN EqCDA) }

1
.....subterm..... T:t
2:n
1. K : CRng
2. S : Type
3. fs : basic-formal-sum(K;S)
4. vs : VectorSpace(K)
5. f : S ⟶ Point(vs)
6. p1 : |K|
7. p2 : S
⊢ (-K p1) = ((-K 1) * p1) ∈ |K|

---

Latex:

---

Latex:

1.  K  :  CRng
2.  S  :  Type
3.  fs  :  basic-formal-sum(K;S)
4.  vs  :  VectorSpace(K)
5.  f  :  S  {}\mrightarrow{}  Point(vs)
\mvdash{}  \mSigma{}\{let  k,s  =  let  k,s  =  p 
                            in  <-K  k,  s> 
        in  k  *  f  s  |  p  \mmember{}  fs\}
=  \mSigma{}\{-K  1  *  let  k,s  =  p 
                      in  k  *  f  s  |  p  \mmember{}  fs\}


By

---

Latex:
(EqCDA  THEN  D  -1  THEN  Reduce  0  THEN  (RWO  "vs-mul-mul"  0  THEN  Auto)  THEN  EqCDA)

---

Home Index