:: RUSUB_5 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let V be non empty RLSStruct ;
let M, N be Affine Subset of V;
pred M 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty right_zeroed RLSStruct
for M being Affine Subset of V holds M is_parallel_to M
proof end;

theorem Th2: :: RUSUB_5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty add-associative right_zeroed right_complementable RLSStruct
for M, N being Affine Subset of V st M is_parallel_to N holds
N is_parallel_to M
proof end;

theorem Th3: :: RUSUB_5:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty Abelian add-associative right_zeroed right_complementable 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 end;

definition
let V be non empty LoopStr ;
let M, N be Subset of V;
func M - N -> Subset of V equals :: RUSUB_5:def 2
{ (u - v) where u, v is Element of V : ( u in M & v in N ) } ;
coherence
{ (u - v) where u, v is Element of V : ( u in M & v in N ) } is Subset of V
proof end;
end;

:: deftheorem defines - RUSUB_5:def 2 :
for V being non empty LoopStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for M, N being Affine Subset of V holds M - N is Affine
proof end;

theorem :: RUSUB_5:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty LoopStr
for M, N being Subset of V st ( M is empty or N is empty ) holds
M + N is empty
proof end;

theorem :: RUSUB_5:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty LoopStr
for M, N being non empty Subset of V holds not M + N is empty
proof end;

theorem :: RUSUB_5:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty LoopStr
for M, N being Subset of V st ( M is empty or N is empty ) holds
M - N is empty
proof end;

theorem Th8: :: RUSUB_5:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty LoopStr
for M, N being non empty Subset of V holds not M - N is empty
proof end;

theorem Th9: :: RUSUB_5:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for M, N being Subset of V
for v being Element of V holds
( M = N + {v} iff M - {v} = N )
proof end;

theorem :: RUSUB_5:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for M, N being Subset of V
for v being Element of V st v in N holds
M + {v} c= M + N
proof end;

theorem :: RUSUB_5:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for M, N being Subset of V
for v being Element of V st v in N holds
M - {v} c= M - N
proof end;

theorem Th12: :: RUSUB_5:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for M being non empty Subset of V holds 0. V in M - M
proof end;

theorem Th13: :: RUSUB_5:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th14: :: RUSUB_5:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th15: :: RUSUB_5:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th16: :: RUSUB_5:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th17: :: RUSUB_5:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th18: :: RUSUB_5:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th19: :: RUSUB_5:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RUSUB_5:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

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 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealUnitarySpace
for W being Subspace of V holds 0. V in Ort_Comp W
proof end;

theorem :: RUSUB_5:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealUnitarySpace holds Ort_Comp ((0). V) = (Omega). V
proof end;

theorem :: RUSUB_5:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealUnitarySpace holds Ort_Comp ((Omega). V) = (0). V
proof end;

theorem :: RUSUB_5:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th25: :: RUSUB_5:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealUnitarySpace
for M being non empty Subset of V holds M c= the carrier of (Ort_Comp (Ort_Comp M))
proof end;

theorem Th26: :: RUSUB_5:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th27: :: RUSUB_5:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RUSUB_5:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealUnitarySpace
for M being non empty Subset of V holds Ort_Comp M = Ort_Comp (Ort_Comp (Ort_Comp M))
proof end;

theorem Th29: :: RUSUB_5:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RUSUB_5:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RUSUB_5:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RUSUB_5:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

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 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th34: :: RUSUB_5:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th35: :: RUSUB_5:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RUSUB_5:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th37: :: RUSUB_5:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealUnitarySpace
for v being Point of V
for r being Real holds Ball v,r in Family_open_set V
proof end;

theorem Th38: :: RUSUB_5:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealUnitarySpace holds the carrier of V in Family_open_set V
proof end;

theorem Th39: :: RUSUB_5:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th40: :: RUSUB_5:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th41: :: RUSUB_5:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealUnitarySpace holds TopStruct(# the carrier of V,(Family_open_set V) #) is TopSpace
proof 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 TopSpace-like ;
coherence
not TopUnitSpace V is empty
;
end;

theorem :: RUSUB_5:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealUnitarySpace
for M being Subset of (TopUnitSpace V) st M = [#] V holds
( M is open & M is closed )
proof end;

theorem :: RUSUB_5:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealUnitarySpace
for M being Subset of (TopUnitSpace V) st M = {} V holds
( M is open & M is closed )
proof end;

theorem :: RUSUB_5:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RUSUB_5:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RUSUB_5:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealUnitarySpace
for v being VECTOR of V
for r being Real st r = 0 holds
Ball v,r is empty
proof end;

theorem :: RUSUB_5:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RUSUB_5:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RUSUB_5:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RUSUB_5:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RUSUB_5:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th53: :: RUSUB_5:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RUSUB_5:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;