R : Type u_1
inst✝ : CommRing R
u v w x : Fin 3 → R
⊢ vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 *
          vecCons (w 1 * x 2 - w 2 * x 1) ![w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 0 +
        vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 *
          vecCons (w 1 * x 2 - w 2 * x 1) ![w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 1 +
      vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 *
        vecCons (w 1 * x 2 - w 2 * x 1) ![w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 2 =
    (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * (v 0 * x 0 + v 1 * x 1 + v 2 * x 2) -
      (u 0 * x 0 + u 1 * x 1 + u 2 * x 2) * (v 0 * w 0 + v 1 * w 1 + v 2 * w 2)
R : Type u_1
inst✝ : CommRing R
u v w x : Fin 3 → R
⊢ ↑(↑crossProduct u) v ⬝ᵥ ↑(↑crossProduct w) x = u ⬝ᵥ w * v ⬝ᵥ x - u ⬝ᵥ x * v ⬝ᵥ w
simp_rw [cross_apply, vec3_dotProduct]
R : Type u_1
inst✝ : CommRing R
u v w x : Fin 3 → R
⊢ (u 1 * v 2 - u 2 * v 1) * (w 1 * x 2 - w 2 * x 1) + (u 2 * v 0 - u 0 * v 2) * (w 2 * x 0 - w 0 * x 2) +
      (u 0 * v 1 - u 1 * v 0) * (w 0 * x 1 - w 1 * x 0) =
    (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * (v 0 * x 0 + v 1 * x 1 + v 2 * x 2) -
      (u 0 * x 0 + u 1 * x 1 + u 2 * x 2) * (v 0 * w 0 + v 1 * w 1 + v 2 * w 2)
R : Type u_1
inst✝ : CommRing R
u v w x : Fin 3 → R
⊢ vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 *
          vecCons (w 1 * x 2 - w 2 * x 1) ![w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 0 +
        vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 *
          vecCons (w 1 * x 2 - w 2 * x 1) ![w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 1 +
      vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 *
        vecCons (w 1 * x 2 - w 2 * x 1) ![w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 2 =
    (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * (v 0 * x 0 + v 1 * x 1 + v 2 * x 2) -
      (u 0 * x 0 + u 1 * x 1 + u 2 * x 2) * (v 0 * w 0 + v 1 * w 1 + v 2 * w 2)
norm_num
no goals
R : Type u_1
inst✝ : CommRing R
u v w x : Fin 3 → R
⊢ (u 1 * v 2 - u 2 * v 1) * (w 1 * x 2 - w 2 * x 1) + (u 2 * v 0 - u 0 * v 2) * (w 2 * x 0 - w 0 * x 2) +
      (u 0 * v 1 - u 1 * v 0) * (w 0 * x 1 - w 1 * x 0) =
    (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * (v 0 * x 0 + v 1 * x 1 + v 2 * x 2) -
      (u 0 * x 0 + u 1 * x 1 + u 2 * x 2) * (v 0 * w 0 + v 1 * w 1 + v 2 * w 2)
ring