Step
*
of Lemma
ip-congruent_functionality
∀[rv:InnerProductSpace]. ∀[a,b,c,d,a2,b2,c2,d2:Point].
  ({ab=cd 
⇐⇒ a2b2=c2d2}) supposing (d ≡ d2 and c ≡ c2 and b ≡ b2 and a ≡ a2)
BY
{ (Auto THEN (D 0 THEN Auto) THEN ParallelLast) }
1
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a2 : Point
7. b2 : Point
8. c2 : Point
9. d2 : Point
10. a ≡ a2
11. b ≡ b2
12. c ≡ c2
13. d ≡ d2
14. ||a - b|| = ||c - d||
⊢ ||a2 - b2|| = ||c2 - d2||
2
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a2 : Point
7. b2 : Point
8. c2 : Point
9. d2 : Point
10. a ≡ a2
11. b ≡ b2
12. c ≡ c2
13. d ≡ d2
14. ||a2 - b2|| = ||c2 - d2||
⊢ ||a - b|| = ||c - d||
Latex:
Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[a,b,c,d,a2,b2,c2,d2:Point].
    (\{ab=cd  \mLeftarrow{}{}\mRightarrow{}  a2b2=c2d2\})  supposing  (d  \mequiv{}  d2  and  c  \mequiv{}  c2  and  b  \mequiv{}  b2  and  a  \mequiv{}  a2)
By
Latex:
(Auto  THEN  (D  0  THEN  Auto)  THEN  ParallelLast)
Home
Index