Step * of Lemma ip-triangle_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 THEN Auto) THEN ParallelLast) }

1
1. rv InnerProductSpace
2. Point
3. Point
4. Point
5. a2 Point
6. b2 Point
7. c2 Point
8. a ≡ a2
9. b ≡ b2
10. c ≡ c2
11. |a b ⋅ b| < (||a b|| ||c b||)
⊢ |a2 b2 ⋅ c2 b2| < (||a2 b2|| ||c2 b2||)

2
1. rv InnerProductSpace
2. Point
3. Point
4. 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||)
⊢ |a b ⋅ b| < (||a b|| ||c b||)


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{}  \{\mDelta{}(a;b;c)  \mLeftarrow{}{}\mRightarrow{}  \mDelta{}(a2;b2;c2)\})


By


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




Home Index