---

Step * of Lemma dot-product-split-first

∀[n:ℕ+]. ∀[x,y:ℝ^n].  (x⋅y = (((x 0) * (y 0)) + λi.(x (i + 1))⋅λi.(y (i + 1))))
BY
{ (Intros THEN Unhide) }

1
.....wf..... 
1. n : ℕ+
2. x : ℝ^n
3. y : ℝ^n
⊢ x⋅y ∈ ℝ

2
.....wf..... 
1. n : ℕ+
2. x : ℝ^n
3. y : ℝ^n
⊢ ((x 0) * (y 0)) + λi.(x (i + 1))⋅λi.(y (i + 1)) ∈ ℝ

3
1. n : ℕ+
2. x : ℝ^n
3. y : ℝ^n
⊢ x⋅y = (((x 0) * (y 0)) + λi.(x (i + 1))⋅λi.(y (i + 1)))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    (x\mcdot{}y  =  (((x  0)  *  (y  0))  +  \mlambda{}i.(x  (i  +  1))\mcdot{}\mlambda{}i.(y  (i  +  1))))


By

---

Latex:
(Intros  THEN  Unhide)

---

Home Index