---

Step * of Lemma rng-pp-nontriv2_wf

∀[r:IntegDom{i}]. ∀[eq:EqDecider(|r|)]. ∀[a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} ].
  (rng-pp-nontriv2(r;eq;a) ∈ ∃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
{ (Auto
   THEN Try ((Subst' rng-pp-nontriv2(r;eq;a) ~ TERMOF{rng-pp-nontrivial-4-ext:o, \\v:l, i:l} r eq a 0 THENM Auto))
   ) }

1
.....equality..... 
1. r : IntegDom{i}
2. eq : EqDecider(|r|)
3. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
⊢ rng-pp-nontriv2(r;eq;a) ~ TERMOF{rng-pp-nontrivial-4-ext:o, \\v:l, i:l} r eq a

---

Latex:

---

Latex:
\mforall{}[r:IntegDom\{i\}].  \mforall{}[eq:EqDecider(|r|)].  \mforall{}[a:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  ].
    (rng-pp-nontriv2(r;eq;a)  \mmember{}  \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)))\000C)
                                                            \mwedge{}  (\mexists{}a:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((a  .  m)  =  0))  \mwedge{}  (\mneg{}((a  .  n)  =  0)))\000C)
                                                            \mwedge{}  (\mexists{}a:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
                                                                    ((\mneg{}\mneg{}((a  .  n)  =  0))  \mwedge{}  (\mneg{}((a  .  l)  =  0))))))


By

---

Latex:
(Auto
  THEN  Try  ((Subst'  rng-pp-nontriv2(r;eq;a)  \msim{}  TERMOF\{rng-pp-nontrivial-4-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  r  eq  a  0
                      THENM  Auto
                      ))
  )

---

Home Index