---

Step * 1 of Lemma null-formal-sum-mul


1. S : Type
2. K : CRng
3. x : basic-formal-sum(K;S)
4. k : |K|
5. b : bag(|K| × S)
6. ss : bag(S)
7. x = ((b + -(b)) + 0 * ss) ∈ bag(|K| × S)
⊢ k * x = ((k * b + -(k * b)) + 0 * ss) ∈ bag(|K| × S)
BY
{ ((RWO "-1" 0 THENA Auto)
   THEN RepUR ``formal-sum-mul neg-bfs zero-bfs`` 0
   THEN (RWW "bag-map-append bag-map-map" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN RepeatFor 2 (EqCDA)
   THEN (((FunExt THENA Auto) THEN Reduce 0 THEN EqCDA THEN Auto) ORELSE (EqCDA THEN (FunExt THENA Auto)))) }

1
1. S : Type
2. K : CRng
3. x : basic-formal-sum(K;S)
4. k : |K|
5. b : bag(|K| × S)
6. ss : bag(S)
7. x = ((b + -(b)) + 0 * ss) ∈ bag(|K| × S)
8. x1 : |K| × S
⊢ ((λx.let k',s = let k,s = x in <-K k, s> in <k * k', s>) x1)
= ((λx.let k,s = let k',s = x in <k * k', s> in <-K k, s>) x1)
∈ (|K| × S)

---

Latex:

---

Latex:

1.  S  :  Type
2.  K  :  CRng
3.  x  :  basic-formal-sum(K;S)
4.  k  :  |K|
5.  b  :  bag(|K|  \mtimes{}  S)
6.  ss  :  bag(S)
7.  x  =  ((b  +  -(b))  +  0  *  ss)
\mvdash{}  k  *  x  =  ((k  *  b  +  -(k  *  b))  +  0  *  ss)


By

---

Latex:
((RWO  "-1"  0  THENA  Auto)
  THEN  RepUR  ``formal-sum-mul  neg-bfs  zero-bfs``  0
  THEN  (RWW  "bag-map-append  bag-map-map"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  RepeatFor  2  (EqCDA)
  THEN  (((FunExt  THENA  Auto)  THEN  Reduce  0  THEN  EqCDA  THEN  Auto)
  ORELSE  (EqCDA  THEN  (FunExt  THENA  Auto))
  ))

---

Home Index