let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } implies W-min P = |[(- 1),0 ]| )
assume A1:
P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 }
; :: thesis: W-min P = |[(- 1),0 ]|
A2:
the carrier of ((TOP-REAL 2) | P) = P
by PRE_TOPC:29;
A3:
W-bound P = - 1
by A1, Lm3;
proj2 .: P = [.(- 1),1.]
by A1, Lm2;
then
(proj2 | P) .: P = [.(- 1),1.]
by RELAT_1:162;
then A4:
(proj2 | P) .: P = [.(- 1),1.]
;
then
lower_bound ((proj2 | P) .: P) = - 1
by JORDAN5A:20;
then
inf (proj2 | P) = - 1
by A2, PSCOMP_1:def 20;
then
S-bound P = - 1
by PSCOMP_1:def 33;
then A5:
SW-corner P = |[(- 1),(- 1)]|
by A3, PSCOMP_1:def 34;
sup ((proj2 | P) .: P) = 1
by A4, JORDAN5A:20;
then
sup (proj2 | P) = 1
by A2, PSCOMP_1:def 21;
then
N-bound P = 1
by PSCOMP_1:def 31;
then A6:
NW-corner P = |[(- 1),1]|
by A3, PSCOMP_1:def 35;
A7:
{|[(- 1),0 ]|} c= (LSeg (SW-corner P),(NW-corner P)) /\ P
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in {|[(- 1),0 ]|} or x in (LSeg (SW-corner P),(NW-corner P)) /\ P )
assume
x in {|[(- 1),0 ]|}
;
:: thesis: x in (LSeg (SW-corner P),(NW-corner P)) /\ P
then A8:
x = |[(- 1),0 ]|
by TARSKI:def 1;
set q =
|[(- 1),0 ]|;
(
|[(- 1),0 ]| `2 = 0 &
|[(- 1),0 ]| `1 = - 1 )
by EUCLID:56;
then |.|[(- 1),0 ]|.| =
sqrt (((- 1) ^2 ) + (0 ^2 ))
by JGRAPH_3:10
.=
1
by SQUARE_1:83
;
then A9:
x in P
by A1, A8;
|[(- 1),0 ]| = |[(((1 / 2) * (- 1)) + ((1 / 2) * (- 1))),(((1 / 2) * (- 1)) + ((1 / 2) * 1))]|
;
then
|[(- 1),0 ]| = |[((1 / 2) * (- 1)),((1 / 2) * (- 1))]| + |[((1 / 2) * (- 1)),((1 / 2) * 1)]|
by EUCLID:60;
then
|[(- 1),0 ]| = |[((1 / 2) * (- 1)),((1 / 2) * (- 1))]| + ((1 / 2) * |[(- 1),1]|)
by EUCLID:62;
then
|[(- 1),0 ]| = ((1 / 2) * |[(- 1),(- 1)]|) + ((1 - (1 / 2)) * |[(- 1),1]|)
by EUCLID:62;
then
|[(- 1),0 ]| in { (((1 - l) * (SW-corner P)) + (l * (NW-corner P))) where l is Real : ( 0 <= l & l <= 1 ) }
by A5, A6;
then
x in LSeg (SW-corner P),
(NW-corner P)
by A8;
hence
x in (LSeg (SW-corner P),(NW-corner P)) /\ P
by A9, XBOOLE_0:def 4;
:: thesis: verum
end;
(LSeg (SW-corner P),(NW-corner P)) /\ P c= {|[(- 1),0 ]|}
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (SW-corner P),(NW-corner P)) /\ P or x in {|[(- 1),0 ]|} )
assume
x in (LSeg (SW-corner P),(NW-corner P)) /\ P
;
:: thesis: x in {|[(- 1),0 ]|}
then A10:
(
x in LSeg (SW-corner P),
(NW-corner P) &
x in P )
by XBOOLE_0:def 4;
then
x in { (((1 - l) * (SW-corner P)) + (l * (NW-corner P))) where l is Real : ( 0 <= l & l <= 1 ) }
;
then consider l being
Real such that A11:
(
x = ((1 - l) * (SW-corner P)) + (l * (NW-corner P)) &
0 <= l &
l <= 1 )
;
x = |[((1 - l) * (- 1)),((1 - l) * (- 1))]| + (l * |[(- 1),1]|)
by A5, A6, A11, EUCLID:62;
then
x = |[((1 - l) * (- 1)),((1 - l) * (- 1))]| + |[(l * (- 1)),(l * 1)]|
by EUCLID:62;
then A12:
x = |[(((1 - l) * (- 1)) + (l * (- 1))),(((1 - l) * (- 1)) + (l * 1))]|
by EUCLID:60;
reconsider q3 =
x as
Point of
(TOP-REAL 2) by A11;
A13:
(
q3 `1 = - 1 &
q3 `2 = ((1 - l) * (- 1)) + l )
by A12, EUCLID:56;
consider q2 being
Point of
(TOP-REAL 2) such that A14:
(
q2 = x &
|.q2.| = 1 )
by A1, A10;
A15: 1 =
sqrt (((- 1) ^2 ) + ((q3 `2 ) ^2 ))
by A13, A14, JGRAPH_3:10
.=
sqrt (1 + ((q3 `2 ) ^2 ))
;
then
(q3 `2 ) ^2 = 0
by XREAL_1:65;
then
q3 `2 = 0
by XCMPLX_1:6;
hence
x in {|[(- 1),0 ]|}
by A12, A13, TARSKI:def 1;
:: thesis: verum
end;
then
(LSeg (SW-corner P),(NW-corner P)) /\ P = {|[(- 1),0 ]|}
by A7, XBOOLE_0:def 10;
then A16:
W-most P = {|[(- 1),0 ]|}
by PSCOMP_1:def 38;
(proj2 | (W-most P)) .: the carrier of ((TOP-REAL 2) | (W-most P)) =
(proj2 | (W-most P)) .: (W-most P)
by PRE_TOPC:29
.=
Im proj2 ,|[(- 1),0 ]|
by A16, RELAT_1:162
.=
{(proj2 . |[(- 1),0 ]|)}
by SETWISEO:13
.=
{(|[(- 1),0 ]| `2 )}
by PSCOMP_1:def 29
.=
{0 }
by EUCLID:56
;
then
lower_bound ((proj2 | (W-most P)) .: the carrier of ((TOP-REAL 2) | (W-most P))) = 0
by SEQ_4:22;
then
inf (proj2 | (W-most P)) = 0
by PSCOMP_1:def 20;
hence
W-min P = |[(- 1),0 ]|
by A3, PSCOMP_1:def 42; :: thesis: verum