---

Step * of Lemma ip-between_functionality

∀[rv:InnerProductSpace]. ∀[a,b,c,a2,b2,c2:Point].  (a ≡ a2 ⇒ b ≡ b2 ⇒ c ≡ c2 ⇒ {a_b_c ⇐⇒ a2_b2_c2})
BY
{ (Auto THEN (D 0 THEN Auto) THEN ParallelLast) }

1
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. a2 : Point
6. b2 : Point
7. c2 : Point
8. a ≡ a2
9. b ≡ b2
10. c ≡ c2
11. ((||a - b|| * ||c - b||) + a - b ⋅ c - b) = r0
⊢ ((||a2 - b2|| * ||c2 - b2||) + a2 - b2 ⋅ c2 - b2) = r0

2
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. a2 : Point
6. b2 : Point
7. c2 : Point
8. a ≡ a2
9. b ≡ b2
10. c ≡ c2
11. ((||a2 - b2|| * ||c2 - b2||) + a2 - b2 ⋅ c2 - b2) = r0
⊢ ((||a - b|| * ||c - b||) + a - b ⋅ c - b) = r0

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[a,b,c,a2,b2,c2:Point].
    (a  \mequiv{}  a2  {}\mRightarrow{}  b  \mequiv{}  b2  {}\mRightarrow{}  c  \mequiv{}  c2  {}\mRightarrow{}  \{a\_b\_c  \mLeftarrow{}{}\mRightarrow{}  a2\_b2\_c2\})


By

---

Latex:
(Auto  THEN  (D  0  THEN  Auto)  THEN  ParallelLast)

---

Home Index