---

Step * 1 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] * 1)) = N[x,y] ∈ |r|
BY
{ (Subst' (Σ(r) 0 ≤ i < m - 1. N[x,i] * if i=y then 1 else 0) = (Σ(r) 0 ≤ i < m - 1. 0) ∈ |r| 0 THENA Auto) }

1
.....equality..... 
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) 0 ≤ i < m - 1. 0) ∈ |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. 0) +r (N[x,m - 1] * 1)) = N[x,y] ∈ |r|

---

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)  =  y
\mvdash{}  ((\mSigma{}(r)  0  \mleq{}  i  <  m  -  1.  N[x,i]  *  if  i=y  then  1  else  0)  +r  (N[x,m  -  1]  *  1))  =  N[x,y]


By

---

Latex:
(Subst'  (\mSigma{}(r)  0  \mleq{}  i  <  m  -  1.  N[x,i]  *  if  i=y  then  1  else  0)  =  (\mSigma{}(r)  0  \mleq{}  i  <  m  -  1.  0)  0  THENA  Auto)

---

Home Index