---

Step * 1 of Lemma nh-comp-cancel


1. I : fset(ℕ)
2. J : fset(ℕ)
3. K : fset(ℕ)
4. f : I ⟶ J
5. g : J ⟶ K
6. h : J ⟶ K
7. x : names(K)
8. (g x) = (h x) ∈ Point(dM(J))
9. v : {g:dma-hom(free-DeMorgan-algebra(names(J);NamesDeq);free-DeMorgan-algebra(names(I);NamesDeq))| 
        ∀i:names(J). ((g <i>) = (f i) ∈ Point(free-DeMorgan-algebra(names(I);NamesDeq)))} 
10. free-dma-lift(names(J);NamesDeq;free-DeMorgan-algebra(names(I);NamesDeq);free-dml-deq(names(I);NamesDeq);f)
= v
∈ {g:dma-hom(free-DeMorgan-algebra(names(J);NamesDeq);free-DeMorgan-algebra(names(I);NamesDeq))| 
   ∀i:names(J). ((g <i>) = (f i) ∈ Point(free-DeMorgan-algebra(names(I);NamesDeq)))} 
⊢ (v (g x)) = (v (h x)) ∈ Point(dM(I))
BY
{ (EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  J  :  fset(\mBbbN{})
3.  K  :  fset(\mBbbN{})
4.  f  :  I  {}\mrightarrow{}  J
5.  g  :  J  {}\mrightarrow{}  K
6.  h  :  J  {}\mrightarrow{}  K
7.  x  :  names(K)
8.  (g  x)  =  (h  x)
9.  v  :  \{g:dma-hom(free-DeMorgan-algebra(names(J);NamesDeq);free-DeMorgan-algebra(names(I);...))| 
                \mforall{}i:names(J).  ((g  <i>)  =  (f  i))\} 
10.  free-dma-lift(names(J);NamesDeq;free-DeMorgan-algebra(names(I);NamesDeq);...;f)
=  v
\mvdash{}  (v  (g  x))  =  (v  (h  x))


By

---

Latex:
(EqCD  THEN  Auto)

---

Home Index