---

Step * 1 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 = 0 ∈ ℤ
⊢ (((a 1) * ((p 0) * (q 1))) 
   +r 
   ((-r ((a 1) * ((p 1) * (q 0)))) +r (((a 2) * ((p 0) * (q 2))) +r (-r ((a 2) * ((p 2) * (q 0)))))))
= 0
∈ |r|
BY
{ ((Assert (((p 0) * (q . a)) +r (-r ((q 0) * (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  =  0
\mvdash{}  (((a  1)  *  ((p  0)  *  (q  1))) 
      +r 
      ((-r  ((a  1)  *  ((p  1)  *  (q  0)))) 
        +r 
        (((a  2)  *  ((p  0)  *  (q  2)))  +r  (-r  ((a  2)  *  ((p  2)  *  (q  0)))))))
=  0


By

---

Latex:
((Assert  (((p  0)  *  (q  .  a))  +r  (-r  ((q  0)  *  (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