---

Step * of Lemma triple-cross-product-zero

∀r:CRng. ∀a,p,q:ℕ3 ⟶ |r|.  (((p . a) = 0 ∈ |r|) ⇒ ((q . a) = 0 ∈ |r|) ⇒ ((a x (p x q)) = 0 ∈ (ℕ3 ⟶ |r|)))
BY
{ (Auto
   THEN (FunExt THENA Auto)
   THEN IntSegCases (-1)
   THEN RepUR ``zero-vector cross-product`` 0
   THEN (RW CRngNormC 0 THENA Auto)) }

1
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|

2
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 = 1 ∈ ℤ
⊢ ((-r ((a 0) * ((p 0) * (q 1)))) 
   +r 
   (((a 0) * ((p 1) * (q 0))) +r (((a 2) * ((p 1) * (q 2))) +r (-r ((a 2) * ((p 2) * (q 1)))))))
= 0
∈ |r|

3
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|

---

Latex:

---

Latex:
\mforall{}r:CRng.  \mforall{}a,p,q:\mBbbN{}3  {}\mrightarrow{}  |r|.    (((p  .  a)  =  0)  {}\mRightarrow{}  ((q  .  a)  =  0)  {}\mRightarrow{}  ((a  x  (p  x  q))  =  0))


By

---

Latex:
(Auto
  THEN  (FunExt  THENA  Auto)
  THEN  IntSegCases  (-1)
  THEN  RepUR  ``zero-vector  cross-product``  0
  THEN  (RW  CRngNormC  0  THENA  Auto))

---

Home Index