let p1, p2 be Point of (TOP-REAL 2); :: thesis: for P being Subset of (TOP-REAL 2)
for A, B, D being real number st p1,p2 realize-max-dist-in P holds
(AffineMap A,B,A,D) . p1,(AffineMap A,B,A,D) . p2 realize-max-dist-in (AffineMap A,B,A,D) .: P
let P be Subset of (TOP-REAL 2); :: thesis: for A, B, D being real number st p1,p2 realize-max-dist-in P holds
(AffineMap A,B,A,D) . p1,(AffineMap A,B,A,D) . p2 realize-max-dist-in (AffineMap A,B,A,D) .: P
let A, B, D be real number ; :: thesis: ( p1,p2 realize-max-dist-in P implies (AffineMap A,B,A,D) . p1,(AffineMap A,B,A,D) . p2 realize-max-dist-in (AffineMap A,B,A,D) .: P )
set a = p1;
set b = p2;
set C = P;
A1: dom (AffineMap A,B,A,D) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
assume A2: p1,p2 realize-max-dist-in P ; :: thesis: (AffineMap A,B,A,D) . p1,(AffineMap A,B,A,D) . p2 realize-max-dist-in (AffineMap A,B,A,D) .: P
then p1 in P by Def1;
hence (AffineMap A,B,A,D) . p1 in (AffineMap A,B,A,D) .: P by A1, FUNCT_1:def 12; :: according to JORDAN24:def 1 :: thesis: ( (AffineMap A,B,A,D) . p2 in (AffineMap A,B,A,D) .: P & ( for x, y being Point of (TOP-REAL 2) st x in (AffineMap A,B,A,D) .: P & y in (AffineMap A,B,A,D) .: P holds
dist ((AffineMap A,B,A,D) . p1),((AffineMap A,B,A,D) . p2) >= dist x,y ) )
p2 in P by A2, Def1;
hence (AffineMap A,B,A,D) . p2 in (AffineMap A,B,A,D) .: P by A1, FUNCT_1:def 12; :: thesis: for x, y being Point of (TOP-REAL 2) st x in (AffineMap A,B,A,D) .: P & y in (AffineMap A,B,A,D) .: P holds
dist ((AffineMap A,B,A,D) . p1),((AffineMap A,B,A,D) . p2) >= dist x,y
let x, y be Point of (TOP-REAL 2); :: thesis: ( x in (AffineMap A,B,A,D) .: P & y in (AffineMap A,B,A,D) .: P implies dist ((AffineMap A,B,A,D) . p1),((AffineMap A,B,A,D) . p2) >= dist x,y )
assume x in (AffineMap A,B,A,D) .: P ; :: thesis: ( not y in (AffineMap A,B,A,D) .: P or dist ((AffineMap A,B,A,D) . p1),((AffineMap A,B,A,D) . p2) >= dist x,y )
then consider X being set such that
A3: X in dom (AffineMap A,B,A,D) and
A4: X in P and
A5: (AffineMap A,B,A,D) . X = x by FUNCT_1:def 12;
reconsider X = X as Point of (TOP-REAL 2) by A3;
assume y in (AffineMap A,B,A,D) .: P ; :: thesis: dist ((AffineMap A,B,A,D) . p1),((AffineMap A,B,A,D) . p2) >= dist x,y
then consider Y being set such that
A6: Y in dom (AffineMap A,B,A,D) and
A7: Y in P and
A8: (AffineMap A,B,A,D) . Y = y by FUNCT_1:def 12;
reconsider Y = Y as Point of (TOP-REAL 2) by A6;
A9: ( ((X `1 ) - (Y `1 )) ^2 >= 0 & ((X `2 ) - (Y `2 )) ^2 >= 0 ) by XREAL_1:65;
A10: ( ((p1 `1 ) - (p2 `1 )) ^2 >= 0 & ((p1 `2 ) - (p2 `2 )) ^2 >= 0 ) by XREAL_1:65;
A11: A ^2 >= 0 by XREAL_1:65;
then A12: sqrt (A ^2 ) >= 0 by SQUARE_1:def 4;
A13: dist ((AffineMap A,B,A,D) . p1),((AffineMap A,B,A,D) . p2) = dist |[((A * (p1 `1 )) + B),((A * (p1 `2 )) + D)]|,((AffineMap A,B,A,D) . p2) by JGRAPH_2:def 2
.= dist |[((A * (p1 `1 )) + B),((A * (p1 `2 )) + D)]|,|[((A * (p2 `1 )) + B),((A * (p2 `2 )) + D)]| by JGRAPH_2:def 2
.= sqrt ((((|[((A * (p1 `1 )) + B),((A * (p1 `2 )) + D)]| `1 ) - (|[((A * (p2 `1 )) + B),((A * (p2 `2 )) + D)]| `1 )) ^2 ) + (((|[((A * (p1 `1 )) + B),((A * (p1 `2 )) + D)]| `2 ) - (|[((A * (p2 `1 )) + B),((A * (p2 `2 )) + D)]| `2 )) ^2 )) by TOPREAL6:101
.= sqrt (((((A * (p1 `1 )) + B) - (|[((A * (p2 `1 )) + B),((A * (p2 `2 )) + D)]| `1 )) ^2 ) + (((|[((A * (p1 `1 )) + B),((A * (p1 `2 )) + D)]| `2 ) - (|[((A * (p2 `1 )) + B),((A * (p2 `2 )) + D)]| `2 )) ^2 )) by EUCLID:56
.= sqrt (((((A * (p1 `1 )) + B) - ((A * (p2 `1 )) + B)) ^2 ) + (((|[((A * (p1 `1 )) + B),((A * (p1 `2 )) + D)]| `2 ) - (|[((A * (p2 `1 )) + B),((A * (p2 `2 )) + D)]| `2 )) ^2 )) by EUCLID:56
.= sqrt (((((A * (p1 `1 )) + B) - ((A * (p2 `1 )) + B)) ^2 ) + ((((A * (p1 `2 )) + D) - (|[((A * (p2 `1 )) + B),((A * (p2 `2 )) + D)]| `2 )) ^2 )) by EUCLID:56
.= sqrt (((((A * (p1 `1 )) + B) - ((A * (p2 `1 )) + B)) ^2 ) + ((((A * (p1 `2 )) + D) - ((A * (p2 `2 )) + D)) ^2 )) by EUCLID:56
.= sqrt ((A ^2 ) * ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 )))
.= (sqrt (A ^2 )) * (sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 ))) by A11, A10, SQUARE_1:97
.= (sqrt (A ^2 )) * (dist p1,p2) by TOPREAL6:101 ;
A14: dist x,y = dist |[((A * (X `1 )) + B),((A * (X `2 )) + D)]|,((AffineMap A,B,A,D) . Y) by A5, A8, JGRAPH_2:def 2
.= dist |[((A * (X `1 )) + B),((A * (X `2 )) + D)]|,|[((A * (Y `1 )) + B),((A * (Y `2 )) + D)]| by JGRAPH_2:def 2
.= sqrt ((((|[((A * (X `1 )) + B),((A * (X `2 )) + D)]| `1 ) - (|[((A * (Y `1 )) + B),((A * (Y `2 )) + D)]| `1 )) ^2 ) + (((|[((A * (X `1 )) + B),((A * (X `2 )) + D)]| `2 ) - (|[((A * (Y `1 )) + B),((A * (Y `2 )) + D)]| `2 )) ^2 )) by TOPREAL6:101
.= sqrt (((((A * (X `1 )) + B) - (|[((A * (Y `1 )) + B),((A * (Y `2 )) + D)]| `1 )) ^2 ) + (((|[((A * (X `1 )) + B),((A * (X `2 )) + D)]| `2 ) - (|[((A * (Y `1 )) + B),((A * (Y `2 )) + D)]| `2 )) ^2 )) by EUCLID:56
.= sqrt (((((A * (X `1 )) + B) - ((A * (Y `1 )) + B)) ^2 ) + (((|[((A * (X `1 )) + B),((A * (X `2 )) + D)]| `2 ) - (|[((A * (Y `1 )) + B),((A * (Y `2 )) + D)]| `2 )) ^2 )) by EUCLID:56
.= sqrt (((((A * (X `1 )) + B) - ((A * (Y `1 )) + B)) ^2 ) + ((((A * (X `2 )) + D) - (|[((A * (Y `1 )) + B),((A * (Y `2 )) + D)]| `2 )) ^2 )) by EUCLID:56
.= sqrt (((((A * (X `1 )) + B) - ((A * (Y `1 )) + B)) ^2 ) + ((((A * (X `2 )) + D) - ((A * (Y `2 )) + D)) ^2 )) by EUCLID:56
.= sqrt ((A ^2 ) * ((((X `1 ) - (Y `1 )) ^2 ) + (((X `2 ) - (Y `2 )) ^2 )))
.= (sqrt (A ^2 )) * (sqrt ((((X `1 ) - (Y `1 )) ^2 ) + (((X `2 ) - (Y `2 )) ^2 ))) by A11, A9, SQUARE_1:97
.= (sqrt (A ^2 )) * (dist X,Y) by TOPREAL6:101 ;
dist p1,p2 >= dist X,Y by A2, A4, A7, Def1;
hence dist ((AffineMap A,B,A,D) . p1),((AffineMap A,B,A,D) . p2) >= dist x,y by A13, A14, A12, XREAL_1:66; :: thesis: verum