---

Step * of Lemma rng-pp-nontrivial-3-ext

∀r:IntegDom{i}. ∀eq:EqDecider(|r|). ∀l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} .
  ∃a,b,c:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
   ((¬¬((a . l) = 0 ∈ |r|))
   ∧ (¬¬((b . l) = 0 ∈ |r|))
   ∧ (¬¬((c . l) = 0 ∈ |r|))
   ∧ (∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a . l) = 0 ∈ |r|)) ∧ (¬((b . l) = 0 ∈ |r|))))
   ∧ (∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((b . l) = 0 ∈ |r|)) ∧ (¬((c . l) = 0 ∈ |r|))))
   ∧ (∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((c . l) = 0 ∈ |r|)) ∧ (¬((a . l) = 0 ∈ |r|)))))
BY
{ Extract of Obid: rng-pp-nontrivial-3
  not unfolding  rng_zero rng_one rng_minus vector-add nonzero-cross-imp non-zero-component
  finishing with xxx(Fold `rng-pp-nontriv1` 0 THEN Auto)xxx
  normalizes to:
  
  λr,eq,l. rng-pp-nontriv1(r;eq;l) }

---

Latex:

---

Latex:
\mforall{}r:IntegDom\{i\}.  \mforall{}eq:EqDecider(|r|).  \mforall{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .
    \mexists{}a,b,c:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
      ((\mneg{}\mneg{}((a  .  l)  =  0))
      \mwedge{}  (\mneg{}\mneg{}((b  .  l)  =  0))
      \mwedge{}  (\mneg{}\mneg{}((c  .  l)  =  0))
      \mwedge{}  (\mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((a  .  l)  =  0))  \mwedge{}  (\mneg{}((b  .  l)  =  0))))
      \mwedge{}  (\mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((b  .  l)  =  0))  \mwedge{}  (\mneg{}((c  .  l)  =  0))))
      \mwedge{}  (\mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((c  .  l)  =  0))  \mwedge{}  (\mneg{}((a  .  l)  =  0)))))


By

---

Latex:
Extract  of  Obid:  rng-pp-nontrivial-3
not  unfolding    rng\_zero  rng\_one  rng\_minus  vector-add  nonzero-cross-imp  non-zero-component
finishing  with  xxx(Fold  `rng-pp-nontriv1`  0  THEN  Auto)xxx
normalizes  to:

\mlambda{}r,eq,l.  rng-pp-nontriv1(r;eq;l)

---

Home Index