---

Step * 1 of Lemma nc-s-i1-j1


1. I : fset(ℕ)
2. i : ℕ
3. j : ℕ
4. ¬j ∈ I
5. (i1) ∈ I+j ⟶ I+i+j
⊢ (i1) = s ⋅ (i1) ⋅ (j1) ∈ I ⟶ I+i
BY
{ ((InstLemma `nh-comp-assoc` [⌜I⌝;⌜I+j⌝;⌜I+i+j⌝;⌜I+i⌝]⋅ THENA Auto) THEN (RWW  "-1 nc-1-s-commute<" 0⋅ THENA Auto)) }

1
1. I : fset(ℕ)
2. i : ℕ
3. j : ℕ
4. ¬j ∈ I
5. (i1) ∈ I+j ⟶ I+i+j
6. ∀f:I ⟶ I+j. ∀g:I+j ⟶ I+i+j. ∀h:I+i+j ⟶ I+i.  (h ⋅ g ⋅ f = h ⋅ g ⋅ f ∈ I ⟶ I+i)
⊢ (i1) = (i1) ⋅ s ⋅ (j1) ∈ I ⟶ I+i

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \mBbbN{}
3.  j  :  \mBbbN{}
4.  \mneg{}j  \mmember{}  I
5.  (i1)  \mmember{}  I+j  {}\mrightarrow{}  I+i+j
\mvdash{}  (i1)  =  s  \mcdot{}  (i1)  \mcdot{}  (j1)


By

---

Latex:
((InstLemma  `nh-comp-assoc`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}I+j\mkleeneclose{};\mkleeneopen{}I+i+j\mkleeneclose{};\mkleeneopen{}I+i\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWW    "-1  nc-1-s-commute<"  0\mcdot{}  THENA  Auto)
  )

---

Home Index