---

Step * 1 1 1 1 of Lemma omral_times_ident_l


1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
4. u : |g|
⊢ (msFor{r↓+gp} x ∈ if 1 =b 0 then 0{g↓oset} else mset_inj{g↓oset}(e) fi 
     msFor{r↓+gp} y ∈ dom(ps)
       when (x * y) =b u.
         ((inj(e,1)[x]) * (ps[y])))
= (ps[u])
∈ |r|
BY
{ ((SplitOnConclITE) THENA Auto) }

1
.....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|

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

---

Latex:

---

Latex:

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


By

---

Latex:
((SplitOnConclITE)  THENA  Auto)

---

Home Index