---

Step * 3 of Lemma triple-cross-product-zero


1. r : CRng
2. a : ℕ3 ⟶ |r|
3. p : ℕ3 ⟶ |r|
4. q : ℕ3 ⟶ |r|
5. (p . a) = 0 ∈ |r|
6. (q . a) = 0 ∈ |r|
7. x : ℤ
8. x = 2 ∈ ℤ
⊢ ((-r ((a 0) * ((p 0) * (q 2)))) 
   +r 
   (((a 0) * ((p 2) * (q 0))) +r ((-r ((a 1) * ((p 1) * (q 2)))) +r ((a 1) * ((p 2) * (q 1))))))
= 0
∈ |r|
BY
{ ((Assert (((p 2) * (q . a)) +r (-r ((q 2) * (p . a)))) = 0 ∈ |r| BY
          ((RWO "-3 -4" 0 THENM RW  RngNormC 0) THEN Auto))
   THEN (RWO "scalar-product-3" (-1) THENA Auto)
   THEN RW CRngNormC (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  a  :  \mBbbN{}3  {}\mrightarrow{}  |r|
3.  p  :  \mBbbN{}3  {}\mrightarrow{}  |r|
4.  q  :  \mBbbN{}3  {}\mrightarrow{}  |r|
5.  (p  .  a)  =  0
6.  (q  .  a)  =  0
7.  x  :  \mBbbZ{}
8.  x  =  2
\mvdash{}  ((-r  ((a  0)  *  ((p  0)  *  (q  2)))) 
      +r 
      (((a  0)  *  ((p  2)  *  (q  0)))  +r  ((-r  ((a  1)  *  ((p  1)  *  (q  2))))  +r  ((a  1)  *  ((p  2)  *  (q  1))))))
=  0


By

---

Latex:
((Assert  (((p  2)  *  (q  .  a))  +r  (-r  ((q  2)  *  (p  .  a))))  =  0  BY
                ((RWO  "-3  -4"  0  THENM  RW    RngNormC  0)  THEN  Auto))
  THEN  (RWO  "scalar-product-3"  (-1)  THENA  Auto)
  THEN  RW  CRngNormC  (-1)
  THEN  Auto)

---

Home Index