:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama

::

:: Received October 25, 2002

:: Copyright (c) 2002-2012 Association of Mizar Users

begin

:: deftheorem Def1 defines is_parallel_to RUSUB_5:def 1 :

for V being non empty RLSStruct

for M, N being Affine Subset of V holds

( M is_parallel_to N iff ex v being VECTOR of V st M = N + {v} );

for V being non empty RLSStruct

for M, N being Affine Subset of V holds

( M is_parallel_to N iff ex v being VECTOR of V st M = N + {v} );

theorem :: RUSUB_5:1

for V being non empty right_zeroed RLSStruct

for M being Affine Subset of V holds M is_parallel_to M

for M being Affine Subset of V holds M is_parallel_to M

proof end;

theorem Th2: :: RUSUB_5:2

for V being non empty right_complementable add-associative right_zeroed RLSStruct

for M, N being Affine Subset of V st M is_parallel_to N holds

N is_parallel_to M

for M, N being Affine Subset of V st M is_parallel_to N holds

N is_parallel_to M

proof end;

theorem Th3: :: RUSUB_5:3

for V being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for M, L, N being Affine Subset of V st M is_parallel_to L & L is_parallel_to N holds

M is_parallel_to N

for M, L, N being Affine Subset of V st M is_parallel_to L & L is_parallel_to N holds

M is_parallel_to N

proof end;

definition

let V be non empty addLoopStr ;

let M, N be Subset of V;

{ (u - v) where u, v is Element of V : ( u in M & v in N ) } is Subset of V

end;
let M, N be Subset of V;

func M - N -> Subset of V equals :: RUSUB_5:def 2

{ (u - v) where u, v is Element of V : ( u in M & v in N ) } ;

coherence { (u - v) where u, v is Element of V : ( u in M & v in N ) } ;

{ (u - v) where u, v is Element of V : ( u in M & v in N ) } is Subset of V

proof end;

:: deftheorem defines - RUSUB_5:def 2 :

for V being non empty addLoopStr

for M, N being Subset of V holds M - N = { (u - v) where u, v is Element of V : ( u in M & v in N ) } ;

for V being non empty addLoopStr

for M, N being Subset of V holds M - N = { (u - v) where u, v is Element of V : ( u in M & v in N ) } ;

theorem :: RUSUB_5:5

for V being non empty addLoopStr

for M, N being Subset of V st ( M is empty or N is empty ) holds

M + N is empty

for M, N being Subset of V st ( M is empty or N is empty ) holds

M + N is empty

proof end;

theorem :: RUSUB_5:7

for V being non empty addLoopStr

for M, N being Subset of V st ( M is empty or N is empty ) holds

M - N is empty

for M, N being Subset of V st ( M is empty or N is empty ) holds

M - N is empty

proof end;

theorem Th9: :: RUSUB_5:9

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for M, N being Subset of V

for v being Element of V holds

( M = N + {v} iff M - {v} = N )

for M, N being Subset of V

for v being Element of V holds

( M = N + {v} iff M - {v} = N )

proof end;

theorem :: RUSUB_5:10

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for M, N being Subset of V

for v being Element of V st v in N holds

M + {v} c= M + N

for M, N being Subset of V

for v being Element of V st v in N holds

M + {v} c= M + N

proof end;

theorem :: RUSUB_5:11

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for M, N being Subset of V

for v being Element of V st v in N holds

M - {v} c= M - N

for M, N being Subset of V

for v being Element of V st v in N holds

M - {v} c= M - N

proof end;

theorem Th13: :: RUSUB_5:13

for V being RealLinearSpace

for M being non empty Affine Subset of V

for v being VECTOR of V st M is Subspace-like & v in M holds

M + {v} c= M

for M being non empty Affine Subset of V

for v being VECTOR of V st M is Subspace-like & v in M holds

M + {v} c= M

proof end;

theorem Th14: :: RUSUB_5:14

for V being RealLinearSpace

for M, N1, N2 being non empty Affine Subset of V st N1 is Subspace-like & N2 is Subspace-like & M is_parallel_to N1 & M is_parallel_to N2 holds

N1 = N2

for M, N1, N2 being non empty Affine Subset of V st N1 is Subspace-like & N2 is Subspace-like & M is_parallel_to N1 & M is_parallel_to N2 holds

N1 = N2

proof end;

theorem Th15: :: RUSUB_5:15

for V being RealLinearSpace

for M being non empty Affine Subset of V

for v being VECTOR of V st v in M holds

0. V in M - {v}

for M being non empty Affine Subset of V

for v being VECTOR of V st v in M holds

0. V in M - {v}

proof end;

theorem Th16: :: RUSUB_5:16

for V being RealLinearSpace

for M being non empty Affine Subset of V

for v being VECTOR of V st v in M holds

ex N being non empty Affine Subset of V st

( N = M - {v} & M is_parallel_to N & N is Subspace-like )

for M being non empty Affine Subset of V

for v being VECTOR of V st v in M holds

ex N being non empty Affine Subset of V st

( N = M - {v} & M is_parallel_to N & N is Subspace-like )

proof end;

theorem Th17: :: RUSUB_5:17

for V being RealLinearSpace

for M being non empty Affine Subset of V

for u, v being VECTOR of V st u in M & v in M holds

M - {v} = M - {u}

for M being non empty Affine Subset of V

for u, v being VECTOR of V st u in M & v in M holds

M - {v} = M - {u}

proof end;

theorem Th18: :: RUSUB_5:18

for V being RealLinearSpace

for M being non empty Affine Subset of V holds M - M = union { (M - {v}) where v is VECTOR of V : v in M }

for M being non empty Affine Subset of V holds M - M = union { (M - {v}) where v is VECTOR of V : v in M }

proof end;

theorem Th19: :: RUSUB_5:19

for V being RealLinearSpace

for M being non empty Affine Subset of V

for v being VECTOR of V st v in M holds

M - {v} = union { (M - {u}) where u is VECTOR of V : u in M }

for M being non empty Affine Subset of V

for v being VECTOR of V st v in M holds

M - {v} = union { (M - {u}) where u is VECTOR of V : u in M }

proof end;

theorem :: RUSUB_5:20

for V being RealLinearSpace

for M being non empty Affine Subset of V ex L being non empty Affine Subset of V st

( L = M - M & L is Subspace-like & M is_parallel_to L )

for M being non empty Affine Subset of V ex L being non empty Affine Subset of V st

( L = M - M & L is Subspace-like & M is_parallel_to L )

proof end;

begin

definition

let V be RealUnitarySpace;

let W be Subspace of V;

ex b_{1} being strict Subspace of V st the carrier of b_{1} = { v where v is VECTOR of V : for w being VECTOR of V st w in W holds

w,v are_orthogonal }

for b_{1}, b_{2} being strict Subspace of V st the carrier of b_{1} = { v where v is VECTOR of V : for w being VECTOR of V st w in W holds

w,v are_orthogonal } & the carrier of b_{2} = { v where v is VECTOR of V : for w being VECTOR of V st w in W holds

w,v are_orthogonal } holds

b_{1} = b_{2}
by RUSUB_1:24;

end;
let W be Subspace of V;

func Ort_Comp W -> strict Subspace of V means :Def3: :: RUSUB_5:def 3

the carrier of it = { v where v is VECTOR of V : for w being VECTOR of V st w in W holds

w,v are_orthogonal } ;

existence the carrier of it = { v where v is VECTOR of V : for w being VECTOR of V st w in W holds

w,v are_orthogonal } ;

ex b

w,v are_orthogonal }

proof end;

uniqueness for b

w,v are_orthogonal } & the carrier of b

w,v are_orthogonal } holds

b

:: deftheorem Def3 defines Ort_Comp RUSUB_5:def 3 :

for V being RealUnitarySpace

for W being Subspace of V

for b_{3} being strict Subspace of V holds

( b_{3} = Ort_Comp W iff the carrier of b_{3} = { v where v is VECTOR of V : for w being VECTOR of V st w in W holds

w,v are_orthogonal } );

for V being RealUnitarySpace

for W being Subspace of V

for b

( b

w,v are_orthogonal } );

definition

let V be RealUnitarySpace;

let M be non empty Subset of V;

ex b_{1} being strict Subspace of V st the carrier of b_{1} = { v where v is VECTOR of V : for w being VECTOR of V st w in M holds

w,v are_orthogonal }

for b_{1}, b_{2} being strict Subspace of V st the carrier of b_{1} = { v where v is VECTOR of V : for w being VECTOR of V st w in M holds

w,v are_orthogonal } & the carrier of b_{2} = { v where v is VECTOR of V : for w being VECTOR of V st w in M holds

w,v are_orthogonal } holds

b_{1} = b_{2}
by RUSUB_1:24;

end;
let M be non empty Subset of V;

func Ort_Comp M -> strict Subspace of V means :Def4: :: RUSUB_5:def 4

the carrier of it = { v where v is VECTOR of V : for w being VECTOR of V st w in M holds

w,v are_orthogonal } ;

existence the carrier of it = { v where v is VECTOR of V : for w being VECTOR of V st w in M holds

w,v are_orthogonal } ;

ex b

w,v are_orthogonal }

proof end;

uniqueness for b

w,v are_orthogonal } & the carrier of b

w,v are_orthogonal } holds

b

:: deftheorem Def4 defines Ort_Comp RUSUB_5:def 4 :

for V being RealUnitarySpace

for M being non empty Subset of V

for b_{3} being strict Subspace of V holds

( b_{3} = Ort_Comp M iff the carrier of b_{3} = { v where v is VECTOR of V : for w being VECTOR of V st w in M holds

w,v are_orthogonal } );

for V being RealUnitarySpace

for M being non empty Subset of V

for b

( b

w,v are_orthogonal } );

theorem :: RUSUB_5:24

for V being RealUnitarySpace

for W being Subspace of V

for v being VECTOR of V st v <> 0. V & v in W holds

not v in Ort_Comp W

for W being Subspace of V

for v being VECTOR of V st v <> 0. V & v in W holds

not v in Ort_Comp W

proof end;

theorem Th25: :: RUSUB_5:25

for V being RealUnitarySpace

for M being non empty Subset of V holds M c= the carrier of (Ort_Comp (Ort_Comp M))

for M being non empty Subset of V holds M c= the carrier of (Ort_Comp (Ort_Comp M))

proof end;

theorem Th26: :: RUSUB_5:26

for V being RealUnitarySpace

for M, N being non empty Subset of V st M c= N holds

the carrier of (Ort_Comp N) c= the carrier of (Ort_Comp M)

for M, N being non empty Subset of V st M c= N holds

the carrier of (Ort_Comp N) c= the carrier of (Ort_Comp M)

proof end;

theorem Th27: :: RUSUB_5:27

for V being RealUnitarySpace

for W being Subspace of V

for M being non empty Subset of V st M = the carrier of W holds

Ort_Comp M = Ort_Comp W

for W being Subspace of V

for M being non empty Subset of V st M = the carrier of W holds

Ort_Comp M = Ort_Comp W

proof end;

theorem :: RUSUB_5:28

for V being RealUnitarySpace

for M being non empty Subset of V holds Ort_Comp M = Ort_Comp (Ort_Comp (Ort_Comp M))

for M being non empty Subset of V holds Ort_Comp M = Ort_Comp (Ort_Comp (Ort_Comp M))

proof end;

theorem Th29: :: RUSUB_5:29

for V being RealUnitarySpace

for x, y being VECTOR of V holds

( ||.(x + y).|| ^2 = ((||.x.|| ^2) + (2 * (x .|. y))) + (||.y.|| ^2) & ||.(x - y).|| ^2 = ((||.x.|| ^2) - (2 * (x .|. y))) + (||.y.|| ^2) )

for x, y being VECTOR of V holds

( ||.(x + y).|| ^2 = ((||.x.|| ^2) + (2 * (x .|. y))) + (||.y.|| ^2) & ||.(x - y).|| ^2 = ((||.x.|| ^2) - (2 * (x .|. y))) + (||.y.|| ^2) )

proof end;

theorem :: RUSUB_5:30

for V being RealUnitarySpace

for x, y being VECTOR of V st x,y are_orthogonal holds

||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2)

for x, y being VECTOR of V st x,y are_orthogonal holds

||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2)

proof end;

:: Parallelogram Law

theorem :: RUSUB_5:31

for V being RealUnitarySpace

for x, y being VECTOR of V holds (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2))

for x, y being VECTOR of V holds (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2))

proof end;

theorem :: RUSUB_5:32

for V being RealUnitarySpace

for v being VECTOR of V ex W being Subspace of V st the carrier of W = { u where u is VECTOR of V : u .|. v = 0 }

for v being VECTOR of V ex W being Subspace of V st the carrier of W = { u where u is VECTOR of V : u .|. v = 0 }

proof end;

begin

definition

let V be RealUnitarySpace;

ex b_{1} being Subset-Family of V st

for M being Subset of V holds

( M in b_{1} iff for x being Point of V st x in M holds

ex r being Real st

( r > 0 & Ball (x,r) c= M ) )

for b_{1}, b_{2} being Subset-Family of V st ( for M being Subset of V holds

( M in b_{1} iff for x being Point of V st x in M holds

ex r being Real st

( r > 0 & Ball (x,r) c= M ) ) ) & ( for M being Subset of V holds

( M in b_{2} iff for x being Point of V st x in M holds

ex r being Real st

( r > 0 & Ball (x,r) c= M ) ) ) holds

b_{1} = b_{2}

end;
func Family_open_set V -> Subset-Family of V means :Def5: :: RUSUB_5:def 5

for M being Subset of V holds

( M in it iff for x being Point of V st x in M holds

ex r being Real st

( r > 0 & Ball (x,r) c= M ) );

existence for M being Subset of V holds

( M in it iff for x being Point of V st x in M holds

ex r being Real st

( r > 0 & Ball (x,r) c= M ) );

ex b

for M being Subset of V holds

( M in b

ex r being Real st

( r > 0 & Ball (x,r) c= M ) )

proof end;

uniqueness for b

( M in b

ex r being Real st

( r > 0 & Ball (x,r) c= M ) ) ) & ( for M being Subset of V holds

( M in b

ex r being Real st

( r > 0 & Ball (x,r) c= M ) ) ) holds

b

proof end;

:: deftheorem Def5 defines Family_open_set RUSUB_5:def 5 :

for V being RealUnitarySpace

for b_{2} being Subset-Family of V holds

( b_{2} = Family_open_set V iff for M being Subset of V holds

( M in b_{2} iff for x being Point of V st x in M holds

ex r being Real st

( r > 0 & Ball (x,r) c= M ) ) );

for V being RealUnitarySpace

for b

( b

( M in b

ex r being Real st

( r > 0 & Ball (x,r) c= M ) ) );

theorem Th33: :: RUSUB_5:33

for V being RealUnitarySpace

for v being Point of V

for r, p being Real st r <= p holds

Ball (v,r) c= Ball (v,p)

for v being Point of V

for r, p being Real st r <= p holds

Ball (v,r) c= Ball (v,p)

proof end;

theorem Th34: :: RUSUB_5:34

for V being RealUnitarySpace

for v being Point of V ex r being Real st

( r > 0 & Ball (v,r) c= the carrier of V )

for v being Point of V ex r being Real st

( r > 0 & Ball (v,r) c= the carrier of V )

proof end;

theorem Th35: :: RUSUB_5:35

for V being RealUnitarySpace

for v, u being Point of V

for r being Real st u in Ball (v,r) holds

ex p being Real st

( p > 0 & Ball (u,p) c= Ball (v,r) )

for v, u being Point of V

for r being Real st u in Ball (v,r) holds

ex p being Real st

( p > 0 & Ball (u,p) c= Ball (v,r) )

proof end;

theorem :: RUSUB_5:36

for V being RealUnitarySpace

for u, v, w being Point of V

for r, p being Real st v in (Ball (u,r)) /\ (Ball (w,p)) holds

ex q being Real st

( Ball (v,q) c= Ball (u,r) & Ball (v,q) c= Ball (w,p) )

for u, v, w being Point of V

for r, p being Real st v in (Ball (u,r)) /\ (Ball (w,p)) holds

ex q being Real st

( Ball (v,q) c= Ball (u,r) & Ball (v,q) c= Ball (w,p) )

proof end;

theorem Th37: :: RUSUB_5:37

for V being RealUnitarySpace

for v being Point of V

for r being Real holds Ball (v,r) in Family_open_set V

for v being Point of V

for r being Real holds Ball (v,r) in Family_open_set V

proof end;

theorem Th39: :: RUSUB_5:39

for V being RealUnitarySpace

for M, N being Subset of V st M in Family_open_set V & N in Family_open_set V holds

M /\ N in Family_open_set V

for M, N being Subset of V st M in Family_open_set V & N in Family_open_set V holds

M /\ N in Family_open_set V

proof end;

theorem Th40: :: RUSUB_5:40

for V being RealUnitarySpace

for A being Subset-Family of V st A c= Family_open_set V holds

union A in Family_open_set V

for A being Subset-Family of V st A c= Family_open_set V holds

union A in Family_open_set V

proof end;

definition

let V be RealUnitarySpace;

TopStruct(# the carrier of V,(Family_open_set V) #) is TopStruct ;

end;
func TopUnitSpace V -> TopStruct equals :: RUSUB_5:def 6

TopStruct(# the carrier of V,(Family_open_set V) #);

coherence TopStruct(# the carrier of V,(Family_open_set V) #);

TopStruct(# the carrier of V,(Family_open_set V) #) is TopStruct ;

:: deftheorem defines TopUnitSpace RUSUB_5:def 6 :

for V being RealUnitarySpace holds TopUnitSpace V = TopStruct(# the carrier of V,(Family_open_set V) #);

for V being RealUnitarySpace holds TopUnitSpace V = TopStruct(# the carrier of V,(Family_open_set V) #);

theorem :: RUSUB_5:42

for V being RealUnitarySpace

for M being Subset of (TopUnitSpace V) st M = [#] V holds

( M is open & M is closed )

for M being Subset of (TopUnitSpace V) st M = [#] V holds

( M is open & M is closed )

proof end;

theorem :: RUSUB_5:43

for V being RealUnitarySpace

for M being Subset of (TopUnitSpace V) st M = {} V holds

( M is open & M is closed ) ;

for M being Subset of (TopUnitSpace V) st M = {} V holds

( M is open & M is closed ) ;

theorem :: RUSUB_5:44

for V being RealUnitarySpace

for v being VECTOR of V

for r being Real st the carrier of V = {(0. V)} & r <> 0 holds

Sphere (v,r) is empty

for v being VECTOR of V

for r being Real st the carrier of V = {(0. V)} & r <> 0 holds

Sphere (v,r) is empty

proof end;

theorem :: RUSUB_5:45

for V being RealUnitarySpace

for v being VECTOR of V

for r being Real st the carrier of V <> {(0. V)} & r > 0 holds

not Sphere (v,r) is empty

for v being VECTOR of V

for r being Real st the carrier of V <> {(0. V)} & r > 0 holds

not Sphere (v,r) is empty

proof end;

theorem :: RUSUB_5:46

for V being RealUnitarySpace

for v being VECTOR of V

for r being Real st r = 0 holds

Ball (v,r) is empty

for v being VECTOR of V

for r being Real st r = 0 holds

Ball (v,r) is empty

proof end;

theorem :: RUSUB_5:47

for V being RealUnitarySpace

for v being VECTOR of V

for r being Real st the carrier of V = {(0. V)} & r > 0 holds

Ball (v,r) = {(0. V)}

for v being VECTOR of V

for r being Real st the carrier of V = {(0. V)} & r > 0 holds

Ball (v,r) = {(0. V)}

proof end;

theorem :: RUSUB_5:48

for V being RealUnitarySpace

for v being VECTOR of V

for r being Real st the carrier of V <> {(0. V)} & r > 0 holds

ex w being VECTOR of V st

( w <> v & w in Ball (v,r) )

for v being VECTOR of V

for r being Real st the carrier of V <> {(0. V)} & r > 0 holds

ex w being VECTOR of V st

( w <> v & w in Ball (v,r) )

proof end;

theorem :: RUSUB_5:49

for V being RealUnitarySpace holds

( the carrier of V = the carrier of (TopUnitSpace V) & the topology of (TopUnitSpace V) = Family_open_set V ) ;

( the carrier of V = the carrier of (TopUnitSpace V) & the topology of (TopUnitSpace V) = Family_open_set V ) ;

theorem Th50: :: RUSUB_5:50

for V being RealUnitarySpace

for M being Subset of (TopUnitSpace V)

for r being Real

for v being Point of V st M = Ball (v,r) holds

M is open

for M being Subset of (TopUnitSpace V)

for r being Real

for v being Point of V st M = Ball (v,r) holds

M is open

proof end;

theorem :: RUSUB_5:51

for V being RealUnitarySpace

for M being Subset of (TopUnitSpace V) holds

( M is open iff for v being Point of V st v in M holds

ex r being Real st

( r > 0 & Ball (v,r) c= M ) )

for M being Subset of (TopUnitSpace V) holds

( M is open iff for v being Point of V st v in M holds

ex r being Real st

( r > 0 & Ball (v,r) c= M ) )

proof end;

theorem :: RUSUB_5:52

for V being RealUnitarySpace

for v1, v2 being Point of V

for r1, r2 being Real ex u being Point of V ex r being Real st (Ball (v1,r1)) \/ (Ball (v2,r2)) c= Ball (u,r)

for v1, v2 being Point of V

for r1, r2 being Real ex u being Point of V ex r being Real st (Ball (v1,r1)) \/ (Ball (v2,r2)) c= Ball (u,r)

proof end;

theorem Th53: :: RUSUB_5:53

for V being RealUnitarySpace

for M being Subset of (TopUnitSpace V)

for v being VECTOR of V

for r being Real st M = cl_Ball (v,r) holds

M is closed

for M being Subset of (TopUnitSpace V)

for v being VECTOR of V

for r being Real st M = cl_Ball (v,r) holds

M is closed

proof end;

theorem :: RUSUB_5:54

for V being RealUnitarySpace

for M being Subset of (TopUnitSpace V)

for v being VECTOR of V

for r being Real st M = Sphere (v,r) holds

M is closed

for M being Subset of (TopUnitSpace V)

for v being VECTOR of V

for r being Real st M = Sphere (v,r) holds

M is closed

proof end;