:: 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;