---

Step * 1 of Lemma ip-congruent-same


1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. r0 = ||b - c||
6. a - a ≡ 0
⊢ b ≡ c
BY
{ ((InstLemma `rv-norm-is-zero` [⌜rv⌝;⌜b - c⌝]⋅ THEN Auto) THEN D -2 THEN EAuto 1) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  r0  =  ||b  -  c||
6.  a  -  a  \mequiv{}  0
\mvdash{}  b  \mequiv{}  c


By

---

Latex:
((InstLemma  `rv-norm-is-zero`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}b  -  c\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  D  -2  THEN  EAuto  1)

---

Home Index