let p1, p2 be Point of (TOP-REAL 2); :: thesis: for P being Subset of (TOP-REAL 2)
for A, B, D being Real 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 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; :: 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 ;
hence (AffineMap (A,B,A,D)) . p1 in (AffineMap (A,B,A,D)) .: P by A1, FUNCT_1:def 6; :: 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;
hence (AffineMap (A,B,A,D)) . p2 in (AffineMap (A,B,A,D)) .: P by A1, FUNCT_1:def 6; :: 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 object 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 6;
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 object 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 6;
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:63;
A10: ( ((p1 `1) - (p2 `1)) ^2 >= 0 & ((p1 `2) - (p2 `2)) ^2 >= 0 ) by XREAL_1:63;
A11: A ^2 >= 0 by XREAL_1:63;
then A12: sqrt (A ^2) >= 0 by SQUARE_1:def 2;
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:92
.= 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:52
.= 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:52
.= 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:52
.= sqrt (((((A * (p1 `1)) + B) - ((A * (p2 `1)) + B)) ^2) + ((((A * (p1 `2)) + D) - ((A * (p2 `2)) + D)) ^2)) by EUCLID:52
.= 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:29
.= (sqrt (A ^2)) * (dist (p1,p2)) by TOPREAL6:92 ;
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:92
.= 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:52
.= 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:52
.= 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:52
.= sqrt (((((A * (X `1)) + B) - ((A * (Y `1)) + B)) ^2) + ((((A * (X `2)) + D) - ((A * (Y `2)) + D)) ^2)) by EUCLID:52
.= 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:29
.= (sqrt (A ^2)) * (dist (X,Y)) by TOPREAL6:92 ;
dist (p1,p2) >= dist (X,Y) by A2, A4, A7;
hence dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) >= dist (x,y) by A13, A14, A12, XREAL_1:64; :: thesis: verum