---

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


1. r : IntegDom{i}
2. eq : EqDecider(|r|)
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. ∀x,y:|r|.  Dec(x = y ∈ |r|)
5. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
7. c : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
8. (a . l) = 0 ∈ |r|
9. (b . l) = 0 ∈ |r|
10. (c . l) = 0 ∈ |r|
11. ¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))
12. ¬((b x c) = 0 ∈ (ℕ3 ⟶ |r|))
13. ¬((c x a) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ ∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((c . l) = 0 ∈ |r|)) ∧ (¬((a . l) = 0 ∈ |r|)))
BY
{ ((InstLemma `cross-product-non-zero-implies-ext` [⌜r⌝;⌜c⌝;⌜a⌝]⋅ THENA Auto) THEN ParallelLast THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}
2.  eq  :  EqDecider(|r|)
3.  l  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
4.  \mforall{}x,y:|r|.    Dec(x  =  y)
5.  a  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
6.  b  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
7.  c  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
8.  (a  .  l)  =  0
9.  (b  .  l)  =  0
10.  (c  .  l)  =  0
11.  \mneg{}((a  x  b)  =  0)
12.  \mneg{}((b  x  c)  =  0)
13.  \mneg{}((c  x  a)  =  0)
\mvdash{}  \mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((c  .  l)  =  0))  \mwedge{}  (\mneg{}((a  .  l)  =  0)))


By

---

Latex:
((InstLemma  `cross-product-non-zero-implies-ext`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  Auto)

---

Home Index