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 E-max P = |[1,0 ]| )
assume A1:
P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 }
; :: thesis: E-max P = |[1,0 ]|
A2:
the carrier of ((TOP-REAL 2) | P) = P
by PRE_TOPC:29;
A3:
E-bound P = 1
by A1, Th31;
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:
SE-corner P = |[1,(- 1)]|
by A3, PSCOMP_1:def 37;
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:
NE-corner P = |[1,1]|
by A3, PSCOMP_1:def 36;
A7:
{|[1,0 ]|} c= (LSeg (SE-corner P),(NE-corner P)) /\ P
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in {|[1,0 ]|} or x in (LSeg (SE-corner P),(NE-corner P)) /\ P )
assume
x in {|[1,0 ]|}
;
:: thesis: x in (LSeg (SE-corner P),(NE-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) * (SE-corner P)) + (l * (NE-corner P))) where l is Real : ( 0 <= l & l <= 1 ) }
by A5, A6;
then
x in LSeg (SE-corner P),
(NE-corner P)
by A8;
hence
x in (LSeg (SE-corner P),(NE-corner P)) /\ P
by A9, XBOOLE_0:def 4;
:: thesis: verum
end;
(LSeg (SE-corner P),(NE-corner P)) /\ P c= {|[1,0 ]|}
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (SE-corner P),(NE-corner P)) /\ P or x in {|[1,0 ]|} )
assume
x in (LSeg (SE-corner P),(NE-corner P)) /\ P
;
:: thesis: x in {|[1,0 ]|}
then A10:
(
x in LSeg (SE-corner P),
(NE-corner P) &
x in P )
by XBOOLE_0:def 4;
then
x in { (((1 - l) * (SE-corner P)) + (l * (NE-corner P))) where l is Real : ( 0 <= l & l <= 1 ) }
;
then consider l being
Real such that A11:
(
x = ((1 - l) * (SE-corner P)) + (l * (NE-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) + 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;
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 (SE-corner P),(NE-corner P)) /\ P = {|[1,0 ]|}
by A7, XBOOLE_0:def 10;
then A15:
E-most P = {|[1,0 ]|}
by PSCOMP_1:def 40;
(proj2 | (E-most P)) .: the carrier of ((TOP-REAL 2) | (E-most P)) =
(proj2 | (E-most P)) .: (E-most P)
by PRE_TOPC:29
.=
Im proj2 ,|[1,0 ]|
by A15, RELAT_1:162
.=
{(proj2 . |[1,0 ]|)}
by SETWISEO:13
.=
{(|[1,0 ]| `2 )}
by PSCOMP_1:def 29
.=
{0 }
by EUCLID:56
;
then
sup ((proj2 | (E-most P)) .: the carrier of ((TOP-REAL 2) | (E-most P))) = 0
by SEQ_4:22;
then
sup (proj2 | (E-most P)) = 0
by PSCOMP_1:def 21;
hence
E-max P = |[1,0 ]|
by A3, PSCOMP_1:def 46; :: thesis: verum