---

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

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

---

Latex:

---

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


By

---

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

\mlambda{}r,eq,a.  rng-pp-nontriv2(r;eq;a)

---

Home Index