let p1, p2 be Point of (TOP-REAL 2); :: thesis: for P being Subset of (TOP-REAL 2)
for A being Real st p1,p2 realize-max-dist-in P holds
(Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P
let P be Subset of (TOP-REAL 2); :: thesis: for A being Real st p1,p2 realize-max-dist-in P holds
(Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P
let A be Real; :: thesis: ( p1,p2 realize-max-dist-in P implies (Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P )
reconsider f = Rotate A as Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) by Lm1;
set C = P;
A1: dom (Rotate A) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
assume A2: p1,p2 realize-max-dist-in P ; :: thesis: (Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P
then ( p1 in P & p2 in P ) by Def1;
hence ( (Rotate A) . p1 in (Rotate A) .: P & (Rotate A) . p2 in (Rotate A) .: P ) by A1, FUNCT_1:def 12; :: according to JORDAN24:def 1 :: thesis: for x, y being Point of (TOP-REAL 2) st x in (Rotate A) .: P & y in (Rotate A) .: P holds
dist ((Rotate A) . p1),((Rotate A) . p2) >= dist x,y
let x, y be Point of (TOP-REAL 2); :: thesis: ( x in (Rotate A) .: P & y in (Rotate A) .: P implies dist ((Rotate A) . p1),((Rotate A) . p2) >= dist x,y )
assume that
A3: x in (Rotate A) .: P and
A4: y in (Rotate A) .: P ; :: thesis: dist ((Rotate A) . p1),((Rotate A) . p2) >= dist x,y
f is isometric by Th2;
then consider g being isometric Function of (Euclid 2),(Euclid 2) such that
A5: f = g by Def2;
consider yy being set such that
A6: yy in dom (Rotate A) and
A7: yy in P and
A8: (Rotate A) . yy = y by A4, FUNCT_1:def 12;
reconsider yy = yy as Point of (TOP-REAL 2) by A6;
consider xx being set such that
A9: xx in dom (Rotate A) and
A10: xx in P and
A11: (Rotate A) . xx = x by A3, FUNCT_1:def 12;
reconsider xx = xx as Point of (TOP-REAL 2) by A9;
reconsider p19 = p1, p29 = p2, xx9 = xx, yy9 = yy as Point of (Euclid 2) by EUCLID:71;
dist p1,p2 >= dist xx,yy by A2, A10, A7, Def1;
then dist p19,p29 >= dist xx,yy by TOPREAL6:def 1;
then dist p19,p29 >= dist xx9,yy9 by TOPREAL6:def 1;
then dist (g . p19),(g . p29) >= dist xx9,yy9 by VECTMETR:def 3;
then dist (g . p19),(g . p29) >= dist (g . xx9),(g . yy9) by VECTMETR:def 3;
then dist ((Rotate A) . p1),((Rotate A) . p2) >= dist (g . xx9),(g . yy9) by A5, TOPREAL6:def 1;
hence dist ((Rotate A) . p1),((Rotate A) . p2) >= dist x,y by A11, A8, A5, TOPREAL6:def 1; :: thesis: verum