---

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


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
BY
{ ((InstLemma `nh-comp-assoc` [⌜I⌝;⌜I+j⌝;⌜I⌝;⌜I+i⌝]⋅ THENA Auto) THEN (RWO "-1<" 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)
7. ∀f:I ⟶ I+j. ∀g:I+j ⟶ I. ∀h:I ⟶ 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
6.  \mforall{}f:I  {}\mrightarrow{}  I+j.  \mforall{}g:I+j  {}\mrightarrow{}  I+i+j.  \mforall{}h:I+i+j  {}\mrightarrow{}  I+i.    (h  \mcdot{}  g  \mcdot{}  f  =  h  \mcdot{}  g  \mcdot{}  f)
\mvdash{}  (i1)  =  (i1)  \mcdot{}  s  \mcdot{}  (j1)


By

---

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

---

Home Index