---

Step * of Lemma rng-pp-nontrivial-2

∀r:IntegDom{i}
  ((∀x,y:|r|.  Dec(x = y ∈ |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|)
         ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|)))
         ∧ (¬((b x c) = 0 ∈ (ℕ3 ⟶ |r|)))
         ∧ (¬((c x a) = 0 ∈ (ℕ3 ⟶ |r|))))))
BY
{ (InstLemma `rng-pp-nontrivial-1-ext` []
   THEN RepeatFor 5 ((ParallelLast' THENA Auto))
   THEN D 0 With ⌜(a + b)⌝ 
   THEN Auto) }

1
1. r : IntegDom{i}
2. ∀x,y:|r|.  Dec(x = y ∈ |r|)
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
5. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. (a . l) = 0 ∈ |r|
7. (b . l) = 0 ∈ |r|
8. ¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ (a + b) ∈ {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 

2
1. r : IntegDom{i}
2. ∀x,y:|r|.  Dec(x = y ∈ |r|)
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
5. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. (a . l) = 0 ∈ |r|
7. (b . l) = 0 ∈ |r|
8. ¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))
9. (a . l) = 0 ∈ |r|
10. (b . l) = 0 ∈ |r|
⊢ ((a + b) . l) = 0 ∈ |r|

3
1. r : IntegDom{i}
2. ∀x,y:|r|.  Dec(x = y ∈ |r|)
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
5. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. [%3] : ((a . l) = 0 ∈ |r|) ∧ ((b . l) = 0 ∈ |r|) ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|)))
7. (a . l) = 0 ∈ |r|
8. (b . l) = 0 ∈ |r|
9. ((a + b) . l) = 0 ∈ |r|
10. ¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ ¬((b x (a + b)) = 0 ∈ (ℕ3 ⟶ |r|))

4
1. r : IntegDom{i}
2. ∀x,y:|r|.  Dec(x = y ∈ |r|)
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
5. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. [%3] : ((a . l) = 0 ∈ |r|) ∧ ((b . l) = 0 ∈ |r|) ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|)))
7. (a . l) = 0 ∈ |r|
8. (b . l) = 0 ∈ |r|
9. ((a + b) . l) = 0 ∈ |r|
10. ¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))
11. ¬((b x (a + b)) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ ¬(((a + b) x a) = 0 ∈ (ℕ3 ⟶ |r|))

---

Latex:

---

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


By

---

Latex:
(InstLemma  `rng-pp-nontrivial-1-ext`  []
  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto))
  THEN  D  0  With  \mkleeneopen{}(a  +  b)\mkleeneclose{} 
  THEN  Auto)

---

Home Index