---

Step * 1 of Lemma fl_all-fl1


1. I : fset(ℕ)
2. i : ℕ
3. x : names(I+i)
4. fl-all-hom(I;i) = fl-all-hom(I;i) ∈ Hom(face_lattice(I+i);face_lattice(I))
5. (∀j:names(I)
      ((¬(j = i ∈ ℤ))
      ⇒ (((fl-all-hom(I;i) (j=0)) = (j=0) ∈ Point(face_lattice(I)))
         ∧ ((fl-all-hom(I;i) (j=1)) = (j=1) ∈ Point(face_lattice(I))))))
∧ ((fl-all-hom(I;i) (i=0)) = 0 ∈ Point(face_lattice(I)))
∧ ((fl-all-hom(I;i) (i=1)) = 0 ∈ Point(face_lattice(I)))
⊢ (fl-all-hom(I;i) (x=1)) = if (x =z i) then 0 else (x=1) fi  ∈ Point(face_lattice(I))
BY
{ (BoolCase ⌜(x =z i)⌝⋅ THENA Auto) }

1
1. I : fset(ℕ)
2. i : ℕ
3. x : names(I+i)
4. fl-all-hom(I;i) = fl-all-hom(I;i) ∈ Hom(face_lattice(I+i);face_lattice(I))
5. (∀j:names(I)
      ((¬(j = i ∈ ℤ))
      ⇒ (((fl-all-hom(I;i) (j=0)) = (j=0) ∈ Point(face_lattice(I)))
         ∧ ((fl-all-hom(I;i) (j=1)) = (j=1) ∈ Point(face_lattice(I))))))
∧ ((fl-all-hom(I;i) (i=0)) = 0 ∈ Point(face_lattice(I)))
∧ ((fl-all-hom(I;i) (i=1)) = 0 ∈ Point(face_lattice(I)))
6. x = i ∈ ℤ
⊢ (fl-all-hom(I;i) (x=1)) = 0 ∈ Point(face_lattice(I))

2
1. I : fset(ℕ)
2. i : ℕ
3. x : names(I+i)
4. x ≠ i
5. fl-all-hom(I;i) = fl-all-hom(I;i) ∈ Hom(face_lattice(I+i);face_lattice(I))
6. (∀j:names(I)
      ((¬(j = i ∈ ℤ))
      ⇒ (((fl-all-hom(I;i) (j=0)) = (j=0) ∈ Point(face_lattice(I)))
         ∧ ((fl-all-hom(I;i) (j=1)) = (j=1) ∈ Point(face_lattice(I))))))
∧ ((fl-all-hom(I;i) (i=0)) = 0 ∈ Point(face_lattice(I)))
∧ ((fl-all-hom(I;i) (i=1)) = 0 ∈ Point(face_lattice(I)))
⊢ (fl-all-hom(I;i) (x=1)) = (x=1) ∈ Point(face_lattice(I))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \mBbbN{}
3.  x  :  names(I+i)
4.  fl-all-hom(I;i)  =  fl-all-hom(I;i)
5.  (\mforall{}j:names(I)
            ((\mneg{}(j  =  i))  {}\mRightarrow{}  (((fl-all-hom(I;i)  (j=0))  =  (j=0))  \mwedge{}  ((fl-all-hom(I;i)  (j=1))  =  (j=1)))))
\mwedge{}  ((fl-all-hom(I;i)  (i=0))  =  0)
\mwedge{}  ((fl-all-hom(I;i)  (i=1))  =  0)
\mvdash{}  (fl-all-hom(I;i)  (x=1))  =  if  (x  =\msubz{}  i)  then  0  else  (x=1)  fi 


By

---

Latex:
(BoolCase  \mkleeneopen{}(x  =\msubz{}  i)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index