---

Step * 1 1 of Lemma mset_prod_mem


1. g : DMon
2. a : MSet{g↓set}
3. b : MSet{g↓set}
4. u : |g|
⊢ ∃b{g↓set} u1 ∈ a. ∃b{g↓set} v ∈ b. ((u1 * v) (=b) u) = ∃b{g↓set} v ∈ a. ∃b{g↓set} w ∈ b. (u =b (v * w))
BY
{ Reduce 0 THENM ((RWN 1 (LemmaC `grp_eq_sym`) 0) THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  DMon
2.  a  :  MSet\{g\mdownarrow{}set\}
3.  b  :  MSet\{g\mdownarrow{}set\}
4.  u  :  |g|
\mvdash{}  \mexists{}\msubb{}\{g\mdownarrow{}set\}  u1  \mmember{}  a.  \mexists{}\msubb{}\{g\mdownarrow{}set\}  v  \mmember{}  b.  ((u1  *  v)  (=\msubb{})  u)  =  \mexists{}\msubb{}\{g\mdownarrow{}set\}  v  \mmember{}  a.  \mexists{}\msubb{}\{g\mdownarrow{}set\}  w  \mmember{}  b.  (u  =\msubb{}  (v  \000C*  w))


By

---

Latex:
Reduce  0  THENM  ((RWN  1  (LemmaC  `grp\_eq\_sym`)  0)  THEN  Auto)

---

Home Index