---

Step * of Lemma matrix-times-id-right

∀[k,m:ℕ]. ∀[r:Rng]. ∀[N:Matrix(k;m;r)].  ((N*I) = N ∈ Matrix(k;m;r))
BY
{ (Auto
   THEN RepUR ``matrix`` 0
   THEN RepeatFor 2 ((FunExt THENA Auto))
   THEN RenameVar `y' (-1)
   THEN RepUR ``matrix-times mx matrix-ap identity-matrix`` 0
   THEN Fold `matrix-ap` 0
   THEN NatInd 2
   THEN Auto
   THEN (RWO "rng_sum_unroll_hi" 0 THENA Auto)
   THEN AutoSplit) }

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

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

---

Latex:

---

Latex:
\mforall{}[k,m:\mBbbN{}].  \mforall{}[r:Rng].  \mforall{}[N:Matrix(k;m;r)].    ((N*I)  =  N)


By

---

Latex:
(Auto
  THEN  RepUR  ``matrix``  0
  THEN  RepeatFor  2  ((FunExt  THENA  Auto))
  THEN  RenameVar  `y'  (-1)
  THEN  RepUR  ``matrix-times  mx  matrix-ap  identity-matrix``  0
  THEN  Fold  `matrix-ap`  0
  THEN  NatInd  2
  THEN  Auto
  THEN  (RWO  "rng\_sum\_unroll\_hi"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index