---

Step * 1 of Lemma mon_for_swap


1. g : IAbMonoid
2. A : Type
3. B : Type
4. f : A ⟶ B ⟶ |g|
5. u : A
6. v : A List
7. ∀bs:B List. ((For{g} x ∈ v. For{g} y ∈ bs. f[x;y]) = (For{g} y ∈ bs. For{g} x ∈ v. f[x;y]) ∈ |g|)
8. bs : B List
⊢ ((For{g} y ∈ bs. f[u;y]) * (For{g} x ∈ v. For{g} y ∈ bs. f[x;y]))
= (For{g} y ∈ bs. (f[u;y] * (For{g} x ∈ v. f[x;y])))
∈ |g|
BY
{ (RWO "-2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  A  :  Type
3.  B  :  Type
4.  f  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  |g|
5.  u  :  A
6.  v  :  A  List
7.  \mforall{}bs:B  List.  ((For\{g\}  x  \mmember{}  v.  For\{g\}  y  \mmember{}  bs.  f[x;y])  =  (For\{g\}  y  \mmember{}  bs.  For\{g\}  x  \mmember{}  v.  f[x;y]))
8.  bs  :  B  List
\mvdash{}  ((For\{g\}  y  \mmember{}  bs.  f[u;y])  *  (For\{g\}  x  \mmember{}  v.  For\{g\}  y  \mmember{}  bs.  f[x;y]))
=  (For\{g\}  y  \mmember{}  bs.  (f[u;y]  *  (For\{g\}  x  \mmember{}  v.  f[x;y])))


By

---

Latex:
(RWO  "-2"  0  THEN  Auto)

---

Home Index