Step
*
2
of Lemma
geo-extend-equal-iff-congruent
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c' : Point
7. d' : Point
8. a # b
9. v : Point
10. bv ≅ cd
11. B(abv)
12. v1 : Point
13. bv1 ≅ c'd'
14. B(abv1)
15. cd ≅ c'd'
⊢ v ≡ v1
BY
{ Assert ⌜bv ≅ bv1⌝ ⋅ }
1
.....assertion.....
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c' : Point
7. d' : Point
8. a # b
9. v : Point
10. bv ≅ cd
11. B(abv)
12. v1 : Point
13. bv1 ≅ c'd'
14. B(abv1)
15. cd ≅ c'd'
⊢ bv ≅ bv1
2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c' : Point
7. d' : Point
8. a # b
9. v : Point
10. bv ≅ cd
11. B(abv)
12. v1 : Point
13. bv1 ≅ c'd'
14. B(abv1)
15. cd ≅ c'd'
16. bv ≅ bv1
⊢ v ≡ v1
Latex:
Latex:
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c' : Point
7. d' : Point
8. a \# b
9. v : Point
10. bv \mcong{} cd
11. B(abv)
12. v1 : Point
13. bv1 \mcong{} c'd'
14. B(abv1)
15. cd \mcong{} c'd'
\mvdash{} v \mequiv{} v1
By
Latex:
Assert \mkleeneopen{}bv \mcong{} bv1\mkleeneclose{} \mcdot{}
Home
Index