let n be Element of NAT ; :: thesis: for x being Element of COMPLEX n
for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
(dist (x,A)) + (dist (x,B)) >= dist (A,B)
let x be Element of COMPLEX n; :: thesis: for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
(dist (x,A)) + (dist (x,B)) >= dist (A,B)
let A, B be Subset of (COMPLEX n); :: thesis: ( A <> {} & B <> {} implies (dist (x,A)) + (dist (x,B)) >= dist (A,B) )
defpred S1[ set ] means $1 in B;
deffunc H1( Element of COMPLEX n) -> Real = |.(x - $1).|;
reconsider Y = { H1(z) where z is Element of COMPLEX n : S1[z] } as Subset of REAL from DOMAIN_1:sch 8();
 defpred S2[ set , set ] means ( $1 in A & $2 in B );
defpred S3[ set ] means $1 in A;
deffunc H2( Element of COMPLEX n, Element of COMPLEX n) -> Real = |.($1 - $2).|;
reconsider X = { H1(z) where z is Element of COMPLEX n : S3[z] } as Subset of REAL from DOMAIN_1:sch 8();
 assume that
A1: A <> {} and
A2: B <> {} ; :: thesis: (dist (x,A)) + (dist (x,B)) >= dist (A,B)
consider z2 being Element of COMPLEX n such that
A3: z2 in B by A2, SUBSET_1:4;
A4: ( Y <> {} & Y is bounded_below )
proof
|.(x - z2).| in Y by A3;
hence Y <> {} ; :: thesis: Y is bounded_below
take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of Y
let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not r in Y or 0 <= r )
assume r in Y ; :: thesis: 0 <= r
then ex z1 being Element of COMPLEX n st
( r = |.(x - z1).| & z1 in B ) ;
hence 0 <= r by Th112; :: thesis: verum
end;
A5: ( lower_bound X = dist (x,A) & lower_bound Y = dist (x,B) ) by Def20;
A6: |.(x - z2).| in Y by A3;
reconsider Z = { H2(z1,z) where z1, z is Element of COMPLEX n : S2[z1,z] } as Subset of REAL from DOMAIN_1:sch 9();
 consider z1 being Element of COMPLEX n such that
A7: z1 in A by A1, SUBSET_1:4;
A8: now
let r be Real; :: thesis: ( r in X ++ Y implies ex r3 being Real st
( r3 in Z & r3 <= r ) )
assume r in X ++ Y ; :: thesis: ex r3 being Real st
( r3 in Z & r3 <= r )
then r in { (r2 + r1) where r2, r1 is Element of COMPLEX : ( r2 in X & r1 in Y ) } by MEMBER_1:def 6;
then consider r2, r1 being Element of COMPLEX such that
A9: r = r2 + r1 and
A10: r2 in X and
A11: r1 in Y ;
consider z2 being Element of COMPLEX n such that
A12: ( r1 = |.(x - z2).| & z2 in B ) by A11;
consider z1 being Element of COMPLEX n such that
A13: r2 = |.(x - z1).| and
A14: z1 in A by A10;
take r3 = |.(z1 - z2).|; :: thesis: ( r3 in Z & r3 <= r )
r2 = |.(z1 - x).| by A13, Th121;
hence ( r3 in Z & r3 <= r ) by A9, A14, A12, Th122; :: thesis: verum
end;
A15: Z is bounded_below
proof
take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of Z
let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not r in Z or 0 <= r )
assume r in Z ; :: thesis: 0 <= r
then ex z1, z being Element of COMPLEX n st
( r = |.(z1 - z).| & z1 in A & z in B ) ;
hence 0 <= r by Th112; :: thesis: verum
end;
A16: ( X <> {} & X is bounded_below )
proof
|.(x - z1).| in X by A7;
hence X <> {} ; :: thesis: X is bounded_below
take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of X
let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not r in X or 0 <= r )
assume r in X ; :: thesis: 0 <= r
then ex z being Element of COMPLEX n st
( r = |.(x - z).| & z in A ) ;
hence 0 <= r by Th112; :: thesis: verum
end;
A17: lower_bound Z = dist (A,B) by Def22;
A18: X ++ Y c= REAL by MEMBERED:3;
|.(x - z1).| in X by A7;
then |.(x - z1).| + |.(x - z2).| in X ++ Y by A6, MEMBER_1:46;
then lower_bound (X ++ Y) >= lower_bound Z by A15, A8, Th143, A18;
hence (dist (x,A)) + (dist (x,B)) >= dist (A,B) by A16, A4, A5, A17, Th142; :: thesis: verum