Step
*
1
2
1
1
1
7
of Lemma
quotient-dl_wf
1. l : BoundedDistributiveLattice
2. eq : Point(l) ⟶ Point(l) ⟶ ℙ
3. EquivRel(Point(l);x,y.eq[x;y])
4. ∀a,c,b,d:Point(l). (eq[a;c] ⇒ eq[b;d] ⇒ eq[a ∧ b;c ∧ d])
5. ∀a,c,b,d:Point(l). (eq[a;c] ⇒ eq[b;d] ⇒ eq[a ∨ b;c ∨ d])
6. l."meet" ∈ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y])
7. l."join" ∈ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y])
8. ∀[a,b:Point(l)]. (a ∧ b = b ∧ a ∈ Point(l))
9. ∀[a,b:Point(l)]. (a ∨ b = b ∨ a ∈ Point(l))
10. ∀[a,b,c:Point(l)]. (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l))
11. ∀[a,b,c:Point(l)]. (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l))
12. ∀[a,b:Point(l)]. (a ∨ a ∧ b = a ∈ Point(l))
13. ∀[a,b:Point(l)]. (a ∧ a ∨ b = a ∈ Point(l))
14. ∀[a:Point(l)]. (a ∨ 0 = a ∈ Point(l))
15. ∀[a:Point(l)]. (a ∧ 1 = a ∈ Point(l))
16. ∀[a,b,c:Point(l)]. (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(l))
17. ∀[a,b:x,y:Point(l)//(eq x y)]. (a ∧ b ∈ x,y:Point(l)//(eq x y))
18. ∀[a,b:x,y:Point(l)//(eq x y)]. (a ∨ b ∈ x,y:Point(l)//(eq x y))
19. a : x,y:Point(l)//(eq x y)
⊢ a ∧ 1 = a ∈ (x,y:Point(l)//(eq x y))
BY
{ OnVar `a' QuotientElimForEquality }
1
1. l : BoundedDistributiveLattice
2. eq : Point(l) ⟶ Point(l) ⟶ ℙ
3. EquivRel(Point(l);x,y.eq[x;y])
4. ∀a,c,b,d:Point(l). (eq[a;c] ⇒ eq[b;d] ⇒ eq[a ∧ b;c ∧ d])
5. ∀a,c,b,d:Point(l). (eq[a;c] ⇒ eq[b;d] ⇒ eq[a ∨ b;c ∨ d])
6. l."meet" ∈ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y])
7. l."join" ∈ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y])
8. ∀[a,b:Point(l)]. (a ∧ b = b ∧ a ∈ Point(l))
9. ∀[a,b:Point(l)]. (a ∨ b = b ∨ a ∈ Point(l))
10. ∀[a,b,c:Point(l)]. (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l))
11. ∀[a,b,c:Point(l)]. (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l))
12. ∀[a,b:Point(l)]. (a ∨ a ∧ b = a ∈ Point(l))
13. ∀[a,b:Point(l)]. (a ∧ a ∨ b = a ∈ Point(l))
14. ∀[a:Point(l)]. (a ∨ 0 = a ∈ Point(l))
15. ∀[a:Point(l)]. (a ∧ 1 = a ∈ Point(l))
16. ∀[a,b,c:Point(l)]. (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(l))
17. ∀[a,b:x,y:Point(l)//(eq x y)]. (a ∧ b ∈ x,y:Point(l)//(eq x y))
18. ∀[a,b:x,y:Point(l)//(eq x y)]. (a ∨ b ∈ x,y:Point(l)//(eq x y))
19. a : Base
20. a1 : Base
21. a = a1 ∈ pertype(λx,y. ((x ∈ Point(l)) ∧ (y ∈ Point(l)) ∧ (eq x y)))
22. a ∈ Point(l)
23. a1 ∈ Point(l)
24. eq a a1
⊢ a ∧ 1 = a1 ∈ (x,y:Point(l)//(eq x y))
Latex:
Latex:
1. l : BoundedDistributiveLattice
2. eq : Point(l) {}\mrightarrow{} Point(l) {}\mrightarrow{} \mBbbP{}
3. EquivRel(Point(l);x,y.eq[x;y])
4. \mforall{}a,c,b,d:Point(l). (eq[a;c] {}\mRightarrow{} eq[b;d] {}\mRightarrow{} eq[a \mwedge{} b;c \mwedge{} d])
5. \mforall{}a,c,b,d:Point(l). (eq[a;c] {}\mRightarrow{} eq[b;d] {}\mRightarrow{} eq[a \mvee{} b;c \mvee{} d])
6. l."meet" \mmember{} (x,y:Point(l)//eq[x;y]) {}\mrightarrow{} (x,y:Point(l)//eq[x;y]) {}\mrightarrow{} (x,y:Point(l)//eq[x;y])
7. l."join" \mmember{} (x,y:Point(l)//eq[x;y]) {}\mrightarrow{} (x,y:Point(l)//eq[x;y]) {}\mrightarrow{} (x,y:Point(l)//eq[x;y])
8. \mforall{}[a,b:Point(l)]. (a \mwedge{} b = b \mwedge{} a)
9. \mforall{}[a,b:Point(l)]. (a \mvee{} b = b \mvee{} a)
10. \mforall{}[a,b,c:Point(l)]. (a \mwedge{} b \mwedge{} c = a \mwedge{} b \mwedge{} c)
11. \mforall{}[a,b,c:Point(l)]. (a \mvee{} b \mvee{} c = a \mvee{} b \mvee{} c)
12. \mforall{}[a,b:Point(l)]. (a \mvee{} a \mwedge{} b = a)
13. \mforall{}[a,b:Point(l)]. (a \mwedge{} a \mvee{} b = a)
14. \mforall{}[a:Point(l)]. (a \mvee{} 0 = a)
15. \mforall{}[a:Point(l)]. (a \mwedge{} 1 = a)
16. \mforall{}[a,b,c:Point(l)]. (a \mwedge{} b \mvee{} c = a \mwedge{} b \mvee{} a \mwedge{} c)
17. \mforall{}[a,b:x,y:Point(l)//(eq x y)]. (a \mwedge{} b \mmember{} x,y:Point(l)//(eq x y))
18. \mforall{}[a,b:x,y:Point(l)//(eq x y)]. (a \mvee{} b \mmember{} x,y:Point(l)//(eq x y))
19. a : x,y:Point(l)//(eq x y)
\mvdash{} a \mwedge{} 1 = a
By
Latex:
OnVar `a' QuotientElimForEquality
Home
Index