---

Step * of Lemma nh-comp-cancel

∀I,J,K:fset(ℕ). ∀f:I ⟶ J. ∀g,h:J ⟶ K. ∀x:names(K).
  (g ⋅ f x) = (h ⋅ f x) ∈ Point(dM(I)) supposing (g x) = (h x) ∈ Point(dM(J))
BY
{ (Auto
   THEN RepUR ``nh-comp dma-lift-compose`` 0
   THEN (GenConclTerm 
         ⌜free-dma-lift(names(J);NamesDeq;free-DeMorgan-algebra(names(I);NamesDeq);free-dml-deq(names(I);NamesDeq);f)⌝⋅
         THENA Auto
         )) }

1
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))

---

Latex:

---

Latex:
\mforall{}I,J,K:fset(\mBbbN{}).  \mforall{}f:I  {}\mrightarrow{}  J.  \mforall{}g,h:J  {}\mrightarrow{}  K.  \mforall{}x:names(K).    (g  \mcdot{}  f  x)  =  (h  \mcdot{}  f  x)  supposing  (g  x)  =  (h  x)


By

---

Latex:
(Auto
  THEN  RepUR  ``nh-comp  dma-lift-compose``  0
  THEN  (GenConclTerm 
              \mkleeneopen{}free-dma-lift(names(J);NamesDeq;free-DeMorgan-algebra(names(I);NamesDeq);...;f)\mkleeneclose{}\mcdot{}
              THENA  Auto
              ))

---

Home Index