---

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


1. r : IntegDom{i}
2. eq : EqDecider(|r|)
3. p : {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 . p) = 0 ∈ |r|
9. (b . p) = 0 ∈ |r|
10. (c . p) = 0 ∈ |r|
11. ¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))
12. ¬((c x a) = 0 ∈ (ℕ3 ⟶ |r|))
13. ¬((b x c) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ ∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a . b) = 0 ∈ |r|)) ∧ (¬((a . c) = 0 ∈ |r|)))
BY
{ ((InstLemma `cross-product-non-zero-implies-ext` [⌜r⌝;⌜b⌝;⌜c⌝]⋅ THENA Auto)
   THEN ParallelLast
   THEN Auto
   THEN RWO "scalar-product-comm" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}
2.  eq  :  EqDecider(|r|)
3.  p  :  \{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  .  p)  =  0
9.  (b  .  p)  =  0
10.  (c  .  p)  =  0
11.  \mneg{}((a  x  b)  =  0)
12.  \mneg{}((c  x  a)  =  0)
13.  \mneg{}((b  x  c)  =  0)
\mvdash{}  \mexists{}a:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((a  .  b)  =  0))  \mwedge{}  (\mneg{}((a  .  c)  =  0)))


By

---

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

---

Home Index