let X be LinearTopSpace; for W being a_neighborhood of 0. X ex U being open a_neighborhood of 0. X st
( U is symmetric & U + U c= W )
let W be a_neighborhood of 0. X; ex U being open a_neighborhood of 0. X st
( U is symmetric & U + U c= W )
(0. X) + (0. X) = 0. X
;
then consider V1, V2 being a_neighborhood of 0. X such that
A1:
V1 + V2 c= W
by Th31;
set U = (((Int V1) /\ (Int V2)) /\ ((- 1) * (Int V1))) /\ ((- 1) * (Int V2));
A2:
( (- 1) * (Int V1) is open & (- 1) * (Int V2) is open )
by Th49;
(- 1) * V2 is a_neighborhood of 0. X
by Th55;
then
0. X in Int ((- 1) * V2)
by CONNSP_2:def 1;
then A3:
0. X in (- 1) * (Int V2)
by Th51;
(- 1) * V1 is a_neighborhood of 0. X
by Th55;
then
0. X in Int ((- 1) * V1)
by CONNSP_2:def 1;
then A4:
0. X in (- 1) * (Int V1)
by Th51;
( 0. X in Int V1 & 0. X in Int V2 )
by CONNSP_2:def 1;
then
0. X in (Int V1) /\ (Int V2)
by XBOOLE_0:def 4;
then
0. X in ((Int V1) /\ (Int V2)) /\ ((- 1) * (Int V1))
by A4, XBOOLE_0:def 4;
then
0. X in (((Int V1) /\ (Int V2)) /\ ((- 1) * (Int V1))) /\ ((- 1) * (Int V2))
by A3, XBOOLE_0:def 4;
then
0. X in Int ((((Int V1) /\ (Int V2)) /\ ((- 1) * (Int V1))) /\ ((- 1) * (Int V2)))
by A2, TOPS_1:23;
then reconsider U = (((Int V1) /\ (Int V2)) /\ ((- 1) * (Int V1))) /\ ((- 1) * (Int V2)) as open a_neighborhood of 0. X by A2, CONNSP_2:def 1;
take
U
; ( U is symmetric & U + U c= W )
((- 1) * (- 1)) * (Int V1) = Int V1
by CONVEX1:32;
then A5:
(- 1) * ((- 1) * (Int V1)) = Int V1
by CONVEX1:37;
((- 1) * (- 1)) * (Int V2) = Int V2
by CONVEX1:32;
then A6:
(- 1) * ((- 1) * (Int V2)) = Int V2
by CONVEX1:37;
thus U =
((Int V1) /\ (Int V2)) /\ (((- 1) * (Int V1)) /\ ((- 1) * (Int V2)))
by XBOOLE_1:16
.=
((- 1) * ((Int V1) /\ (Int V2))) /\ ((Int V1) /\ (Int V2))
by Th15
.=
((- 1) * ((Int V1) /\ (Int V2))) /\ ((- 1) * (((- 1) * (Int V1)) /\ ((- 1) * (Int V2))))
by A5, A6, Th15
.=
(- 1) * (((Int V1) /\ (Int V2)) /\ (((- 1) * (Int V1)) /\ ((- 1) * (Int V2))))
by Th15
.=
- U
by XBOOLE_1:16
; RLTOPSP1:def 5 U + U c= W
let x be object ; TARSKI:def 3 ( not x in U + U or x in W )
assume
x in U + U
; x in W
then
x in { (u + v) where u, v is Point of X : ( u in U & v in U ) }
by RUSUB_4:def 9;
then consider u, v being Point of X such that
A7:
u + v = x
and
A8:
u in U
and
A9:
v in U
;
A10:
U = ((Int V1) /\ (Int V2)) /\ (((- 1) * (Int V1)) /\ ((- 1) * (Int V2)))
by XBOOLE_1:16;
then
v in (Int V1) /\ (Int V2)
by A9, XBOOLE_0:def 4;
then A11:
v in Int V2
by XBOOLE_0:def 4;
( Int V1 c= V1 & Int V2 c= V2 )
by TOPS_1:16;
then A12:
(Int V1) + (Int V2) c= V1 + V2
by Th11;
u in (Int V1) /\ (Int V2)
by A8, A10, XBOOLE_0:def 4;
then
u in Int V1
by XBOOLE_0:def 4;
then
u + v in { (u9 + v9) where u9, v9 is Point of X : ( u9 in Int V1 & v9 in Int V2 ) }
by A11;
then
u + v in (Int V1) + (Int V2)
by RUSUB_4:def 9;
then
u + v in V1 + V2
by A12;
hence
x in W
by A1, A7; verum