:: RUSUB_5 semantic presentation
begin
definition
let V be non empty RLSStruct ;
let M, N be Affine Subset of V;
predM is_parallel_to N means :Def1: :: RUSUB_5:def 1
ex v being VECTOR of V st M = N + {v};
end;
:: 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} );
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
proof
let V be non empty right_zeroed RLSStruct ; ::_thesis: for M being Affine Subset of V holds M is_parallel_to M
let M be Affine Subset of V; ::_thesis: M is_parallel_to M
take 0. V ; :: according to RUSUB_5:def_1 ::_thesis: M = M + {(0. V)}
for x being set st x in M + {(0. V)} holds
x in M
proof
let x be set ; ::_thesis: ( x in M + {(0. V)} implies x in M )
assume x in M + {(0. V)} ; ::_thesis: x in M
then x in { (u + v) where u, v is Element of V : ( u in M & v in {(0. V)} ) } by RUSUB_4:def_9;
then consider u, v being Element of V such that
A1: ( x = u + v & u in M ) and
A2: v in {(0. V)} ;
v = 0. V by A2, TARSKI:def_1;
hence x in M by A1, RLVECT_1:def_4; ::_thesis: verum
end;
then A3: M + {(0. V)} c= M by TARSKI:def_3;
for x being set st x in M holds
x in M + {(0. V)}
proof
let x be set ; ::_thesis: ( x in M implies x in M + {(0. V)} )
assume A4: x in M ; ::_thesis: x in M + {(0. V)}
then reconsider x = x as Element of V ;
( x = x + (0. V) & 0. V in {(0. V)} ) by RLVECT_1:def_4, TARSKI:def_1;
then x in { (u + v) where u, v is Element of V : ( u in M & v in {(0. V)} ) } by A4;
hence x in M + {(0. V)} by RUSUB_4:def_9; ::_thesis: verum
end;
then M c= M + {(0. V)} by TARSKI:def_3;
hence M = M + {(0. V)} by A3, XBOOLE_0:def_10; ::_thesis: verum
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
proof
let V be non empty right_complementable add-associative right_zeroed RLSStruct ; ::_thesis: for M, N being Affine Subset of V st M is_parallel_to N holds
N is_parallel_to M
let M, N be Affine Subset of V; ::_thesis: ( M is_parallel_to N implies N is_parallel_to M )
assume M is_parallel_to N ; ::_thesis: N is_parallel_to M
then consider w1 being VECTOR of V such that
A1: M = N + {w1} by Def1;
set w2 = - w1;
for x being set st x in N holds
x in M + {(- w1)}
proof
let x be set ; ::_thesis: ( x in N implies x in M + {(- w1)} )
assume A2: x in N ; ::_thesis: x in M + {(- w1)}
then reconsider x = x as Element of V ;
set y = x + w1;
w1 in {w1} by TARSKI:def_1;
then x + w1 in { (u + v) where u, v is Element of V : ( u in N & v in {w1} ) } by A2;
then A3: x + w1 in M by A1, RUSUB_4:def_9;
x + (w1 + (- w1)) = (x + w1) + (- w1) by RLVECT_1:def_3;
then x + (0. V) = (x + w1) + (- w1) by RLVECT_1:5;
then A4: x = (x + w1) + (- w1) by RLVECT_1:4;
- w1 in {(- w1)} by TARSKI:def_1;
then x in { (u + v) where u, v is Element of V : ( u in M & v in {(- w1)} ) } by A3, A4;
hence x in M + {(- w1)} by RUSUB_4:def_9; ::_thesis: verum
end;
then A5: N c= M + {(- w1)} by TARSKI:def_3;
take - w1 ; :: according to RUSUB_5:def_1 ::_thesis: N = M + {(- w1)}
for x being set st x in M + {(- w1)} holds
x in N
proof
let x be set ; ::_thesis: ( x in M + {(- w1)} implies x in N )
assume A6: x in M + {(- w1)} ; ::_thesis: x in N
then x in { (u + v) where u, v is Element of V : ( u in M & v in {(- w1)} ) } by RUSUB_4:def_9;
then consider u9, v9 being Element of V such that
A7: x = u9 + v9 and
A8: u9 in M and
A9: v9 in {(- w1)} ;
reconsider x = x as Element of V by A6;
x = u9 + (- w1) by A7, A9, TARSKI:def_1;
then x + w1 = u9 + ((- w1) + w1) by RLVECT_1:def_3;
then A10: x + w1 = u9 + (0. V) by RLVECT_1:5;
u9 in { (u + v) where u, v is Element of V : ( u in N & v in {w1} ) } by A1, A8, RUSUB_4:def_9;
then consider u1, v1 being Element of V such that
A11: ( u9 = u1 + v1 & u1 in N ) and
A12: v1 in {w1} ;
w1 = v1 by A12, TARSKI:def_1;
hence x in N by A10, A11, RLVECT_1:4, RLVECT_1:8; ::_thesis: verum
end;
then M + {(- w1)} c= N by TARSKI:def_3;
hence N = M + {(- w1)} by A5, XBOOLE_0:def_10; ::_thesis: verum
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
proof
let V be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: 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
let M, L, N be Affine Subset of V; ::_thesis: ( M is_parallel_to L & L is_parallel_to N implies M is_parallel_to N )
assume that
A1: M is_parallel_to L and
A2: L is_parallel_to N ; ::_thesis: M is_parallel_to N
consider v1 being Element of V such that
A3: M = L + {v1} by A1, Def1;
consider u1 being Element of V such that
A4: L = N + {u1} by A2, Def1;
set w = u1 + v1;
for x being set st x in N + {(u1 + v1)} holds
x in M
proof
let x be set ; ::_thesis: ( x in N + {(u1 + v1)} implies x in M )
A5: u1 in {u1} by TARSKI:def_1;
assume A6: x in N + {(u1 + v1)} ; ::_thesis: x in M
then reconsider x = x as Element of V ;
x in { (u + v) where u, v is Element of V : ( u in N & v in {(u1 + v1)} ) } by A6, RUSUB_4:def_9;
then consider u2, v2 being Element of V such that
A7: x = u2 + v2 and
A8: u2 in N and
A9: v2 in {(u1 + v1)} ;
x = u2 + (u1 + v1) by A7, A9, TARSKI:def_1
.= (u2 + u1) + v1 by RLVECT_1:def_3 ;
then x - v1 = (u2 + u1) + (v1 - v1) by RLVECT_1:def_3
.= (u2 + u1) + (0. V) by RLVECT_1:15
.= u2 + u1 by RLVECT_1:4 ;
then x - v1 in { (u + v) where u, v is Element of V : ( u in N & v in {u1} ) } by A8, A5;
then A10: x - v1 in L by A4, RUSUB_4:def_9;
set y = x - v1;
A11: v1 in {v1} by TARSKI:def_1;
(x - v1) + v1 = x - (v1 - v1) by RLVECT_1:29
.= x - (0. V) by RLVECT_1:15
.= x by RLVECT_1:13 ;
then x in { (u + v) where u, v is Element of V : ( u in L & v in {v1} ) } by A10, A11;
hence x in M by A3, RUSUB_4:def_9; ::_thesis: verum
end;
then A12: N + {(u1 + v1)} c= M by TARSKI:def_3;
for x being set st x in M holds
x in N + {(u1 + v1)}
proof
let x be set ; ::_thesis: ( x in M implies x in N + {(u1 + v1)} )
A13: u1 + v1 in {(u1 + v1)} by TARSKI:def_1;
assume A14: x in M ; ::_thesis: x in N + {(u1 + v1)}
then reconsider x = x as Element of V ;
x in { (u + v) where u, v is Element of V : ( u in L & v in {v1} ) } by A3, A14, RUSUB_4:def_9;
then consider u2, v2 being Element of V such that
A15: x = u2 + v2 and
A16: u2 in L and
A17: v2 in {v1} ;
A18: v2 = v1 by A17, TARSKI:def_1;
u2 in { (u + v) where u, v is Element of V : ( u in N & v in {u1} ) } by A4, A16, RUSUB_4:def_9;
then consider u3, v3 being Element of V such that
A19: u2 = u3 + v3 and
A20: u3 in N and
A21: v3 in {u1} ;
v3 = u1 by A21, TARSKI:def_1;
then x = u3 + (u1 + v1) by A15, A19, A18, RLVECT_1:def_3;
then x in { (u + v) where u, v is Element of V : ( u in N & v in {(u1 + v1)} ) } by A20, A13;
hence x in N + {(u1 + v1)} by RUSUB_4:def_9; ::_thesis: verum
end;
then M c= N + {(u1 + v1)} by TARSKI:def_3;
then M = N + {(u1 + v1)} by A12, XBOOLE_0:def_10;
hence M is_parallel_to N by Def1; ::_thesis: verum
end;
definition
let V be non empty addLoopStr ;
let M, N be Subset of V;
funcM - 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 ) } is Subset of V
proof
defpred S1[ set , set ] means ( $1 in M & $2 in N );
deffunc H1( Element of V, Element of V) -> Element of the carrier of V = $1 - $2;
{ H1(u,v) where u, v is Element of V : S1[u,v] } is Subset of V from DOMAIN_1:sch_9();
hence { (u - v) where u, v is Element of V : ( u in M & v in N ) } is Subset of V ; ::_thesis: verum
end;
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 ) } ;
theorem Th4: :: RUSUB_5:4
for V being RealLinearSpace
for M, N being Affine Subset of V holds M - N is Affine
proof
let V be RealLinearSpace; ::_thesis: for M, N being Affine Subset of V holds M - N is Affine
let M, N be Affine Subset of V; ::_thesis: M - N is Affine
for x, y being VECTOR of V
for a being Real st x in M - N & y in M - N holds
((1 - a) * x) + (a * y) in M - N
proof
let x, y be VECTOR of V; ::_thesis: for a being Real st x in M - N & y in M - N holds
((1 - a) * x) + (a * y) in M - N
let a be Real; ::_thesis: ( x in M - N & y in M - N implies ((1 - a) * x) + (a * y) in M - N )
assume that
A1: x in M - N and
A2: y in M - N ; ::_thesis: ((1 - a) * x) + (a * y) in M - N
consider u1, v1 being Element of V such that
A3: x = u1 - v1 and
A4: ( u1 in M & v1 in N ) by A1;
consider u2, v2 being Element of V such that
A5: y = u2 - v2 and
A6: ( u2 in M & v2 in N ) by A2;
A7: ((1 - a) * x) + (a * y) = (((1 - a) * u1) - ((1 - a) * v1)) + (a * (u2 - v2)) by A3, A5, RLVECT_1:34
.= (((1 - a) * u1) - ((1 - a) * v1)) + ((a * u2) - (a * v2)) by RLVECT_1:34
.= ((((1 - a) * u1) + (- ((1 - a) * v1))) + (a * u2)) - (a * v2) by RLVECT_1:def_3
.= ((((1 - a) * u1) + (a * u2)) + (- ((1 - a) * v1))) + (- (a * v2)) by RLVECT_1:def_3
.= (((1 - a) * u1) + (a * u2)) + ((- ((1 - a) * v1)) + (- (a * v2))) by RLVECT_1:def_3
.= (((1 - a) * u1) + (a * u2)) - (((1 - a) * v1) + (a * v2)) by RLVECT_1:31 ;
( ((1 - a) * u1) + (a * u2) in M & ((1 - a) * v1) + (a * v2) in N ) by A4, A6, RUSUB_4:def_4;
hence ((1 - a) * x) + (a * y) in M - N by A7; ::_thesis: verum
end;
hence M - N is Affine by RUSUB_4:def_4; ::_thesis: verum
end;
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
proof
let V be non empty addLoopStr ; ::_thesis: for M, N being Subset of V st ( M is empty or N is empty ) holds
M + N is empty
let M, N be Subset of V; ::_thesis: ( ( M is empty or N is empty ) implies M + N is empty )
assume A1: ( M is empty or N is empty ) ; ::_thesis: M + N is empty
assume not M + N is empty ; ::_thesis: contradiction
then consider x being set such that
A2: x in M + N by XBOOLE_0:def_1;
x in { (u + v) where u, v is Element of V : ( u in M & v in N ) } by A2, RUSUB_4:def_9;
then ex u, v being Element of V st
( x = u + v & u in M & v in N ) ;
hence contradiction by A1; ::_thesis: verum
end;
theorem :: RUSUB_5:6
for V being non empty addLoopStr
for M, N being non empty Subset of V holds not M + N is empty
proof
let V be non empty addLoopStr ; ::_thesis: for M, N being non empty Subset of V holds not M + N is empty
let M, N be non empty Subset of V; ::_thesis: not M + N is empty
consider x being set such that
A1: x in M by XBOOLE_0:def_1;
consider y being set such that
A2: y in N by XBOOLE_0:def_1;
reconsider x = x, y = y as Element of V by A1, A2;
x + y in { (u + v) where u, v is Element of V : ( u in M & v in N ) } by A1, A2;
hence not M + N is empty by RUSUB_4:def_9; ::_thesis: verum
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
proof
let V be non empty addLoopStr ; ::_thesis: for M, N being Subset of V st ( M is empty or N is empty ) holds
M - N is empty
let M, N be Subset of V; ::_thesis: ( ( M is empty or N is empty ) implies M - N is empty )
assume A1: ( M is empty or N is empty ) ; ::_thesis: M - N is empty
assume not M - N is empty ; ::_thesis: contradiction
then consider x being set such that
A2: x in M - N by XBOOLE_0:def_1;
ex u, v being Element of V st
( x = u - v & u in M & v in N ) by A2;
hence contradiction by A1; ::_thesis: verum
end;
theorem Th8: :: RUSUB_5:8
for V being non empty addLoopStr
for M, N being non empty Subset of V holds not M - N is empty
proof
let V be non empty addLoopStr ; ::_thesis: for M, N being non empty Subset of V holds not M - N is empty
let M, N be non empty Subset of V; ::_thesis: not M - N is empty
consider x being set such that
A1: x in M by XBOOLE_0:def_1;
consider y being set such that
A2: y in N by XBOOLE_0:def_1;
reconsider x = x, y = y as Element of V by A1, A2;
x - y in { (u - v) where u, v is Element of V : ( u in M & v in N ) } by A1, A2;
hence not M - N is empty ; ::_thesis: verum
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 )
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for M, N being Subset of V
for v being Element of V holds
( M = N + {v} iff M - {v} = N )
let M, N be Subset of V; ::_thesis: for v being Element of V holds
( M = N + {v} iff M - {v} = N )
let v be Element of V; ::_thesis: ( M = N + {v} iff M - {v} = N )
A1: ( M - {v} = N implies M = N + {v} )
proof
assume A2: M - {v} = N ; ::_thesis: M = N + {v}
for x being set st x in N + {v} holds
x in M
proof
let x be set ; ::_thesis: ( x in N + {v} implies x in M )
assume A3: x in N + {v} ; ::_thesis: x in M
then reconsider x = x as Element of V ;
x in { (u1 + v1) where u1, v1 is Element of V : ( u1 in N & v1 in {v} ) } by A3, RUSUB_4:def_9;
then consider u1, v1 being Element of V such that
A4: x = u1 + v1 and
A5: u1 in N and
A6: v1 in {v} ;
A7: x - v1 = u1 + (v1 - v1) by A4, RLVECT_1:def_3
.= u1 + (0. V) by RLVECT_1:15
.= u1 by RLVECT_1:4 ;
v1 = v by A6, TARSKI:def_1;
then consider u2, v2 being Element of V such that
A8: x - v = u2 - v2 and
A9: u2 in M and
A10: v2 in {v} by A2, A5, A7;
v2 = v by A10, TARSKI:def_1;
then (x - v) + v = u2 - (v - v) by A8, RLVECT_1:29
.= u2 - (0. V) by RLVECT_1:15
.= u2 by RLVECT_1:13 ;
then u2 = x - (v - v) by RLVECT_1:29
.= x - (0. V) by RLVECT_1:15 ;
hence x in M by A9, RLVECT_1:13; ::_thesis: verum
end;
then A11: N + {v} c= M by TARSKI:def_3;
for x being set st x in M holds
x in N + {v}
proof
let x be set ; ::_thesis: ( x in M implies x in N + {v} )
assume A12: x in M ; ::_thesis: x in N + {v}
then reconsider x = x as Element of V ;
A13: v in {v} by TARSKI:def_1;
then x - v in { (u2 - v2) where u2, v2 is Element of V : ( u2 in M & v2 in {v} ) } by A12;
then consider u2 being Element of V such that
A14: x - v = u2 and
A15: u2 in N by A2;
u2 + v = x - (v - v) by A14, RLVECT_1:29
.= x - (0. V) by RLVECT_1:15
.= x by RLVECT_1:13 ;
then x in { (u1 + v1) where u1, v1 is Element of V : ( u1 in N & v1 in {v} ) } by A13, A15;
hence x in N + {v} by RUSUB_4:def_9; ::_thesis: verum
end;
then M c= N + {v} by TARSKI:def_3;
hence M = N + {v} by A11, XBOOLE_0:def_10; ::_thesis: verum
end;
( M = N + {v} implies M - {v} = N )
proof
assume A16: M = N + {v} ; ::_thesis: M - {v} = N
for x being set st x in M - {v} holds
x in N
proof
let x be set ; ::_thesis: ( x in M - {v} implies x in N )
assume A17: x in M - {v} ; ::_thesis: x in N
then reconsider x = x as Element of V ;
consider u1, v1 being Element of V such that
A18: x = u1 - v1 and
A19: u1 in M and
A20: v1 in {v} by A17;
A21: x + v1 = u1 - (v1 - v1) by A18, RLVECT_1:29
.= u1 - (0. V) by RLVECT_1:15
.= u1 by RLVECT_1:13 ;
v1 = v by A20, TARSKI:def_1;
then x + v in { (u2 + v2) where u2, v2 is Element of V : ( u2 in N & v2 in {v} ) } by A16, A19, A21, RUSUB_4:def_9;
then consider u2, v2 being Element of V such that
A22: ( x + v = u2 + v2 & u2 in N ) and
A23: v2 in {v} ;
v2 = v by A23, TARSKI:def_1;
hence x in N by A22, RLVECT_1:8; ::_thesis: verum
end;
then A24: M - {v} c= N by TARSKI:def_3;
for x being set st x in N holds
x in M - {v}
proof
let x be set ; ::_thesis: ( x in N implies x in M - {v} )
assume A25: x in N ; ::_thesis: x in M - {v}
then reconsider x = x as Element of V ;
A26: v in {v} by TARSKI:def_1;
then x + v in { (u2 + v2) where u2, v2 is Element of V : ( u2 in N & v2 in {v} ) } by A25;
then x + v in M by A16, RUSUB_4:def_9;
then consider u2 being Element of V such that
A27: x + v = u2 and
A28: u2 in M ;
u2 - v = x + (v - v) by A27, RLVECT_1:def_3
.= x + (0. V) by RLVECT_1:15
.= x by RLVECT_1:4 ;
hence x in M - {v} by A26, A28; ::_thesis: verum
end;
then N c= M - {v} by TARSKI:def_3;
hence M - {v} = N by A24, XBOOLE_0:def_10; ::_thesis: verum
end;
hence ( M = N + {v} iff M - {v} = N ) by A1; ::_thesis: verum
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
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for M, N being Subset of V
for v being Element of V st v in N holds
M + {v} c= M + N
let M, N be Subset of V; ::_thesis: for v being Element of V st v in N holds
M + {v} c= M + N
let v be Element of V; ::_thesis: ( v in N implies M + {v} c= M + N )
assume A1: v in N ; ::_thesis: M + {v} c= M + N
for x being set st x in M + {v} holds
x in M + N
proof
let x be set ; ::_thesis: ( x in M + {v} implies x in M + N )
assume A2: x in M + {v} ; ::_thesis: x in M + N
then reconsider x = x as Element of V ;
x in { (u1 + v1) where u1, v1 is Element of V : ( u1 in M & v1 in {v} ) } by A2, RUSUB_4:def_9;
then consider u2, v2 being Element of V such that
A3: x = u2 + v2 and
A4: u2 in M and
A5: v2 in {v} ;
x = u2 + v by A3, A5, TARSKI:def_1;
then x in { (u1 + v1) where u1, v1 is Element of V : ( u1 in M & v1 in N ) } by A1, A4;
hence x in M + N by RUSUB_4:def_9; ::_thesis: verum
end;
hence M + {v} c= M + N by TARSKI:def_3; ::_thesis: verum
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
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for M, N being Subset of V
for v being Element of V st v in N holds
M - {v} c= M - N
let M, N be Subset of V; ::_thesis: for v being Element of V st v in N holds
M - {v} c= M - N
let v be Element of V; ::_thesis: ( v in N implies M - {v} c= M - N )
assume A1: v in N ; ::_thesis: M - {v} c= M - N
for x being set st x in M - {v} holds
x in M - N
proof
let x be set ; ::_thesis: ( x in M - {v} implies x in M - N )
assume A2: x in M - {v} ; ::_thesis: x in M - N
then reconsider x = x as Element of V ;
consider u2, v2 being Element of V such that
A3: x = u2 - v2 and
A4: u2 in M and
A5: v2 in {v} by A2;
x = u2 - v by A3, A5, TARSKI:def_1;
hence x in M - N by A1, A4; ::_thesis: verum
end;
hence M - {v} c= M - N by TARSKI:def_3; ::_thesis: verum
end;
theorem Th12: :: RUSUB_5:12
for V being RealLinearSpace
for M being non empty Subset of V holds 0. V in M - M
proof
let V be RealLinearSpace; ::_thesis: for M being non empty Subset of V holds 0. V in M - M
let M be non empty Subset of V; ::_thesis: 0. V in M - M
consider v being set such that
A1: v in M by XBOOLE_0:def_1;
reconsider v = v as Element of V by A1;
v - v in { (u1 - v1) where u1, v1 is Element of V : ( u1 in M & v1 in M ) } by A1;
hence 0. V in M - M by RLVECT_1:15; ::_thesis: verum
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
proof
let V be RealLinearSpace; ::_thesis: 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
let M be non empty Affine Subset of V; ::_thesis: for v being VECTOR of V st M is Subspace-like & v in M holds
M + {v} c= M
let v be VECTOR of V; ::_thesis: ( M is Subspace-like & v in M implies M + {v} c= M )
assume A1: ( M is Subspace-like & v in M ) ; ::_thesis: M + {v} c= M
for x being set st x in M + {v} holds
x in M
proof
let x be set ; ::_thesis: ( x in M + {v} implies x in M )
assume A2: x in M + {v} ; ::_thesis: x in M
then reconsider x = x as Element of V ;
x in { (u1 + v1) where u1, v1 is Element of V : ( u1 in M & v1 in {v} ) } by A2, RUSUB_4:def_9;
then consider u1, v1 being Element of V such that
A3: ( x = u1 + v1 & u1 in M ) and
A4: v1 in {v} ;
v1 = v by A4, TARSKI:def_1;
hence x in M by A1, A3, RUSUB_4:def_7; ::_thesis: verum
end;
hence M + {v} c= M by TARSKI:def_3; ::_thesis: verum
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
proof
let V be RealLinearSpace; ::_thesis: 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
let M, N1, N2 be non empty Affine Subset of V; ::_thesis: ( N1 is Subspace-like & N2 is Subspace-like & M is_parallel_to N1 & M is_parallel_to N2 implies N1 = N2 )
assume that
A1: N1 is Subspace-like and
A2: N2 is Subspace-like and
A3: M is_parallel_to N1 and
A4: M is_parallel_to N2 ; ::_thesis: N1 = N2
N2 is_parallel_to M by A4, Th2;
then N2 is_parallel_to N1 by A3, Th3;
then consider v2 being VECTOR of V such that
A5: N2 = N1 + {v2} by Def1;
N1 is_parallel_to M by A3, Th2;
then N1 is_parallel_to N2 by A4, Th3;
then consider v1 being VECTOR of V such that
A6: N1 = N2 + {v1} by Def1;
0. V in N2 by A2, RUSUB_4:def_7;
then 0. V in { (p + q) where p, q is Element of V : ( p in N1 & q in {v2} ) } by A5, RUSUB_4:def_9;
then consider p2, q2 being Element of V such that
A7: 0. V = p2 + q2 and
A8: p2 in N1 and
A9: q2 in {v2} ;
0. V = p2 + v2 by A7, A9, TARSKI:def_1;
then A10: - v2 in N1 by A8, RLVECT_1:6;
v2 = - (- v2) by RLVECT_1:17
.= (- 1) * (- v2) by RLVECT_1:16 ;
then v2 in N1 by A1, A10, RUSUB_4:def_7;
then A11: N2 c= N1 by A1, A5, Th13;
0. V in N1 by A1, RUSUB_4:def_7;
then 0. V in { (p + q) where p, q is Element of V : ( p in N2 & q in {v1} ) } by A6, RUSUB_4:def_9;
then consider p1, q1 being Element of V such that
A12: 0. V = p1 + q1 and
A13: p1 in N2 and
A14: q1 in {v1} ;
0. V = p1 + v1 by A12, A14, TARSKI:def_1;
then A15: - v1 in N2 by A13, RLVECT_1:6;
v1 = - (- v1) by RLVECT_1:17
.= (- 1) * (- v1) by RLVECT_1:16 ;
then v1 in N2 by A2, A15, RUSUB_4:def_7;
then N1 c= N2 by A2, A6, Th13;
hence N1 = N2 by A11, XBOOLE_0:def_10; ::_thesis: verum
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}
proof
let V be RealLinearSpace; ::_thesis: 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}
let M be non empty Affine Subset of V; ::_thesis: for v being VECTOR of V st v in M holds
0. V in M - {v}
let v be VECTOR of V; ::_thesis: ( v in M implies 0. V in M - {v} )
A1: ( v in {v} & 0. V = v - v ) by RLVECT_1:15, TARSKI:def_1;
assume v in M ; ::_thesis: 0. V in M - {v}
hence 0. V in M - {v} by A1; ::_thesis: verum
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 )
proof
let V be RealLinearSpace; ::_thesis: 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 )
let M be non empty Affine Subset of V; ::_thesis: 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 )
let v be VECTOR of V; ::_thesis: ( v in M implies ex N being non empty Affine Subset of V st
( N = M - {v} & M is_parallel_to N & N is Subspace-like ) )
( not {v} is empty & {v} is Affine ) by RUSUB_4:23;
then reconsider N = M - {v} as non empty Affine Subset of V by Th4, Th8;
assume v in M ; ::_thesis: ex N being non empty Affine Subset of V st
( N = M - {v} & M is_parallel_to N & N is Subspace-like )
then A1: 0. V in N by Th15;
take N ; ::_thesis: ( N = M - {v} & M is_parallel_to N & N is Subspace-like )
M is_parallel_to N
proof
take v ; :: according to RUSUB_5:def_1 ::_thesis: M = N + {v}
thus M = N + {v} by Th9; ::_thesis: verum
end;
hence ( N = M - {v} & M is_parallel_to N & N is Subspace-like ) by A1, RUSUB_4:26; ::_thesis: verum
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}
proof
let V be RealLinearSpace; ::_thesis: 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}
let M be non empty Affine Subset of V; ::_thesis: for u, v being VECTOR of V st u in M & v in M holds
M - {v} = M - {u}
let u, v be VECTOR of V; ::_thesis: ( u in M & v in M implies M - {v} = M - {u} )
assume ( u in M & v in M ) ; ::_thesis: M - {v} = M - {u}
then ( ex N1 being non empty Affine Subset of V st
( N1 = M - {u} & M is_parallel_to N1 & N1 is Subspace-like ) & ex N2 being non empty Affine Subset of V st
( N2 = M - {v} & M is_parallel_to N2 & N2 is Subspace-like ) ) by Th16;
hence M - {v} = M - {u} by Th14; ::_thesis: verum
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 }
proof
let V be RealLinearSpace; ::_thesis: for M being non empty Affine Subset of V holds M - M = union { (M - {v}) where v is VECTOR of V : v in M }
let M be non empty Affine Subset of V; ::_thesis: M - M = union { (M - {v}) where v is VECTOR of V : v in M }
for x being set st x in M - M holds
x in union { (M - {v}) where v is VECTOR of V : v in M }
proof
let x be set ; ::_thesis: ( x in M - M implies x in union { (M - {v}) where v is VECTOR of V : v in M } )
assume A1: x in M - M ; ::_thesis: x in union { (M - {v}) where v is VECTOR of V : v in M }
then reconsider x = x as Element of V ;
consider u1, v1 being Element of V such that
A2: ( x = u1 - v1 & u1 in M ) and
A3: v1 in M by A1;
v1 in {v1} by TARSKI:def_1;
then A4: x in { (p - q) where p, q is Element of V : ( p in M & q in {v1} ) } by A2;
M - {v1} in { (M - {v}) where v is VECTOR of V : v in M } by A3;
hence x in union { (M - {v}) where v is VECTOR of V : v in M } by A4, TARSKI:def_4; ::_thesis: verum
end;
then A5: M - M c= union { (M - {v}) where v is VECTOR of V : v in M } by TARSKI:def_3;
for x being set st x in union { (M - {v}) where v is VECTOR of V : v in M } holds
x in M - M
proof
let x be set ; ::_thesis: ( x in union { (M - {v}) where v is VECTOR of V : v in M } implies x in M - M )
assume x in union { (M - {v}) where v is VECTOR of V : v in M } ; ::_thesis: x in M - M
then consider N being set such that
A6: x in N and
A7: N in { (M - {v}) where v is VECTOR of V : v in M } by TARSKI:def_4;
consider v1 being VECTOR of V such that
A8: N = M - {v1} and
A9: v1 in M by A7;
consider p1, q1 being Element of V such that
A10: ( x = p1 - q1 & p1 in M ) and
A11: q1 in {v1} by A6, A8;
q1 = v1 by A11, TARSKI:def_1;
hence x in M - M by A9, A10; ::_thesis: verum
end;
then union { (M - {v}) where v is VECTOR of V : v in M } c= M - M by TARSKI:def_3;
hence M - M = union { (M - {v}) where v is VECTOR of V : v in M } by A5, XBOOLE_0:def_10; ::_thesis: verum
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 }
proof
let V be RealLinearSpace; ::_thesis: 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 }
let M be non empty Affine Subset of V; ::_thesis: 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 }
let v be VECTOR of V; ::_thesis: ( v in M implies M - {v} = union { (M - {u}) where u is VECTOR of V : u in M } )
assume A1: v in M ; ::_thesis: M - {v} = union { (M - {u}) where u is VECTOR of V : u in M }
for x being set st x in union { (M - {u}) where u is VECTOR of V : u in M } holds
x in M - {v}
proof
let x be set ; ::_thesis: ( x in union { (M - {u}) where u is VECTOR of V : u in M } implies x in M - {v} )
assume x in union { (M - {u}) where u is VECTOR of V : u in M } ; ::_thesis: x in M - {v}
then consider N being set such that
A2: x in N and
A3: N in { (M - {u}) where u is VECTOR of V : u in M } by TARSKI:def_4;
ex v1 being VECTOR of V st
( N = M - {v1} & v1 in M ) by A3;
hence x in M - {v} by A1, A2, Th17; ::_thesis: verum
end;
then A4: union { (M - {u}) where u is VECTOR of V : u in M } c= M - {v} by TARSKI:def_3;
for x being set st x in M - {v} holds
x in union { (M - {u}) where u is VECTOR of V : u in M }
proof
let x be set ; ::_thesis: ( x in M - {v} implies x in union { (M - {u}) where u is VECTOR of V : u in M } )
assume A5: x in M - {v} ; ::_thesis: x in union { (M - {u}) where u is VECTOR of V : u in M }
M - {v} in { (M - {u}) where u is VECTOR of V : u in M } by A1;
hence x in union { (M - {u}) where u is VECTOR of V : u in M } by A5, TARSKI:def_4; ::_thesis: verum
end;
then M - {v} c= union { (M - {u}) where u is VECTOR of V : u in M } by TARSKI:def_3;
hence M - {v} = union { (M - {u}) where u is VECTOR of V : u in M } by A4, XBOOLE_0:def_10; ::_thesis: verum
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 )
proof
let V be RealLinearSpace; ::_thesis: 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 )
let M be non empty Affine Subset of V; ::_thesis: ex L being non empty Affine Subset of V st
( L = M - M & L is Subspace-like & M is_parallel_to L )
reconsider L = M - M as non empty Affine Subset of V by Th4, Th8;
consider v being set such that
A1: v in M by XBOOLE_0:def_1;
reconsider v = v as VECTOR of V by A1;
take L ; ::_thesis: ( L = M - M & L is Subspace-like & M is_parallel_to L )
A2: 0. V in L by Th12;
( not {v} is empty & {v} is Affine ) by RUSUB_4:23;
then reconsider N = M - {v} as non empty Affine Subset of V by Th4, Th8;
A3: M is_parallel_to N
proof
take v ; :: according to RUSUB_5:def_1 ::_thesis: M = N + {v}
thus M = N + {v} by Th9; ::_thesis: verum
end;
N = union { (M - {u}) where u is VECTOR of V : u in M } by A1, Th19
.= L by Th18 ;
hence ( L = M - M & L is Subspace-like & M is_parallel_to L ) by A3, A2, RUSUB_4:26; ::_thesis: verum
end;
begin
definition
let V be RealUnitarySpace;
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
ex b1 being strict Subspace of V st the carrier of b1 = { v where v is VECTOR of V : for w being VECTOR of V st w in W holds
w,v are_orthogonal }
proof
defpred S1[ VECTOR of V] means for w being VECTOR of V st w in W holds
w,$1 are_orthogonal ;
reconsider A = { v where v is VECTOR of V : S1[v] } as Subset of V from DOMAIN_1:sch_7();
A1: for v, u being VECTOR of V st v in A & u in A holds
v + u in A
proof
let v, u be VECTOR of V; ::_thesis: ( v in A & u in A implies v + u in A )
assume that
A2: v in A and
A3: u in A ; ::_thesis: v + u in A
for w being VECTOR of V st w in W holds
w,v + u are_orthogonal
proof
let w be VECTOR of V; ::_thesis: ( w in W implies w,v + u are_orthogonal )
assume A4: w in W ; ::_thesis: w,v + u are_orthogonal
ex u9 being VECTOR of V st
( u = u9 & ( for w being VECTOR of V st w in W holds
w,u9 are_orthogonal ) ) by A3;
then w,u are_orthogonal by A4;
then A5: w .|. u = 0 by BHSP_1:def_3;
ex v9 being VECTOR of V st
( v = v9 & ( for w being VECTOR of V st w in W holds
w,v9 are_orthogonal ) ) by A2;
then w,v are_orthogonal by A4;
then w .|. v = 0 by BHSP_1:def_3;
then w .|. (v + u) = 0 + 0 by A5, BHSP_1:2;
hence w,v + u are_orthogonal by BHSP_1:def_3; ::_thesis: verum
end;
hence v + u in A ; ::_thesis: verum
end;
for w being VECTOR of V st w in W holds
w, 0. V are_orthogonal
proof
let w be VECTOR of V; ::_thesis: ( w in W implies w, 0. V are_orthogonal )
assume w in W ; ::_thesis: w, 0. V are_orthogonal
w .|. (0. V) = 0 by BHSP_1:15;
hence w, 0. V are_orthogonal by BHSP_1:def_3; ::_thesis: verum
end;
then A6: 0. V in A ;
for a being Real
for v being VECTOR of V st v in A holds
a * v in A
proof
let a be Real; ::_thesis: for v being VECTOR of V st v in A holds
a * v in A
let v be VECTOR of V; ::_thesis: ( v in A implies a * v in A )
assume v in A ; ::_thesis: a * v in A
then A7: ex v9 being VECTOR of V st
( v = v9 & ( for w being VECTOR of V st w in W holds
w,v9 are_orthogonal ) ) ;
for w being VECTOR of V st w in W holds
w,a * v are_orthogonal
proof
let w be VECTOR of V; ::_thesis: ( w in W implies w,a * v are_orthogonal )
assume w in W ; ::_thesis: w,a * v are_orthogonal
then A8: w,v are_orthogonal by A7;
w .|. (a * v) = a * (w .|. v) by BHSP_1:3
.= a * 0 by A8, BHSP_1:def_3 ;
hence w,a * v are_orthogonal by BHSP_1:def_3; ::_thesis: verum
end;
hence a * v in A ; ::_thesis: verum
end;
then A is linearly-closed by A1, RLSUB_1:def_1;
hence ex b1 being strict Subspace of V st the carrier of b1 = { v where v is VECTOR of V : for w being VECTOR of V st w in W holds
w,v are_orthogonal } by A6, RUSUB_1:29; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = { 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 b2 = { v where v is VECTOR of V : for w being VECTOR of V st w in W holds
w,v are_orthogonal } holds
b1 = b2 by RUSUB_1:24;
end;
:: deftheorem Def3 defines Ort_Comp RUSUB_5:def_3_:_
for V being RealUnitarySpace
for W being Subspace of V
for b3 being strict Subspace of V holds
( b3 = Ort_Comp W iff the carrier of b3 = { v where v is VECTOR of V : for w being VECTOR of V st w in W holds
w,v are_orthogonal } );
definition
let V be RealUnitarySpace;
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
ex b1 being strict Subspace of V st the carrier of b1 = { v where v is VECTOR of V : for w being VECTOR of V st w in M holds
w,v are_orthogonal }
proof
defpred S1[ VECTOR of V] means for w being VECTOR of V st w in M holds
w,$1 are_orthogonal ;
reconsider A = { v where v is VECTOR of V : S1[v] } as Subset of V from DOMAIN_1:sch_7();
A1: for v, u being VECTOR of V st v in A & u in A holds
v + u in A
proof
let v, u be VECTOR of V; ::_thesis: ( v in A & u in A implies v + u in A )
assume that
A2: v in A and
A3: u in A ; ::_thesis: v + u in A
for w being VECTOR of V st w in M holds
w,v + u are_orthogonal
proof
let w be VECTOR of V; ::_thesis: ( w in M implies w,v + u are_orthogonal )
assume A4: w in M ; ::_thesis: w,v + u are_orthogonal
ex u9 being VECTOR of V st
( u = u9 & ( for w being VECTOR of V st w in M holds
w,u9 are_orthogonal ) ) by A3;
then w,u are_orthogonal by A4;
then A5: w .|. u = 0 by BHSP_1:def_3;
ex v9 being VECTOR of V st
( v = v9 & ( for w being VECTOR of V st w in M holds
w,v9 are_orthogonal ) ) by A2;
then w,v are_orthogonal by A4;
then w .|. v = 0 by BHSP_1:def_3;
then w .|. (v + u) = 0 + 0 by A5, BHSP_1:2;
hence w,v + u are_orthogonal by BHSP_1:def_3; ::_thesis: verum
end;
hence v + u in A ; ::_thesis: verum
end;
for w being VECTOR of V st w in M holds
w, 0. V are_orthogonal
proof
let w be VECTOR of V; ::_thesis: ( w in M implies w, 0. V are_orthogonal )
assume w in M ; ::_thesis: w, 0. V are_orthogonal
w .|. (0. V) = 0 by BHSP_1:15;
hence w, 0. V are_orthogonal by BHSP_1:def_3; ::_thesis: verum
end;
then A6: 0. V in A ;
for a being Real
for v being VECTOR of V st v in A holds
a * v in A
proof
let a be Real; ::_thesis: for v being VECTOR of V st v in A holds
a * v in A
let v be VECTOR of V; ::_thesis: ( v in A implies a * v in A )
assume v in A ; ::_thesis: a * v in A
then A7: ex v9 being VECTOR of V st
( v = v9 & ( for w being VECTOR of V st w in M holds
w,v9 are_orthogonal ) ) ;
for w being VECTOR of V st w in M holds
w,a * v are_orthogonal
proof
let w be VECTOR of V; ::_thesis: ( w in M implies w,a * v are_orthogonal )
assume w in M ; ::_thesis: w,a * v are_orthogonal
then A8: w,v are_orthogonal by A7;
w .|. (a * v) = a * (w .|. v) by BHSP_1:3
.= a * 0 by A8, BHSP_1:def_3 ;
hence w,a * v are_orthogonal by BHSP_1:def_3; ::_thesis: verum
end;
hence a * v in A ; ::_thesis: verum
end;
then A is linearly-closed by A1, RLSUB_1:def_1;
hence ex b1 being strict Subspace of V st the carrier of b1 = { v where v is VECTOR of V : for w being VECTOR of V st w in M holds
w,v are_orthogonal } by A6, RUSUB_1:29; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = { 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 b2 = { v where v is VECTOR of V : for w being VECTOR of V st w in M holds
w,v are_orthogonal } holds
b1 = b2 by RUSUB_1:24;
end;
:: deftheorem Def4 defines Ort_Comp RUSUB_5:def_4_:_
for V being RealUnitarySpace
for M being non empty Subset of V
for b3 being strict Subspace of V holds
( b3 = Ort_Comp M iff the carrier of b3 = { v where v is VECTOR of V : for w being VECTOR of V st w in M holds
w,v are_orthogonal } );
theorem :: RUSUB_5:21
for V being RealUnitarySpace
for W being Subspace of V holds 0. V in Ort_Comp W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V holds 0. V in Ort_Comp W
let W be Subspace of V; ::_thesis: 0. V in Ort_Comp W
for w being VECTOR of V st w in W holds
w, 0. V are_orthogonal
proof
let w be VECTOR of V; ::_thesis: ( w in W implies w, 0. V are_orthogonal )
assume w in W ; ::_thesis: w, 0. V are_orthogonal
w .|. (0. V) = 0 by BHSP_1:15;
hence w, 0. V are_orthogonal by BHSP_1:def_3; ::_thesis: verum
end;
then 0. V in { v where v is VECTOR of V : for w being VECTOR of V st w in W holds
w,v are_orthogonal } ;
then 0. V in the carrier of (Ort_Comp W) by Def3;
hence 0. V in Ort_Comp W by STRUCT_0:def_5; ::_thesis: verum
end;
theorem :: RUSUB_5:22
for V being RealUnitarySpace holds Ort_Comp ((0). V) = (Omega). V
proof
let V be RealUnitarySpace; ::_thesis: Ort_Comp ((0). V) = (Omega). V
for x being set st x in the carrier of ((Omega). V) holds
x in the carrier of (Ort_Comp ((0). V))
proof
let x be set ; ::_thesis: ( x in the carrier of ((Omega). V) implies x in the carrier of (Ort_Comp ((0). V)) )
assume x in the carrier of ((Omega). V) ; ::_thesis: x in the carrier of (Ort_Comp ((0). V))
then x in (Omega). V by STRUCT_0:def_5;
then x in UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by RUSUB_1:def_3;
then reconsider x = x as Element of V by STRUCT_0:def_5;
for w being VECTOR of V st w in (0). V holds
w,x are_orthogonal
proof
let w be VECTOR of V; ::_thesis: ( w in (0). V implies w,x are_orthogonal )
assume w in (0). V ; ::_thesis: w,x are_orthogonal
then w in the carrier of ((0). V) by STRUCT_0:def_5;
then w in {(0. V)} by RUSUB_1:def_2;
then w .|. x = (0. V) .|. x by TARSKI:def_1
.= 0 by BHSP_1:14 ;
hence w,x are_orthogonal by BHSP_1:def_3; ::_thesis: verum
end;
then x in { v where v is VECTOR of V : for w being VECTOR of V st w in (0). V holds
w,v are_orthogonal } ;
hence x in the carrier of (Ort_Comp ((0). V)) by Def3; ::_thesis: verum
end;
then A1: the carrier of ((Omega). V) c= the carrier of (Ort_Comp ((0). V)) by TARSKI:def_3;
for x being set st x in the carrier of (Ort_Comp ((0). V)) holds
x in the carrier of ((Omega). V)
proof
let x be set ; ::_thesis: ( x in the carrier of (Ort_Comp ((0). V)) implies x in the carrier of ((Omega). V) )
assume x in the carrier of (Ort_Comp ((0). V)) ; ::_thesis: x in the carrier of ((Omega). V)
then x in Ort_Comp ((0). V) by STRUCT_0:def_5;
then x in V by RUSUB_1:2;
then x in the carrier of V by STRUCT_0:def_5;
then x in UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by STRUCT_0:def_5;
then x in (Omega). V by RUSUB_1:def_3;
hence x in the carrier of ((Omega). V) by STRUCT_0:def_5; ::_thesis: verum
end;
then the carrier of (Ort_Comp ((0). V)) c= the carrier of ((Omega). V) by TARSKI:def_3;
then the carrier of ((Omega). V) = the carrier of (Ort_Comp ((0). V)) by A1, XBOOLE_0:def_10;
hence Ort_Comp ((0). V) = (Omega). V by RUSUB_1:24; ::_thesis: verum
end;
theorem :: RUSUB_5:23
for V being RealUnitarySpace holds Ort_Comp ((Omega). V) = (0). V
proof
let V be RealUnitarySpace; ::_thesis: Ort_Comp ((Omega). V) = (0). V
for x being set st x in the carrier of (Ort_Comp ((Omega). V)) holds
x in the carrier of ((0). V)
proof
let x be set ; ::_thesis: ( x in the carrier of (Ort_Comp ((Omega). V)) implies x in the carrier of ((0). V) )
assume x in the carrier of (Ort_Comp ((Omega). V)) ; ::_thesis: x in the carrier of ((0). V)
then x in { v where v is VECTOR of V : for w being VECTOR of V st w in (Omega). V holds
w,v are_orthogonal } by Def3;
then A1: ex v being VECTOR of V st
( x = v & ( for w being VECTOR of V st w in (Omega). V holds
w,v are_orthogonal ) ) ;
then reconsider x = x as VECTOR of V ;
x in UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by STRUCT_0:def_5;
then x in (Omega). V by RUSUB_1:def_3;
then x,x are_orthogonal by A1;
then 0 = x .|. x by BHSP_1:def_3;
then x = 0. V by BHSP_1:def_2;
then x in {(0. V)} by TARSKI:def_1;
hence x in the carrier of ((0). V) by RUSUB_1:def_2; ::_thesis: verum
end;
then A2: the carrier of (Ort_Comp ((Omega). V)) c= the carrier of ((0). V) by TARSKI:def_3;
for x being set st x in the carrier of ((0). V) holds
x in the carrier of (Ort_Comp ((Omega). V))
proof
let x be set ; ::_thesis: ( x in the carrier of ((0). V) implies x in the carrier of (Ort_Comp ((Omega). V)) )
assume x in the carrier of ((0). V) ; ::_thesis: x in the carrier of (Ort_Comp ((Omega). V))
then A3: x in {(0. V)} by RUSUB_1:def_2;
then reconsider x = x as VECTOR of V ;
for w being VECTOR of V st w in (Omega). V holds
w,x are_orthogonal
proof
let w be VECTOR of V; ::_thesis: ( w in (Omega). V implies w,x are_orthogonal )
assume w in (Omega). V ; ::_thesis: w,x are_orthogonal
w .|. x = w .|. (0. V) by A3, TARSKI:def_1
.= 0 by BHSP_1:15 ;
hence w,x are_orthogonal by BHSP_1:def_3; ::_thesis: verum
end;
then x in { v where v is VECTOR of V : for w being VECTOR of V st w in (Omega). V holds
w,v are_orthogonal } ;
hence x in the carrier of (Ort_Comp ((Omega). V)) by Def3; ::_thesis: verum
end;
then the carrier of ((0). V) c= the carrier of (Ort_Comp ((Omega). V)) by TARSKI:def_3;
then the carrier of (Ort_Comp ((Omega). V)) = the carrier of ((0). V) by A2, XBOOLE_0:def_10;
hence Ort_Comp ((Omega). V) = (0). V by RUSUB_1:24; ::_thesis: verum
end;
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
proof
let V be RealUnitarySpace; ::_thesis: 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
let W be Subspace of V; ::_thesis: for v being VECTOR of V st v <> 0. V & v in W holds
not v in Ort_Comp W
let v be VECTOR of V; ::_thesis: ( v <> 0. V & v in W implies not v in Ort_Comp W )
assume A1: v <> 0. V ; ::_thesis: ( not v in W or not v in Ort_Comp W )
( v in W implies not v in Ort_Comp W )
proof
assume A2: v in W ; ::_thesis: not v in Ort_Comp W
assume v in Ort_Comp W ; ::_thesis: contradiction
then v in the carrier of (Ort_Comp W) by STRUCT_0:def_5;
then v in { v1 where v1 is VECTOR of V : for w being VECTOR of V st w in W holds
w,v1 are_orthogonal } by Def3;
then ex v1 being VECTOR of V st
( v = v1 & ( for w being VECTOR of V st w in W holds
w,v1 are_orthogonal ) ) ;
then v,v are_orthogonal by A2;
then 0 = v .|. v by BHSP_1:def_3;
hence contradiction by A1, BHSP_1:def_2; ::_thesis: verum
end;
hence ( not v in W or not v in Ort_Comp W ) ; ::_thesis: verum
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))
proof
let V be RealUnitarySpace; ::_thesis: for M being non empty Subset of V holds M c= the carrier of (Ort_Comp (Ort_Comp M))
let M be non empty Subset of V; ::_thesis: M c= the carrier of (Ort_Comp (Ort_Comp M))
for x being set st x in M holds
x in the carrier of (Ort_Comp (Ort_Comp M))
proof
let x be set ; ::_thesis: ( x in M implies x in the carrier of (Ort_Comp (Ort_Comp M)) )
assume A1: x in M ; ::_thesis: x in the carrier of (Ort_Comp (Ort_Comp M))
then reconsider x = x as VECTOR of V ;
for y being VECTOR of V st y in Ort_Comp M holds
x,y are_orthogonal
proof
let y be VECTOR of V; ::_thesis: ( y in Ort_Comp M implies x,y are_orthogonal )
assume y in Ort_Comp M ; ::_thesis: x,y are_orthogonal
then y in the carrier of (Ort_Comp M) by STRUCT_0:def_5;
then y in { v where v is VECTOR of V : for w being VECTOR of V st w in M holds
w,v are_orthogonal } by Def4;
then ex v being VECTOR of V st
( y = v & ( for w being VECTOR of V st w in M holds
w,v are_orthogonal ) ) ;
hence x,y are_orthogonal by A1; ::_thesis: verum
end;
then x in { v where v is VECTOR of V : for w being VECTOR of V st w in Ort_Comp M holds
w,v are_orthogonal } ;
hence x in the carrier of (Ort_Comp (Ort_Comp M)) by Def3; ::_thesis: verum
end;
hence M c= the carrier of (Ort_Comp (Ort_Comp M)) by TARSKI:def_3; ::_thesis: verum
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)
proof
let V be RealUnitarySpace; ::_thesis: 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)
let M, N be non empty Subset of V; ::_thesis: ( M c= N implies the carrier of (Ort_Comp N) c= the carrier of (Ort_Comp M) )
assume A1: M c= N ; ::_thesis: the carrier of (Ort_Comp N) c= the carrier of (Ort_Comp M)
for x being set st x in the carrier of (Ort_Comp N) holds
x in the carrier of (Ort_Comp M)
proof
let x be set ; ::_thesis: ( x in the carrier of (Ort_Comp N) implies x in the carrier of (Ort_Comp M) )
assume x in the carrier of (Ort_Comp N) ; ::_thesis: x in the carrier of (Ort_Comp M)
then x in { v where v is VECTOR of V : for w being VECTOR of V st w in N holds
w,v are_orthogonal } by Def4;
then A2: ex v1 being VECTOR of V st
( x = v1 & ( for w being VECTOR of V st w in N holds
w,v1 are_orthogonal ) ) ;
then reconsider x = x as VECTOR of V ;
for y being VECTOR of V st y in M holds
y,x are_orthogonal by A1, A2;
then x in { v where v is VECTOR of V : for w being VECTOR of V st w in M holds
w,v are_orthogonal } ;
hence x in the carrier of (Ort_Comp M) by Def4; ::_thesis: verum
end;
hence the carrier of (Ort_Comp N) c= the carrier of (Ort_Comp M) by TARSKI:def_3; ::_thesis: verum
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
proof
let V be RealUnitarySpace; ::_thesis: 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
let W be Subspace of V; ::_thesis: for M being non empty Subset of V st M = the carrier of W holds
Ort_Comp M = Ort_Comp W
let M be non empty Subset of V; ::_thesis: ( M = the carrier of W implies Ort_Comp M = Ort_Comp W )
assume A1: M = the carrier of W ; ::_thesis: Ort_Comp M = Ort_Comp W
for x being set st x in the carrier of (Ort_Comp W) holds
x in the carrier of (Ort_Comp M)
proof
let x be set ; ::_thesis: ( x in the carrier of (Ort_Comp W) implies x in the carrier of (Ort_Comp M) )
assume x in the carrier of (Ort_Comp W) ; ::_thesis: x in the carrier of (Ort_Comp M)
then x in { v where v is VECTOR of V : for w being VECTOR of V st w in W holds
w,v are_orthogonal } by Def3;
then consider v being VECTOR of V such that
A2: x = v and
A3: for w being VECTOR of V st w in W holds
w,v are_orthogonal ;
for w being VECTOR of V st w in M holds
w,v are_orthogonal
proof
let w be VECTOR of V; ::_thesis: ( w in M implies w,v are_orthogonal )
assume w in M ; ::_thesis: w,v are_orthogonal
then w in W by A1, STRUCT_0:def_5;
hence w,v are_orthogonal by A3; ::_thesis: verum
end;
then x in { v1 where v1 is VECTOR of V : for w being VECTOR of V st w in M holds
w,v1 are_orthogonal } by A2;
hence x in the carrier of (Ort_Comp M) by Def4; ::_thesis: verum
end;
then A4: the carrier of (Ort_Comp W) c= the carrier of (Ort_Comp M) by TARSKI:def_3;
for x being set st x in the carrier of (Ort_Comp M) holds
x in the carrier of (Ort_Comp W)
proof
let x be set ; ::_thesis: ( x in the carrier of (Ort_Comp M) implies x in the carrier of (Ort_Comp W) )
assume x in the carrier of (Ort_Comp M) ; ::_thesis: x in the carrier of (Ort_Comp W)
then x in { v where v is VECTOR of V : for w being VECTOR of V st w in M holds
w,v are_orthogonal } by Def4;
then consider v being VECTOR of V such that
A5: x = v and
A6: for w being VECTOR of V st w in M holds
w,v are_orthogonal ;
for w being VECTOR of V st w in W holds
w,v are_orthogonal
proof
let w be VECTOR of V; ::_thesis: ( w in W implies w,v are_orthogonal )
assume w in W ; ::_thesis: w,v are_orthogonal
then w in M by A1, STRUCT_0:def_5;
hence w,v are_orthogonal by A6; ::_thesis: verum
end;
then x in { v1 where v1 is VECTOR of V : for w being VECTOR of V st w in W holds
w,v1 are_orthogonal } by A5;
hence x in the carrier of (Ort_Comp W) by Def3; ::_thesis: verum
end;
then the carrier of (Ort_Comp M) c= the carrier of (Ort_Comp W) by TARSKI:def_3;
then the carrier of (Ort_Comp W) = the carrier of (Ort_Comp M) by A4, XBOOLE_0:def_10;
hence Ort_Comp M = Ort_Comp W by RUSUB_1:24; ::_thesis: verum
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))
proof
let V be RealUnitarySpace; ::_thesis: for M being non empty Subset of V holds Ort_Comp M = Ort_Comp (Ort_Comp (Ort_Comp M))
let M be non empty Subset of V; ::_thesis: Ort_Comp M = Ort_Comp (Ort_Comp (Ort_Comp M))
set N = the carrier of (Ort_Comp M);
reconsider N = the carrier of (Ort_Comp M) as Subset of V by RUSUB_1:def_1;
reconsider N = N as non empty Subset of V ;
set L = the carrier of (Ort_Comp (Ort_Comp M));
reconsider L = the carrier of (Ort_Comp (Ort_Comp M)) as Subset of V by RUSUB_1:def_1;
reconsider L = L as non empty Subset of V ;
N c= the carrier of (Ort_Comp (Ort_Comp N)) by Th25;
then A1: N c= the carrier of (Ort_Comp (Ort_Comp (Ort_Comp M))) by Th27;
the carrier of (Ort_Comp L) c= the carrier of (Ort_Comp M) by Th25, Th26;
then the carrier of (Ort_Comp (Ort_Comp (Ort_Comp M))) c= the carrier of (Ort_Comp M) by Th27;
then the carrier of (Ort_Comp (Ort_Comp (Ort_Comp M))) = the carrier of (Ort_Comp M) by A1, XBOOLE_0:def_10;
hence Ort_Comp M = Ort_Comp (Ort_Comp (Ort_Comp M)) by RUSUB_1:24; ::_thesis: verum
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) )
proof
let V be RealUnitarySpace; ::_thesis: 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) )
let x, y be VECTOR of V; ::_thesis: ( ||.(x + y).|| ^2 = ((||.x.|| ^2) + (2 * (x .|. y))) + (||.y.|| ^2) & ||.(x - y).|| ^2 = ((||.x.|| ^2) - (2 * (x .|. y))) + (||.y.|| ^2) )
A1: x .|. x >= 0 by BHSP_1:def_2;
||.(x + y).|| = sqrt ((x + y) .|. (x + y)) by BHSP_1:def_4;
then A2: sqrt (||.(x + y).|| ^2) = sqrt ((x + y) .|. (x + y)) by BHSP_1:28, SQUARE_1:22;
A3: y .|. y >= 0 by BHSP_1:def_2;
( (x + y) .|. (x + y) >= 0 & ||.(x + y).|| ^2 >= 0 ) by BHSP_1:def_2, XREAL_1:63;
then ||.(x + y).|| ^2 = (x + y) .|. (x + y) by A2, SQUARE_1:28
.= ((x .|. x) + (2 * (x .|. y))) + (y .|. y) by BHSP_1:16
.= (((sqrt (x .|. x)) ^2) + (2 * (x .|. y))) + (y .|. y) by A1, SQUARE_1:def_2
.= ((||.x.|| ^2) + (2 * (x .|. y))) + (y .|. y) by BHSP_1:def_4
.= ((||.x.|| ^2) + (2 * (x .|. y))) + ((sqrt (y .|. y)) ^2) by A3, SQUARE_1:def_2 ;
hence ||.(x + y).|| ^2 = ((||.x.|| ^2) + (2 * (x .|. y))) + (||.y.|| ^2) by BHSP_1:def_4; ::_thesis: ||.(x - y).|| ^2 = ((||.x.|| ^2) - (2 * (x .|. y))) + (||.y.|| ^2)
||.(x - y).|| = sqrt ((x - y) .|. (x - y)) by BHSP_1:def_4;
then A4: sqrt (||.(x - y).|| ^2) = sqrt ((x - y) .|. (x - y)) by BHSP_1:28, SQUARE_1:22;
( (x - y) .|. (x - y) >= 0 & ||.(x - y).|| ^2 >= 0 ) by BHSP_1:def_2, XREAL_1:63;
then ||.(x - y).|| ^2 = (x - y) .|. (x - y) by A4, SQUARE_1:28
.= ((x .|. x) - (2 * (x .|. y))) + (y .|. y) by BHSP_1:18
.= (((sqrt (x .|. x)) ^2) - (2 * (x .|. y))) + (y .|. y) by A1, SQUARE_1:def_2
.= ((||.x.|| ^2) - (2 * (x .|. y))) + (y .|. y) by BHSP_1:def_4
.= ((||.x.|| ^2) - (2 * (x .|. y))) + ((sqrt (y .|. y)) ^2) by A3, SQUARE_1:def_2 ;
hence ||.(x - y).|| ^2 = ((||.x.|| ^2) - (2 * (x .|. y))) + (||.y.|| ^2) by BHSP_1:def_4; ::_thesis: verum
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)
proof
let V be RealUnitarySpace; ::_thesis: for x, y being VECTOR of V st x,y are_orthogonal holds
||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2)
let x, y be VECTOR of V; ::_thesis: ( x,y are_orthogonal implies ||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2) )
assume x,y are_orthogonal ; ::_thesis: ||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2)
then A1: x .|. y = 0 by BHSP_1:def_3;
||.(x + y).|| ^2 = ((||.x.|| ^2) + (2 * (x .|. y))) + (||.y.|| ^2) by Th29;
hence ||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2) by A1; ::_thesis: verum
end;
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))
proof
let V be RealUnitarySpace; ::_thesis: for x, y being VECTOR of V holds (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2))
let x, y be VECTOR of V; ::_thesis: (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2))
(||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (((||.x.|| ^2) + (2 * (x .|. y))) + (||.y.|| ^2)) + (||.(x - y).|| ^2) by Th29
.= (((||.x.|| ^2) + (2 * (x .|. y))) + (||.y.|| ^2)) + (((||.x.|| ^2) - (2 * (x .|. y))) + (||.y.|| ^2)) by Th29
.= ((||.x.|| ^2) + (||.x.|| ^2)) + (2 * (||.y.|| ^2)) ;
hence (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2)) ; ::_thesis: verum
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 }
proof
let V be RealUnitarySpace; ::_thesis: 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 }
let v be VECTOR of V; ::_thesis: ex W being Subspace of V st the carrier of W = { u where u is VECTOR of V : u .|. v = 0 }
set M = { u where u is VECTOR of V : u .|. v = 0 } ;
for x being set st x in { u where u is VECTOR of V : u .|. v = 0 } holds
x in the carrier of V
proof
let x be set ; ::_thesis: ( x in { u where u is VECTOR of V : u .|. v = 0 } implies x in the carrier of V )
assume x in { u where u is VECTOR of V : u .|. v = 0 } ; ::_thesis: x in the carrier of V
then ex u being VECTOR of V st
( x = u & u .|. v = 0 ) ;
hence x in the carrier of V ; ::_thesis: verum
end;
then reconsider M = { u where u is VECTOR of V : u .|. v = 0 } as Subset of V by TARSKI:def_3;
(0. V) .|. v = 0 by BHSP_1:14;
then A1: 0. V in M ;
then reconsider M = M as non empty Subset of V ;
for x, y being VECTOR of V
for a being Real st x in M & y in M holds
((1 - a) * x) + (a * y) in M
proof
let x, y be VECTOR of V; ::_thesis: for a being Real st x in M & y in M holds
((1 - a) * x) + (a * y) in M
let a be Real; ::_thesis: ( x in M & y in M implies ((1 - a) * x) + (a * y) in M )
assume that
A2: x in M and
A3: y in M ; ::_thesis: ((1 - a) * x) + (a * y) in M
consider u2 being VECTOR of V such that
A4: y = u2 and
A5: u2 .|. v = 0 by A3;
consider u1 being VECTOR of V such that
A6: x = u1 and
A7: u1 .|. v = 0 by A2;
(((1 - a) * u1) + (a * u2)) .|. v = (((1 - a) * u1) .|. v) + ((a * u2) .|. v) by BHSP_1:def_2
.= ((1 - a) * (u1 .|. v)) + ((a * u2) .|. v) by BHSP_1:def_2
.= a * 0 by A7, A5, BHSP_1:def_2 ;
hence ((1 - a) * x) + (a * y) in M by A6, A4; ::_thesis: verum
end;
then reconsider M = M as non empty Affine Subset of V by RUSUB_4:def_4;
take Lin M ; ::_thesis: the carrier of (Lin M) = { u where u is VECTOR of V : u .|. v = 0 }
thus the carrier of (Lin M) = { u where u is VECTOR of V : u .|. v = 0 } by A1, RUSUB_4:28; ::_thesis: verum
end;
begin
definition
let V be RealUnitarySpace;
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
ex b1 being Subset-Family of V st
for M being Subset of V holds
( M in b1 iff for x being Point of V st x in M holds
ex r being Real st
( r > 0 & Ball (x,r) c= M ) )
proof
defpred S1[ Subset of V] means for x being Point of V st x in $1 holds
ex r being Real st
( r > 0 & Ball (x,r) c= $1 );
ex F being Subset-Family of V st
for M being Subset of V holds
( M in F iff S1[M] ) from SUBSET_1:sch_3();
hence ex b1 being Subset-Family of V st
for M being Subset of V holds
( M in b1 iff for x being Point of V st x in M holds
ex r being Real st
( r > 0 & Ball (x,r) c= M ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of V st ( for M being Subset of V holds
( M in b1 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 b2 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
b1 = b2
proof
let FX, GX be Subset-Family of V; ::_thesis: ( ( for M being Subset of V holds
( M in FX 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 GX iff for x being Point of V st x in M holds
ex r being Real st
( r > 0 & Ball (x,r) c= M ) ) ) implies FX = GX )
assume A1: for M being Subset of V holds
( M in FX iff for x being Point of V st x in M holds
ex r being Real st
( r > 0 & Ball (x,r) c= M ) ) ; ::_thesis: ( ex M being Subset of V st
( ( M in GX implies for x being Point of V st x in M holds
ex r being Real st
( r > 0 & Ball (x,r) c= M ) ) implies ( ( for x being Point of V st x in M holds
ex r being Real st
( r > 0 & Ball (x,r) c= M ) ) & not M in GX ) ) or FX = GX )
assume A2: for N being Subset of V holds
( N in GX iff for y being Point of V st y in N holds
ex p being Real st
( p > 0 & Ball (y,p) c= N ) ) ; ::_thesis: FX = GX
for Y being Subset of V holds
( Y in FX iff Y in GX )
proof
let Y be Subset of V; ::_thesis: ( Y in FX iff Y in GX )
A3: now__::_thesis:_(_Y_in_GX_implies_Y_in_FX_)
assume Y in GX ; ::_thesis: Y in FX
then for x being Point of V st x in Y holds
ex r being Real st
( r > 0 & Ball (x,r) c= Y ) by A2;
hence Y in FX by A1; ::_thesis: verum
end;
now__::_thesis:_(_Y_in_FX_implies_Y_in_GX_)
assume Y in FX ; ::_thesis: Y in GX
then for x being Point of V st x in Y holds
ex r being Real st
( r > 0 & Ball (x,r) c= Y ) by A1;
hence Y in GX by A2; ::_thesis: verum
end;
hence ( Y in FX iff Y in GX ) by A3; ::_thesis: verum
end;
hence FX = GX by SETFAM_1:31; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines Family_open_set RUSUB_5:def_5_:_
for V being RealUnitarySpace
for b2 being Subset-Family of V holds
( b2 = Family_open_set V iff for M being Subset of V holds
( M in b2 iff for x being Point of V st x in M holds
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)
proof
let V be RealUnitarySpace; ::_thesis: for v being Point of V
for r, p being Real st r <= p holds
Ball (v,r) c= Ball (v,p)
let v be Point of V; ::_thesis: for r, p being Real st r <= p holds
Ball (v,r) c= Ball (v,p)
let r, p be Real; ::_thesis: ( r <= p implies Ball (v,r) c= Ball (v,p) )
assume A1: r <= p ; ::_thesis: Ball (v,r) c= Ball (v,p)
for u being Point of V st u in Ball (v,r) holds
u in Ball (v,p)
proof
let u be Point of V; ::_thesis: ( u in Ball (v,r) implies u in Ball (v,p) )
assume u in Ball (v,r) ; ::_thesis: u in Ball (v,p)
then dist (v,u) < r by BHSP_2:41;
then (dist (v,u)) + r < r + p by A1, XREAL_1:8;
then dist (v,u) < (r + p) - r by XREAL_1:20;
hence u in Ball (v,p) by BHSP_2:41; ::_thesis: verum
end;
hence Ball (v,r) c= Ball (v,p) by SUBSET_1:2; ::_thesis: verum
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 )
proof
let V be RealUnitarySpace; ::_thesis: for v being Point of V ex r being Real st
( r > 0 & Ball (v,r) c= the carrier of V )
let v be Point of V; ::_thesis: ex r being Real st
( r > 0 & Ball (v,r) c= the carrier of V )
consider r being Real such that
A1: r = 1 ;
take r ; ::_thesis: ( r > 0 & Ball (v,r) c= the carrier of V )
thus r > 0 by A1; ::_thesis: Ball (v,r) c= the carrier of V
thus Ball (v,r) c= the carrier of V ; ::_thesis: verum
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) )
proof
let V be RealUnitarySpace; ::_thesis: 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) )
let v, u be Point of V; ::_thesis: 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) )
let r be Real; ::_thesis: ( u in Ball (v,r) implies ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) ) )
assume u in Ball (v,r) ; ::_thesis: ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) )
then A1: dist (v,u) < r by BHSP_2:41;
thus ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) ) ::_thesis: verum
proof
set p = r - (dist (v,u));
take r - (dist (v,u)) ; ::_thesis: ( r - (dist (v,u)) > 0 & Ball (u,(r - (dist (v,u)))) c= Ball (v,r) )
thus r - (dist (v,u)) > 0 by A1, XREAL_1:50; ::_thesis: Ball (u,(r - (dist (v,u)))) c= Ball (v,r)
for w being Point of V st w in Ball (u,(r - (dist (v,u)))) holds
w in Ball (v,r)
proof
let w be Point of V; ::_thesis: ( w in Ball (u,(r - (dist (v,u)))) implies w in Ball (v,r) )
assume w in Ball (u,(r - (dist (v,u)))) ; ::_thesis: w in Ball (v,r)
then dist (u,w) < r - (dist (v,u)) by BHSP_2:41;
then A2: (dist (v,u)) + (dist (u,w)) < r by XREAL_1:20;
(dist (v,u)) + (dist (u,w)) >= dist (v,w) by BHSP_1:35;
then dist (v,w) < r by A2, XXREAL_0:2;
hence w in Ball (v,r) by BHSP_2:41; ::_thesis: verum
end;
hence Ball (u,(r - (dist (v,u)))) c= Ball (v,r) by SUBSET_1:2; ::_thesis: verum
end;
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) )
proof
let V be RealUnitarySpace; ::_thesis: 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) )
let u, v, w be Point of V; ::_thesis: 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) )
let r, p be Real; ::_thesis: ( v in (Ball (u,r)) /\ (Ball (w,p)) implies ex q being Real st
( Ball (v,q) c= Ball (u,r) & Ball (v,q) c= Ball (w,p) ) )
assume A1: v in (Ball (u,r)) /\ (Ball (w,p)) ; ::_thesis: ex q being Real st
( Ball (v,q) c= Ball (u,r) & Ball (v,q) c= Ball (w,p) )
then v in Ball (u,r) by XBOOLE_0:def_4;
then consider s being Real such that
s > 0 and
A2: Ball (v,s) c= Ball (u,r) by Th35;
v in Ball (w,p) by A1, XBOOLE_0:def_4;
then consider t being Real such that
t > 0 and
A3: Ball (v,t) c= Ball (w,p) by Th35;
take q = min (s,t); ::_thesis: ( Ball (v,q) c= Ball (u,r) & Ball (v,q) c= Ball (w,p) )
Ball (v,q) c= Ball (v,s) by Th33, XXREAL_0:17;
hence Ball (v,q) c= Ball (u,r) by A2, XBOOLE_1:1; ::_thesis: Ball (v,q) c= Ball (w,p)
Ball (v,q) c= Ball (v,t) by Th33, XXREAL_0:17;
hence Ball (v,q) c= Ball (w,p) by A3, XBOOLE_1:1; ::_thesis: verum
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
proof
let V be RealUnitarySpace; ::_thesis: for v being Point of V
for r being Real holds Ball (v,r) in Family_open_set V
let v be Point of V; ::_thesis: for r being Real holds Ball (v,r) in Family_open_set V
let r be Real; ::_thesis: Ball (v,r) in Family_open_set V
for u being Point of V st u in Ball (v,r) holds
ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) ) by Th35;
hence Ball (v,r) in Family_open_set V by Def5; ::_thesis: verum
end;
theorem Th38: :: RUSUB_5:38
for V being RealUnitarySpace holds the carrier of V in Family_open_set V
proof
let V be RealUnitarySpace; ::_thesis: the carrier of V in Family_open_set V
( the carrier of V c= the carrier of V & ( for v being Point of V st v in the carrier of V holds
ex p being Real st
( p > 0 & Ball (v,p) c= the carrier of V ) ) ) by Th34;
hence the carrier of V in Family_open_set V by Def5; ::_thesis: verum
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
proof
let V be RealUnitarySpace; ::_thesis: 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
let M, N be Subset of V; ::_thesis: ( M in Family_open_set V & N in Family_open_set V implies M /\ N in Family_open_set V )
assume that
A1: M in Family_open_set V and
A2: N in Family_open_set V ; ::_thesis: M /\ N in Family_open_set V
for v being Point of V st v in M /\ N holds
ex q being Real st
( q > 0 & Ball (v,q) c= M /\ N )
proof
let v be Point of V; ::_thesis: ( v in M /\ N implies ex q being Real st
( q > 0 & Ball (v,q) c= M /\ N ) )
assume A3: v in M /\ N ; ::_thesis: ex q being Real st
( q > 0 & Ball (v,q) c= M /\ N )
then v in M by XBOOLE_0:def_4;
then consider p being Real such that
A4: p > 0 and
A5: Ball (v,p) c= M by A1, Def5;
v in N by A3, XBOOLE_0:def_4;
then consider r being Real such that
A6: r > 0 and
A7: Ball (v,r) c= N by A2, Def5;
take q = min (p,r); ::_thesis: ( q > 0 & Ball (v,q) c= M /\ N )
thus q > 0 by A4, A6, XXREAL_0:15; ::_thesis: Ball (v,q) c= M /\ N
Ball (v,q) c= Ball (v,r) by Th33, XXREAL_0:17;
then A8: Ball (v,q) c= N by A7, XBOOLE_1:1;
Ball (v,q) c= Ball (v,p) by Th33, XXREAL_0:17;
then Ball (v,q) c= M by A5, XBOOLE_1:1;
hence Ball (v,q) c= M /\ N by A8, XBOOLE_1:19; ::_thesis: verum
end;
hence M /\ N in Family_open_set V by Def5; ::_thesis: verum
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
proof
let V be RealUnitarySpace; ::_thesis: for A being Subset-Family of V st A c= Family_open_set V holds
union A in Family_open_set V
let A be Subset-Family of V; ::_thesis: ( A c= Family_open_set V implies union A in Family_open_set V )
assume A1: A c= Family_open_set V ; ::_thesis: union A in Family_open_set V
for x being Point of V st x in union A holds
ex r being Real st
( r > 0 & Ball (x,r) c= union A )
proof
let x be Point of V; ::_thesis: ( x in union A implies ex r being Real st
( r > 0 & Ball (x,r) c= union A ) )
assume x in union A ; ::_thesis: ex r being Real st
( r > 0 & Ball (x,r) c= union A )
then consider W being set such that
A2: x in W and
A3: W in A by TARSKI:def_4;
reconsider W = W as Subset of V by A3;
consider r being Real such that
A4: r > 0 and
A5: Ball (x,r) c= W by A1, A2, A3, Def5;
take r ; ::_thesis: ( r > 0 & Ball (x,r) c= union A )
thus r > 0 by A4; ::_thesis: Ball (x,r) c= union A
W c= union A by A3, ZFMISC_1:74;
hence Ball (x,r) c= union A by A5, XBOOLE_1:1; ::_thesis: verum
end;
hence union A in Family_open_set V by Def5; ::_thesis: verum
end;
theorem Th41: :: RUSUB_5:41
for V being RealUnitarySpace holds TopStruct(# the carrier of V,(Family_open_set V) #) is TopSpace
proof
let V be RealUnitarySpace; ::_thesis: TopStruct(# the carrier of V,(Family_open_set V) #) is TopSpace
set T = TopStruct(# the carrier of V,(Family_open_set V) #);
A1: for p, q being Subset of TopStruct(# the carrier of V,(Family_open_set V) #) st p in the topology of TopStruct(# the carrier of V,(Family_open_set V) #) & q in the topology of TopStruct(# the carrier of V,(Family_open_set V) #) holds
p /\ q in the topology of TopStruct(# the carrier of V,(Family_open_set V) #) by Th39;
( the carrier of TopStruct(# the carrier of V,(Family_open_set V) #) in the topology of TopStruct(# the carrier of V,(Family_open_set V) #) & ( for a being Subset-Family of TopStruct(# the carrier of V,(Family_open_set V) #) st a c= the topology of TopStruct(# the carrier of V,(Family_open_set V) #) holds
union a in the topology of TopStruct(# the carrier of V,(Family_open_set V) #) ) ) by Th38, Th40;
hence TopStruct(# the carrier of V,(Family_open_set V) #) is TopSpace by A1, PRE_TOPC:def_1; ::_thesis: verum
end;
definition
let V be RealUnitarySpace;
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) #) is TopStruct ;
end;
:: deftheorem defines TopUnitSpace RUSUB_5:def_6_:_
for V being RealUnitarySpace holds TopUnitSpace V = TopStruct(# the carrier of V,(Family_open_set V) #);
registration
let V be RealUnitarySpace;
cluster TopUnitSpace V -> TopSpace-like ;
coherence
TopUnitSpace V is TopSpace-like by Th41;
end;
registration
let V be RealUnitarySpace;
cluster TopUnitSpace V -> non empty ;
coherence
not TopUnitSpace V is empty ;
end;
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 )
proof
let V be RealUnitarySpace; ::_thesis: for M being Subset of (TopUnitSpace V) st M = [#] V holds
( M is open & M is closed )
let M be Subset of (TopUnitSpace V); ::_thesis: ( M = [#] V implies ( M is open & M is closed ) )
A1: [#] (TopUnitSpace V) = the carrier of TopStruct(# the carrier of V,(Family_open_set V) #) ;
assume M = [#] V ; ::_thesis: ( M is open & M is closed )
hence ( M is open & M is closed ) by A1; ::_thesis: verum
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 ) ;
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
proof
let V be RealUnitarySpace; ::_thesis: 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
let v be VECTOR of V; ::_thesis: for r being Real st the carrier of V = {(0. V)} & r <> 0 holds
Sphere (v,r) is empty
let r be Real; ::_thesis: ( the carrier of V = {(0. V)} & r <> 0 implies Sphere (v,r) is empty )
assume that
A1: the carrier of V = {(0. V)} and
A2: r <> 0 ; ::_thesis: Sphere (v,r) is empty
assume not Sphere (v,r) is empty ; ::_thesis: contradiction
then consider x being set such that
A3: x in Sphere (v,r) by XBOOLE_0:def_1;
Sphere (v,r) = { y where y is Point of V : ||.(v - y).|| = r } by BHSP_2:def_7;
then consider w being Point of V such that
x = w and
A4: ||.(v - w).|| = r by A3;
v - w <> 0. V by A2, A4, BHSP_1:26;
hence contradiction by A1, TARSKI:def_1; ::_thesis: verum
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
proof
let V be RealUnitarySpace; ::_thesis: 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
let v be VECTOR of V; ::_thesis: for r being Real st the carrier of V <> {(0. V)} & r > 0 holds
not Sphere (v,r) is empty
let r be Real; ::_thesis: ( the carrier of V <> {(0. V)} & r > 0 implies not Sphere (v,r) is empty )
assume that
A1: the carrier of V <> {(0. V)} and
A2: r > 0 ; ::_thesis: not Sphere (v,r) is empty
now__::_thesis:_not_Sphere_(v,r)_is_empty
percases ( v = 0. V or v <> 0. V ) ;
supposeA3: v = 0. V ; ::_thesis: not Sphere (v,r) is empty
ex u being VECTOR of V st u <> 0. V
proof
not the carrier of V c= {(0. V)} by A1, XBOOLE_0:def_10;
then NonZero V <> {} by XBOOLE_1:37;
then consider u being set such that
A4: u in NonZero V by XBOOLE_0:def_1;
A5: not u in {(0. V)} by A4, XBOOLE_0:def_5;
reconsider u = u as VECTOR of V by A4;
take u ; ::_thesis: u <> 0. V
thus u <> 0. V by A5, TARSKI:def_1; ::_thesis: verum
end;
then consider u being VECTOR of V such that
A6: u <> 0. V ;
set a = ||.u.||;
A7: ||.u.|| <> 0 by A6, BHSP_1:26;
set u9 = (r * (1 / ||.u.||)) * u;
A8: ||.u.|| >= 0 by BHSP_1:28;
||.(v - ((r * (1 / ||.u.||)) * u)).|| = ||.(- ((r * (1 / ||.u.||)) * u)).|| by A3, RLVECT_1:14
.= ||.((r * (1 / ||.u.||)) * u).|| by BHSP_1:31
.= (abs (r * (1 / ||.u.||))) * ||.u.|| by BHSP_1:27 ;
then ||.(v - ((r * (1 / ||.u.||)) * u)).|| = (r * (1 / ||.u.||)) * ||.u.|| by A2, A8, ABSVALUE:def_1
.= r by A7, XCMPLX_1:109 ;
then (r * (1 / ||.u.||)) * u in { y where y is Point of V : ||.(v - y).|| = r } ;
hence not Sphere (v,r) is empty by BHSP_2:def_7; ::_thesis: verum
end;
supposeA9: v <> 0. V ; ::_thesis: not Sphere (v,r) is empty
set a = ||.v.||;
A10: ||.v.|| <> 0 by A9, BHSP_1:26;
set u9 = (1 - (r / ||.v.||)) * v;
A11: ||.(v - ((1 - (r / ||.v.||)) * v)).|| = ||.((1 * v) - ((1 - (r / ||.v.||)) * v)).|| by RLVECT_1:def_8
.= ||.((1 - (1 - (r / ||.v.||))) * v).|| by RLVECT_1:35
.= (abs (r / ||.v.||)) * ||.v.|| by BHSP_1:27 ;
||.v.|| >= 0 by BHSP_1:28;
then ||.(v - ((1 - (r / ||.v.||)) * v)).|| = (r / ||.v.||) * ||.v.|| by A2, A11, ABSVALUE:def_1
.= r / (||.v.|| / ||.v.||) by XCMPLX_1:81
.= r by A10, XCMPLX_1:51 ;
then (1 - (r / ||.v.||)) * v in { y where y is Point of V : ||.(v - y).|| = r } ;
hence not Sphere (v,r) is empty by BHSP_2:def_7; ::_thesis: verum
end;
end;
end;
hence not Sphere (v,r) is empty ; ::_thesis: verum
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
proof
let V be RealUnitarySpace; ::_thesis: for v being VECTOR of V
for r being Real st r = 0 holds
Ball (v,r) is empty
let v be VECTOR of V; ::_thesis: for r being Real st r = 0 holds
Ball (v,r) is empty
let r be Real; ::_thesis: ( r = 0 implies Ball (v,r) is empty )
assume A1: r = 0 ; ::_thesis: Ball (v,r) is empty
assume not Ball (v,r) is empty ; ::_thesis: contradiction
then consider u being set such that
A2: u in Ball (v,r) by XBOOLE_0:def_1;
u in { y where y is Point of V : ||.(v - y).|| < r } by A2, BHSP_2:def_5;
then ex w being Point of V st
( u = w & ||.(v - w).|| < r ) ;
hence contradiction by A1, BHSP_1:28; ::_thesis: verum
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)}
proof
let V be RealUnitarySpace; ::_thesis: 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)}
let v be VECTOR of V; ::_thesis: for r being Real st the carrier of V = {(0. V)} & r > 0 holds
Ball (v,r) = {(0. V)}
let r be Real; ::_thesis: ( the carrier of V = {(0. V)} & r > 0 implies Ball (v,r) = {(0. V)} )
assume that
A1: the carrier of V = {(0. V)} and
A2: r > 0 ; ::_thesis: Ball (v,r) = {(0. V)}
for w being VECTOR of V st w in {(0. V)} holds
w in Ball (v,r)
proof
let w be VECTOR of V; ::_thesis: ( w in {(0. V)} implies w in Ball (v,r) )
assume A3: w in {(0. V)} ; ::_thesis: w in Ball (v,r)
v = 0. V by A1, TARSKI:def_1;
then ||.(v - w).|| = ||.((0. V) - (0. V)).|| by A3, TARSKI:def_1
.= ||.(0. V).|| by RLVECT_1:13
.= 0 by BHSP_1:26 ;
then w in { y where y is Point of V : ||.(v - y).|| < r } by A2;
hence w in Ball (v,r) by BHSP_2:def_5; ::_thesis: verum
end;
then {(0. V)} c= Ball (v,r) by SUBSET_1:2;
hence Ball (v,r) = {(0. V)} by A1, XBOOLE_0:def_10; ::_thesis: verum
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) )
proof
let V be RealUnitarySpace; ::_thesis: 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) )
let v be VECTOR of V; ::_thesis: 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) )
let r be Real; ::_thesis: ( the carrier of V <> {(0. V)} & r > 0 implies ex w being VECTOR of V st
( w <> v & w in Ball (v,r) ) )
assume that
A1: the carrier of V <> {(0. V)} and
A2: r > 0 ; ::_thesis: ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )
consider r9 being real number such that
A3: 0 < r9 and
A4: r9 < r by A2, XREAL_1:5;
reconsider r9 = r9 as Real by XREAL_0:def_1;
now__::_thesis:_ex_w_being_VECTOR_of_V_st_
(_w_<>_v_&_w_in_Ball_(v,r)_)
percases ( v = 0. V or v <> 0. V ) ;
supposeA5: v = 0. V ; ::_thesis: ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )
ex w being VECTOR of V st
( w <> 0. V & ||.w.|| < r )
proof
not the carrier of V c= {(0. V)} by A1, XBOOLE_0:def_10;
then NonZero V <> {} by XBOOLE_1:37;
then consider u being set such that
A6: u in NonZero V by XBOOLE_0:def_1;
A7: not u in {(0. V)} by A6, XBOOLE_0:def_5;
reconsider u = u as VECTOR of V by A6;
A8: u <> 0. V by A7, TARSKI:def_1;
then A9: ||.u.|| <> 0 by BHSP_1:26;
set a = ||.u.||;
A10: ||.u.|| >= 0 by BHSP_1:28;
take w = (r9 / ||.u.||) * u; ::_thesis: ( w <> 0. V & ||.w.|| < r )
A11: ||.w.|| = (abs (r9 / ||.u.||)) * ||.u.|| by BHSP_1:27
.= (r9 / ||.u.||) * ||.u.|| by A3, A10, ABSVALUE:def_1
.= r9 / (||.u.|| / ||.u.||) by XCMPLX_1:81
.= r9 by A9, XCMPLX_1:51 ;
r9 / ||.u.|| > 0 by A3, A9, A10, XREAL_1:139;
hence ( w <> 0. V & ||.w.|| < r ) by A4, A8, A11, RLVECT_1:11; ::_thesis: verum
end;
then consider u being VECTOR of V such that
A12: u <> 0. V and
A13: ||.u.|| < r ;
||.(v - u).|| = ||.(- u).|| by A5, RLVECT_1:14
.= ||.u.|| by BHSP_1:31 ;
then u in { y where y is Point of V : ||.(v - y).|| < r } by A13;
then u in Ball (v,r) by BHSP_2:def_5;
hence ex w being VECTOR of V st
( w <> v & w in Ball (v,r) ) by A5, A12; ::_thesis: verum
end;
supposeA14: v <> 0. V ; ::_thesis: ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )
set a = ||.v.||;
A15: ||.v.|| <> 0 by A14, BHSP_1:26;
set u9 = (1 - (r9 / ||.v.||)) * v;
A16: ||.(v - ((1 - (r9 / ||.v.||)) * v)).|| = ||.((1 * v) - ((1 - (r9 / ||.v.||)) * v)).|| by RLVECT_1:def_8
.= ||.((1 - (1 - (r9 / ||.v.||))) * v).|| by RLVECT_1:35
.= (abs (r9 / ||.v.||)) * ||.v.|| by BHSP_1:27 ;
||.v.|| >= 0 by BHSP_1:28;
then A17: ||.(v - ((1 - (r9 / ||.v.||)) * v)).|| = (r9 / ||.v.||) * ||.v.|| by A3, A16, ABSVALUE:def_1
.= r9 / (||.v.|| / ||.v.||) by XCMPLX_1:81
.= r9 by A15, XCMPLX_1:51 ;
then v - ((1 - (r9 / ||.v.||)) * v) <> 0. V by A3, BHSP_1:26;
then A18: v <> (1 - (r9 / ||.v.||)) * v by RLVECT_1:15;
(1 - (r9 / ||.v.||)) * v in { y where y is Point of V : ||.(v - y).|| < r } by A4, A17;
then (1 - (r9 / ||.v.||)) * v in Ball (v,r) by BHSP_2:def_5;
hence ex w being VECTOR of V st
( w <> v & w in Ball (v,r) ) by A18; ::_thesis: verum
end;
end;
end;
hence ex w being VECTOR of V st
( w <> v & w in Ball (v,r) ) ; ::_thesis: verum
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 ) ;
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
proof
let V be RealUnitarySpace; ::_thesis: 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
let M be Subset of (TopUnitSpace V); ::_thesis: for r being Real
for v being Point of V st M = Ball (v,r) holds
M is open
let r be Real; ::_thesis: for v being Point of V st M = Ball (v,r) holds
M is open
let v be Point of V; ::_thesis: ( M = Ball (v,r) implies M is open )
assume M = Ball (v,r) ; ::_thesis: M is open
then M in Family_open_set V by Th37;
hence M is open by PRE_TOPC:def_2; ::_thesis: verum
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 ) )
proof
let V be RealUnitarySpace; ::_thesis: 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 ) )
let M be Subset of (TopUnitSpace V); ::_thesis: ( 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 ) )
thus ( M is open implies for v being Point of V st v in M holds
ex r being Real st
( r > 0 & Ball (v,r) c= M ) ) ::_thesis: ( ( for v being Point of V st v in M holds
ex r being Real st
( r > 0 & Ball (v,r) c= M ) ) implies M is open )
proof
assume M is open ; ::_thesis: for v being Point of V st v in M holds
ex r being Real st
( r > 0 & Ball (v,r) c= M )
then A1: M in the topology of (TopUnitSpace V) by PRE_TOPC:def_2;
let v be Point of V; ::_thesis: ( v in M implies ex r being Real st
( r > 0 & Ball (v,r) c= M ) )
assume v in M ; ::_thesis: ex r being Real st
( r > 0 & Ball (v,r) c= M )
hence ex r being Real st
( r > 0 & Ball (v,r) c= M ) by A1, Def5; ::_thesis: verum
end;
assume for v being Point of V st v in M holds
ex r being Real st
( r > 0 & Ball (v,r) c= M ) ; ::_thesis: M is open
hence M in the topology of (TopUnitSpace V) by Def5; :: according to PRE_TOPC:def_2 ::_thesis: verum
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)
proof
let V be RealUnitarySpace; ::_thesis: 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)
let v1, v2 be Point of V; ::_thesis: 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)
let r1, r2 be Real; ::_thesis: ex u being Point of V ex r being Real st (Ball (v1,r1)) \/ (Ball (v2,r2)) c= Ball (u,r)
reconsider u = v1 as Point of V ;
reconsider r = ((abs r1) + (abs r2)) + (dist (v1,v2)) as Real ;
take u ; ::_thesis: ex r being Real st (Ball (v1,r1)) \/ (Ball (v2,r2)) c= Ball (u,r)
take r ; ::_thesis: (Ball (v1,r1)) \/ (Ball (v2,r2)) c= Ball (u,r)
for a being set st a in (Ball (v1,r1)) \/ (Ball (v2,r2)) holds
a in Ball (u,r)
proof
let a be set ; ::_thesis: ( a in (Ball (v1,r1)) \/ (Ball (v2,r2)) implies a in Ball (u,r) )
assume A1: a in (Ball (v1,r1)) \/ (Ball (v2,r2)) ; ::_thesis: a in Ball (u,r)
then reconsider a = a as Point of V ;
now__::_thesis:_(_(_a_in_Ball_(v1,r1)_&_a_in_Ball_(u,r)_)_or_(_a_in_Ball_(v2,r2)_&_a_in_Ball_(u,r)_)_)
percases ( a in Ball (v1,r1) or a in Ball (v2,r2) ) by A1, XBOOLE_0:def_3;
case a in Ball (v1,r1) ; ::_thesis: a in Ball (u,r)
then A2: dist (u,a) < r1 by BHSP_2:41;
( r1 <= abs r1 & 0 <= abs r2 ) by ABSVALUE:4, COMPLEX1:46;
then A3: r1 + 0 <= (abs r1) + (abs r2) by XREAL_1:7;
0 <= dist (v1,v2) by BHSP_1:37;
then r1 + 0 <= ((abs r1) + (abs r2)) + (dist (v1,v2)) by A3, XREAL_1:7;
then (dist (u,a)) - r < r1 - r1 by A2, XREAL_1:14;
then ((dist (u,a)) - r) + r < 0 + r by XREAL_1:8;
hence a in Ball (u,r) by BHSP_2:41; ::_thesis: verum
end;
case a in Ball (v2,r2) ; ::_thesis: a in Ball (u,r)
then dist (v2,a) < r2 by BHSP_2:41;
then (dist (v2,a)) - (abs r2) < r2 - r2 by ABSVALUE:4, XREAL_1:14;
then ((dist (v2,a)) - (abs r2)) + (abs r2) < 0 + (abs r2) by XREAL_1:8;
then (dist (u,a)) - (abs r2) < ((dist (v1,v2)) + (dist (v2,a))) - (dist (v2,a)) by BHSP_1:35, XREAL_1:15;
then ((dist (u,a)) - (abs r2)) - (abs r1) < (dist (v1,v2)) - 0 by COMPLEX1:46, XREAL_1:14;
then ((dist (u,a)) - ((abs r1) + (abs r2))) + ((abs r1) + (abs r2)) < ((abs r1) + (abs r2)) + (dist (v1,v2)) by XREAL_1:8;
hence a in Ball (u,r) by BHSP_2:41; ::_thesis: verum
end;
end;
end;
hence a in Ball (u,r) ; ::_thesis: verum
end;
hence (Ball (v1,r1)) \/ (Ball (v2,r2)) c= Ball (u,r) by TARSKI:def_3; ::_thesis: verum
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
proof
let V be RealUnitarySpace; ::_thesis: 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
let M be Subset of (TopUnitSpace V); ::_thesis: for v being VECTOR of V
for r being Real st M = cl_Ball (v,r) holds
M is closed
let v be VECTOR of V; ::_thesis: for r being Real st M = cl_Ball (v,r) holds
M is closed
let r be Real; ::_thesis: ( M = cl_Ball (v,r) implies M is closed )
assume A1: M = cl_Ball (v,r) ; ::_thesis: M is closed
for x being set holds
( x in M ` iff ex Q being Subset of (TopUnitSpace V) st
( Q is open & Q c= M ` & x in Q ) )
proof
let x be set ; ::_thesis: ( x in M ` iff ex Q being Subset of (TopUnitSpace V) st
( Q is open & Q c= M ` & x in Q ) )
thus ( x in M ` implies ex Q being Subset of (TopUnitSpace V) st
( Q is open & Q c= M ` & x in Q ) ) ::_thesis: ( ex Q being Subset of (TopUnitSpace V) st
( Q is open & Q c= M ` & x in Q ) implies x in M ` )
proof
assume A2: x in M ` ; ::_thesis: ex Q being Subset of (TopUnitSpace V) st
( Q is open & Q c= M ` & x in Q )
then reconsider e = x as Point of V ;
reconsider Q = Ball (e,((dist (e,v)) - r)) as Subset of (TopUnitSpace V) ;
take Q ; ::_thesis: ( Q is open & Q c= M ` & x in Q )
thus Q is open by Th50; ::_thesis: ( Q c= M ` & x in Q )
thus Q c= M ` ::_thesis: x in Q
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Q or q in M ` )
assume A3: q in Q ; ::_thesis: q in M `
then reconsider f = q as Point of V ;
dist (e,v) <= (dist (e,f)) + (dist (f,v)) by BHSP_1:35;
then A4: (dist (e,v)) - r <= ((dist (e,f)) + (dist (f,v))) - r by XREAL_1:9;
dist (e,f) < (dist (e,v)) - r by A3, BHSP_2:41;
then dist (e,f) < ((dist (e,f)) + (dist (f,v))) - r by A4, XXREAL_0:2;
then (dist (e,f)) - (dist (e,f)) < (((dist (e,f)) + (dist (f,v))) - r) - (dist (e,f)) by XREAL_1:9;
then 0 < (((dist (e,f)) - (dist (e,f))) + (dist (f,v))) - r ;
then dist (f,v) > r by XREAL_1:47;
then not q in M by A1, BHSP_2:48;
hence q in M ` by A3, SUBSET_1:29; ::_thesis: verum
end;
not x in M by A2, XBOOLE_0:def_5;
then dist (v,e) > r by A1, BHSP_2:48;
then (dist (e,v)) - r > r - r by XREAL_1:9;
hence x in Q by BHSP_2:42; ::_thesis: verum
end;
thus ( ex Q being Subset of (TopUnitSpace V) st
( Q is open & Q c= M ` & x in Q ) implies x in M ` ) ; ::_thesis: verum
end;
then M ` is open by TOPS_1:25;
hence M is closed by TOPS_1:3; ::_thesis: verum
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
proof
let V be RealUnitarySpace; ::_thesis: 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
let M be Subset of (TopUnitSpace V); ::_thesis: for v being VECTOR of V
for r being Real st M = Sphere (v,r) holds
M is closed
let v be VECTOR of V; ::_thesis: for r being Real st M = Sphere (v,r) holds
M is closed
let r be Real; ::_thesis: ( M = Sphere (v,r) implies M is closed )
reconsider B = cl_Ball (v,r), C = Ball (v,r) as Subset of (TopUnitSpace V) ;
assume A1: M = Sphere (v,r) ; ::_thesis: M is closed
A2: M ` = (B `) \/ C
proof
hereby :: according to XBOOLE_0:def_10,TARSKI:def_3 ::_thesis: (B `) \/ C c= M `
let a be set ; ::_thesis: ( a in M ` implies a in (B `) \/ C )
assume A3: a in M ` ; ::_thesis: a in (B `) \/ C
then reconsider e = a as Point of V ;
not a in M by A3, XBOOLE_0:def_5;
then dist (e,v) <> r by A1, BHSP_2:52;
then ( dist (e,v) < r or dist (e,v) > r ) by XXREAL_0:1;
then ( e in Ball (v,r) or not e in cl_Ball (v,r) ) by BHSP_2:41, BHSP_2:48;
then ( e in Ball (v,r) or e in (cl_Ball (v,r)) ` ) by SUBSET_1:29;
hence a in (B `) \/ C by XBOOLE_0:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (B `) \/ C or a in M ` )
assume A4: a in (B `) \/ C ; ::_thesis: a in M `
then reconsider e = a as Point of V ;
( a in B ` or a in C ) by A4, XBOOLE_0:def_3;
then ( not e in cl_Ball (v,r) or e in C ) by XBOOLE_0:def_5;
then ( dist (e,v) > r or dist (e,v) < r ) by BHSP_2:41, BHSP_2:48;
then not a in M by A1, BHSP_2:52;
hence a in M ` by A4, SUBSET_1:29; ::_thesis: verum
end;
( B is closed & C is open ) by Th50, Th53;
hence M is closed by A2, TOPS_1:3; ::_thesis: verum
end;