---

Step * 2 of Lemma matrix-times-id-right


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|
BY
{ ((RWO "-4" 0 THENA (Auto THEN All (Unfold `matrix`) THEN Auto)) THEN RW (RngNormC) 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "-4"  0  THENA  (Auto  THEN  All  (Unfold  `matrix`)  THEN  Auto))  THEN  RW  (RngNormC)  0  THEN  Auto)

---

Home Index