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 THEN Auto) THEN ParallelLast) }

1
1. rv InnerProductSpace
2. Point
3. Point
4. Point
5. 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. Point
3. Point
4. Point
5. 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