---

Step * 1 of Lemma prod_in_mset_prod


1. g : DMon
2. a : MSet{g↓set}
3. b : MSet{g↓set}
4. u : |g|
5. v : |g|
6. ↑(u
∈b a)
7. ↑(v
∈b b)
⊢ ↑((u * v)
∈b msFor{<MSet{g↓set},⋃,0>} u ∈ a
     msFor{<MSet{g↓set},⋃,0>} v ∈ b
       mset_inj{g↓set}(u * v))
BY
{ ((RWH (LambdaC λz:MSet{g↓set}. (u * v)
   ∈b z) 0 
   THENM RWD (LemmaWithC [`n',<𝔹,∨b>] `dist_hom_over_mset_for`) 0 
   THENM Reduce 0) 
   THEN Auto
   ) }

1
1. g : DMon
2. a : MSet{g↓set}
3. b : MSet{g↓set}
4. u : |g|
5. v : |g|
6. ↑(u
∈b a)
7. ↑(v
∈b b)
⊢ ↑(∃b{g↓set} u1 ∈ a
               ∃b{g↓set} v1 ∈ b
                          ((u * v)
                         ∈b mset_inj{g↓set}(u1 * v1)))

---

Latex:

---

Latex:

1.  g  :  DMon
2.  a  :  MSet\{g\mdownarrow{}set\}
3.  b  :  MSet\{g\mdownarrow{}set\}
4.  u  :  |g|
5.  v  :  |g|
6.  \muparrow{}(u
\mmember{}\msubb{}  a)
7.  \muparrow{}(v
\mmember{}\msubb{}  b)
\mvdash{}  \muparrow{}((u  *  v)
\mmember{}\msubb{}  msFor\{<MSet\{g\mdownarrow{}set\},\mcup{},0>\}  u  \mmember{}  a
          msFor\{<MSet\{g\mdownarrow{}set\},\mcup{},0>\}  v  \mmember{}  b
              mset\_inj\{g\mdownarrow{}set\}(u  *  v))


By

---

Latex:
((RWH  (LambdaC  \mlambda{}z:MSet\{g\mdownarrow{}set\}.  (u  *  v)
  \mmember{}\msubb{}  z)  0 
  THENM  RWD  (LemmaWithC  [`n',<\mBbbB{},\mvee{}\msubb{}>]  `dist\_hom\_over\_mset\_for`)  0 
  THENM  Reduce  0) 
  THEN  Auto
  )

---

Home Index