---

Step * of Lemma matrix-times-id-left

∀[k,m:ℕ]. ∀[r:Rng]. ∀[N:Matrix(k;m;r)].  ((I*N) = 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 1
   THEN Auto) }

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
⊢ (Σ(r) 0 ≤ i < k. if x=i then 1 else 0 * N[i,y]) = N[x,y] ∈ |r|

---

Latex:

---

Latex:
\mforall{}[k,m:\mBbbN{}].  \mforall{}[r:Rng].  \mforall{}[N:Matrix(k;m;r)].    ((I*N)  =  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  1
  THEN  Auto)

---

Home Index