---

Step * 2 of Lemma int-dot-add-right


1. u : ℤ
2. v : ℤ List
3. ∀[as,bs:ℤ List].  v ⋅ as + bs ~ v ⋅ as + v ⋅ bs supposing ||as|| = ||bs|| ∈ ℤ
⊢ ∀[as,bs:ℤ List].  [u / v] ⋅ as + bs ~ [u / v] ⋅ as + [u / v] ⋅ bs supposing ||as|| = ||bs|| ∈ ℤ
BY
{ (RepeatFor 2 (InductionOnList)
   THEN (UnivCD THENA Auto)
   THEN RecUnfold `int-vec-add` 0⋅
   THEN Reduce 0
   THEN Reduce (-1)
   THEN Auto') }

1
1. u : ℤ
2. v : ℤ List
3. ∀[as,bs:ℤ List].  v ⋅ as + bs ~ v ⋅ as + v ⋅ bs supposing ||as|| = ||bs|| ∈ ℤ
4. u1 : ℤ
5. v1 : ℤ List
6. ∀[bs:ℤ List]. [u / v] ⋅ v1 + bs ~ [u / v] ⋅ v1 + [u / v] ⋅ bs supposing ||v1|| = ||bs|| ∈ ℤ
7. u2 : ℤ
8. v2 : ℤ List
9. [u / v] ⋅ [u1 / v1] + v2 ~ [u / v] ⋅ [u1 / v1] + [u / v] ⋅ v2 supposing ||[u1 / v1]|| = ||v2|| ∈ ℤ
10. (||v1|| + 1) = (||v2|| + 1) ∈ ℤ
⊢ ((u * (u1 + u2)) + v ⋅ v1 + v2) = (((u * u1) + v ⋅ v1) + (u * u2) + v ⋅ v2) ∈ ℤ

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}[as,bs:\mBbbZ{}  List].    v  \mcdot{}  as  +  bs  \msim{}  v  \mcdot{}  as  +  v  \mcdot{}  bs  supposing  ||as||  =  ||bs||
\mvdash{}  \mforall{}[as,bs:\mBbbZ{}  List].    [u  /  v]  \mcdot{}  as  +  bs  \msim{}  [u  /  v]  \mcdot{}  as  +  [u  /  v]  \mcdot{}  bs  supposing  ||as||  =  ||bs||


By

---

Latex:
(RepeatFor  2  (InductionOnList)
  THEN  (UnivCD  THENA  Auto)
  THEN  RecUnfold  `int-vec-add`  0\mcdot{}
  THEN  Reduce  0
  THEN  Reduce  (-1)
  THEN  Auto')

---

Home Index