---

Step * 1 1 1 1 of Lemma dot-product-split


1. n : ℕ
2. k : ℕn
3. x : ℝ^n
4. y : ℝ^n
5. λi.(x (0 + i)) ∈ ℝ^n - 0
6. λi.(y (0 + i)) ∈ ℝ^n - 0
7. x⋅y = r0
⊢ x⋅y = λi.(x (0 + i))⋅λi.(y (0 + i))
BY
{ ((Assert req-vec(n;λi.(x (0 + i));x) BY
          (D 0 THEN (Reduce 0 THEN Auto) THEN Subst' 0 + i ~ i 0 THEN Auto))
   THEN (Assert req-vec(n;λi.(y (0 + i));y) BY
               (D 0 THEN (Reduce 0 THEN Auto) THEN Subst' 0 + i ~ i 0 THEN Auto))
   ) }

1
1. n : ℕ
2. k : ℕn
3. x : ℝ^n
4. y : ℝ^n
5. λi.(x (0 + i)) ∈ ℝ^n - 0
6. λi.(y (0 + i)) ∈ ℝ^n - 0
7. x⋅y = r0
8. req-vec(n;λi.(x (0 + i));x)
9. req-vec(n;λi.(y (0 + i));y)
⊢ x⋅y = λi.(x (0 + i))⋅λi.(y (0 + i))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}n
3.  x  :  \mBbbR{}\^{}n
4.  y  :  \mBbbR{}\^{}n
5.  \mlambda{}i.(x  (0  +  i))  \mmember{}  \mBbbR{}\^{}n  -  0
6.  \mlambda{}i.(y  (0  +  i))  \mmember{}  \mBbbR{}\^{}n  -  0
7.  x\mcdot{}y  =  r0
\mvdash{}  x\mcdot{}y  =  \mlambda{}i.(x  (0  +  i))\mcdot{}\mlambda{}i.(y  (0  +  i))


By

---

Latex:
((Assert  req-vec(n;\mlambda{}i.(x  (0  +  i));x)  BY
                (D  0  THEN  (Reduce  0  THEN  Auto)  THEN  Subst'  0  +  i  \msim{}  i  0  THEN  Auto))
  THEN  (Assert  req-vec(n;\mlambda{}i.(y  (0  +  i));y)  BY
                          (D  0  THEN  (Reduce  0  THEN  Auto)  THEN  Subst'  0  +  i  \msim{}  i  0  THEN  Auto))
  )

---

Home Index