---

Step * 4 of Lemma rng-pp-nontrivial-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. [%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|))
BY
{ (ParallelOp -2
   THEN (RWW "cross-product-distrib2 cross-product-same zero-vector-add-left" (-1) THENA Auto)
   THEN (RW RngNormC  (-1) THENA Auto)
   THEN (RWO "cross-product-anti-comm" 0 THENA Auto)
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}
2.  \mforall{}x,y:|r|.    Dec(x  =  y)
3.  l  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
4.  a  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
5.  b  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
6.  [\%3]  :  ((a  .  l)  =  0)  \mwedge{}  ((b  .  l)  =  0)  \mwedge{}  (\mneg{}((a  x  b)  =  0))
7.  (a  .  l)  =  0
8.  (b  .  l)  =  0
9.  ((a  +  b)  .  l)  =  0
10.  \mneg{}((a  x  b)  =  0)
11.  \mneg{}((b  x  (a  +  b))  =  0)
\mvdash{}  \mneg{}(((a  +  b)  x  a)  =  0)


By

---

Latex:
(ParallelOp  -2
  THEN  (RWW  "cross-product-distrib2  cross-product-same  zero-vector-add-left"  (-1)  THENA  Auto)
  THEN  (RW  RngNormC    (-1)  THENA  Auto)
  THEN  (RWO  "cross-product-anti-comm"  0  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index