---

Step * 1 of Lemma nc-m-nc-1


1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. j : {j:ℕ| ¬j ∈ I+i} 
4. (m(i;j) ⋅ (j1) i) = (j1) i ∧ (j1) j ∈ Point(dM(I+i))
⊢ (m(i;j) ⋅ (j1) i) = (1 i) ∈ Point(dM(I+i))
BY
{ (NthHypEq (-1)
   THEN EqCDA
   THEN ((RepUR ``nh-id nc-1`` 0 THEN Subst' {{}} ~ 1 0) THENA Auto)
   THEN (OReduce 0 THENA Auto)) }

1
1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. j : {j:ℕ| ¬j ∈ I+i} 
4. (m(i;j) ⋅ (j1) i) = (j1) i ∧ (j1) j ∈ Point(dM(I+i))
⊢ <i> = if (i =z j) then 1 else <i> fi  ∧ 1 ∈ Point(dM(I+i))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
3.  j  :  \{j:\mBbbN{}|  \mneg{}j  \mmember{}  I+i\} 
4.  (m(i;j)  \mcdot{}  (j1)  i)  =  (j1)  i  \mwedge{}  (j1)  j
\mvdash{}  (m(i;j)  \mcdot{}  (j1)  i)  =  (1  i)


By

---

Latex:
(NthHypEq  (-1)
  THEN  EqCDA
  THEN  ((RepUR  ``nh-id  nc-1``  0  THEN  Subst'  \{\{\}\}  \msim{}  1  0)  THENA  Auto)
  THEN  (OReduce  0  THENA  Auto))

---

Home Index