---

Step * 2 1 2 of Lemma omral_scale_non_zero_vals


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|)
⊢ ¬↑(((v * vq) =b 0) ∨b(0 ∈b map(λx.(snd(x));<k,v>* ps)))
BY
{ ((RW bool_to_propC 0 
THENM ProveProp) THEN Auto) }

---

Latex:

---

Latex:

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.  \mneg{}((v  *  vq)  =  0)
\mvdash{}  \mneg{}\muparrow{}(((v  *  vq)  =\msubb{}  0)  \mvee{}\msubb{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));<k,v>*  ps)))


By

---

Latex:
((RW  bool\_to\_propC  0 
THENM  ProveProp)  THEN  Auto)

---

Home Index