let p be Point of (TOP-REAL 2); :: thesis: for P being non empty compact Subset of (TOP-REAL 2)
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle 0 ,0 ,1 & f = Sq_Circ holds
( (f . p) `2 >= 0 iff p `2 >= 0 )
let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle 0 ,0 ,1 & f = Sq_Circ holds
( (f . p) `2 >= 0 iff p `2 >= 0 )
let f be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: ( P = circle 0 ,0 ,1 & f = Sq_Circ implies ( (f . p) `2 >= 0 iff p `2 >= 0 ) )
assume A1: ( P = circle 0 ,0 ,1 & f = Sq_Circ ) ; :: thesis: ( (f . p) `2 >= 0 iff p `2 >= 0 )
thus ( (f . p) `2 >= 0 implies p `2 >= 0 ) :: thesis: ( p `2 >= 0 implies (f . p) `2 >= 0 )
proof
assume A2: (f . p) `2 >= 0 ; :: thesis: p `2 >= 0
reconsider g = Sq_Circ " as Function of (TOP-REAL 2),(TOP-REAL 2) by JGRAPH_3:39;
A3: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
set q = f . p;
now
per cases ( f . p = 0. (TOP-REAL 2) or f . p <> 0. (TOP-REAL 2) ) ;
case f . p = 0. (TOP-REAL 2) ; :: thesis: (g . (f . p)) `2 >= 0
hence (g . (f . p)) `2 >= 0 by A2, JGRAPH_3:38; :: thesis: verum
end;
case A4: f . p <> 0. (TOP-REAL 2) ; :: thesis: (g . (f . p)) `2 >= 0
now
per cases ( ( (f . p) `2 <= (f . p) `1 & - ((f . p) `1 ) <= (f . p) `2 ) or ( (f . p) `2 >= (f . p) `1 & (f . p) `2 <= - ((f . p) `1 ) ) or ( not ( (f . p) `2 <= (f . p) `1 & - ((f . p) `1 ) <= (f . p) `2 ) & not ( (f . p) `2 >= (f . p) `1 & (f . p) `2 <= - ((f . p) `1 ) ) ) ) ;
case ( ( (f . p) `2 <= (f . p) `1 & - ((f . p) `1 ) <= (f . p) `2 ) or ( (f . p) `2 >= (f . p) `1 & (f . p) `2 <= - ((f . p) `1 ) ) ) ; :: thesis: (g . (f . p)) `2 >= 0
then g . (f . p) = |[(((f . p) `1 ) * (sqrt (1 + ((((f . p) `2 ) / ((f . p) `1 )) ^2 )))),(((f . p) `2 ) * (sqrt (1 + ((((f . p) `2 ) / ((f . p) `1 )) ^2 ))))]| by A4, JGRAPH_3:38;
then A5: (g . (f . p)) `2 = ((f . p) `2 ) * (sqrt (1 + ((((f . p) `2 ) / ((f . p) `1 )) ^2 ))) by EUCLID:56;
A6: (((f . p) `2 ) / ((f . p) `1 )) ^2 >= 0 by XREAL_1:65;
sqrt (1 + ((((f . p) `2 ) / ((f . p) `1 )) ^2 )) > 0 by A6, SQUARE_1:93;
hence (g . (f . p)) `2 >= 0 by A2, A5; :: thesis: verum
end;
case ( not ( (f . p) `2 <= (f . p) `1 & - ((f . p) `1 ) <= (f . p) `2 ) & not ( (f . p) `2 >= (f . p) `1 & (f . p) `2 <= - ((f . p) `1 ) ) ) ; :: thesis: (g . (f . p)) `2 >= 0
then g . (f . p) = |[(((f . p) `1 ) * (sqrt (1 + ((((f . p) `1 ) / ((f . p) `2 )) ^2 )))),(((f . p) `2 ) * (sqrt (1 + ((((f . p) `1 ) / ((f . p) `2 )) ^2 ))))]| by A4, JGRAPH_3:38;
then A7: (g . (f . p)) `2 = ((f . p) `2 ) * (sqrt (1 + ((((f . p) `1 ) / ((f . p) `2 )) ^2 ))) by EUCLID:56;
A8: (((f . p) `1 ) / ((f . p) `2 )) ^2 >= 0 by XREAL_1:65;
sqrt (1 + ((((f . p) `1 ) / ((f . p) `2 )) ^2 )) > 0 by A8, SQUARE_1:93;
hence (g . (f . p)) `2 >= 0 by A2, A7; :: thesis: verum
end;
end;
end;
hence (g . (f . p)) `2 >= 0 ; :: thesis: verum
end;
end;
end;
hence p `2 >= 0 by A1, A3, FUNCT_1:56; :: thesis: verum
end;
thus ( p `2 >= 0 implies (f . p) `2 >= 0 ) :: thesis: verum
proof
assume A9: p `2 >= 0 ; :: thesis: (f . p) `2 >= 0
now
per cases ( p = 0. (TOP-REAL 2) or p <> 0. (TOP-REAL 2) ) ;
case A10: p <> 0. (TOP-REAL 2) ; :: thesis: (f . p) `2 >= 0
now
per cases ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or ( not ( p `2 <= p `1 & - (p `1 ) <= p `2 ) & not ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) ) ;
case ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) ; :: thesis: (f . p) `2 >= 0
then f . p = |[((p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| by A1, A10, JGRAPH_3:def 1;
then A11: (f . p) `2 = (p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))) by EUCLID:56;
A12: ((p `2 ) / (p `1 )) ^2 >= 0 by XREAL_1:65;
sqrt (1 + (((p `2 ) / (p `1 )) ^2 )) > 0 by A12, SQUARE_1:93;
hence (f . p) `2 >= 0 by A9, A11; :: thesis: verum
end;
case ( not ( p `2 <= p `1 & - (p `1 ) <= p `2 ) & not ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) ; :: thesis: (f . p) `2 >= 0
then f . p = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| by A1, A10, JGRAPH_3:def 1;
then A13: (f . p) `2 = (p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))) by EUCLID:56;
A14: ((p `1 ) / (p `2 )) ^2 >= 0 by XREAL_1:65;
sqrt (1 + (((p `1 ) / (p `2 )) ^2 )) > 0 by A14, SQUARE_1:93;
hence (f . p) `2 >= 0 by A9, A13; :: thesis: verum
end;
end;
end;
hence (f . p) `2 >= 0 ; :: thesis: verum
end;
end;
end;
hence (f . p) `2 >= 0 ; :: thesis: verum
end;