---

Step * 1 1 1 1 1 of Lemma omral_times_ident_l

.....truecase..... 
1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
4. u : |g|
5. 1 = 0 ∈ |r|
⊢ (msFor{r↓+gp} x ∈ 0{g↓oset}. msFor{r↓+gp} y ∈ dom(ps). when (x * y) =b u. ((inj(e,1)[x]) * (ps[y]))) = (ps[u]) ∈ |r|
BY
{ Reduce 0 }

1
1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
4. u : |g|
5. 1 = 0 ∈ |r|
⊢ 0 = (ps[u]) ∈ |r|

---

Latex:

---

Latex:
.....truecase..... 
1.  g  :  OCMon
2.  r  :  CDRng
3.  ps  :  |omral(g;r)|
4.  u  :  |g|
5.  1  =  0
\mvdash{}  (msFor\{r\mdownarrow{}+gp\}  x  \mmember{}  0\{g\mdownarrow{}oset\}
          msFor\{r\mdownarrow{}+gp\}  y  \mmember{}  dom(ps)
              when  (x  *  y)  =\msubb{}  u.
                  ((inj(e,1)[x])  *  (ps[y])))
=  (ps[u])


By

---

Latex:
Reduce  0

---

Home Index