Step
*
1
1
2
of Lemma
dma-lift-compose-assoc
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))))
⊢ (free-dma-lift(K;eqk;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);free-dma-lift(J;eqj;...;free-dml-deq(I;eqi);f)
o g)
(h x))
= ((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))
(h x))
∈ Point(free-DeMorgan-algebra(I;eqi))
BY
{ ((Assert ∀i:J. (<i> ∈ Point(free-DeMorgan-algebra(J;eqj))) BY
(RWO "free-dma-point" 0 THEN Auto))
THEN (InstLemma `free-dma-lift-unique2` [⌜K⌝;⌜eqk⌝;⌜free-DeMorgan-algebra(I;eqi)⌝;⌜free-dml-deq(I;eqi)⌝]⋅ THENA Auto)
THEN BHyp -1
THEN Auto) }
1
.....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))
2
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. i : K
⊢ ((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))
<i>)
= ((free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f) o g) i)
∈ Point(free-DeMorgan-algebra(I;eqi))
Latex:
Latex:
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))))
\mvdash{} (free-dma-lift(K;eqk;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);... o g)
(h x))
= ((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))
(h x))
By
Latex:
((Assert \mforall{}i:J. (<i> \mmember{} Point(free-DeMorgan-algebra(J;eqj))) BY
(RWO "free-dma-point" 0 THEN Auto))
THEN (InstLemma `free-dma-lift-unique2` [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}eqk\mkleeneclose{};\mkleeneopen{}free-DeMorgan-algebra(I;eqi)\mkleeneclose{};
\mkleeneopen{}free-dml-deq(I;eqi)\mkleeneclose{}]\mcdot{}
THENA Auto
)
THEN BHyp -1
THEN Auto)
Home
Index