---

Step * 1 of Lemma matrix-times-id-left


1. m : ℕ
2. r : Rng
3. y : ℕm
4. k : ℤ
5. 0 < k
6. ∀N:Matrix(k - 1;m;r). ∀x:ℕk - 1.  ((Σ(r) 0 ≤ i < k - 1. if x=i then 1 else 0 * N[i,y]) = N[x,y] ∈ |r|)
7. N : Matrix(k;m;r)
8. x : ℕk
⊢ (Σ(r) 0 ≤ i < k. if x=i then 1 else 0 * N[i,y]) = N[x,y] ∈ |r|
BY
{ ((RWO "rng_sum_unroll_hi" 0 THENA Auto) THEN AutoSplit) }

1
1. m : ℕ
2. r : Rng
3. y : ℕm
4. k : ℤ
5. 0 < k
6. ∀N:Matrix(k - 1;m;r). ∀x:ℕk - 1.  ((Σ(r) 0 ≤ i < k - 1. if x=i then 1 else 0 * N[i,y]) = N[x,y] ∈ |r|)
7. N : Matrix(k;m;r)
8. x : ℕk
9. x = (k - 1) ∈ ℤ
⊢ ((Σ(r) 0 ≤ i < k - 1. if x=i then 1 else 0 * N[i,y]) +r (1 * N[k - 1,y])) = N[x,y] ∈ |r|

2
1. m : ℕ
2. r : Rng
3. y : ℕm
4. k : ℤ
5. 0 < k
6. ∀N:Matrix(k - 1;m;r). ∀x:ℕk - 1.  ((Σ(r) 0 ≤ i < k - 1. if x=i then 1 else 0 * N[i,y]) = N[x,y] ∈ |r|)
7. N : Matrix(k;m;r)
8. x : ℕk
9. x ≠ k - 1
⊢ ((Σ(r) 0 ≤ i < k - 1. if x=i then 1 else 0 * N[i,y]) +r (0 * N[k - 1,y])) = N[x,y] ∈ |r|

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}
2.  r  :  Rng
3.  y  :  \mBbbN{}m
4.  k  :  \mBbbZ{}
5.  0  <  k
6.  \mforall{}N:Matrix(k  -  1;m;r).  \mforall{}x:\mBbbN{}k  -  1.    ((\mSigma{}(r)  0  \mleq{}  i  <  k  -  1.  if  x=i  then  1  else  0  *  N[i,y])  =  N[x,y])
7.  N  :  Matrix(k;m;r)
8.  x  :  \mBbbN{}k
\mvdash{}  (\mSigma{}(r)  0  \mleq{}  i  <  k.  if  x=i  then  1  else  0  *  N[i,y])  =  N[x,y]


By

---

Latex:
((RWO  "rng\_sum\_unroll\_hi"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index