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;
assume A1: 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 A2: ( p1 in P & p2 in P & ( for x, y being Point of (TOP-REAL 2) st x in P & y in P holds
dist p1,p2 >= dist x,y ) ) by Def1;
A3: dom (AffineMap A,B,A,D) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
hence (AffineMap A,B,A,D) . p1 in (AffineMap A,B,A,D) .: P by A2, 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 ) )
thus (AffineMap A,B,A,D) . p2 in (AffineMap A,B,A,D) .: P by A2, A3, 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
A4: ( X in dom (AffineMap A,B,A,D) & X in P & (AffineMap A,B,A,D) . X = x ) by FUNCT_1:def 12;
reconsider X = X as Point of (TOP-REAL 2) by A4;
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
A5: ( Y in dom (AffineMap A,B,A,D) & Y in P & (AffineMap A,B,A,D) . Y = y ) by FUNCT_1:def 12;
reconsider Y = Y as Point of (TOP-REAL 2) by A5;
A6: dist p1,p2 >= dist X,Y by A1, A4, A5, Def1;
A7: ( A ^2 >= 0 & ((p1 `1 ) - (p2 `1 )) ^2 >= 0 & ((p1 `2 ) - (p2 `2 )) ^2 >= 0 & ((X `1 ) - (Y `1 )) ^2 >= 0 & ((X `2 ) - (Y `2 )) ^2 >= 0 ) by XREAL_1:65;
A9: 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 A7, SQUARE_1:97
.= (sqrt (A ^2 )) * (dist p1,p2) by TOPREAL6:101 ;
A10: dist x,y = dist |[((A * (X `1 )) + B),((A * (X `2 )) + D)]|,((AffineMap A,B,A,D) . Y) by A4, A5, 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 A7, SQUARE_1:97
.= (sqrt (A ^2 )) * (dist X,Y) by TOPREAL6:101 ;
sqrt (A ^2 ) >= 0 by A7, SQUARE_1:def 4;
hence dist ((AffineMap A,B,A,D) . p1),((AffineMap A,B,A,D) . p2) >= dist x,y by A6, A9, A10, XREAL_1:66; :: thesis: verum