Step
*
1
1
2
1
of Lemma
dma-lift-compose-assoc
.....wf.....
1. I : Type
2. J : Type
3. K : Type
4. H : Type
5. eqi : EqDecider(I)
6. eqj : EqDecider(J)
7. eqk : EqDecider(K)
8. f : J ⟶ Point(free-DeMorgan-algebra(I;eqi))
9. g : K ⟶ Point(free-DeMorgan-algebra(J;eqj))
10. h : H ⟶ Point(free-DeMorgan-algebra(K;eqk))
11. x : H
12. ∀X:Type. ∀eq:EqDecider(X). (free-dml-deq(X;eq) ∈ EqDecider(Point(free-DeMorgan-algebra(X;eq))))
13. ∀i:J. (<i> ∈ Point(free-DeMorgan-algebra(J;eqj)))
14. ∀[f:K ⟶ Point(free-DeMorgan-algebra(I;eqi))].
∀[g:dma-hom(free-DeMorgan-algebra(K;eqk);free-DeMorgan-algebra(I;eqi))].
∀x:Point(free-DeMorgan-algebra(K;eqk))
((free-dma-lift(K;eqk;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f) x)
= (g x)
∈ Point(free-DeMorgan-algebra(I;eqi)))
supposing ∀i:K. ((g <i>) = (f i) ∈ Point(free-DeMorgan-algebra(I;eqi)))
⊢ free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f)
o free-dma-lift(K;eqk;free-DeMorgan-algebra(J;eqj);free-dml-deq(J;eqj);g)
∈ dma-hom(free-DeMorgan-algebra(K;eqk);free-DeMorgan-algebra(I;eqi))
BY
{ ((Assert ∀k:K. (<k> ∈ Point(free-DeMorgan-algebra(K;eqk))) BY
(RWO "free-dma-point" 0 THEN Auto))
THEN (GenConclTerm ⌜free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f)⌝⋅ THENA Auto)
THEN (GenConclTerm ⌜free-dma-lift(K;eqk;free-DeMorgan-algebra(J;eqj);free-dml-deq(J;eqj);g)⌝⋅ THENA Auto)) }
1
1. I : Type
2. J : Type
3. K : Type
4. H : Type
5. eqi : EqDecider(I)
6. eqj : EqDecider(J)
7. eqk : EqDecider(K)
8. f : J ⟶ Point(free-DeMorgan-algebra(I;eqi))
9. g : K ⟶ Point(free-DeMorgan-algebra(J;eqj))
10. h : H ⟶ Point(free-DeMorgan-algebra(K;eqk))
11. x : H
12. ∀X:Type. ∀eq:EqDecider(X). (free-dml-deq(X;eq) ∈ EqDecider(Point(free-DeMorgan-algebra(X;eq))))
13. ∀i:J. (<i> ∈ Point(free-DeMorgan-algebra(J;eqj)))
14. ∀[f:K ⟶ Point(free-DeMorgan-algebra(I;eqi))].
∀[g:dma-hom(free-DeMorgan-algebra(K;eqk);free-DeMorgan-algebra(I;eqi))].
∀x:Point(free-DeMorgan-algebra(K;eqk))
((free-dma-lift(K;eqk;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f) x)
= (g x)
∈ Point(free-DeMorgan-algebra(I;eqi)))
supposing ∀i:K. ((g <i>) = (f i) ∈ Point(free-DeMorgan-algebra(I;eqi)))
15. ∀k:K. (<k> ∈ Point(free-DeMorgan-algebra(K;eqk)))
16. v : {g:dma-hom(free-DeMorgan-algebra(J;eqj);free-DeMorgan-algebra(I;eqi))|
∀i:J. ((g <i>) = (f i) ∈ Point(free-DeMorgan-algebra(I;eqi)))}
17. free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f)
= v
∈ {g:dma-hom(free-DeMorgan-algebra(J;eqj);free-DeMorgan-algebra(I;eqi))|
∀i:J. ((g <i>) = (f i) ∈ Point(free-DeMorgan-algebra(I;eqi)))}
18. v1 : {g1:dma-hom(free-DeMorgan-algebra(K;eqk);free-DeMorgan-algebra(J;eqj))|
∀i:K. ((g1 <i>) = (g i) ∈ Point(free-DeMorgan-algebra(J;eqj)))}
19. free-dma-lift(K;eqk;free-DeMorgan-algebra(J;eqj);free-dml-deq(J;eqj);g)
= v1
∈ {g1:dma-hom(free-DeMorgan-algebra(K;eqk);free-DeMorgan-algebra(J;eqj))|
∀i:K. ((g1 <i>) = (g i) ∈ Point(free-DeMorgan-algebra(J;eqj)))}
⊢ v o v1 ∈ dma-hom(free-DeMorgan-algebra(K;eqk);free-DeMorgan-algebra(I;eqi))
Latex:
Latex:
.....wf.....
1. I : Type
2. J : Type
3. K : Type
4. H : Type
5. eqi : EqDecider(I)
6. eqj : EqDecider(J)
7. eqk : EqDecider(K)
8. f : J {}\mrightarrow{} Point(free-DeMorgan-algebra(I;eqi))
9. g : K {}\mrightarrow{} Point(free-DeMorgan-algebra(J;eqj))
10. h : H {}\mrightarrow{} Point(free-DeMorgan-algebra(K;eqk))
11. x : H
12. \mforall{}X:Type. \mforall{}eq:EqDecider(X). (free-dml-deq(X;eq) \mmember{} EqDecider(Point(free-DeMorgan-algebra(X;eq))))
13. \mforall{}i:J. (<i> \mmember{} Point(free-DeMorgan-algebra(J;eqj)))
14. \mforall{}[f:K {}\mrightarrow{} Point(free-DeMorgan-algebra(I;eqi))].
\mforall{}[g:dma-hom(free-DeMorgan-algebra(K;eqk);free-DeMorgan-algebra(I;eqi))].
\mforall{}x:Point(free-DeMorgan-algebra(K;eqk))
((free-dma-lift(K;eqk;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f) x) = (g x))
supposing \mforall{}i:K. ((g <i>) = (f i))
\mvdash{} free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f)
o free-dma-lift(K;eqk;free-DeMorgan-algebra(J;eqj);free-dml-deq(J;eqj);g)
\mmember{} dma-hom(free-DeMorgan-algebra(K;eqk);free-DeMorgan-algebra(I;eqi))
By
Latex:
((Assert \mforall{}k:K. (<k> \mmember{} Point(free-DeMorgan-algebra(K;eqk))) BY
(RWO "free-dma-point" 0 THEN Auto))
THEN (GenConclTerm \mkleeneopen{}free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f)\mkleeneclose{}\mcdot{}
THENA Auto
)
THEN (GenConclTerm \mkleeneopen{}free-dma-lift(K;eqk;free-DeMorgan-algebra(J;eqj);free-dml-deq(J;eqj);g)\mkleeneclose{}\mcdot{}
THENA Auto
))
Home
Index