---

Step * 2 1 1 of Lemma omral_scale_non_zero_vals

.....truecase..... 
1. g : OCMon
2. r : CDRng
3. (r↓+gp ∈ AbDMon) ∧ (r↓xmn ∈ AbDMon)
4. k : |g|
5. v : |r|
6. kq : |g|
7. vq : |r|
8. ps : (|g| × |r|) List
9. (¬↑(0 ∈b map(λx.(snd(x));ps))) ⇒ (¬↑(0 ∈b map(λx.(snd(x));<k,v>* ps)))
10. (¬(vq = 0 ∈ |r|)) ∧ (¬↑(0 ∈b map(λx.(snd(x));ps)))
11. (v * vq) = 0 ∈ |r|
⊢ ¬↑(0 ∈b map(λx.(snd(x));<k,v>* ps))
BY
{ ((BHyp 9) THEN Auto) }

---

Latex:

---

Latex:
.....truecase..... 
1.  g  :  OCMon
2.  r  :  CDRng
3.  (r\mdownarrow{}+gp  \mmember{}  AbDMon)  \mwedge{}  (r\mdownarrow{}xmn  \mmember{}  AbDMon)
4.  k  :  |g|
5.  v  :  |r|
6.  kq  :  |g|
7.  vq  :  |r|
8.  ps  :  (|g|  \mtimes{}  |r|)  List
9.  (\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps)))  {}\mRightarrow{}  (\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));<k,v>*  ps)))
10.  (\mneg{}(vq  =  0))  \mwedge{}  (\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps)))
11.  (v  *  vq)  =  0
\mvdash{}  \mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));<k,v>*  ps))


By

---

Latex:
((BHyp  9)  THEN  Auto)

---

Home Index