:: RLAFFIN3 semantic presentation
begin
Lm1: for n being Nat
for f being b1 -element real-valued FinSequence holds f is Point of (TOP-REAL n)
proof
let n be Nat; ::_thesis: for f being n -element real-valued FinSequence holds f is Point of (TOP-REAL n)
let f be n -element real-valued FinSequence; ::_thesis: f is Point of (TOP-REAL n)
( len f = n & @ (@ f) = f ) by CARD_1:def_7;
hence f is Point of (TOP-REAL n) by TOPREAL3:46; ::_thesis: verum
end;
theorem Th1: :: RLAFFIN3:1
for f1, f2 being real-valued FinSequence
for r being real number holds (Intervals (f1,r)) ^ (Intervals (f2,r)) = Intervals ((f1 ^ f2),r)
proof
let f1, f2 be real-valued FinSequence; ::_thesis: for r being real number holds (Intervals (f1,r)) ^ (Intervals (f2,r)) = Intervals ((f1 ^ f2),r)
let r be real number ; ::_thesis: (Intervals (f1,r)) ^ (Intervals (f2,r)) = Intervals ((f1 ^ f2),r)
set I1 = Intervals (f1,r);
set I2 = Intervals (f2,r);
set f12 = f1 ^ f2;
set I12 = Intervals ((f1 ^ f2),r);
A1: dom (Intervals ((f1 ^ f2),r)) = dom (f1 ^ f2) by EUCLID_9:def_3;
A2: ( len (f1 ^ f2) = (len f1) + (len f2) & len ((Intervals (f1,r)) ^ (Intervals (f2,r))) = (len (Intervals (f1,r))) + (len (Intervals (f2,r))) ) by FINSEQ_1:22;
A3: dom (Intervals (f1,r)) = dom f1 by EUCLID_9:def_3;
then A4: len (Intervals (f1,r)) = len f1 by FINSEQ_3:29;
A5: dom (Intervals (f2,r)) = dom f2 by EUCLID_9:def_3;
then len (Intervals (f2,r)) = len f2 by FINSEQ_3:29;
then A6: dom ((Intervals (f1,r)) ^ (Intervals (f2,r))) = dom (Intervals ((f1 ^ f2),r)) by A1, A4, A2, FINSEQ_3:29;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_((Intervals_(f1,r))_^_(Intervals_(f2,r)))_holds_
((Intervals_(f1,r))_^_(Intervals_(f2,r)))_._i_=_(Intervals_((f1_^_f2),r))_._i
let i be Nat; ::_thesis: ( i in dom ((Intervals (f1,r)) ^ (Intervals (f2,r))) implies ((Intervals (f1,r)) ^ (Intervals (f2,r))) . b1 = (Intervals ((f1 ^ f2),r)) . b1 )
assume A7: i in dom ((Intervals (f1,r)) ^ (Intervals (f2,r))) ; ::_thesis: ((Intervals (f1,r)) ^ (Intervals (f2,r))) . b1 = (Intervals ((f1 ^ f2),r)) . b1
then A8: (Intervals ((f1 ^ f2),r)) . i = ].(((f1 ^ f2) . i) - r),(((f1 ^ f2) . i) + r).[ by A1, A6, EUCLID_9:def_3;
percases ( i in dom (Intervals (f1,r)) or ex j being Nat st
( j in dom (Intervals (f2,r)) & i = (len (Intervals (f1,r))) + j ) ) by A7, FINSEQ_1:25;
supposeA9: i in dom (Intervals (f1,r)) ; ::_thesis: ((Intervals (f1,r)) ^ (Intervals (f2,r))) . b1 = (Intervals ((f1 ^ f2),r)) . b1
then ( ((Intervals (f1,r)) ^ (Intervals (f2,r))) . i = (Intervals (f1,r)) . i & (f1 ^ f2) . i = f1 . i ) by A3, FINSEQ_1:def_7;
hence ((Intervals (f1,r)) ^ (Intervals (f2,r))) . i = (Intervals ((f1 ^ f2),r)) . i by A3, A8, A9, EUCLID_9:def_3; ::_thesis: verum
end;
suppose ex j being Nat st
( j in dom (Intervals (f2,r)) & i = (len (Intervals (f1,r))) + j ) ; ::_thesis: ((Intervals (f1,r)) ^ (Intervals (f2,r))) . b1 = (Intervals ((f1 ^ f2),r)) . b1
then consider j being Nat such that
A10: j in dom (Intervals (f2,r)) and
A11: i = (len (Intervals (f1,r))) + j ;
( ((Intervals (f1,r)) ^ (Intervals (f2,r))) . i = (Intervals (f2,r)) . j & (f1 ^ f2) . i = f2 . j ) by A5, A4, A10, A11, FINSEQ_1:def_7;
hence ((Intervals (f1,r)) ^ (Intervals (f2,r))) . i = (Intervals ((f1 ^ f2),r)) . i by A5, A8, A10, EUCLID_9:def_3; ::_thesis: verum
end;
end;
end;
hence (Intervals (f1,r)) ^ (Intervals (f2,r)) = Intervals ((f1 ^ f2),r) by A6, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th2: :: RLAFFIN3:2
for x being set
for f1, f2 being FinSequence holds
( x in product (f1 ^ f2) iff ex p1, p2 being FinSequence st
( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 ) )
proof
let x be set ; ::_thesis: for f1, f2 being FinSequence holds
( x in product (f1 ^ f2) iff ex p1, p2 being FinSequence st
( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 ) )
let f1, f2 be FinSequence; ::_thesis: ( x in product (f1 ^ f2) iff ex p1, p2 being FinSequence st
( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 ) )
set f12 = f1 ^ f2;
A1: len (f1 ^ f2) = (len f1) + (len f2) by FINSEQ_1:22;
dom f1 = Seg (len f1) by FINSEQ_1:def_3;
then A2: (f1 ^ f2) | (Seg (len f1)) = f1 by FINSEQ_1:21;
hereby ::_thesis: ( ex p1, p2 being FinSequence st
( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 ) implies x in product (f1 ^ f2) )
assume A3: x in product (f1 ^ f2) ; ::_thesis: ex p1 being set ex p2 being FinSequence st
( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 )
then consider g being Function such that
A4: x = g and
A5: dom g = dom (f1 ^ f2) and
A6: for y being set st y in dom (f1 ^ f2) holds
g . y in (f1 ^ f2) . y by CARD_3:def_5;
dom (f1 ^ f2) = Seg (len (f1 ^ f2)) by FINSEQ_1:def_3;
then reconsider g = g as FinSequence by A5, FINSEQ_1:def_2;
set p1 = g | (len f1);
consider p2 being FinSequence such that
A7: g = (g | (len f1)) ^ p2 by FINSEQ_1:80;
take p1 = g | (len f1); ::_thesis: ex p2 being FinSequence st
( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 )
take p2 = p2; ::_thesis: ( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 )
thus ( x = p1 ^ p2 & p1 in product f1 ) by A2, A3, A4, A7, PRALG_3:1; ::_thesis: p2 in product f2
A8: len (f1 ^ f2) = len g by A5, FINSEQ_3:29;
then A9: len f1 = len p1 by A1, FINSEQ_1:59, NAT_1:11;
len g = (len p1) + (len p2) by A7, FINSEQ_1:22;
then A10: dom f2 = dom p2 by A1, A8, A9, FINSEQ_3:29;
now__::_thesis:_for_y_being_set_st_y_in_dom_f2_holds_
p2_._y_in_f2_._y
let y be set ; ::_thesis: ( y in dom f2 implies p2 . y in f2 . y )
assume A11: y in dom f2 ; ::_thesis: p2 . y in f2 . y
then reconsider i = y as Nat ;
i + (len f1) in dom (f1 ^ f2) by A11, FINSEQ_1:28;
then ( g . (i + (len f1)) in (f1 ^ f2) . (i + (len f1)) & (f1 ^ f2) . (i + (len f1)) = f2 . i ) by A6, A11, FINSEQ_1:def_7;
hence p2 . y in f2 . y by A7, A9, A10, A11, FINSEQ_1:def_7; ::_thesis: verum
end;
hence p2 in product f2 by A10, CARD_3:def_5; ::_thesis: verum
end;
given p1, p2 being FinSequence such that A12: x = p1 ^ p2 and
A13: p1 in product f1 and
A14: p2 in product f2 ; ::_thesis: x in product (f1 ^ f2)
A15: ex g being Function st
( p2 = g & dom g = dom f2 & ( for y being set st y in dom f2 holds
g . y in f2 . y ) ) by A14, CARD_3:def_5;
A16: ex g being Function st
( p1 = g & dom g = dom f1 & ( for y being set st y in dom f1 holds
g . y in f1 . y ) ) by A13, CARD_3:def_5;
then A17: len p1 = len f1 by FINSEQ_3:29;
A18: now__::_thesis:_for_y_being_set_st_y_in_dom_(f1_^_f2)_holds_
(p1_^_p2)_._y_in_(f1_^_f2)_._y
let y be set ; ::_thesis: ( y in dom (f1 ^ f2) implies (p1 ^ p2) . b1 in (f1 ^ f2) . b1 )
assume A19: y in dom (f1 ^ f2) ; ::_thesis: (p1 ^ p2) . b1 in (f1 ^ f2) . b1
then reconsider i = y as Nat ;
percases ( i in dom f1 or ex j being Nat st
( j in dom f2 & i = (len f1) + j ) ) by A19, FINSEQ_1:25;
supposeA20: i in dom f1 ; ::_thesis: (p1 ^ p2) . b1 in (f1 ^ f2) . b1
then ( (f1 ^ f2) . y = f1 . i & (p1 ^ p2) . y = p1 . i ) by A16, FINSEQ_1:def_7;
hence (p1 ^ p2) . y in (f1 ^ f2) . y by A16, A20; ::_thesis: verum
end;
suppose ex j being Nat st
( j in dom f2 & i = (len f1) + j ) ; ::_thesis: (p1 ^ p2) . b1 in (f1 ^ f2) . b1
then consider j being Nat such that
A21: j in dom f2 and
A22: i = (len f1) + j ;
( (f1 ^ f2) . y = f2 . j & (p1 ^ p2) . y = p2 . j ) by A15, A17, A21, A22, FINSEQ_1:def_7;
hence (p1 ^ p2) . y in (f1 ^ f2) . y by A15, A21; ::_thesis: verum
end;
end;
end;
( len (p1 ^ p2) = (len p1) + (len p2) & len p2 = len f2 ) by A15, FINSEQ_1:22, FINSEQ_3:29;
then dom (p1 ^ p2) = dom (f1 ^ f2) by A1, A17, FINSEQ_3:29;
hence x in product (f1 ^ f2) by A12, A18, CARD_3:def_5; ::_thesis: verum
end;
Lm2: for V being RealLinearSpace
for A being Subset of V holds Lin A = Lin (A \ {(0. V)})
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds Lin A = Lin (A \ {(0. V)})
let A be Subset of V; ::_thesis: Lin A = Lin (A \ {(0. V)})
percases ( not 0. V in A or 0. V in A ) ;
suppose not 0. V in A ; ::_thesis: Lin A = Lin (A \ {(0. V)})
hence Lin A = Lin (A \ {(0. V)}) by ZFMISC_1:57; ::_thesis: verum
end;
supposeA1: 0. V in A ; ::_thesis: Lin A = Lin (A \ {(0. V)})
{(0. V)} = the carrier of ((0). V) by RLSUB_1:def_3;
then A2: Lin {(0. V)} = (0). V by RLVECT_3:18;
A = (A \ {(0. V)}) \/ {(0. V)} by A1, ZFMISC_1:116;
hence Lin A = (Lin (A \ {(0. V)})) + ((0). V) by A2, RLVECT_3:22
.= Lin (A \ {(0. V)}) by RLSUB_2:9 ;
::_thesis: verum
end;
end;
end;
theorem Th3: :: RLAFFIN3:3
for V being RealLinearSpace holds
( V is finite-dimensional iff (Omega). V is finite-dimensional )
proof
let V be RealLinearSpace; ::_thesis: ( V is finite-dimensional iff (Omega). V is finite-dimensional )
set O = (Omega). V;
thus ( V is finite-dimensional implies (Omega). V is finite-dimensional ) ; ::_thesis: ( (Omega). V is finite-dimensional implies V is finite-dimensional )
assume (Omega). V is finite-dimensional ; ::_thesis: V is finite-dimensional
then consider A being finite Subset of ((Omega). V) such that
A1: A is Basis of (Omega). V by RLVECT_5:def_1;
A2: RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = (Omega). V by RLSUB_1:def_4;
then reconsider a = A as finite Subset of V ;
Lin A = (Omega). V by A1, RLVECT_3:def_3;
then A3: Lin a = (Omega). V by RLVECT_5:20;
A is linearly-independent by A1, RLVECT_3:def_3;
then a is linearly-independent by RLVECT_5:14;
then a is Basis of V by A2, A3, RLVECT_3:def_3;
hence V is finite-dimensional by RLVECT_5:def_1; ::_thesis: verum
end;
registration
let V be finite-dimensional RealLinearSpace;
cluster affinely-independent -> finite affinely-independent for Element of bool the carrier of V;
coherence
for b1 being affinely-independent Subset of V holds b1 is finite
proof
let A be affinely-independent Subset of V; ::_thesis: A is finite
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: A is finite
hence A is finite ; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: A is finite
then consider v being VECTOR of V such that
v in A and
A1: ((- v) + A) \ {(0. V)} is linearly-independent by RLAFFIN1:def_4;
set vA = (- v) + A;
(((- v) + A) \ {(0. V)}) \/ {(0. V)} = ((- v) + A) \/ {(0. V)} by XBOOLE_1:39;
then A2: ( card ((- v) + A) = card A & (- v) + A c= (((- v) + A) \ {(0. V)}) \/ {(0. V)} ) by RLAFFIN1:7, XBOOLE_1:7;
((- v) + A) \ {(0. V)} is finite by A1, RLVECT_5:24;
hence A is finite by A2; ::_thesis: verum
end;
end;
end;
end;
registration
let n be Nat;
cluster TOP-REAL n -> add-continuous Mult-continuous ;
coherence
( TOP-REAL n is add-continuous & TOP-REAL n is Mult-continuous )
proof
set T = TOP-REAL n;
set E = Euclid n;
set TE = TopSpaceMetr (Euclid n);
A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
A2: n in NAT by ORDINAL1:def_12;
thus TOP-REAL n is add-continuous ::_thesis: TOP-REAL n is Mult-continuous
proof
let x1, x2 be Point of (TOP-REAL n); :: according to RLTOPSP1:def_8 ::_thesis: for b1 being Element of bool the carrier of (TOP-REAL n) holds
( not b1 is open or not x1 + x2 in b1 or ex b2, b3 being Element of bool the carrier of (TOP-REAL n) st
( b2 is open & b3 is open & x1 in b2 & x2 in b3 & b2 + b3 c= b1 ) )
let V be Subset of (TOP-REAL n); ::_thesis: ( not V is open or not x1 + x2 in V or ex b1, b2 being Element of bool the carrier of (TOP-REAL n) st
( b1 is open & b2 is open & x1 in b1 & x2 in b2 & b1 + b2 c= V ) )
assume that
A3: V is open and
A4: x1 + x2 in V ; ::_thesis: ex b1, b2 being Element of bool the carrier of (TOP-REAL n) st
( b1 is open & b2 is open & x1 in b1 & x2 in b2 & b1 + b2 c= V )
reconsider X1 = x1, X2 = x2, X12 = x1 + x2 as Point of (Euclid n) by A1, TOPMETR:12;
reconsider v = V as Subset of (TopSpaceMetr (Euclid n)) by A1;
V in the topology of (TOP-REAL n) by A3, PRE_TOPC:def_2;
then v is open by A1, PRE_TOPC:def_2;
then consider r being real number such that
A5: r > 0 and
A6: Ball (X12,r) c= v by A4, TOPMETR:15;
set r2 = r / 2;
reconsider B1 = Ball (X1,(r / 2)), B2 = Ball (X2,(r / 2)) as Subset of (TOP-REAL n) by A1, TOPMETR:12;
take B1 ; ::_thesis: ex b1 being Element of bool the carrier of (TOP-REAL n) st
( B1 is open & b1 is open & x1 in B1 & x2 in b1 & B1 + b1 c= V )
take B2 ; ::_thesis: ( B1 is open & B2 is open & x1 in B1 & x2 in B2 & B1 + B2 c= V )
thus ( B1 is open & B2 is open & x1 in B1 & x2 in B2 ) by A5, GOBOARD6:1, GOBOARD6:3, XREAL_1:215; ::_thesis: B1 + B2 c= V
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B1 + B2 or x in V )
assume x in B1 + B2 ; ::_thesis: x in V
then x in { (b1 + b2) where b1, b2 is Element of (TOP-REAL n) : ( b1 in B1 & b2 in B2 ) } by RUSUB_4:def_9;
then consider b1, b2 being Element of (TOP-REAL n) such that
A7: x = b1 + b2 and
A8: b1 in B1 and
A9: b2 in B2 ;
reconsider e1 = b1, e2 = b2, e12 = b1 + b2 as Point of (Euclid n) by A1, TOPMETR:12;
reconsider y1 = x1, y2 = x2, c1 = b1, c2 = b2 as Element of REAL n by EUCLID:22;
dist (X2,e2) < r / 2 by A9, METRIC_1:11;
then A10: |.(y2 - c2).| < r / 2 by A2, SPPOL_1:5;
dist (X1,e1) < r / 2 by A8, METRIC_1:11;
then |.(y1 - c1).| < r / 2 by A2, SPPOL_1:5;
then A11: |.(y1 - c1).| + |.(y2 - c2).| < (r / 2) + (r / 2) by A10, XREAL_1:8;
A12: (y1 + y2) - (c1 + c2) = (y1 + y2) + (- (c2 + c1)) by RVSUM_1:31
.= (y1 + y2) + ((- c2) + (- c1)) by RVSUM_1:26
.= ((y1 + y2) + (- c2)) + (- c1) by RVSUM_1:15
.= ((y2 + (- c2)) + y1) + (- c1) by RVSUM_1:15
.= (y2 + (- c2)) + (y1 + (- c1)) by RVSUM_1:15
.= (y2 - c2) + (y1 + (- c1)) by RVSUM_1:31
.= (y2 - c2) + (y1 - c1) by RVSUM_1:31 ;
A13: dist (X12,e12) = |.((y1 - c1) + (y2 - c2)).| by A2, A12, SPPOL_1:5;
|.((y1 - c1) + (y2 - c2)).| <= |.(y1 - c1).| + |.(y2 - c2).| by EUCLID:12;
then dist (X12,e12) < r by A11, A13, XXREAL_0:2;
then e12 in Ball (X12,r) by METRIC_1:11;
hence x in V by A6, A7; ::_thesis: verum
end;
let a be Real; :: according to RLTOPSP1:def_9 ::_thesis: for b1 being Element of the carrier of (TOP-REAL n)
for b2 being Element of bool the carrier of (TOP-REAL n) holds
( not b2 is open or not a * b1 in b2 or ex b3 being Element of REAL ex b4 being Element of bool the carrier of (TOP-REAL n) st
( b4 is open & b1 in b4 & ( for b5 being Element of REAL holds
( b3 <= abs (b5 - a) or b5 * b4 c= b2 ) ) ) )
let x be Point of (TOP-REAL n); ::_thesis: for b1 being Element of bool the carrier of (TOP-REAL n) holds
( not b1 is open or not a * x in b1 or ex b2 being Element of REAL ex b3 being Element of bool the carrier of (TOP-REAL n) st
( b3 is open & x in b3 & ( for b4 being Element of REAL holds
( b2 <= abs (b4 - a) or b4 * b3 c= b1 ) ) ) )
let V be Subset of (TOP-REAL n); ::_thesis: ( not V is open or not a * x in V or ex b1 being Element of REAL ex b2 being Element of bool the carrier of (TOP-REAL n) st
( b2 is open & x in b2 & ( for b3 being Element of REAL holds
( b1 <= abs (b3 - a) or b3 * b2 c= V ) ) ) )
assume that
A14: V is open and
A15: a * x in V ; ::_thesis: ex b1 being Element of REAL ex b2 being Element of bool the carrier of (TOP-REAL n) st
( b2 is open & x in b2 & ( for b3 being Element of REAL holds
( b1 <= abs (b3 - a) or b3 * b2 c= V ) ) )
reconsider X = x, AX = a * x as Point of (Euclid n) by A1, TOPMETR:12;
reconsider v = V as Subset of (TopSpaceMetr (Euclid n)) by A1;
V in the topology of (TOP-REAL n) by A14, PRE_TOPC:def_2;
then v is open by A1, PRE_TOPC:def_2;
then consider r being real number such that
A16: r > 0 and
A17: Ball (AX,r) c= v by A15, TOPMETR:15;
set r2 = r / 2;
A18: r / 2 > 0 by A16, XREAL_1:215;
then A19: (r / 2) / 2 > 0 by XREAL_1:215;
ex m being positive Real st (abs a) * m < r / 2
proof
percases ( abs a = 0 or abs a > 0 ) by COMPLEX1:46;
suppose abs a = 0 ; ::_thesis: ex m being positive Real st (abs a) * m < r / 2
then (abs a) * 1 < r / 2 by A16, XREAL_1:215;
hence ex m being positive Real st (abs a) * m < r / 2 ; ::_thesis: verum
end;
supposeA20: abs a > 0 ; ::_thesis: ex m being positive Real st (abs a) * m < r / 2
then reconsider m = ((r / 2) / 2) / (abs a) as positive Real by A19, XREAL_1:139;
take m ; ::_thesis: (abs a) * m < r / 2
(r / 2) / 2 < r / 2 by A16, XREAL_1:215, XREAL_1:216;
hence (abs a) * m < r / 2 by A20, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;
then consider m being positive Real such that
A21: (abs a) * m < r / 2 ;
reconsider B = Ball (X,m) as Subset of (TOP-REAL n) by A1, TOPMETR:12;
reconsider nr = (r / 2) / (|.x.| + m) as positive Real by A18, XREAL_1:139;
take nr ; ::_thesis: ex b1 being Element of bool the carrier of (TOP-REAL n) st
( b1 is open & x in b1 & ( for b2 being Element of REAL holds
( nr <= abs (b2 - a) or b2 * b1 c= V ) ) )
take B ; ::_thesis: ( B is open & x in B & ( for b1 being Element of REAL holds
( nr <= abs (b1 - a) or b1 * B c= V ) ) )
thus ( B is open & x in B ) by GOBOARD6:1, GOBOARD6:3; ::_thesis: for b1 being Element of REAL holds
( nr <= abs (b1 - a) or b1 * B c= V )
let s be Real; ::_thesis: ( nr <= abs (s - a) or s * B c= V )
assume A22: abs (s - a) < nr ; ::_thesis: s * B c= V
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in s * B or z in V )
assume z in s * B ; ::_thesis: z in V
then z in { (s * b) where b is Element of (TOP-REAL n) : b in B } by CONVEX1:def_1;
then consider b being Element of (TOP-REAL n) such that
A23: z = s * b and
A24: b in B ;
reconsider e = b, se = s * b as Point of (Euclid n) by A1, TOPMETR:12;
reconsider y = x, c = b as Element of REAL n by EUCLID:22;
reconsider Y = y, C = c as Element of n -tuples_on REAL by EUCLID:def_1;
c = C - (n |-> 0) by RVSUM_1:32
.= C - (Y - Y) by RVSUM_1:37
.= (C - Y) + Y by RVSUM_1:41 ;
then A25: |.c.| <= |.(c - y).| + |.y.| by EUCLID:12;
A26: dist (X,e) < m by A24, METRIC_1:11;
then |.(c - y).| < m by A2, SPPOL_1:5;
then |.(c - y).| + |.y.| <= m + |.x.| by XREAL_1:6;
then |.c.| <= m + |.x.| by A25, XXREAL_0:2;
then A27: nr * |.c.| <= nr * (m + |.x.|) by XREAL_1:64;
(a * y) + (- (a * c)) = (a * y) + ((- 1) * (a * c)) by RVSUM_1:54
.= (a * y) + (((- 1) * a) * c) by RVSUM_1:49
.= (a * y) + (a * ((- 1) * c)) by RVSUM_1:49
.= a * (y + ((- 1) * c)) by RVSUM_1:51
.= a * (y + (- c)) by RVSUM_1:54
.= a * (y - c) by RVSUM_1:31 ;
then A28: |.((a * y) + (- (a * c))).| = (abs a) * |.(y - c).| by EUCLID:11;
( abs a >= 0 & |.(y - c).| = dist (X,e) ) by A2, COMPLEX1:46, SPPOL_1:5;
then |.((a * y) + (- (a * c))).| <= (abs a) * m by A26, A28, XREAL_1:64;
then A29: |.((a * y) + (- (a * c))).| < r / 2 by A21, XXREAL_0:2;
(a * c) + (- (s * c)) = (a * c) + ((- 1) * (s * c)) by RVSUM_1:54
.= (a * c) + (((- 1) * s) * c) by RVSUM_1:49
.= (a + ((- 1) * s)) * c by RVSUM_1:50 ;
then |.((a * c) + (- (s * c))).| = (abs (a - s)) * |.c.| by EUCLID:11
.= (abs (- (a - s))) * |.c.| by COMPLEX1:52 ;
then ( nr * (|.x.| + m) = r / 2 & |.((a * c) + (- (s * c))).| <= nr * |.c.| ) by A22, XCMPLX_1:87, XREAL_1:64;
then |.((a * c) + (- (s * c))).| <= r / 2 by A27, XXREAL_0:2;
then A30: ( |.(((a * y) + (- (a * c))) + ((a * c) + (- (s * c)))).| <= |.((a * y) + (- (a * c))).| + |.((a * c) + (- (s * c))).| & |.((a * y) + (- (a * c))).| + |.((a * c) + (- (s * c))).| < (r / 2) + (r / 2) ) by A29, EUCLID:12, XREAL_1:8;
(a * y) - (s * c) = ((a * Y) - (n |-> 0)) - (s * C) by RVSUM_1:32
.= ((a * y) - ((a * C) - (a * C))) - (s * c) by RVSUM_1:37
.= (((a * y) - (a * C)) + (a * C)) - (s * c) by RVSUM_1:41
.= (((a * y) - (a * C)) + (a * C)) + (- (s * c)) by RVSUM_1:31
.= ((a * y) - (a * C)) + ((a * c) + (- (s * c))) by RVSUM_1:15
.= ((a * y) + (- (a * c))) + ((a * c) + (- (s * c))) by RVSUM_1:31 ;
then dist (AX,se) = |.(((a * y) + (- (a * c))) + ((a * c) + (- (s * c)))).| by A2, SPPOL_1:5;
then dist (AX,se) < r by A30, XXREAL_0:2;
then se in Ball (AX,r) by METRIC_1:11;
hence z in V by A17, A23; ::_thesis: verum
end;
cluster TOP-REAL n -> finite-dimensional ;
coherence
TOP-REAL n is finite-dimensional
proof
RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RealVectSpace (Seg n) by EUCLID:def_8;
then (Omega). (TOP-REAL n) = RealVectSpace (Seg n) by RLSUB_1:def_4;
hence TOP-REAL n is finite-dimensional by Th3; ::_thesis: verum
end;
end;
theorem Th4: :: RLAFFIN3:4
for n being Nat holds dim (TOP-REAL n) = n
proof
let n be Nat; ::_thesis: dim (TOP-REAL n) = n
RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RealVectSpace (Seg n) by EUCLID:def_8;
then (Omega). (TOP-REAL n) = RealVectSpace (Seg n) by RLSUB_1:def_4;
then dim ((Omega). (TOP-REAL n)) = n by EUCLID_7:46;
hence dim (TOP-REAL n) = n by RLVECT_5:30; ::_thesis: verum
end;
theorem Th5: :: RLAFFIN3:5
for V being finite-dimensional RealLinearSpace
for A being affinely-independent Subset of V holds card A <= 1 + (dim V)
proof
let V be finite-dimensional RealLinearSpace; ::_thesis: for A being affinely-independent Subset of V holds card A <= 1 + (dim V)
let A be affinely-independent Subset of V; ::_thesis: card A <= 1 + (dim V)
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: card A <= 1 + (dim V)
hence card A <= 1 + (dim V) ; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: card A <= 1 + (dim V)
then consider v being VECTOR of V such that
v in A and
A1: ((- v) + A) \ {(0. V)} is linearly-independent by RLAFFIN1:def_4;
set vA = (- v) + A;
((- v) + A) \ {(0. V)} misses {(0. V)} by XBOOLE_1:79;
then A2: ( card {(0. V)} = 1 & card ((((- v) + A) \ {(0. V)}) \/ {(0. V)}) = (card (((- v) + A) \ {(0. V)})) + (card {(0. V)}) ) by CARD_2:40, CARD_2:42;
A3: card ((- v) + A) = card A by RLAFFIN1:7;
reconsider vA = (- v) + A as finite set ;
card (vA \ {(0. V)}) = dim (Lin (((- v) + A) \ {(0. V)})) by A1, RLVECT_5:29;
then card (vA \ {(0. V)}) <= dim V by RLVECT_5:28;
then A4: card ((vA \ {(0. V)}) \/ {(0. V)}) <= 1 + (dim V) by A2, XREAL_1:7;
(vA \ {(0. V)}) \/ {(0. V)} = vA \/ {(0. V)} by XBOOLE_1:39;
then card A <= card ((vA \ {(0. V)}) \/ {(0. V)}) by A3, NAT_1:43, XBOOLE_1:7;
hence card A <= 1 + (dim V) by A4, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
theorem Th6: :: RLAFFIN3:6
for V being finite-dimensional RealLinearSpace
for A being affinely-independent Subset of V holds
( card A = (dim V) + 1 iff Affin A = [#] V )
proof
let V be finite-dimensional RealLinearSpace; ::_thesis: for A being affinely-independent Subset of V holds
( card A = (dim V) + 1 iff Affin A = [#] V )
let A be affinely-independent Subset of V; ::_thesis: ( card A = (dim V) + 1 iff Affin A = [#] V )
A1: 0. V in [#] V ;
A2: A c= Affin A by RLAFFIN1:49;
hereby ::_thesis: ( Affin A = [#] V implies card A = (dim V) + 1 )
assume A3: card A = (dim V) + 1 ; ::_thesis: [#] V = Affin A
then not A is empty ;
then consider v being VECTOR of V such that
A4: v in A and
A5: ((- v) + A) \ {(0. V)} is linearly-independent by RLAFFIN1:def_4;
set vA = (- v) + A;
reconsider vA = (- v) + A as finite Subset of V ;
(- v) + v in { ((- v) + w) where w is Element of V : w in A } by A4;
then A6: (- v) + v in vA by RUSUB_4:def_8;
A7: ( card vA = card A & card {(0. V)} = 1 ) by CARD_2:42, RLAFFIN1:7;
(- v) + v = 0. V by RLVECT_1:5;
then vA = (vA \ {(0. V)}) \/ {(0. V)} by A6, ZFMISC_1:116;
then A8: card A = (card (vA \ {(0. V)})) + 1 by A7, CARD_2:40, XBOOLE_1:79;
dim (Lin (vA \ {(0. V)})) = card (vA \ {(0. V)}) by A5, RLVECT_5:29;
then (Omega). V = (Omega). (Lin (vA \ {(0. V)})) by A3, A8, RLVECT_5:31
.= Lin (vA \ {(0. V)}) by RLSUB_1:def_4 ;
then RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = Lin (vA \ {(0. V)}) by RLSUB_1:def_4;
then A9: [#] V = the carrier of (Lin vA) by Lm2;
then v in Lin vA by STRUCT_0:def_5;
hence [#] V = v + (Lin vA) by A9, RLSUB_1:48
.= v + (Up (Lin vA)) by RUSUB_4:30
.= Affin A by A2, A4, RLAFFIN1:57 ;
::_thesis: verum
end;
assume A10: Affin A = [#] V ; ::_thesis: card A = (dim V) + 1
then not A is empty ;
then consider v being VECTOR of V such that
A11: v in A and
A12: ((- v) + A) \ {(0. V)} is linearly-independent by RLAFFIN1:def_4;
set vA = (- v) + A;
reconsider vA = (- v) + A as finite Subset of V ;
[#] V = v + (Up (Lin vA)) by A10, RLAFFIN1:57
.= v + (Lin vA) by RUSUB_4:30 ;
then [#] (Lin vA) = the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by A1, RLSUB_1:47
.= the carrier of ((Omega). V) by RLSUB_1:def_4 ;
then Lin vA = (Omega). V by RLSUB_1:30
.= RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLSUB_1:def_4 ;
then RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = Lin (vA \ {(0. V)}) by Lm2;
then A13: vA \ {(0. V)} is Basis of V by A12, RLVECT_3:def_3;
(- v) + v in { ((- v) + w) where w is Element of V : w in A } by A11;
then A14: (- v) + v in vA by RUSUB_4:def_8;
(- v) + v = 0. V by RLVECT_1:5;
then A15: vA = (vA \ {(0. V)}) \/ {(0. V)} by A14, ZFMISC_1:116;
( card vA = card A & card {(0. V)} = 1 ) by CARD_2:42, RLAFFIN1:7;
hence card A = (card (vA \ {(0. V)})) + 1 by A15, CARD_2:40, XBOOLE_1:79
.= (dim V) + 1 by A13, RLVECT_5:def_2 ;
::_thesis: verum
end;
begin
theorem Th7: :: RLAFFIN3:7
for k, n being Nat
for An being Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k) st k <= n & An = { v where v is Element of (TOP-REAL n) : v | k in Ak } holds
( An is open iff Ak is open )
proof
let k, n be Nat; ::_thesis: for An being Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k) st k <= n & An = { v where v is Element of (TOP-REAL n) : v | k in Ak } holds
( An is open iff Ak is open )
let An be Subset of (TOP-REAL n); ::_thesis: for Ak being Subset of (TOP-REAL k) st k <= n & An = { v where v is Element of (TOP-REAL n) : v | k in Ak } holds
( An is open iff Ak is open )
let Ak be Subset of (TOP-REAL k); ::_thesis: ( k <= n & An = { v where v is Element of (TOP-REAL n) : v | k in Ak } implies ( An is open iff Ak is open ) )
assume k <= n ; ::_thesis: ( not An = { v where v is Element of (TOP-REAL n) : v | k in Ak } or ( An is open iff Ak is open ) )
then reconsider nk = n - k as Element of NAT by NAT_1:21;
A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider an = An as Subset of (TopSpaceMetr (Euclid n)) ;
A2: TopStruct(# the carrier of (TOP-REAL k), the topology of (TOP-REAL k) #) = TopSpaceMetr (Euclid k) by EUCLID:def_8;
then reconsider ak = Ak as Subset of (TopSpaceMetr (Euclid k)) ;
assume A3: An = { v where v is Element of (TOP-REAL n) : v | k in Ak } ; ::_thesis: ( An is open iff Ak is open )
hereby ::_thesis: ( Ak is open implies An is open )
assume An is open ; ::_thesis: Ak is open
then an in the topology of (TOP-REAL n) by PRE_TOPC:def_2;
then A4: an is open by A1, PRE_TOPC:def_2;
for e being Point of (Euclid k) st e in ak holds
ex r being real number st
( r > 0 & OpenHypercube (e,r) c= ak )
proof
( len (nk |-> 0) = nk & @ (@ (nk |-> 0)) = nk |-> 0 ) by CARD_1:def_7;
then reconsider nk0 = nk |-> 0 as Point of (Euclid nk) by TOPREAL3:45;
let e be Point of (Euclid k); ::_thesis: ( e in ak implies ex r being real number st
( r > 0 & OpenHypercube (e,r) c= ak ) )
A5: ( @ (@ (e ^ (nk |-> 0))) = e ^ (nk |-> 0) & len (e ^ nk0) = n ) by CARD_1:def_7;
then reconsider en = e ^ nk0 as Point of (Euclid n) by TOPREAL3:45;
reconsider En = e ^ nk0 as Point of (TOP-REAL n) by A5, TOPREAL3:46;
len e = k by CARD_1:def_7;
then dom e = Seg k by FINSEQ_1:def_3;
then A6: e = En | k by FINSEQ_1:21;
assume e in ak ; ::_thesis: ex r being real number st
( r > 0 & OpenHypercube (e,r) c= ak )
then en in an by A3, A6;
then consider m being non zero Element of NAT such that
A7: OpenHypercube (en,(1 / m)) c= an by A4, EUCLID_9:23;
take r = 1 / m; ::_thesis: ( r > 0 & OpenHypercube (e,r) c= ak )
thus r > 0 by XREAL_1:139; ::_thesis: OpenHypercube (e,r) c= ak
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in OpenHypercube (e,r) or y in ak )
assume A8: y in OpenHypercube (e,r) ; ::_thesis: y in ak
then reconsider p = y as Point of (TopSpaceMetr (Euclid k)) ;
A9: p in product (Intervals (e,r)) by A8, EUCLID_9:def_4;
reconsider P = p as Point of (TOP-REAL k) by A2;
nk0 in OpenHypercube (nk0,r) by EUCLID_9:11, XREAL_1:139;
then A10: nk0 in product (Intervals (nk0,r)) by EUCLID_9:def_4;
(Intervals (e,r)) ^ (Intervals (nk0,r)) = Intervals (en,r) by Th1;
then P ^ nk0 in product (Intervals (en,r)) by A10, A9, Th2;
then P ^ nk0 in OpenHypercube (en,r) by EUCLID_9:def_4;
then P ^ nk0 in an by A7;
then consider v being Element of (TOP-REAL n) such that
A11: ( v = P ^ nk0 & v | k in Ak ) by A3;
len P = k by CARD_1:def_7;
then dom P = Seg k by FINSEQ_1:def_3;
hence y in ak by A11, FINSEQ_1:21; ::_thesis: verum
end;
then ak is open by EUCLID_9:24;
then ak in the topology of (TOP-REAL k) by A2, PRE_TOPC:def_2;
hence Ak is open by PRE_TOPC:def_2; ::_thesis: verum
end;
assume Ak is open ; ::_thesis: An is open
then ak in the topology of (TOP-REAL k) by PRE_TOPC:def_2;
then A12: ak is open by A2, PRE_TOPC:def_2;
for e being Point of (Euclid n) st e in an holds
ex r being real number st
( r > 0 & OpenHypercube (e,r) c= an )
proof
let e be Point of (Euclid n); ::_thesis: ( e in an implies ex r being real number st
( r > 0 & OpenHypercube (e,r) c= an ) )
assume e in an ; ::_thesis: ex r being real number st
( r > 0 & OpenHypercube (e,r) c= an )
then consider v being Element of (TOP-REAL n) such that
A13: e = v and
A14: v | k in Ak by A3;
reconsider vk = v | k as Point of (TOP-REAL k) by A14;
A15: len vk = k by CARD_1:def_7;
@ (@ vk) = vk ;
then reconsider Vk = vk as Point of (Euclid k) by A15, TOPREAL3:45;
consider m being non zero Element of NAT such that
A16: OpenHypercube (Vk,(1 / m)) c= ak by A12, A14, EUCLID_9:23;
take r = 1 / m; ::_thesis: ( r > 0 & OpenHypercube (e,r) c= an )
thus r > 0 by XREAL_1:139; ::_thesis: OpenHypercube (e,r) c= an
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in OpenHypercube (e,r) or y in an )
assume A17: y in OpenHypercube (e,r) ; ::_thesis: y in an
then A18: y in product (Intervals (e,r)) by EUCLID_9:def_4;
reconsider Y = y as Point of (TOP-REAL n) by A1, A17;
A19: len v = n by CARD_1:def_7;
consider q being FinSequence such that
A20: @ (@ v) = vk ^ q by FINSEQ_1:80;
reconsider q = q as FinSequence of REAL by A20, FINSEQ_1:36;
len v = (len vk) + (len q) by A20, FINSEQ_1:22;
then reconsider Q = q as Point of (Euclid nk) by A15, A19, TOPREAL3:45;
(Intervals (Vk,r)) ^ (Intervals (Q,r)) = Intervals (e,r) by A13, A20, Th1;
then consider p1, p2 being FinSequence such that
A21: y = p1 ^ p2 and
A22: p1 in product (Intervals (Vk,r)) and
p2 in product (Intervals (Q,r)) by A18, Th2;
A23: p1 in OpenHypercube (Vk,(1 / m)) by A22, EUCLID_9:def_4;
then len p1 = k by A2, CARD_1:def_7;
then Y | k = Y | (dom p1) by FINSEQ_1:def_3
.= p1 by A21, FINSEQ_1:21 ;
hence y in an by A3, A16, A23; ::_thesis: verum
end;
then an is open by EUCLID_9:24;
then an in the topology of (TOP-REAL n) by A1, PRE_TOPC:def_2;
hence An is open by PRE_TOPC:def_2; ::_thesis: verum
end;
Lm3: for n being Nat holds the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)
proof
let n be Nat; ::_thesis: the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)
thus the carrier of (n -VectSp_over F_Real) = n -tuples_on the carrier of F_Real by MATRIX13:102
.= REAL n by EUCLID:def_1, VECTSP_1:def_5
.= the carrier of (TOP-REAL n) by EUCLID:22 ; ::_thesis: verum
end;
theorem Th8: :: RLAFFIN3:8
for k, n being Nat
for Ak being Subset of (TOP-REAL k)
for A being Subset of (TOP-REAL (k + n)) st A = { (v ^ (n |-> 0)) where v is Element of (TOP-REAL k) : verum } holds
for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds
( Ak is open iff B is open )
proof
let k, n be Nat; ::_thesis: for Ak being Subset of (TOP-REAL k)
for A being Subset of (TOP-REAL (k + n)) st A = { (v ^ (n |-> 0)) where v is Element of (TOP-REAL k) : verum } holds
for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds
( Ak is open iff B is open )
let Ak be Subset of (TOP-REAL k); ::_thesis: for A being Subset of (TOP-REAL (k + n)) st A = { (v ^ (n |-> 0)) where v is Element of (TOP-REAL k) : verum } holds
for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds
( Ak is open iff B is open )
set kn = k + n;
set TRn = TOP-REAL (k + n);
set TRk = TOP-REAL k;
let A be Subset of (TOP-REAL (k + n)); ::_thesis: ( A = { (v ^ (n |-> 0)) where v is Element of (TOP-REAL k) : verum } implies for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds
( Ak is open iff B is open ) )
assume A1: A = { (v ^ (n |-> 0)) where v is Element of (TOP-REAL k) : verum } ; ::_thesis: for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds
( Ak is open iff B is open )
A2: TopStruct(# the carrier of (TOP-REAL k), the topology of (TOP-REAL k) #) = TopSpaceMetr (Euclid k) by EUCLID:def_8;
then reconsider p = Ak as Subset of (TopSpaceMetr (Euclid k)) ;
set TRA = (TOP-REAL (k + n)) | A;
let B be Subset of ((TOP-REAL (k + n)) | A); ::_thesis: ( B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } implies ( Ak is open iff B is open ) )
assume A3: B = { v where v is Element of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } ; ::_thesis: ( Ak is open iff B is open )
A4: [#] ((TOP-REAL (k + n)) | A) = A by PRE_TOPC:def_5;
A5: k + n >= k by NAT_1:11;
hereby ::_thesis: ( B is open implies Ak is open )
set PP = { v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } ;
{ v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } c= [#] (TOP-REAL (k + n))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } or x in [#] (TOP-REAL (k + n)) )
assume x in { v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } ; ::_thesis: x in [#] (TOP-REAL (k + n))
then ex v being Element of (TOP-REAL (k + n)) st
( x = v & v | k in Ak ) ;
hence x in [#] (TOP-REAL (k + n)) ; ::_thesis: verum
end;
then reconsider PP = { v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } as Subset of (TOP-REAL (k + n)) ;
A6: PP /\ A c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PP /\ A or x in B )
assume A7: x in PP /\ A ; ::_thesis: x in B
then x in PP by XBOOLE_0:def_4;
then consider v being Element of (TOP-REAL (k + n)) such that
A8: ( x = v & v | k in Ak ) ;
x in A by A7, XBOOLE_0:def_4;
hence x in B by A3, A8; ::_thesis: verum
end;
assume Ak is open ; ::_thesis: B is open
then PP is open by A5, Th7;
then PP in the topology of (TOP-REAL (k + n)) by PRE_TOPC:def_2;
then A9: PP /\ ([#] ((TOP-REAL (k + n)) | A)) in the topology of ((TOP-REAL (k + n)) | A) by PRE_TOPC:def_4;
B c= PP /\ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in PP /\ A )
assume x in B ; ::_thesis: x in PP /\ A
then consider v being Element of (TOP-REAL (k + n)) such that
A10: x = v and
A11: v | k in Ak and
A12: v in A by A3;
v in PP by A11;
hence x in PP /\ A by A10, A12, XBOOLE_0:def_4; ::_thesis: verum
end;
then B = PP /\ A by A6, XBOOLE_0:def_10;
hence B is open by A4, A9, PRE_TOPC:def_2; ::_thesis: verum
end;
assume B is open ; ::_thesis: Ak is open
then B in the topology of ((TOP-REAL (k + n)) | A) by PRE_TOPC:def_2;
then consider Q being Subset of (TOP-REAL (k + n)) such that
A13: Q in the topology of (TOP-REAL (k + n)) and
A14: Q /\ ([#] ((TOP-REAL (k + n)) | A)) = B by PRE_TOPC:def_4;
A15: TopStruct(# the carrier of (TOP-REAL (k + n)), the topology of (TOP-REAL (k + n)) #) = TopSpaceMetr (Euclid (k + n)) by EUCLID:def_8;
then reconsider q = Q as Subset of (TopSpaceMetr (Euclid (k + n))) ;
A16: q is open by A13, A15, PRE_TOPC:def_2;
for e being Point of (Euclid k) st e in p holds
ex r being real number st
( r > 0 & OpenHypercube (e,r) c= p )
proof
let e be Point of (Euclid k); ::_thesis: ( e in p implies ex r being real number st
( r > 0 & OpenHypercube (e,r) c= p ) )
A17: len (n |-> 0) = n by CARD_1:def_7;
A18: @ (@ (e ^ (n |-> 0))) = e ^ (n |-> 0) ;
A19: len e = k by CARD_1:def_7;
then len (e ^ (n |-> 0)) = k + n by A17, FINSEQ_1:22;
then reconsider e0 = e ^ (n |-> 0) as Point of (Euclid (k + n)) by A18, TOPREAL3:45;
dom e = Seg k by A19, FINSEQ_1:def_3;
then A20: e = e0 | k by FINSEQ_1:21;
n |-> 0 = @ (@ (n |-> 0)) ;
then reconsider N = n |-> 0 as Element of (Euclid n) by A17, TOPREAL3:45;
e is Element of (TOP-REAL k) by Lm1;
then A21: e0 in A by A1;
assume e in p ; ::_thesis: ex r being real number st
( r > 0 & OpenHypercube (e,r) c= p )
then e0 in B by A3, A21, A20;
then e0 in q by A14, XBOOLE_0:def_4;
then consider m being non zero Element of NAT such that
A22: OpenHypercube (e0,(1 / m)) c= q by A16, EUCLID_9:23;
set r = 1 / m;
take 1 / m ; ::_thesis: ( 1 / m > 0 & OpenHypercube (e,(1 / m)) c= p )
thus 1 / m > 0 by XREAL_1:139; ::_thesis: OpenHypercube (e,(1 / m)) c= p
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OpenHypercube (e,(1 / m)) or x in p )
N in OpenHypercube (N,(1 / m)) by EUCLID_9:11, XREAL_1:139;
then A23: N in product (Intervals (N,(1 / m))) by EUCLID_9:def_4;
assume A24: x in OpenHypercube (e,(1 / m)) ; ::_thesis: x in p
then reconsider w = x as Point of (TOP-REAL k) by A2;
A25: (Intervals (e,(1 / m))) ^ (Intervals (N,(1 / m))) = Intervals ((e ^ N),(1 / m)) by Th1;
w in product (Intervals (e,(1 / m))) by A24, EUCLID_9:def_4;
then w ^ N in product (Intervals (e0,(1 / m))) by A23, A25, Th2;
then A26: w ^ N in OpenHypercube (e0,(1 / m)) by EUCLID_9:def_4;
w ^ N in A by A1;
then w ^ N in B by A4, A14, A22, A26, XBOOLE_0:def_4;
then A27: ex v being Element of (TOP-REAL (k + n)) st
( w ^ N = v & v | k in Ak & v in A ) by A3;
len w = k by CARD_1:def_7;
then (w ^ N) | k = (w ^ N) | (dom w) by FINSEQ_1:def_3
.= w by FINSEQ_1:21 ;
hence x in p by A27; ::_thesis: verum
end;
then p is open by EUCLID_9:24;
then Ak in the topology of (TOP-REAL k) by A2, PRE_TOPC:def_2;
hence Ak is open by PRE_TOPC:def_2; ::_thesis: verum
end;
theorem Th9: :: RLAFFIN3:9
for V being RealLinearSpace
for A being affinely-independent Subset of V
for B being Subset of V st B c= A holds
(conv A) /\ (Affin B) = conv B
proof
let V be RealLinearSpace; ::_thesis: for A being affinely-independent Subset of V
for B being Subset of V st B c= A holds
(conv A) /\ (Affin B) = conv B
let A be affinely-independent Subset of V; ::_thesis: for B being Subset of V st B c= A holds
(conv A) /\ (Affin B) = conv B
let B be Subset of V; ::_thesis: ( B c= A implies (conv A) /\ (Affin B) = conv B )
A1: conv B c= Affin B by RLAFFIN1:65;
assume A2: B c= A ; ::_thesis: (conv A) /\ (Affin B) = conv B
thus (conv A) /\ (Affin B) c= conv B :: according to XBOOLE_0:def_10 ::_thesis: conv B c= (conv A) /\ (Affin B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (conv A) /\ (Affin B) or x in conv B )
assume A3: x in (conv A) /\ (Affin B) ; ::_thesis: x in conv B
then A4: x in Affin B by XBOOLE_0:def_4;
A5: x in conv A by A3, XBOOLE_0:def_4;
A6: now__::_thesis:_for_v_being_Element_of_V_st_v_in_B_holds_
0_<=_(x_|--_B)_._v
let v be Element of V; ::_thesis: ( v in B implies 0 <= (x |-- B) . v )
x |-- B = x |-- A by A2, A4, RLAFFIN1:77;
hence ( v in B implies 0 <= (x |-- B) . v ) by A5, RLAFFIN1:71; ::_thesis: verum
end;
B is affinely-independent by A2, RLAFFIN1:43;
hence x in conv B by A4, A6, RLAFFIN1:73; ::_thesis: verum
end;
conv B c= conv A by A2, RLAFFIN1:3;
hence conv B c= (conv A) /\ (Affin B) by A1, XBOOLE_1:19; ::_thesis: verum
end;
theorem Th10: :: RLAFFIN3:10
for r being Real
for V being non empty RLSStruct
for A being non empty set
for f being PartFunc of A, the carrier of V
for X being set holds (r (#) f) .: X = r * (f .: X)
proof
let r be Real; ::_thesis: for V being non empty RLSStruct
for A being non empty set
for f being PartFunc of A, the carrier of V
for X being set holds (r (#) f) .: X = r * (f .: X)
let V be non empty RLSStruct ; ::_thesis: for A being non empty set
for f being PartFunc of A, the carrier of V
for X being set holds (r (#) f) .: X = r * (f .: X)
let A be non empty set ; ::_thesis: for f being PartFunc of A, the carrier of V
for X being set holds (r (#) f) .: X = r * (f .: X)
let f be PartFunc of A, the carrier of V; ::_thesis: for X being set holds (r (#) f) .: X = r * (f .: X)
let X be set ; ::_thesis: (r (#) f) .: X = r * (f .: X)
set rf = r (#) f;
A1: dom (r (#) f) = dom f by VFUNCT_1:def_4;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: r * (f .: X) c= (r (#) f) .: X
let y be set ; ::_thesis: ( y in (r (#) f) .: X implies y in r * (f .: X) )
assume y in (r (#) f) .: X ; ::_thesis: y in r * (f .: X)
then consider x being set such that
A2: x in dom (r (#) f) and
A3: x in X and
A4: y = (r (#) f) . x by FUNCT_1:def_6;
(r (#) f) . x = (r (#) f) /. x by A2, PARTFUN1:def_6;
then A5: y = r * (f /. x) by A2, A4, VFUNCT_1:def_4;
f . x = f /. x by A1, A2, PARTFUN1:def_6;
then f /. x in f .: X by A1, A2, A3, FUNCT_1:def_6;
then y in { (r * v) where v is Element of V : v in f .: X } by A5;
hence y in r * (f .: X) by CONVEX1:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in r * (f .: X) or y in (r (#) f) .: X )
assume y in r * (f .: X) ; ::_thesis: y in (r (#) f) .: X
then y in { (r * v) where v is Element of V : v in f .: X } by CONVEX1:def_1;
then consider v being Element of V such that
A6: y = r * v and
A7: v in f .: X ;
consider x being set such that
A8: x in dom f and
A9: x in X and
A10: v = f . x by A7, FUNCT_1:def_6;
v = f /. x by A8, A10, PARTFUN1:def_6;
then y = (r (#) f) /. x by A1, A6, A8, VFUNCT_1:def_4
.= (r (#) f) . x by A1, A8, PARTFUN1:def_6 ;
hence y in (r (#) f) .: X by A1, A8, A9, FUNCT_1:def_6; ::_thesis: verum
end;
theorem Th11: :: RLAFFIN3:11
for n being Nat
for An being Subset of (TOP-REAL n) st 0* n in An holds
Affin An = [#] (Lin An)
proof
let n be Nat; ::_thesis: for An being Subset of (TOP-REAL n) st 0* n in An holds
Affin An = [#] (Lin An)
let An be Subset of (TOP-REAL n); ::_thesis: ( 0* n in An implies Affin An = [#] (Lin An) )
set TR = TOP-REAL n;
set A = An;
A1: ( 0* n = 0. (TOP-REAL n) & An c= Affin An ) by EUCLID:66, RLAFFIN1:49;
assume 0* n in An ; ::_thesis: Affin An = [#] (Lin An)
hence Affin An = (0. (TOP-REAL n)) + (Up (Lin ((- (0. (TOP-REAL n))) + An))) by A1, RLAFFIN1:57
.= Up (Lin ((- (0. (TOP-REAL n))) + An)) by RLAFFIN1:6
.= Up (Lin ((0. (TOP-REAL n)) + An)) by RLVECT_1:12
.= Up (Lin An) by RLAFFIN1:6
.= [#] (Lin An) by RUSUB_4:def_5 ;
::_thesis: verum
end;
registration
let V be non empty addLoopStr ;
let A be finite Subset of V;
let v be Element of V;
clusterv + A -> finite ;
coherence
v + A is finite
proof
deffunc H1( Element of V) -> Element of the carrier of V = v + V;
card { H1(w) where w is Element of V : w in A } c= card A from TREES_2:sch_2();
then card (v + A) is finite by RUSUB_4:def_8;
hence v + A is finite ; ::_thesis: verum
end;
end;
Lm4: for V being non empty RLSStruct
for A being Subset of V
for r being Real holds card (r * A) c= card A
proof
let V be non empty RLSStruct ; ::_thesis: for A being Subset of V
for r being Real holds card (r * A) c= card A
let A be Subset of V; ::_thesis: for r being Real holds card (r * A) c= card A
let r be real number ; ::_thesis: ( r is Real implies card (r * A) c= card A )
deffunc H1( Element of V) -> Element of the carrier of V = r * $1;
card { H1(w) where w is Element of V : w in A } c= card A from TREES_2:sch_2();
hence ( r is Real implies card (r * A) c= card A ) by CONVEX1:def_1; ::_thesis: verum
end;
registration
let V be non empty RLSStruct ;
let A be finite Subset of V;
let r be Real;
clusterr * A -> finite ;
coherence
r * A is finite
proof
card (r * A) c= card A by Lm4;
hence r * A is finite ; ::_thesis: verum
end;
end;
theorem Th12: :: RLAFFIN3:12
for r being Real
for V being RealLinearSpace
for A being Subset of V holds
( card A = card (r * A) iff ( r <> 0 or A is trivial ) )
proof
let r be Real; ::_thesis: for V being RealLinearSpace
for A being Subset of V holds
( card A = card (r * A) iff ( r <> 0 or A is trivial ) )
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds
( card A = card (r * A) iff ( r <> 0 or A is trivial ) )
let A be Subset of V; ::_thesis: ( card A = card (r * A) iff ( r <> 0 or A is trivial ) )
A1: card {(0. V)} = 1 by CARD_2:42;
hereby ::_thesis: ( ( r <> 0 or A is trivial ) implies card A = card (r * A) )
assume A2: card A = card (r * A) ; ::_thesis: ( r = 0 implies A is trivial )
assume A3: r = 0 ; ::_thesis: A is trivial
then A4: r * A c= {(0. V)} by RLAFFIN1:12;
then reconsider a = A as finite set by A2;
reconsider rA = r * A as finite set by A4;
card rA <= card {(0. V)} by A3, NAT_1:43, RLAFFIN1:12;
then card a < 1 + 1 by A1, A2, NAT_1:13;
hence A is trivial by NAT_D:60; ::_thesis: verum
end;
assume A5: ( r <> 0 or A is trivial ) ; ::_thesis: card A = card (r * A)
percases ( r <> 0 or A is empty or ( r = 0 & A is 1 -element ) ) by A5;
supposeA6: r <> 0 ; ::_thesis: card A = card (r * A)
A7: ( 1 * A = A & ((1 / r) * r) * A = (1 / r) * (r * A) ) by RLAFFIN1:10, RLAFFIN1:11;
A8: card (r * A) c= card A by Lm4;
(1 / r) * r = 1 by A6, XCMPLX_1:87;
then card A c= card (r * A) by A7, Lm4;
hence card A = card (r * A) by A8, XBOOLE_0:def_10; ::_thesis: verum
end;
supposeA9: A is empty ; ::_thesis: card A = card (r * A)
r * A is empty
proof
assume not r * A is empty ; ::_thesis: contradiction
then consider x being set such that
A10: x in r * A by XBOOLE_0:def_1;
x in { (r * v) where v is Element of V : v in A } by A10, CONVEX1:def_1;
then ex v being Element of V st
( x = r * v & v in A ) ;
hence contradiction by A9; ::_thesis: verum
end;
hence card A = card (r * A) by A9; ::_thesis: verum
end;
supposeA11: ( r = 0 & A is 1 -element ) ; ::_thesis: card A = card (r * A)
then consider x being set such that
A12: A = {x} by ZFMISC_1:131;
r * A = {(0. V)} by A11, CONVEX1:34;
hence card A = card (r * A) by A1, A12, CARD_2:42; ::_thesis: verum
end;
end;
end;
registration
let V be non empty RLSStruct ;
let f be FinSequence of V;
let r be Real;
clusterr (#) f -> FinSequence-like ;
coherence
r (#) f is FinSequence-like
proof
dom (r (#) f) = dom f by VFUNCT_1:def_4
.= Seg (len f) by FINSEQ_1:def_3 ;
hence r (#) f is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum
end;
end;
begin
definition
let X be finite set ;
mode Enumeration of X -> one-to-one FinSequence means :Def1: :: RLAFFIN3:def 1
rng it = X;
existence
ex b1 being one-to-one FinSequence st rng b1 = X
proof
ex p being FinSequence st
( rng p = X & p is one-to-one ) by FINSEQ_4:58;
hence ex b1 being one-to-one FinSequence st rng b1 = X ; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Enumeration RLAFFIN3:def_1_:_
for X being finite set
for b2 being one-to-one FinSequence holds
( b2 is Enumeration of X iff rng b2 = X );
definition
let X be 1-sorted ;
let A be finite Subset of X;
:: original: Enumeration
redefine mode Enumeration of A -> one-to-one FinSequence of X;
coherence
for b1 being Enumeration of A holds b1 is one-to-one FinSequence of X
proof
let E be Enumeration of A; ::_thesis: E is one-to-one FinSequence of X
rng E = A by Def1;
hence E is one-to-one FinSequence of X by FINSEQ_1:def_4; ::_thesis: verum
end;
end;
theorem Th13: :: RLAFFIN3:13
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for A being finite Subset of V
for E being Enumeration of A
for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for A being finite Subset of V
for E being Enumeration of A
for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A
let A be finite Subset of V; ::_thesis: for E being Enumeration of A
for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A
let E be Enumeration of A; ::_thesis: for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A
let v be Element of V; ::_thesis: E + ((card A) |-> v) is Enumeration of v + A
A1: rng E = A by Def1;
then A2: len E = card A by FINSEQ_4:62;
then reconsider e = E, cAv = (card A) |-> v as Element of (card A) -tuples_on the carrier of V by FINSEQ_2:92;
A3: len (e + cAv) = card A by CARD_1:def_7;
then A4: dom (e + cAv) = Seg (card A) by FINSEQ_1:def_3;
A5: dom e = Seg (card A) by A2, FINSEQ_1:def_3;
A6: rng (e + cAv) c= v + A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (e + cAv) or y in v + A )
assume y in rng (e + cAv) ; ::_thesis: y in v + A
then consider x being set such that
A7: x in dom (e + cAv) and
A8: (e + cAv) . x = y by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A7;
A9: e . x in rng e by A5, A4, A7, FUNCT_1:def_3;
then reconsider Ex = e . x as Element of V ;
cAv . x = v by A4, A7, FINSEQ_2:57;
then y = Ex + v by A7, A8, FVSUM_1:17;
then y = v + Ex by RLVECT_1:def_2;
then y in { (v + w) where w is Element of V : w in A } by A1, A9;
hence y in v + A by RUSUB_4:def_8; ::_thesis: verum
end;
v + A c= rng (e + cAv)
proof
let vA be set ; :: according to TARSKI:def_3 ::_thesis: ( not vA in v + A or vA in rng (e + cAv) )
assume vA in v + A ; ::_thesis: vA in rng (e + cAv)
then vA in { (v + a) where a is Element of V : a in A } by RUSUB_4:def_8;
then consider a being Element of V such that
A10: vA = v + a and
A11: a in A ;
consider x being set such that
A12: x in dom E and
A13: E . x = a by A1, A11, FUNCT_1:def_3;
reconsider x = x as Element of NAT by A12;
cAv . x = v by A5, A12, FINSEQ_2:57;
then (e + cAv) . x = a + v by A5, A4, A12, A13, FVSUM_1:17
.= vA by A10, RLVECT_1:def_2 ;
hence vA in rng (e + cAv) by A5, A4, A12, FUNCT_1:def_3; ::_thesis: verum
end;
then A14: v + A = rng (e + cAv) by A6, XBOOLE_0:def_10;
card A = card (v + A) by RLAFFIN1:7;
then e + cAv is one-to-one by A3, A14, FINSEQ_4:62;
hence E + ((card A) |-> v) is Enumeration of v + A by A14, Def1; ::_thesis: verum
end;
theorem :: RLAFFIN3:14
for r being Real
for V being RealLinearSpace
for Av being finite Subset of V
for E being Enumeration of Av holds
( r (#) E is Enumeration of r * Av iff ( r <> 0 or Av is trivial ) )
proof
let r be Real; ::_thesis: for V being RealLinearSpace
for Av being finite Subset of V
for E being Enumeration of Av holds
( r (#) E is Enumeration of r * Av iff ( r <> 0 or Av is trivial ) )
let V be RealLinearSpace; ::_thesis: for Av being finite Subset of V
for E being Enumeration of Av holds
( r (#) E is Enumeration of r * Av iff ( r <> 0 or Av is trivial ) )
let Av be finite Subset of V; ::_thesis: for E being Enumeration of Av holds
( r (#) E is Enumeration of r * Av iff ( r <> 0 or Av is trivial ) )
let EV be Enumeration of Av; ::_thesis: ( r (#) EV is Enumeration of r * Av iff ( r <> 0 or Av is trivial ) )
set rE = r (#) EV;
A1: dom (r (#) EV) = dom EV by VFUNCT_1:def_4;
then A2: len (r (#) EV) = len EV by FINSEQ_3:29;
A3: rng EV = Av by Def1;
then A4: card Av = len EV by FINSEQ_4:62;
A5: rng (r (#) EV) = (r (#) EV) .: (dom EV) by A1, RELAT_1:113
.= r * (EV .: (dom EV)) by Th10
.= r * Av by A3, RELAT_1:113 ;
A6: card {(0. V)} = 1 by CARD_2:42;
hereby ::_thesis: ( ( r <> 0 or Av is trivial ) implies r (#) EV is Enumeration of r * Av )
reconsider rA = r * Av as finite set ;
assume r (#) EV is Enumeration of r * Av ; ::_thesis: ( r = 0 implies Av is trivial )
then A7: card (r * Av) = card Av by A4, A2, A5, FINSEQ_4:62;
assume r = 0 ; ::_thesis: Av is trivial
then card Av <= 1 by A6, A7, NAT_1:43, RLAFFIN1:12;
then card Av < 1 + 1 by NAT_1:13;
hence Av is trivial by NAT_D:60; ::_thesis: verum
end;
assume ( r <> 0 or Av is trivial ) ; ::_thesis: r (#) EV is Enumeration of r * Av
then card Av = card (r * Av) by Th12;
then r (#) EV is one-to-one by A4, A2, A5, FINSEQ_4:62;
hence r (#) EV is Enumeration of r * Av by A5, Def1; ::_thesis: verum
end;
theorem Th15: :: RLAFFIN3:15
for n, m being Nat
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
for A being finite Subset of (TOP-REAL n)
for E being Enumeration of A holds (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A
proof
let n, m be Nat; ::_thesis: for M being Matrix of n,m,F_Real st the_rank_of M = n holds
for A being finite Subset of (TOP-REAL n)
for E being Enumeration of A holds (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A
let M be Matrix of n,m,F_Real; ::_thesis: ( the_rank_of M = n implies for A being finite Subset of (TOP-REAL n)
for E being Enumeration of A holds (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A )
assume A1: the_rank_of M = n ; ::_thesis: for A being finite Subset of (TOP-REAL n)
for E being Enumeration of A holds (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A
set MT = Mx2Tran M;
A2: Mx2Tran M is one-to-one by A1, MATRTOP1:39;
set TRn = TOP-REAL n;
let A be finite Subset of (TOP-REAL n); ::_thesis: for E being Enumeration of A holds (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A
let E be Enumeration of A; ::_thesis: (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A
A3: rng E = A by Def1;
dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def_1;
then len ((Mx2Tran M) * E) = len E by A3, FINSEQ_2:29;
then A4: dom ((Mx2Tran M) * E) = dom E by FINSEQ_3:29;
rng ((Mx2Tran M) * E) = ((Mx2Tran M) * E) .: (dom ((Mx2Tran M) * E)) by RELAT_1:113
.= (Mx2Tran M) .: (E .: (dom E)) by A4, RELAT_1:126
.= (Mx2Tran M) .: A by A3, RELAT_1:113 ;
hence (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A by A2, Def1; ::_thesis: verum
end;
definition
let V be RealLinearSpace;
let Av be finite Subset of V;
let E be Enumeration of Av;
let x be set ;
funcx |-- E -> FinSequence of REAL equals :: RLAFFIN3:def 2
(x |-- Av) * E;
coherence
(x |-- Av) * E is FinSequence of REAL ;
end;
:: deftheorem defines |-- RLAFFIN3:def_2_:_
for V being RealLinearSpace
for Av being finite Subset of V
for E being Enumeration of Av
for x being set holds x |-- E = (x |-- Av) * E;
theorem Th16: :: RLAFFIN3:16
for x being set
for V being RealLinearSpace
for Av being finite Subset of V
for E being Enumeration of Av holds len (x |-- E) = card Av
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for Av being finite Subset of V
for E being Enumeration of Av holds len (x |-- E) = card Av
let V be RealLinearSpace; ::_thesis: for Av being finite Subset of V
for E being Enumeration of Av holds len (x |-- E) = card Av
let Av be finite Subset of V; ::_thesis: for E being Enumeration of Av holds len (x |-- E) = card Av
let E be Enumeration of Av; ::_thesis: len (x |-- E) = card Av
rng E = Av by Def1;
then len E = card Av by FINSEQ_4:62;
hence len (x |-- E) = card Av by FINSEQ_2:33; ::_thesis: verum
end;
theorem Th17: :: RLAFFIN3:17
for V being RealLinearSpace
for v, w being VECTOR of V
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E
proof
let V be RealLinearSpace; ::_thesis: for v, w being VECTOR of V
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E
let v, w be VECTOR of V; ::_thesis: for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E
let Affv be finite affinely-independent Subset of V; ::_thesis: for EV being Enumeration of Affv
for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E
let EV be Enumeration of Affv; ::_thesis: for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E
set E = EV;
let Ev be Enumeration of v + Affv; ::_thesis: ( w in Affin Affv & Ev = EV + ((card Affv) |-> v) implies w |-- EV = (v + w) |-- Ev )
assume that
A1: w in Affin Affv and
A2: Ev = EV + ((card Affv) |-> v) ; ::_thesis: w |-- EV = (v + w) |-- Ev
set wA = w |-- Affv;
A3: sum (w |-- Affv) = 1 by A1, RLAFFIN1:def_7;
v + w in { (v + u) where u is VECTOR of V : u in Affin Affv } by A1;
then A4: v + w in v + (Affin Affv) by RUSUB_4:def_8;
rng EV = Affv by Def1;
then A5: len EV = card Affv by FINSEQ_4:62;
then reconsider e = EV, cAv = (card Affv) |-> v as Element of (card Affv) -tuples_on the carrier of V by FINSEQ_2:92;
A6: ( Affin (v + Affv) = v + (Affin Affv) & 1 * v = v ) by RLAFFIN1:53, RLVECT_1:def_8;
( Carrier (v + (w |-- Affv)) = v + (Carrier (w |-- Affv)) & Carrier (w |-- Affv) c= Affv ) by RLAFFIN1:16, RLVECT_2:def_6;
then Carrier (v + (w |-- Affv)) c= v + Affv by RLTOPSP1:8;
then reconsider vwA = v + (w |-- Affv) as Linear_Combination of v + Affv by RLVECT_2:def_6;
Sum (w |-- Affv) = w by A1, RLAFFIN1:def_7;
then A7: Sum vwA = (1 * v) + w by A3, RLAFFIN1:39;
A8: len (w |-- EV) = card Affv by Th16;
A9: card Affv = card (v + Affv) by RLAFFIN1:7;
then len ((v + w) |-- Ev) = card Affv by Th16;
then A10: dom (w |-- EV) = dom ((v + w) |-- Ev) by A8, FINSEQ_3:29;
rng Ev = v + Affv by Def1;
then A11: len Ev = card Affv by A9, FINSEQ_4:62;
sum vwA = 1 by A3, RLAFFIN1:37;
then A12: vwA = (v + w) |-- (v + Affv) by A4, A7, A6, RLAFFIN1:def_7;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(w_|--_EV)_holds_
((v_+_w)_|--_Ev)_._i_=_(w_|--_EV)_._i
let i be Nat; ::_thesis: ( i in dom (w |-- EV) implies ((v + w) |-- Ev) . i = (w |-- EV) . i )
assume A13: i in dom (w |-- EV) ; ::_thesis: ((v + w) |-- Ev) . i = (w |-- EV) . i
then A14: (w |-- EV) . i = (w |-- Affv) . (EV . i) by FUNCT_1:12;
dom EV = dom (w |-- EV) by A8, A5, FINSEQ_3:29;
then A15: EV . i = EV /. i by A13, PARTFUN1:def_6;
i in Seg (card Affv) by A8, A13, FINSEQ_1:def_3;
then A16: cAv . i = v by FINSEQ_2:57;
A17: ((v + w) |-- Ev) . i = ((v + w) |-- (v + Affv)) . (Ev . i) by A10, A13, FUNCT_1:12;
dom Ev = dom (w |-- EV) by A8, A11, FINSEQ_3:29;
then Ev . i = (EV /. i) + v by A2, A13, A16, A15, FVSUM_1:17;
hence ((v + w) |-- Ev) . i = (w |-- Affv) . (((EV /. i) + v) - v) by A12, A17, RLAFFIN1:def_1
.= (w |-- Affv) . ((EV /. i) + (v - v)) by RLVECT_1:28
.= (w |-- Affv) . ((EV /. i) + (0. V)) by RLVECT_1:15
.= (w |-- EV) . i by A14, A15, RLVECT_1:def_4 ;
::_thesis: verum
end;
hence w |-- EV = (v + w) |-- Ev by A10, FINSEQ_1:13; ::_thesis: verum
end;
theorem :: RLAFFIN3:18
for r being Real
for V being RealLinearSpace
for v being VECTOR of V
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
proof
let r be Real; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
let v be VECTOR of V; ::_thesis: for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
let Affv be finite affinely-independent Subset of V; ::_thesis: for EV being Enumeration of Affv
for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
let EV be Enumeration of Affv; ::_thesis: for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
set E = EV;
let rE be Enumeration of r * Affv; ::_thesis: ( v in Affin Affv & rE = r (#) EV & r <> 0 implies v |-- EV = (r * v) |-- rE )
assume that
A1: v in Affin Affv and
A2: rE = r (#) EV and
A3: r <> 0 ; ::_thesis: v |-- EV = (r * v) |-- rE
set vA = v |-- Affv;
A4: Carrier (v |-- Affv) c= Affv by RLVECT_2:def_6;
A5: r * v in { (r * u) where u is VECTOR of V : u in Affin Affv } by A1;
A6: dom rE = dom EV by A2, VFUNCT_1:def_4;
Carrier (r (*) (v |-- Affv)) = r * (Carrier (v |-- Affv)) by A3, RLAFFIN1:23;
then Carrier (r (*) (v |-- Affv)) c= r * Affv by A4, CONVEX1:39;
then reconsider rvA = r (*) (v |-- Affv) as Linear_Combination of r * Affv by RLVECT_2:def_6;
sum (v |-- Affv) = 1 by A1, RLAFFIN1:def_7;
then A7: sum rvA = 1 by A3, RLAFFIN1:38;
Sum (v |-- Affv) = v by A1, RLAFFIN1:def_7;
then A8: Sum rvA = r * v by RLAFFIN1:40;
A9: len ((r * v) |-- rE) = card (r * Affv) by Th16;
A10: len (v |-- EV) = card Affv by Th16;
rng EV = Affv by Def1;
then len EV = card Affv by FINSEQ_4:62;
then A11: dom (v |-- EV) = dom EV by A10, FINSEQ_3:29;
card Affv = card (r * Affv) by A3, Th12;
then A12: dom (v |-- EV) = dom ((r * v) |-- rE) by A10, A9, FINSEQ_3:29;
Affin (r * Affv) = r * (Affin Affv) by A3, RLAFFIN1:55;
then r * v in Affin (r * Affv) by A5, CONVEX1:def_1;
then A13: rvA = (r * v) |-- (r * Affv) by A7, A8, RLAFFIN1:def_7;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_(v_|--_EV)_holds_
((r_*_v)_|--_rE)_._k_=_(v_|--_EV)_._k
let k be Nat; ::_thesis: ( k in dom (v |-- EV) implies ((r * v) |-- rE) . k = (v |-- EV) . k )
assume A14: k in dom (v |-- EV) ; ::_thesis: ((r * v) |-- rE) . k = (v |-- EV) . k
then A15: ( (v |-- EV) . k = (v |-- Affv) . (EV . k) & EV /. k = EV . k ) by A11, FUNCT_1:12, PARTFUN1:def_6;
A16: rE /. k = r * (EV /. k) by A2, A11, A6, A14, VFUNCT_1:def_4;
( ((r * v) |-- rE) . k = rvA . (rE . k) & rE /. k = rE . k ) by A13, A12, A11, A6, A14, FUNCT_1:12, PARTFUN1:def_6;
hence ((r * v) |-- rE) . k = (v |-- Affv) . ((r ") * (r * (EV /. k))) by A3, A16, RLAFFIN1:def_2
.= (v |-- Affv) . (((r ") * r) * (EV /. k)) by RLVECT_1:def_7
.= (v |-- Affv) . (1 * (EV /. k)) by A3, XCMPLX_0:def_7
.= (v |-- EV) . k by A15, RLVECT_1:def_8 ;
::_thesis: verum
end;
hence v |-- EV = (r * v) |-- rE by A12, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th19: :: RLAFFIN3:19
for n, m being Nat
for Affn being affinely-independent Subset of (TOP-REAL n)
for EN being Enumeration of Affn
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
for ME being Enumeration of (Mx2Tran M) .: Affn st ME = (Mx2Tran M) * EN holds
for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME
proof
let n, m be Nat; ::_thesis: for Affn being affinely-independent Subset of (TOP-REAL n)
for EN being Enumeration of Affn
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
for ME being Enumeration of (Mx2Tran M) .: Affn st ME = (Mx2Tran M) * EN holds
for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME
let Affn be affinely-independent Subset of (TOP-REAL n); ::_thesis: for EN being Enumeration of Affn
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
for ME being Enumeration of (Mx2Tran M) .: Affn st ME = (Mx2Tran M) * EN holds
for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME
let EN be Enumeration of Affn; ::_thesis: for M being Matrix of n,m,F_Real st the_rank_of M = n holds
for ME being Enumeration of (Mx2Tran M) .: Affn st ME = (Mx2Tran M) * EN holds
for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME
set TRn = TOP-REAL n;
let M be Matrix of n,m,F_Real; ::_thesis: ( the_rank_of M = n implies for ME being Enumeration of (Mx2Tran M) .: Affn st ME = (Mx2Tran M) * EN holds
for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME )
assume A1: the_rank_of M = n ; ::_thesis: for ME being Enumeration of (Mx2Tran M) .: Affn st ME = (Mx2Tran M) * EN holds
for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME
set MT = Mx2Tran M;
A2: Mx2Tran M is one-to-one by A1, MATRTOP1:39;
set E = EN;
set A = Affn;
let ME be Enumeration of (Mx2Tran M) .: Affn; ::_thesis: ( ME = (Mx2Tran M) * EN implies for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME )
assume A3: ME = (Mx2Tran M) * EN ; ::_thesis: for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME
dom (Mx2Tran M) = the carrier of (TOP-REAL n) by FUNCT_2:def_1;
then Affn,(Mx2Tran M) .: Affn are_equipotent by A2, CARD_1:33;
then A4: card Affn = card ((Mx2Tran M) .: Affn) by CARD_1:5;
let v be Element of (TOP-REAL n); ::_thesis: ( v in Affin Affn implies v |-- EN = ((Mx2Tran M) . v) |-- ME )
assume A5: v in Affin Affn ; ::_thesis: v |-- EN = ((Mx2Tran M) . v) |-- ME
set MTv = (Mx2Tran M) . v;
A6: len (v |-- EN) = card Affn by Th16;
A7: len (((Mx2Tran M) . v) |-- ME) = card ((Mx2Tran M) .: Affn) by Th16;
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_card_Affn_holds_
(v_|--_EN)_._i_=_(((Mx2Tran_M)_._v)_|--_ME)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= card Affn implies (v |-- EN) . i = (((Mx2Tran M) . v) |-- ME) . i )
assume A8: ( 1 <= i & i <= card Affn ) ; ::_thesis: (v |-- EN) . i = (((Mx2Tran M) . v) |-- ME) . i
then A9: i in dom (((Mx2Tran M) . v) |-- ME) by A4, A7, FINSEQ_3:25;
then A10: i in dom ME by FUNCT_1:11;
A11: i in dom (v |-- EN) by A6, A8, FINSEQ_3:25;
then i in dom EN by FUNCT_1:11;
then EN . i in rng EN by FUNCT_1:def_3;
then reconsider Ei = EN . i as Element of (TOP-REAL n) ;
thus (v |-- EN) . i = (v |-- Affn) . Ei by A11, FUNCT_1:12
.= (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: Affn)) . ((Mx2Tran M) . Ei) by A1, A5, MATRTOP2:25
.= (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: Affn)) . (ME . i) by A3, A10, FUNCT_1:12
.= (((Mx2Tran M) . v) |-- ME) . i by A9, FUNCT_1:12 ; ::_thesis: verum
end;
hence v |-- EN = ((Mx2Tran M) . v) |-- ME by A4, A7, A6, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th20: :: RLAFFIN3:20
for x being set
for V being RealLinearSpace
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for A being Subset of V st A c= Affv & x in Affin Affv holds
( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds
(x |-- EV) . y = 0 )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for A being Subset of V st A c= Affv & x in Affin Affv holds
( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds
(x |-- EV) . y = 0 )
let V be RealLinearSpace; ::_thesis: for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for A being Subset of V st A c= Affv & x in Affin Affv holds
( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds
(x |-- EV) . y = 0 )
let Affv be finite affinely-independent Subset of V; ::_thesis: for EV being Enumeration of Affv
for A being Subset of V st A c= Affv & x in Affin Affv holds
( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds
(x |-- EV) . y = 0 )
let EV be Enumeration of Affv; ::_thesis: for A being Subset of V st A c= Affv & x in Affin Affv holds
( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds
(x |-- EV) . y = 0 )
let B be Subset of V; ::_thesis: ( B c= Affv & x in Affin Affv implies ( x in Affin B iff for y being set st y in dom (x |-- EV) & not EV . y in B holds
(x |-- EV) . y = 0 ) )
assume A1: B c= Affv ; ::_thesis: ( not x in Affin Affv or ( x in Affin B iff for y being set st y in dom (x |-- EV) & not EV . y in B holds
(x |-- EV) . y = 0 ) )
set xA = x |-- Affv;
set xB = x |-- B;
set cA = card Affv;
set E = EV;
assume A2: x in Affin Affv ; ::_thesis: ( x in Affin B iff for y being set st y in dom (x |-- EV) & not EV . y in B holds
(x |-- EV) . y = 0 )
set xE = x |-- EV;
A3: len (x |-- EV) = card Affv by Th16;
A4: rng EV = Affv by Def1;
then len EV = card Affv by FINSEQ_4:62;
then A5: dom (x |-- EV) = dom EV by A3, FINSEQ_3:29;
A6: Carrier (x |-- B) c= B by RLVECT_2:def_6;
hereby ::_thesis: ( ( for y being set st y in dom (x |-- EV) & not EV . y in B holds
(x |-- EV) . y = 0 ) implies x in Affin B )
assume x in Affin B ; ::_thesis: for y being set st y in dom (x |-- EV) & not EV . y in B holds
(x |-- EV) . y = 0
then A7: x |-- B = x |-- Affv by A1, RLAFFIN1:77;
let y be set ; ::_thesis: ( y in dom (x |-- EV) & not EV . y in B implies (x |-- EV) . y = 0 )
assume that
A8: y in dom (x |-- EV) and
A9: not EV . y in B ; ::_thesis: (x |-- EV) . y = 0
y in dom EV by A8, FUNCT_1:11;
then EV . y in Affv by A4, FUNCT_1:def_3;
then reconsider Ey = EV . y as Element of V ;
( (x |-- EV) . y = (x |-- Affv) . (EV . y) & not Ey in Carrier (x |-- B) ) by A6, A8, A9, FUNCT_1:12;
hence (x |-- EV) . y = 0 by A7, RLVECT_2:19; ::_thesis: verum
end;
assume A10: for y being set st y in dom (x |-- EV) & not EV . y in B holds
(x |-- EV) . y = 0 ; ::_thesis: x in Affin B
A11: now__::_thesis:_for_y_being_set_st_y_in_Affv_\_B_holds_
(x_|--_Affv)_._y_=_0
let y be set ; ::_thesis: ( y in Affv \ B implies (x |-- Affv) . y = 0 )
assume A12: y in Affv \ B ; ::_thesis: (x |-- Affv) . y = 0
then y in Affv by XBOOLE_0:def_5;
then consider z being set such that
A13: ( z in dom EV & EV . z = y ) by A4, FUNCT_1:def_3;
not y in B by A12, XBOOLE_0:def_5;
then (x |-- EV) . z = 0 by A5, A10, A13;
hence (x |-- Affv) . y = 0 by A5, A13, FUNCT_1:12; ::_thesis: verum
end;
Affv \ (Affv \ B) = Affv /\ B by XBOOLE_1:48
.= B by A1, XBOOLE_1:28 ;
hence x in Affin B by A2, A11, RLAFFIN1:75; ::_thesis: verum
end;
theorem :: RLAFFIN3:21
for x being set
for k being Nat
for V being RealLinearSpace
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv st x in Affin Affv holds
( x in Affin (EV .: (Seg k)) iff x |-- EV = ((x |-- EV) | k) ^ (((card Affv) -' k) |-> 0) )
proof
let x be set ; ::_thesis: for k being Nat
for V being RealLinearSpace
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv st x in Affin Affv holds
( x in Affin (EV .: (Seg k)) iff x |-- EV = ((x |-- EV) | k) ^ (((card Affv) -' k) |-> 0) )
let k be Nat; ::_thesis: for V being RealLinearSpace
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv st x in Affin Affv holds
( x in Affin (EV .: (Seg k)) iff x |-- EV = ((x |-- EV) | k) ^ (((card Affv) -' k) |-> 0) )
let V be RealLinearSpace; ::_thesis: for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv st x in Affin Affv holds
( x in Affin (EV .: (Seg k)) iff x |-- EV = ((x |-- EV) | k) ^ (((card Affv) -' k) |-> 0) )
let Affv be finite affinely-independent Subset of V; ::_thesis: for EV being Enumeration of Affv st x in Affin Affv holds
( x in Affin (EV .: (Seg k)) iff x |-- EV = ((x |-- EV) | k) ^ (((card Affv) -' k) |-> 0) )
let E be Enumeration of Affv; ::_thesis: ( x in Affin Affv implies ( x in Affin (E .: (Seg k)) iff x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) ) )
set B = E .: (Seg k);
set cA = card Affv;
set cAk = (card Affv) -' k;
set xE = x |-- E;
set xEk = (x |-- E) | k;
set cAk0 = ((card Affv) -' k) |-> 0;
A1: E .: (Seg k) c= rng E by RELAT_1:111;
assume A2: x in Affin Affv ; ::_thesis: ( x in Affin (E .: (Seg k)) iff x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) )
then reconsider v = x as Element of V ;
A3: len (x |-- E) = card Affv by Th16;
A4: rng E = Affv by Def1;
then A5: len E = card Affv by FINSEQ_4:62;
percases ( k > card Affv or k <= card Affv ) ;
supposeA6: k > card Affv ; ::_thesis: ( x in Affin (E .: (Seg k)) iff x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) )
then Seg (card Affv) c= Seg k by FINSEQ_1:5;
then dom E c= Seg k by A5, FINSEQ_1:def_3;
then (dom E) /\ (Seg k) = dom E by XBOOLE_1:28;
then A7: E .: (Seg k) = E .: (dom E) by RELAT_1:112;
(card Affv) - k < 0 by A6, XREAL_1:49;
then (card Affv) -' k = 0 by XREAL_0:def_2;
then A8: ((card Affv) -' k) |-> 0 is empty ;
(x |-- E) | k = x |-- E by A3, A6, FINSEQ_1:58;
hence ( x in Affin (E .: (Seg k)) iff x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) ) by A2, A4, A8, A7, FINSEQ_1:34, RELAT_1:113; ::_thesis: verum
end;
supposeA9: k <= card Affv ; ::_thesis: ( x in Affin (E .: (Seg k)) iff x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) )
A10: len (((card Affv) -' k) |-> 0) = (card Affv) -' k by CARD_1:def_7;
A11: len ((x |-- E) | k) = k by A3, A9, FINSEQ_1:59;
(card Affv) -' k = (card Affv) - k by A9, XREAL_1:233;
then A12: len (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) = k + ((card Affv) - k) by A11, A10, FINSEQ_1:22;
hereby ::_thesis: ( x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) implies x in Affin (E .: (Seg k)) )
assume A13: x in Affin (E .: (Seg k)) ; ::_thesis: x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(x_|--_E)_holds_
(((x_|--_E)_|_k)_^_(((card_Affv)_-'_k)_|->_0))_._i_=_(x_|--_E)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len (x |-- E) implies (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . b1 = (x |-- E) . b1 )
assume A14: ( 1 <= i & i <= len (x |-- E) ) ; ::_thesis: (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . b1 = (x |-- E) . b1
then A15: i in dom (x |-- E) by FINSEQ_3:25;
A16: i in dom E by A3, A5, A14, FINSEQ_3:25;
A17: i in dom (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) by A3, A12, A14, FINSEQ_3:25;
percases ( i in dom ((x |-- E) | k) or ex n being Nat st
( n in dom (((card Affv) -' k) |-> 0) & i = k + n ) ) by A11, A17, FINSEQ_1:25;
supposeA18: i in dom ((x |-- E) | k) ; ::_thesis: (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . b1 = (x |-- E) . b1
hence (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . i = ((x |-- E) | k) . i by FINSEQ_1:def_7
.= (x |-- E) . i by A18, FUNCT_1:47 ;
::_thesis: verum
end;
suppose ex n being Nat st
( n in dom (((card Affv) -' k) |-> 0) & i = k + n ) ; ::_thesis: (x |-- E) . b1 = (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . b1
then consider n being Nat such that
A19: n in dom (((card Affv) -' k) |-> 0) and
A20: i = k + n ;
A21: not E . i in E .: (Seg k)
proof
assume E . i in E .: (Seg k) ; ::_thesis: contradiction
then consider t being set such that
A22: ( t in dom E & t in Seg k & E . t = E . i ) by FUNCT_1:def_6;
i in Seg k by A16, A22, FUNCT_1:def_4;
then A23: i <= k by FINSEQ_1:1;
i >= k by A20, NAT_1:11;
then i = k by A23, XXREAL_0:1;
hence contradiction by A19, A20, FINSEQ_3:25; ::_thesis: verum
end;
(((card Affv) -' k) |-> 0) . n = 0 ;
then (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . i = 0 by A11, A19, A20, FINSEQ_1:def_7;
hence (x |-- E) . i = (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . i by A2, A1, A4, A13, A15, A21, Th20; ::_thesis: verum
end;
end;
end;
hence x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) by A12, Th16, FINSEQ_1:14; ::_thesis: verum
end;
assume A24: x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) ; ::_thesis: x in Affin (E .: (Seg k))
A25: dom (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) = dom (x |-- E) by A3, A12, FINSEQ_3:29;
now__::_thesis:_for_y_being_set_st_y_in_dom_(x_|--_E)_&_not_E_._y_in_E_.:_(Seg_k)_holds_
(x_|--_E)_._y_=_0
let y be set ; ::_thesis: ( y in dom (x |-- E) & not E . y in E .: (Seg k) implies (x |-- E) . y = 0 )
assume that
A26: y in dom (x |-- E) and
A27: not E . y in E .: (Seg k) ; ::_thesis: (x |-- E) . y = 0
reconsider i = y as Nat by A26;
i in dom E by A3, A5, A26, FINSEQ_3:29;
then not i in Seg k by A27, FUNCT_1:def_6;
then not i in dom ((x |-- E) | k) by A11, FINSEQ_1:def_3;
then consider n being Nat such that
A28: ( n in dom (((card Affv) -' k) |-> 0) & i = k + n ) by A11, A25, A26, FINSEQ_1:25;
(((card Affv) -' k) |-> 0) . n = 0 ;
hence (x |-- E) . y = 0 by A11, A24, A28, FINSEQ_1:def_7; ::_thesis: verum
end;
hence x in Affin (E .: (Seg k)) by A2, A1, A4, Th20; ::_thesis: verum
end;
end;
end;
theorem Th22: :: RLAFFIN3:22
for x being set
for k being Nat
for V being RealLinearSpace
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv st k <= card Affv & x in Affin Affv holds
( x in Affin (Affv \ (EV .: (Seg k))) iff x |-- EV = (k |-> 0) ^ ((x |-- EV) /^ k) )
proof
let x be set ; ::_thesis: for k being Nat
for V being RealLinearSpace
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv st k <= card Affv & x in Affin Affv holds
( x in Affin (Affv \ (EV .: (Seg k))) iff x |-- EV = (k |-> 0) ^ ((x |-- EV) /^ k) )
let k be Nat; ::_thesis: for V being RealLinearSpace
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv st k <= card Affv & x in Affin Affv holds
( x in Affin (Affv \ (EV .: (Seg k))) iff x |-- EV = (k |-> 0) ^ ((x |-- EV) /^ k) )
let V be RealLinearSpace; ::_thesis: for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv st k <= card Affv & x in Affin Affv holds
( x in Affin (Affv \ (EV .: (Seg k))) iff x |-- EV = (k |-> 0) ^ ((x |-- EV) /^ k) )
let Affv be finite affinely-independent Subset of V; ::_thesis: for EV being Enumeration of Affv st k <= card Affv & x in Affin Affv holds
( x in Affin (Affv \ (EV .: (Seg k))) iff x |-- EV = (k |-> 0) ^ ((x |-- EV) /^ k) )
let E be Enumeration of Affv; ::_thesis: ( k <= card Affv & x in Affin Affv implies ( x in Affin (Affv \ (E .: (Seg k))) iff x |-- E = (k |-> 0) ^ ((x |-- E) /^ k) ) )
set cA = card Affv;
set B = E .: (Seg k);
set AB = Affv \ (E .: (Seg k));
set xE = x |-- E;
set xEk = (x |-- E) | k;
set xA = x |-- Affv;
set k0 = k |-> 0;
A1: Affv \ (E .: (Seg k)) c= Affv by XBOOLE_1:36;
A2: x |-- E = ((x |-- E) | k) ^ ((x |-- E) /^ k) by RFINSEQ:8;
assume A3: k <= card Affv ; ::_thesis: ( not x in Affin Affv or ( x in Affin (Affv \ (E .: (Seg k))) iff x |-- E = (k |-> 0) ^ ((x |-- E) /^ k) ) )
then A4: Seg k c= Seg (card Affv) by FINSEQ_1:5;
A5: len (x |-- E) = card Affv by Th16;
then A6: Seg (card Affv) = dom (x |-- E) by FINSEQ_1:def_3;
A7: rng E = Affv by Def1;
then len E = card Affv by FINSEQ_4:62;
then A8: dom E = dom (x |-- E) by A5, FINSEQ_3:29;
assume A9: x in Affin Affv ; ::_thesis: ( x in Affin (Affv \ (E .: (Seg k))) iff x |-- E = (k |-> 0) ^ ((x |-- E) /^ k) )
A10: ( len (k |-> 0) = k & len ((x |-- E) | k) = k ) by A3, A5, CARD_1:def_7, FINSEQ_1:59;
hereby ::_thesis: ( x |-- E = (k |-> 0) ^ ((x |-- E) /^ k) implies x in Affin (Affv \ (E .: (Seg k))) )
assume A11: x in Affin (Affv \ (E .: (Seg k))) ; ::_thesis: x |-- E = (k |-> 0) ^ ((x |-- E) /^ k)
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_k_holds_
((x_|--_E)_|_k)_._i_=_(k_|->_0)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= k implies ((x |-- E) | k) . i = (k |-> 0) . i )
assume ( 1 <= i & i <= k ) ; ::_thesis: ((x |-- E) | k) . i = (k |-> 0) . i
then A12: i in Seg k by FINSEQ_1:1;
then E . i in E .: (Seg k) by A8, A4, A6, FUNCT_1:def_6;
then not E . i in Affv \ (E .: (Seg k)) by XBOOLE_0:def_5;
then (x |-- E) . i = 0 by A9, A1, A4, A6, A11, A12, Th20;
hence ((x |-- E) | k) . i = (k |-> 0) . i by A12, FUNCT_1:49; ::_thesis: verum
end;
hence x |-- E = (k |-> 0) ^ ((x |-- E) /^ k) by A10, A2, FINSEQ_1:14; ::_thesis: verum
end;
assume x |-- E = (k |-> 0) ^ ((x |-- E) /^ k) ; ::_thesis: x in Affin (Affv \ (E .: (Seg k)))
then A13: (x |-- E) | k = k |-> 0 by A2, FINSEQ_1:33;
now__::_thesis:_for_y_being_set_st_y_in_dom_(x_|--_E)_&_not_E_._y_in_Affv_\_(E_.:_(Seg_k))_holds_
(x_|--_E)_._y_=_0
let y be set ; ::_thesis: ( y in dom (x |-- E) & not E . y in Affv \ (E .: (Seg k)) implies (x |-- E) . y = 0 )
assume that
A14: y in dom (x |-- E) and
A15: not E . y in Affv \ (E .: (Seg k)) ; ::_thesis: (x |-- E) . y = 0
E . y in Affv by A7, A8, A14, FUNCT_1:def_3;
then E . y in E .: (Seg k) by A15, XBOOLE_0:def_5;
then consider z being set such that
A16: z in dom E and
A17: z in Seg k and
A18: E . z = E . y by FUNCT_1:def_6;
z = y by A8, A14, A16, A18, FUNCT_1:def_4;
then ((x |-- E) | k) . y = (x |-- E) . y by A17, FUNCT_1:49;
hence (x |-- E) . y = 0 by A13; ::_thesis: verum
end;
hence x in Affin (Affv \ (E .: (Seg k))) by A9, A1, Th20; ::_thesis: verum
end;
theorem Th23: :: RLAFFIN3:23
for n being Nat
for Affn being affinely-independent Subset of (TOP-REAL n)
for EN being Enumeration of Affn st 0* n in Affn & EN . (len EN) = 0* n holds
( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )
proof
let n be Nat; ::_thesis: for Affn being affinely-independent Subset of (TOP-REAL n)
for EN being Enumeration of Affn st 0* n in Affn & EN . (len EN) = 0* n holds
( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )
let Affn be affinely-independent Subset of (TOP-REAL n); ::_thesis: for EN being Enumeration of Affn st 0* n in Affn & EN . (len EN) = 0* n holds
( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )
let EN be Enumeration of Affn; ::_thesis: ( 0* n in Affn & EN . (len EN) = 0* n implies ( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A ) ) )
set A = Affn;
set E = EN;
assume that
A1: 0* n in Affn and
A2: EN . (len EN) = 0* n ; ::_thesis: ( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )
A3: card Affn >= 1 by A1, NAT_1:14;
set cA = (card Affn) -' 1;
A4: rng EN = Affn by Def1;
(card Affn) -' 1 = (card Affn) - 1 by A1, NAT_1:14, XREAL_1:233;
then A5: len EN = ((card Affn) -' 1) + 1 by A4, FINSEQ_4:62;
A6: len EN = card Affn by A4, FINSEQ_4:62;
A7: not 0* n in rng (EN | ((card Affn) -' 1))
proof
A8: len EN in dom EN by A6, A3, FINSEQ_3:25;
assume 0* n in rng (EN | ((card Affn) -' 1)) ; ::_thesis: contradiction
then consider x being set such that
A9: x in dom (EN | ((card Affn) -' 1)) and
A10: (EN | ((card Affn) -' 1)) . x = 0* n by FUNCT_1:def_3;
A11: x in Seg ((card Affn) -' 1) by A9, RELAT_1:57;
( x in dom EN & (EN | ((card Affn) -' 1)) . x = EN . x ) by A9, FUNCT_1:47, RELAT_1:57;
then x = ((card Affn) -' 1) + 1 by A2, A5, A10, A8, FUNCT_1:def_4;
then ((card Affn) -' 1) + 1 <= (card Affn) -' 1 by A11, FINSEQ_1:1;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
EN = (EN | ((card Affn) -' 1)) ^ <*(EN . (len EN))*> by A5, FINSEQ_3:55;
then A12: Affn = (rng (EN | ((card Affn) -' 1))) \/ (rng <*(EN . (len EN))*>) by A4, FINSEQ_1:31
.= (rng (EN | ((card Affn) -' 1))) \/ {(0* n)} by A2, FINSEQ_1:38 ;
hence A13: Affn \ {(0* n)} = rng (EN | ((card Affn) -' 1)) by A7, ZFMISC_1:117; ::_thesis: for A being Subset of (n -VectSp_over F_Real) st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A
let A1 be Subset of (n -VectSp_over F_Real); ::_thesis: ( Affn = A1 implies EN | ((card Affn) -' 1) is OrdBasis of Lin A1 )
assume A14: Affn = A1 ; ::_thesis: EN | ((card Affn) -' 1) is OrdBasis of Lin A1
A1 c= [#] (Lin A1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A1 or x in [#] (Lin A1) )
assume x in A1 ; ::_thesis: x in [#] (Lin A1)
then x in Lin A1 by VECTSP_7:8;
hence x in [#] (Lin A1) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider e = EN as FinSequence of (Lin A1) by A4, A14, FINSEQ_1:def_4;
0* n = 0. (TOP-REAL n) by EUCLID:66;
then Affn \ {(0* n)} is linearly-independent by A1, RLAFFIN1:46;
then A1 \ {(0* n)} is linearly-independent by A14, MATRTOP2:7;
then A15: rng (e | ((card Affn) -' 1)) is linearly-independent by A14, A13, VECTSP_9:12;
[#] (Lin A1) = [#] (Lin Affn) by A14, MATRTOP2:6
.= [#] (Lin (Affn \ {(0. (TOP-REAL n))})) by Lm2
.= [#] (Lin (Affn \ {(0* n)})) by EUCLID:66
.= [#] (Lin (A1 \ {(0* n)})) by A14, MATRTOP2:6 ;
then Lin A1 = Lin (A1 \ {(0* n)}) by VECTSP_4:29
.= Lin (rng (e | ((card Affn) -' 1))) by A12, A7, A14, VECTSP_9:17, ZFMISC_1:117 ;
then ( e | ((card Affn) -' 1) is one-to-one & rng (e | ((card Affn) -' 1)) is Basis of Lin A1 ) by A15, FUNCT_1:52, VECTSP_7:def_3;
hence EN | ((card Affn) -' 1) is OrdBasis of Lin A1 by MATRLIN:def_2; ::_thesis: verum
end;
Lm5: 0 in REAL
by XREAL_0:def_1;
theorem Th24: :: RLAFFIN3:24
for n being Nat
for Affn being affinely-independent Subset of (TOP-REAL n)
for EN being Enumeration of Affn
for A being Subset of (n -VectSp_over F_Real) st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds
for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds
for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)
proof
let n be Nat; ::_thesis: for Affn being affinely-independent Subset of (TOP-REAL n)
for EN being Enumeration of Affn
for A being Subset of (n -VectSp_over F_Real) st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds
for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds
for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)
let Affn be affinely-independent Subset of (TOP-REAL n); ::_thesis: for EN being Enumeration of Affn
for A being Subset of (n -VectSp_over F_Real) st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds
for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds
for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)
let EN be Enumeration of Affn; ::_thesis: for A being Subset of (n -VectSp_over F_Real) st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds
for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds
for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)
reconsider Z = 0 as Element of REAL by Lm5;
set TR = TOP-REAL n;
set A = Affn;
set V = n -VectSp_over F_Real;
set E = EN;
let A1 be Subset of (n -VectSp_over F_Real); ::_thesis: ( Affn = A1 & 0* n in Affn & EN . (len EN) = 0* n implies for B being OrdBasis of Lin A1 st B = EN | ((card Affn) -' 1) holds
for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1) )
assume that
A1: Affn = A1 and
A2: 0* n in Affn and
A3: EN . (len EN) = 0* n ; ::_thesis: for B being OrdBasis of Lin A1 st B = EN | ((card Affn) -' 1) holds
for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)
deffunc H1( set ) -> Element of REAL = Z;
A4: Affin Affn = [#] (Lin Affn) by A2, Th11;
set cA = (card Affn) -' 1;
let B be OrdBasis of Lin A1; ::_thesis: ( B = EN | ((card Affn) -' 1) implies for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1) )
assume A5: B = EN | ((card Affn) -' 1) ; ::_thesis: for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)
A6: rng B = Affn \ {(0* n)} by A2, A3, A5, Th23;
then reconsider rB = rng B as Subset of (TOP-REAL n) ;
let v be Element of (Lin A1); ::_thesis: v |-- B = (v |-- EN) | ((card Affn) -' 1)
set vB = v |-- B;
consider KV being Linear_Combination of Lin A1 such that
A7: v = Sum KV and
A8: Carrier KV c= rng B and
A9: for k being Nat st 1 <= k & k <= len (v |-- B) holds
(v |-- B) /. k = KV . (B /. k) by MATRLIN:def_7;
A10: (v |-- EN) | ((card Affn) -' 1) = (v |-- Affn) * (EN | ((card Affn) -' 1)) by RELAT_1:83;
dom (v |-- Affn) = [#] (TOP-REAL n) by FUNCT_2:def_1;
then rB c= dom (v |-- Affn) ;
then A11: len ((v |-- EN) | ((card Affn) -' 1)) = len B by A5, A10, FINSEQ_2:29;
A12: [#] (Lin A1) = [#] (Lin Affn) by A1, MATRTOP2:6;
then reconsider RB = rB as Subset of (Lin Affn) ;
reconsider KR = KV as Linear_Combination of Lin Affn by A12, MATRTOP2:11;
A13: Carrier KR = Carrier KV by MATRTOP2:12;
consider KR1 being Linear_Combination of TOP-REAL n such that
A14: Carrier KR1 = Carrier KR and
A15: Sum KR1 = Sum KR by RLVECT_5:11;
rng B c= Affn by A6, XBOOLE_1:36;
then A16: Carrier KR1 c= Affn by A8, A13, A14, XBOOLE_1:1;
reconsider KR2 = KR1 | ([#] (Lin Affn)) as Linear_Combination of Lin Affn by MATRTOP2:10;
A17: ( Carrier KR2 = Carrier KR1 & Sum KR2 = Sum KR1 ) by A14, RLVECT_5:10;
reconsider KR1 = KR1 as Linear_Combination of Affn by A16, RLVECT_2:def_6;
consider KR0 being Function of the carrier of (TOP-REAL n),REAL such that
A18: KR0 . (0. (TOP-REAL n)) = 1 - (sum KR1) and
A19: for u being Element of (TOP-REAL n) st u <> 0. (TOP-REAL n) holds
KR0 . u = H1(u) from FUNCT_2:sch_6();
reconsider KR0 = KR0 as Element of Funcs ( the carrier of (TOP-REAL n),REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_(TOP-REAL_n)_st_not_u_in_{(0._(TOP-REAL_n))}_holds_
KR0_._u_=_0
let u be VECTOR of (TOP-REAL n); ::_thesis: ( not u in {(0. (TOP-REAL n))} implies KR0 . u = 0 )
assume not u in {(0. (TOP-REAL n))} ; ::_thesis: KR0 . u = 0
then u <> 0. (TOP-REAL n) by TARSKI:def_1;
hence KR0 . u = 0 by A19; ::_thesis: verum
end;
then reconsider KR0 = KR0 as Linear_Combination of TOP-REAL n by RLVECT_2:def_3;
Carrier KR0 c= {(0. (TOP-REAL n))}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier KR0 or x in {(0. (TOP-REAL n))} )
assume that
A20: x in Carrier KR0 and
A21: not x in {(0. (TOP-REAL n))} ; ::_thesis: contradiction
( KR0 . x <> 0 & x <> 0. (TOP-REAL n) ) by A20, A21, RLVECT_2:19, TARSKI:def_1;
hence contradiction by A19, A20; ::_thesis: verum
end;
then reconsider KR0 = KR0 as Linear_Combination of {(0. (TOP-REAL n))} by RLVECT_2:def_6;
A22: Carrier KR0 c= {(0. (TOP-REAL n))} by RLVECT_2:def_6;
rng B is Basis of Lin A1 by MATRLIN:def_2;
then rng B is linearly-independent by VECTSP_7:def_3;
then rng B is linearly-independent Subset of (n -VectSp_over F_Real) by VECTSP_9:11;
then rB is linearly-independent by MATRTOP2:7;
then A23: RB is linearly-independent by RLVECT_5:15;
A24: len (v |-- B) = len B by MATRLIN:def_7;
A25: Sum KR0 = (KR0 . (0. (TOP-REAL n))) * (0. (TOP-REAL n)) by RLVECT_2:32
.= 0. (TOP-REAL n) by RLVECT_1:10 ;
A26: 0. (TOP-REAL n) = 0* n by EUCLID:66;
then {(0. (TOP-REAL n))} c= Affn by A2, ZFMISC_1:31;
then reconsider KR0 = KR0 as Linear_Combination of Affn by RLVECT_2:21;
reconsider K = KR1 + KR0 as Linear_Combination of Affn by RLVECT_2:38;
A27: sum K = (sum KR1) + (sum KR0) by RLAFFIN1:34
.= (sum KR1) + (1 - (sum KR1)) by A18, A22, RLAFFIN1:32
.= 1 ;
Sum K = (Sum KR1) + (Sum KR0) by RLVECT_3:1
.= Sum KR1 by A25, RLVECT_1:def_4
.= v by A7, A15, MATRTOP2:12 ;
then A28: v |-- Affn = K by A12, A4, A27, RLAFFIN1:def_7;
now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_B_holds_
((v_|--_EN)_|_((card_Affn)_-'_1))_._k_=_(v_|--_B)_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len B implies ((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k )
reconsider Bk = B /. k as Element of (TOP-REAL n) by A12, RLSUB_1:10;
assume A29: ( 1 <= k & k <= len B ) ; ::_thesis: ((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k
then A30: ( (v |-- B) /. k = KV . Bk & k in dom ((v |-- EN) | ((card Affn) -' 1)) ) by A24, A9, A11, FINSEQ_3:25;
A31: k in dom B by A29, FINSEQ_3:25;
then A32: Bk = B . k by PARTFUN1:def_6;
then Bk in rng B by A31, FUNCT_1:def_3;
then Bk <> 0. (TOP-REAL n) by A6, A26, ZFMISC_1:56;
then not Bk in Carrier KR0 by A22, TARSKI:def_1;
then A33: KR0 . Bk = 0 by RLVECT_2:19;
k in dom (v |-- B) by A24, A29, FINSEQ_3:25;
then A34: (v |-- B) . k = (v |-- B) /. k by PARTFUN1:def_6;
K . Bk = (KR1 . Bk) + (KR0 . Bk) by RLVECT_2:def_10;
then K . Bk = KR2 . Bk by A12, A33, FUNCT_1:49
.= KV . Bk by A23, A8, A13, A14, A15, A17, RLVECT_5:1 ;
hence ((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k by A5, A28, A10, A30, A34, A32, FUNCT_1:12; ::_thesis: verum
end;
hence v |-- B = (v |-- EN) | ((card Affn) -' 1) by A24, A11, FINSEQ_1:14; ::_thesis: verum
end;
Lm6: for k being Nat
for V being LinearTopSpace
for A being finite affinely-independent Subset of V
for E being Enumeration of A
for v being Point of V
for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds
for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }
proof
let k be Nat; ::_thesis: for V being LinearTopSpace
for A being finite affinely-independent Subset of V
for E being Enumeration of A
for v being Point of V
for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds
for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }
let V be LinearTopSpace; ::_thesis: for A being finite affinely-independent Subset of V
for E being Enumeration of A
for v being Point of V
for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds
for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }
let A be finite affinely-independent Subset of V; ::_thesis: for E being Enumeration of A
for v being Point of V
for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds
for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }
let E be Enumeration of A; ::_thesis: for v being Point of V
for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds
for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }
let v be Point of V; ::_thesis: for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds
for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }
let Ev be Enumeration of v + A; ::_thesis: ( Ev = E + ((card A) |-> v) implies for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } )
assume A1: Ev = E + ((card A) |-> v) ; ::_thesis: for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }
set T = transl (v,V);
let X be set ; ::_thesis: (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }
set U = { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } ;
set W = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } ;
A2: Affin (v + A) = v + (Affin A) by RLAFFIN1:53;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } c= (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) }
let y be set ; ::_thesis: ( y in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } implies y in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } )
assume y in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } ; ::_thesis: y in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }
then consider x being set such that
x in dom (transl (v,V)) and
A3: x in { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } and
A4: (transl (v,V)) . x = y by FUNCT_1:def_6;
consider u being Point of V such that
A5: x = u and
A6: u in Affin A and
A7: (u |-- E) | k in X by A3;
v + u in { (v + t) where t is Point of V : t in Affin A } by A6;
then A8: v + u in Affin (v + A) by A2, RUSUB_4:def_8;
u |-- E = (v + u) |-- Ev by A1, A6, Th17;
then v + u in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } by A7, A8;
hence y in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } by A4, A5, RLTOPSP1:def_10; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } or y in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } )
assume y in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } ; ::_thesis: y in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) }
then consider w being Point of V such that
A9: y = w and
A10: w in Affin (v + A) and
A11: (w |-- Ev) | k in X ;
w in { (v + t) where t is Point of V : t in Affin A } by A2, A10, RUSUB_4:def_8;
then consider u being Point of V such that
A12: w = v + u and
A13: u in Affin A ;
w |-- Ev = u |-- E by A1, A12, A13, Th17;
then ( dom (transl (v,V)) = the carrier of V & u in { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } ) by A11, A13, FUNCT_2:52;
then (transl (v,V)) . u in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } by FUNCT_1:def_6;
hence y in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } by A9, A12, RLTOPSP1:def_10; ::_thesis: verum
end;
Lm7: for n, k being Nat st k <= n holds
for A being non empty finite affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
for E being Enumeration of A st E . (len E) = 0* n holds
for P being Subset of (TOP-REAL k)
for B being Subset of (TOP-REAL n) st B = { pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in P } holds
( P is open iff B is open )
proof
let n, k be Nat; ::_thesis: ( k <= n implies for A being non empty finite affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
for E being Enumeration of A st E . (len E) = 0* n holds
for P being Subset of (TOP-REAL k)
for B being Subset of (TOP-REAL n) st B = { pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in P } holds
( P is open iff B is open ) )
assume A1: k <= n ; ::_thesis: for A being non empty finite affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
for E being Enumeration of A st E . (len E) = 0* n holds
for P being Subset of (TOP-REAL k)
for B being Subset of (TOP-REAL n) st B = { pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in P } holds
( P is open iff B is open )
set V = n -VectSp_over F_Real;
set TRn = TOP-REAL n;
let A be non empty finite affinely-independent Subset of (TOP-REAL n); ::_thesis: ( card A = n + 1 implies for E being Enumeration of A st E . (len E) = 0* n holds
for P being Subset of (TOP-REAL k)
for B being Subset of (TOP-REAL n) st B = { pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in P } holds
( P is open iff B is open ) )
reconsider A1 = A as Subset of (n -VectSp_over F_Real) by Lm3;
set TRk = TOP-REAL k;
set cA = (card A) -' 1;
assume A2: card A = n + 1 ; ::_thesis: for E being Enumeration of A st E . (len E) = 0* n holds
for P being Subset of (TOP-REAL k)
for B being Subset of (TOP-REAL n) st B = { pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in P } holds
( P is open iff B is open )
dim (TOP-REAL n) = n by Th4;
then A3: Affin A = [#] (TOP-REAL n) by A2, Th6;
0* n = 0. (TOP-REAL n) by EUCLID:66;
then A4: Lin (A \ {(0* n)}) = Lin A by Lm2;
let E be Enumeration of A; ::_thesis: ( E . (len E) = 0* n implies for P being Subset of (TOP-REAL k)
for B being Subset of (TOP-REAL n) st B = { pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in P } holds
( P is open iff B is open ) )
reconsider e = E as FinSequence of (n -VectSp_over F_Real) by Lm3;
A5: rng E = A by Def1;
then A6: len E = card A by FINSEQ_4:62;
n < n + 1 by NAT_1:13;
then reconsider M = FinS2MX (e | n) as Matrix of n,F_Real by A2, A6, FINSEQ_1:59;
A7: (card A) - 1 = (card A) -' 1 by NAT_1:14, XREAL_1:233;
set MT = Mx2Tran M;
assume A8: E . (len E) = 0* n ; ::_thesis: for P being Subset of (TOP-REAL k)
for B being Subset of (TOP-REAL n) st B = { pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in P } holds
( P is open iff B is open )
let P be Subset of (TOP-REAL k); ::_thesis: for B being Subset of (TOP-REAL n) st B = { pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in P } holds
( P is open iff B is open )
let B be Subset of (TOP-REAL n); ::_thesis: ( B = { pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in P } implies ( P is open iff B is open ) )
set PP = { v where v is Element of (TOP-REAL n) : v | k in P } ;
{ v where v is Element of (TOP-REAL n) : v | k in P } c= the carrier of (TOP-REAL n)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Element of (TOP-REAL n) : v | k in P } or x in the carrier of (TOP-REAL n) )
assume x in { v where v is Element of (TOP-REAL n) : v | k in P } ; ::_thesis: x in the carrier of (TOP-REAL n)
then ex v being Element of (TOP-REAL n) st
( x = v & v | k in P ) ;
hence x in the carrier of (TOP-REAL n) ; ::_thesis: verum
end;
then reconsider PP = { v where v is Element of (TOP-REAL n) : v | k in P } as Subset of (TOP-REAL n) ;
assume A9: B = { v where v is Element of (TOP-REAL n) : (v |-- E) | k in P } ; ::_thesis: ( P is open iff B is open )
card A >= 1 by NAT_1:14;
then len E in dom E by A6, FINSEQ_3:25;
then A10: 0* n in A by A8, A5, FUNCT_1:def_3;
then A11: ( [#] (Lin (A \ {(0* n)})) = [#] (Lin (A1 \ {(0* n)})) & rng (E | ((card A) -' 1)) = A \ {(0* n)} ) by A8, Th23, MATRTOP2:6;
[#] (Lin A) = [#] (Lin A1) by MATRTOP2:6;
then A12: Lin (lines M) = Lin A1 by A2, A7, A4, A11, VECTSP_4:29;
then reconsider BE = E | ((card A) -' 1) as OrdBasis of Lin (lines M) by A8, A10, Th23;
rng BE is Basis of Lin (lines M) by MATRLIN:def_2;
then rng BE is linearly-independent by VECTSP_7:def_3;
then A13: lines M is linearly-independent by A2, A7, VECTSP_9:11;
BE = M by A2, A7;
then M is one-to-one by MATRLIN:def_2;
then A14: the_rank_of M = n by A13, MATRIX13:121;
then Det M <> 0. F_Real by MATRIX13:83;
then A15: M is invertible by LAPLACE:34;
Mx2Tran M is onto by A14, MATRTOP1:41;
then A16: rng (Mx2Tran M) = the carrier of (TOP-REAL n) by FUNCT_2:def_3;
A17: B c= (Mx2Tran M) .: PP
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in (Mx2Tran M) .: PP )
assume x in B ; ::_thesis: x in (Mx2Tran M) .: PP
then consider v being Element of (TOP-REAL n) such that
A18: x = v and
A19: (v |-- E) | k in P by A9;
consider f being set such that
A20: ( f in dom (Mx2Tran M) & (Mx2Tran M) . f = v ) by A16, FUNCT_1:def_3;
len (v |-- E) = n + 1 by A2, Th16;
then len ((v |-- E) | n) = n by FINSEQ_1:59, NAT_1:11;
then (v |-- E) | n is Element of n -tuples_on REAL by FINSEQ_2:92;
then (v |-- E) | n in n -tuples_on REAL ;
then (v |-- E) | n in REAL n by EUCLID:def_1;
then A21: (v |-- E) | n is Element of (TOP-REAL n) by EUCLID:22;
reconsider w = v as Element of (Lin (lines M)) by A2, A7, A3, A10, A4, A11, Th11;
A22: ((v |-- E) | n) | k = (v |-- E) | k by A1, FINSEQ_1:82;
f = w |-- BE by A2, A7, A20, MATRTOP2:17
.= (w |-- E) | ((card A) -' 1) by A8, A10, A12, Th24 ;
then f in PP by A2, A7, A19, A21, A22;
hence x in (Mx2Tran M) .: PP by A18, A20, FUNCT_1:def_6; ::_thesis: verum
end;
(Mx2Tran M) .: PP c= B
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Mx2Tran M) .: PP or y in B )
assume y in (Mx2Tran M) .: PP ; ::_thesis: y in B
then consider x being set such that
x in dom (Mx2Tran M) and
A23: x in PP and
A24: (Mx2Tran M) . x = y by FUNCT_1:def_6;
consider f being Element of (TOP-REAL n) such that
A25: ( x = f & f | k in P ) by A23;
reconsider MTf = (Mx2Tran M) . f as Element of (Lin (lines M)) by A2, A7, A3, A10, A4, A11, Th11;
f = MTf |-- BE by A2, A7, MATRTOP2:17
.= (MTf |-- E) | ((card A) -' 1) by A8, A10, A12, Th24 ;
then f | k = (MTf |-- E) | k by A1, A2, A7, FINSEQ_1:82;
hence y in B by A9, A24, A25; ::_thesis: verum
end;
then A26: (Mx2Tran M) .: PP = B by A17, XBOOLE_0:def_10;
( P is open iff PP is open ) by A1, Th7;
hence ( P is open iff B is open ) by A15, A26, TOPGRP_1:25; ::_thesis: verum
end;
Lm8: for n, k being Nat
for A being non empty finite affinely-independent Subset of (TOP-REAL n) st k < card A holds
for E being Enumeration of A st E . (len E) = 0* n holds
for P being Subset of (TOP-REAL k)
for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds
( P is open iff B is open )
proof
let n, k be Nat; ::_thesis: for A being non empty finite affinely-independent Subset of (TOP-REAL n) st k < card A holds
for E being Enumeration of A st E . (len E) = 0* n holds
for P being Subset of (TOP-REAL k)
for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds
( P is open iff B is open )
set TRn = TOP-REAL n;
let A be non empty finite affinely-independent Subset of (TOP-REAL n); ::_thesis: ( k < card A implies for E being Enumeration of A st E . (len E) = 0* n holds
for P being Subset of (TOP-REAL k)
for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds
( P is open iff B is open ) )
assume A1: k < card A ; ::_thesis: for E being Enumeration of A st E . (len E) = 0* n holds
for P being Subset of (TOP-REAL k)
for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds
( P is open iff B is open )
reconsider c1 = (card A) - 1 as Element of NAT by NAT_1:14, NAT_1:21;
set AA = Affin A;
let E be Enumeration of A; ::_thesis: ( E . (len E) = 0* n implies for P being Subset of (TOP-REAL k)
for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds
( P is open iff B is open ) )
assume A2: E . (len E) = 0* n ; ::_thesis: for P being Subset of (TOP-REAL k)
for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds
( P is open iff B is open )
A3: rng E = A by Def1;
then A4: len E = card A by FINSEQ_4:62;
then A5: len E >= 1 by NAT_1:14;
then A6: len E in dom E by FINSEQ_3:25;
then A7: 0* n in rng E by A2, FUNCT_1:def_3;
A8: 0. (TOP-REAL n) = 0* n by EUCLID:66;
then A9: 0. (TOP-REAL n) in A by A2, A3, A6, FUNCT_1:def_3;
then A10: A \ {(0. (TOP-REAL n))} is linearly-independent by RLAFFIN1:46;
card A <= 1 + (dim (TOP-REAL n)) by Th5;
then c1 + 1 <= 1 + n by Th4;
then A11: c1 <= n by XREAL_1:6;
set nc = n -' c1;
let P be Subset of (TOP-REAL k); ::_thesis: for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds
( P is open iff B is open )
let B be Subset of ((TOP-REAL n) | (Affin A)); ::_thesis: ( B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } implies ( P is open iff B is open ) )
assume A12: B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } ; ::_thesis: ( P is open iff B is open )
A13: [#] ((TOP-REAL n) | (Affin A)) = Affin A by PRE_TOPC:def_5;
consider F being FinSequence such that
A14: rng F = A \ {(0. (TOP-REAL n))} and
A15: F is one-to-one by FINSEQ_4:58;
set V = n -VectSp_over F_Real;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
len Bn = n by MATRTOP1:19;
then reconsider BnC = FinS2MX (Bn | c1) as Matrix of c1,n,F_Real by A11, FINSEQ_1:59;
reconsider MBC = Mx2Tran BnC as Function ;
A16: c1 + 1 = card A ;
A17: len F = card (A \ {(0. (TOP-REAL n))}) by A14, A15, FINSEQ_4:62
.= c1 by A9, A16, STIRL2_1:55 ;
set MBc = Mx2Tran BnC;
set TRc = TOP-REAL c1;
A18: ( dom (Mx2Tran BnC) = [#] (TOP-REAL c1) & (Mx2Tran BnC) . (0. (TOP-REAL c1)) = 0. (TOP-REAL n) ) by FUNCT_2:def_1, MATRTOP1:29;
rng Bn is Basis of n -VectSp_over F_Real by MATRLIN:def_2;
then rng Bn is linearly-independent by VECTSP_7:def_3;
then A19: rng (Bn | c1) is linearly-independent by RELAT_1:70, VECTSP_7:1;
reconsider F = F as FinSequence of (TOP-REAL n) by A14, FINSEQ_1:def_4;
[#] (Lin (rng (Bn | (len F)))) c= the carrier of (n -VectSp_over F_Real) by VECTSP_4:def_2;
then reconsider BF = [#] (Lin (rng (Bn | (len F)))) as Subset of (TOP-REAL n) by Lm3;
A20: rng MBC = BF by A17, MATRTOP2:18;
consider M being Matrix of n,F_Real such that
A21: M is invertible and
A22: M | (len F) = F by A10, A14, A15, MATRTOP2:19;
set MTI = Mx2Tran (M ~);
A23: [#] ((TOP-REAL n) | BF) = BF by PRE_TOPC:def_5;
M ~ is invertible by A21, MATRIX_6:16;
then A24: Det (M ~) <> 0. F_Real by LAPLACE:34;
then A25: the_rank_of (M ~) = n by MATRIX13:83;
then reconsider MTe = (Mx2Tran (M ~)) * E as Enumeration of (Mx2Tran (M ~)) .: A by Th15;
A26: rng MTe = (Mx2Tran (M ~)) .: A by Def1;
( dom (Mx2Tran (M ~)) = [#] (TOP-REAL n) & Mx2Tran (M ~) is one-to-one ) by A24, FUNCT_2:def_1, MATRTOP1:40;
then A,(Mx2Tran (M ~)) .: A are_equipotent by CARD_1:33;
then A27: card A = card ((Mx2Tran (M ~)) .: A) by CARD_1:5;
then len MTe = len E by A4, A26, FINSEQ_4:62;
then len E in dom MTe by A5, FINSEQ_3:25;
then A28: MTe . (len E) = (Mx2Tran (M ~)) . (0. (TOP-REAL n)) by A2, A8, FUNCT_1:12
.= 0. (TOP-REAL n) by MATRTOP1:29 ;
set MT = Mx2Tran M;
Affin A = [#] (Lin A) by A3, A7, Th11
.= [#] (Lin (rng F)) by A14, Lm2 ;
then A29: (Mx2Tran M) .: BF = Affin A by A10, A14, A15, A21, A22, MATRTOP2:21;
then A30: rng ((Mx2Tran M) | BF) = Affin A by RELAT_1:115;
A31: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def_1;
then dom ((Mx2Tran M) | BF) = BF by RELAT_1:62;
then reconsider MT1 = (Mx2Tran M) | BF as Function of ((TOP-REAL n) | BF),((TOP-REAL n) | (Affin A)) by A13, A23, A30, FUNCT_2:1;
reconsider MT = Mx2Tran M as Function ;
A32: Det M <> 0. F_Real by A21, LAPLACE:34;
then A33: MT " = Mx2Tran (M ~) by MATRTOP1:43;
MT1 is being_homeomorphism by A21, A29, METRIZTS:2;
then A34: ( MT1 " B is open iff B is open ) by TOPGRP_1:26;
set nc0 = (n -' c1) |-> 0;
set Vc1 = { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } ;
A35: n -' c1 = n - c1 by A11, XREAL_1:233;
then A36: n = c1 + (n -' c1) ;
A37: MT is one-to-one by A32, MATRTOP1:40;
then A38: MT " (Affin A) = BF by A29, A31, FUNCT_1:94;
A39: MT " A c= MT " (Affin A) by RELAT_1:143, RLAFFIN1:49;
then A40: (Mx2Tran (M ~)) .: A c= BF by A33, A37, A38, FUNCT_1:85;
Bn is one-to-one by MATRLIN:def_2;
then Bn | c1 is one-to-one by FUNCT_1:52;
then A41: the_rank_of BnC = c1 by A19, MATRIX13:121;
then A42: MBC is one-to-one by MATRTOP1:39;
then A43: dom (MBC ") = rng MBC by FUNCT_1:33;
then reconsider MBCe = (MBC ") * MTe as FinSequence by A20, A26, A40, FINSEQ_1:16;
A44: rng MBCe = (MBC ") .: ((Mx2Tran (M ~)) .: A) by A26, RELAT_1:127;
(Mx2Tran (M ~)) .: A is affinely-independent by A25, MATRTOP2:24;
then (Mx2Tran BnC) " ((Mx2Tran (M ~)) .: A) is affinely-independent by A41, MATRTOP2:27;
then reconsider R = rng MBCe as finite affinely-independent Subset of (TOP-REAL c1) by A42, A44, FUNCT_1:85;
reconsider MBCe = MBCe as Enumeration of R by A42, Def1;
reconsider MBCeE = (Mx2Tran BnC) * MBCe as Enumeration of (Mx2Tran BnC) .: R by A41, Th15;
MBC * (MBC ") = id (rng MBC) by A42, FUNCT_1:39;
then A45: MBCeE = (id (rng MBC)) * MTe by RELAT_1:36
.= MTe by A20, A26, A40, RELAT_1:53 ;
set PPP = { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } ;
A46: { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } c= [#] (TOP-REAL c1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } or x in [#] (TOP-REAL c1) )
assume x in { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } ; ::_thesis: x in [#] (TOP-REAL c1)
then ex v being Element of (TOP-REAL c1) st
( x = v & (v |-- MBCe) | k in P ) ;
hence x in [#] (TOP-REAL c1) ; ::_thesis: verum
end;
A47: (Mx2Tran (M ~)) .: A = MT " A by A33, A37, FUNCT_1:85;
A48: MT " B c= MT " (Affin A) by A13, RELAT_1:143;
A49: (Mx2Tran (M ~)) .: A,R are_equipotent by A20, A42, A43, A40, A44, CARD_1:33;
then A50: c1 + 1 = card R by A27, CARD_1:5;
then A51: ( k <= c1 & not R is empty ) by A1, NAT_1:13;
reconsider PPP = { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } as Subset of (TOP-REAL c1) by A46;
set nPP = { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } ;
dim (TOP-REAL c1) = c1 by Th4;
then A52: Affin R = [#] (TOP-REAL c1) by A50, Th6;
A53: (Mx2Tran BnC) .: R = MBC .: ((MBC ") .: ((Mx2Tran (M ~)) .: A)) by A26, RELAT_1:127
.= (MBC * (MBC ")) .: ((Mx2Tran (M ~)) .: A) by RELAT_1:126
.= (id (rng MBC)) .: ((Mx2Tran (M ~)) .: A) by A42, FUNCT_1:39
.= (Mx2Tran (M ~)) .: A by A47, A38, A39, A20, FUNCT_1:92 ;
A54: MT " B c= { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MT " B or x in { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } )
assume A55: x in MT " B ; ::_thesis: x in { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) }
then reconsider w = x as Element of ((TOP-REAL n) | BF) by A29, A23, A31, A37, A48, FUNCT_1:94;
MT . x in B by A55, FUNCT_1:def_7;
then consider v being Element of ((TOP-REAL n) | (Affin A)) such that
A56: MT . x = v and
A57: (v |-- E) | k in P by A12;
x in dom MT by A55, FUNCT_1:def_7;
then A58: (Mx2Tran (M ~)) . v = x by A33, A37, A56, FUNCT_1:34;
x in BF by A38, A48, A55;
then reconsider W = x as Element of (TOP-REAL n) ;
A59: v in Affin A by A13;
consider u being set such that
A60: u in dom (Mx2Tran BnC) and
A61: (Mx2Tran BnC) . u = w by A38, A48, A20, A55, FUNCT_1:def_3;
A62: W | c1 = u by A60, A61, MATRTOP1:38;
reconsider u = u as Element of (TOP-REAL c1) by A60;
u |-- MBCe = w |-- MTe by A61, A53, A45, A41, A52, Th19
.= v |-- E by A25, A58, A59, Th19 ;
then u in PPP by A57;
hence x in { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } by A38, A48, A55, A62; ::_thesis: verum
end;
A63: BF c= { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BF or x in { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } )
assume A64: x in BF ; ::_thesis: x in { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum }
then reconsider f = x as Element of (TOP-REAL n) ;
len f = n by CARD_1:def_7;
then len (f | c1) = c1 by A11, FINSEQ_1:59;
then f | c1 is c1 -element by CARD_1:def_7;
then A65: f | c1 is Element of (TOP-REAL c1) by Lm1;
f in Lin (rng (Bn | c1)) by A17, A64, STRUCT_0:def_5;
then f = (f | c1) ^ ((n -' c1) |-> 0) by MATRTOP2:20;
hence x in { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } by A65; ::_thesis: verum
end;
{ (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } c= BF
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } or x in BF )
assume x in { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } ; ::_thesis: x in BF
then consider v being Element of (TOP-REAL c1) such that
A66: x = v ^ ((n -' c1) |-> 0) and
verum ;
len v = c1 by CARD_1:def_7;
then (v ^ ((n -' c1) |-> 0)) | c1 = (v ^ ((n -' c1) |-> 0)) | (dom v) by FINSEQ_1:def_3
.= v by FINSEQ_1:21 ;
then v ^ ((n -' c1) |-> 0) in Lin (rng (Bn | c1)) by A35, MATRTOP2:20;
hence x in BF by A17, A66, STRUCT_0:def_5; ::_thesis: verum
end;
then A67: BF = { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } by A63, XBOOLE_0:def_10;
A68: { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } c= MT " B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } or x in MT " B )
assume x in { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } ; ::_thesis: x in MT " B
then consider v being Element of (TOP-REAL n) such that
A69: x = v and
A70: v | c1 in PPP and
A71: v in BF ;
consider v1 being Element of (TOP-REAL c1) such that
A72: v = v1 ^ ((n -' c1) |-> 0) by A67, A71;
consider u being Element of (TOP-REAL c1) such that
A73: u = v | c1 and
A74: (u |-- MBCe) | k in P by A70;
set w = (Mx2Tran BnC) . u;
A75: (Mx2Tran BnC) . u = (Mx2Tran (M ~)) . (MT . ((Mx2Tran BnC) . u)) by A31, A33, A37, FUNCT_1:34;
dom (Mx2Tran BnC) = [#] (TOP-REAL c1) by FUNCT_2:def_1;
then A76: (Mx2Tran BnC) . u in BF by A20, FUNCT_1:def_3;
then A77: MT . ((Mx2Tran BnC) . u) in Affin A by A29, A31, FUNCT_1:def_6;
u |-- MBCe = ((Mx2Tran BnC) . u) |-- MBCeE by A41, A52, Th19
.= (MT . ((Mx2Tran BnC) . u)) |-- E by A25, A75, A77, Th19, A53, A45 ;
then A78: MT . ((Mx2Tran BnC) . u) in B by A12, A13, A74, A77;
consider w1 being Element of (TOP-REAL c1) such that
A79: (Mx2Tran BnC) . u = w1 ^ ((n -' c1) |-> 0) by A67, A76;
w1 = ((Mx2Tran BnC) . u) | (dom w1) by A79, FINSEQ_1:21
.= ((Mx2Tran BnC) . u) | (Seg (len w1)) by FINSEQ_1:def_3
.= ((Mx2Tran BnC) . u) | c1 by CARD_1:def_7
.= v | c1 by A73, MATRTOP1:38
.= v | (Seg (len v1)) by CARD_1:def_7
.= v | (dom v1) by FINSEQ_1:def_3
.= v1 by A72, FINSEQ_1:21 ;
hence x in MT " B by A31, A69, A79, A72, A78, FUNCT_1:def_7; ::_thesis: verum
end;
A80: len MBCe = len E by A4, A50, FINSEQ_4:62;
then len E in dom MBCe by A5, FINSEQ_3:25;
then MBCe . (len E) = (MBC ") . (0. (TOP-REAL n)) by A28, FUNCT_1:12
.= 0. (TOP-REAL c1) by A42, A18, FUNCT_1:34 ;
then A81: MBCe . (len MBCe) = 0* c1 by A80, EUCLID:70;
MT1 " B = BF /\ (MT " B) by FUNCT_1:70
.= MT " B by A13, A38, RELAT_1:143, XBOOLE_1:28 ;
then MT1 " B = { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } by A54, A68, XBOOLE_0:def_10;
then A82: ( PPP is open iff B is open ) by A34, A67, A36, Th8;
card R = c1 + 1 by A27, A49, CARD_1:5;
hence ( P is open iff B is open ) by A81, A82, A51, Lm7; ::_thesis: verum
end;
theorem Th25: :: RLAFFIN3:25
for n, k being Nat
for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is open iff An is open )
proof
let n, k be Nat; ::_thesis: for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is open iff An is open )
let Affn be affinely-independent Subset of (TOP-REAL n); ::_thesis: for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is open iff An is open )
let Ak be Subset of (TOP-REAL k); ::_thesis: for EN being Enumeration of Affn
for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is open iff An is open )
set A = Affn;
set AA = Affin Affn;
set TRn = TOP-REAL n;
let EN be Enumeration of Affn; ::_thesis: for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is open iff An is open )
let An be Subset of (TOP-REAL n); ::_thesis: ( k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } implies ( Ak is open iff An is open ) )
assume that
A1: k <= n and
A2: card Affn = n + 1 and
A3: An = { v where v is Element of (TOP-REAL n) : (v |-- EN) | k in Ak } ; ::_thesis: ( Ak is open iff An is open )
set E = EN;
A4: rng EN = Affn by Def1;
then A5: len EN = card Affn by FINSEQ_4:62;
then A6: len EN >= 1 by A2, NAT_1:14;
then A7: len EN in dom EN by FINSEQ_3:25;
then EN . (len EN) in Affn by A4, FUNCT_1:def_3;
then reconsider EL = EN . (len EN) as Element of (TOP-REAL n) ;
A8: card ((- EL) + Affn) = n + 1 by A2, RLAFFIN1:7;
set BB = { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ;
A9: { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } c= An
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } or x in An )
assume x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ; ::_thesis: x in An
then ex u being Element of (TOP-REAL n) st
( x = u & u in Affin Affn & (u |-- EN) | k in Ak ) ;
hence x in An by A3; ::_thesis: verum
end;
reconsider Ev = EN + ((card Affn) |-> (- EL)) as Enumeration of (- EL) + Affn by Th13;
set TB = { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } ;
set T = transl ((- EL),(TOP-REAL n));
A10: dim (TOP-REAL n) = n by Th4;
then A11: [#] (TOP-REAL n) = Affin Affn by A2, Th6;
An c= { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in An or x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } )
assume x in An ; ::_thesis: x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) }
then consider v being Element of (TOP-REAL n) such that
A12: ( x = v & (v |-- EN) | k in Ak ) by A3;
thus x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } by A11, A12; ::_thesis: verum
end;
then { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } = An by A9, XBOOLE_0:def_10;
then A13: (transl ((- EL),(TOP-REAL n))) .: An = { w where w is Element of (TOP-REAL n) : ( w in Affin ((- EL) + Affn) & (w |-- Ev) | k in Ak ) } by Lm6;
A14: (transl ((- EL),(TOP-REAL n))) .: An c= { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (transl ((- EL),(TOP-REAL n))) .: An or x in { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } )
assume x in (transl ((- EL),(TOP-REAL n))) .: An ; ::_thesis: x in { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak }
then ex w being Element of (TOP-REAL n) st
( x = w & w in Affin ((- EL) + Affn) & (w |-- Ev) | k in Ak ) by A13;
hence x in { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } ; ::_thesis: verum
end;
A15: card ((- EL) + Affn) = card Affn by RLAFFIN1:7;
then A16: Affin ((- EL) + Affn) = [#] (TOP-REAL n) by A2, A10, Th6;
{ w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } c= (transl ((- EL),(TOP-REAL n))) .: An
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } or x in (transl ((- EL),(TOP-REAL n))) .: An )
assume x in { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } ; ::_thesis: x in (transl ((- EL),(TOP-REAL n))) .: An
then consider w being Element of (TOP-REAL n) such that
A17: ( x = w & (w |-- Ev) | k in Ak ) ;
thus x in (transl ((- EL),(TOP-REAL n))) .: An by A16, A13, A17; ::_thesis: verum
end;
then A18: (transl ((- EL),(TOP-REAL n))) .: An = { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } by A14, XBOOLE_0:def_10;
len EN in Seg (card Affn) by A5, A6;
then A19: ((card Affn) |-> (- EL)) . (len EN) = - EL by FINSEQ_2:57;
A20: rng Ev = (- EL) + Affn by Def1;
then len Ev = card Affn by A15, FINSEQ_4:62;
then dom EN = dom Ev by A5, FINSEQ_3:29;
then Ev . (len EN) = EL + (- EL) by A7, A19, FVSUM_1:17
.= 0. (TOP-REAL n) by RLVECT_1:5
.= 0* n by EUCLID:70 ;
then A21: Ev . (len Ev) = 0* n by A5, A15, A20, FINSEQ_4:62;
not (- EL) + Affn is empty by A2, A15;
then ( (transl ((- EL),(TOP-REAL n))) .: An is open iff Ak is open ) by A1, A21, A8, A18, Lm7;
hence ( Ak is open iff An is open ) by TOPGRP_1:25; ::_thesis: verum
set TAA = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn);
A22: rng ((transl ((- EL),(TOP-REAL n))) | (Affin Affn)) = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) by RELAT_1:115;
dom (transl ((- EL),(TOP-REAL n))) = [#] (TOP-REAL n) by FUNCT_2:52;
then A23: dom ((transl ((- EL),(TOP-REAL n))) | (Affin Affn)) = Affin Affn by RELAT_1:62;
( [#] ((TOP-REAL n) | (Affin Affn)) = Affin Affn & [#] ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) ) by PRE_TOPC:def_5;
then reconsider TA = (transl ((- EL),(TOP-REAL n))) | (Affin Affn) as Function of ((TOP-REAL n) | (Affin Affn)),((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) by A23, A22, FUNCT_2:1;
reconsider TAB = TA .: An as Subset of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) ;
reconsider TAB = TA .: An as Subset of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) ;
end;
theorem Th26: :: RLAFFIN3:26
for n, k being Nat
for An being Subset of (TOP-REAL n)
for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is closed iff An is closed )
proof
let n, k be Nat; ::_thesis: for An being Subset of (TOP-REAL n)
for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is closed iff An is closed )
let An be Subset of (TOP-REAL n); ::_thesis: for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is closed iff An is closed )
let Affn be affinely-independent Subset of (TOP-REAL n); ::_thesis: for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is closed iff An is closed )
let Ak be Subset of (TOP-REAL k); ::_thesis: for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is closed iff An is closed )
set TRn = TOP-REAL n;
set TRk = TOP-REAL k;
set A = Affn;
let E be Enumeration of Affn; ::_thesis: ( k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in Ak } implies ( Ak is closed iff An is closed ) )
assume that
A1: ( k <= n & card Affn = n + 1 ) and
A2: An = { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak } ; ::_thesis: ( Ak is closed iff An is closed )
set B1 = { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } ;
A3: k < card Affn by A1, NAT_1:13;
A4: An ` c= { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in An ` or x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } )
assume A5: x in An ` ; ::_thesis: x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` }
then reconsider f = x as Element of (TOP-REAL n) ;
set fE = f |-- E;
len (f |-- E) = card Affn by Th16;
then len ((f |-- E) | k) = k by A3, FINSEQ_1:59;
then A6: (f |-- E) | k is Element of (TOP-REAL k) by TOPREAL3:46;
assume not x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } ; ::_thesis: contradiction
then not (f |-- E) | k in Ak ` ;
then (f |-- E) | k in Ak by A6, XBOOLE_0:def_5;
then f in An by A2;
hence contradiction by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
{ v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } c= An `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } or x in An ` )
assume x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } ; ::_thesis: x in An `
then consider v being Element of (TOP-REAL n) such that
A7: x = v and
A8: (v |-- E) | k in Ak ` ;
assume not x in An ` ; ::_thesis: contradiction
then v in An by A7, XBOOLE_0:def_5;
then ex w being Element of (TOP-REAL n) st
( v = w & (w |-- E) | k in Ak ) by A2;
hence contradiction by A8, XBOOLE_0:def_5; ::_thesis: verum
end;
then An ` = { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } by A4, XBOOLE_0:def_10;
then ( Ak ` is open iff An ` is open ) by A1, Th25;
hence ( Ak is closed iff An is closed ) by TOPS_1:3; ::_thesis: verum
end;
registration
let n be Nat;
cluster Affine -> closed for Element of bool the carrier of (TOP-REAL n);
coherence
for b1 being Subset of (TOP-REAL n) st b1 is Affine holds
b1 is closed
proof
set TRn = TOP-REAL n;
let A be Subset of (TOP-REAL n); ::_thesis: ( A is Affine implies A is closed )
assume A is Affine ; ::_thesis: A is closed
then A1: Affin A = A by RLAFFIN1:50;
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: A is closed
hence A is closed ; ::_thesis: verum
end;
supposeA2: not A is empty ; ::_thesis: A is closed
{} (TOP-REAL n) c= A by XBOOLE_1:2;
then consider Ia being affinely-independent Subset of (TOP-REAL n) such that
{} c= Ia and
Ia c= A and
A3: Affin Ia = A by A1, RLAFFIN1:60;
consider IA being affinely-independent Subset of (TOP-REAL n) such that
A4: Ia c= IA and
IA c= [#] (TOP-REAL n) and
A5: Affin IA = Affin ([#] (TOP-REAL n)) by RLAFFIN1:60;
reconsider IB = IA \ Ia as affinely-independent Subset of (TOP-REAL n) by RLAFFIN1:43, XBOOLE_1:36;
set cIB = card IB;
A6: dim (TOP-REAL n) = n by Th4;
then A7: card IB <= n + 1 by Th5;
[#] (TOP-REAL n) is Affine by RUSUB_4:22;
then A8: Affin ([#] (TOP-REAL n)) = [#] (TOP-REAL n) by RLAFFIN1:50;
then A9: card IA = n + 1 by A5, A6, Th6;
not Ia is empty by A2, A3;
then IA meets Ia by A4, XBOOLE_1:67;
then IA <> IB by XBOOLE_1:83;
then card IB <> n + 1 by A9, CARD_FIN:1, XBOOLE_1:36;
then A10: card IB < n + 1 by A7, XXREAL_0:1;
then A11: card IB < card IA by A5, A8, A6, Th6;
set TRc = TOP-REAL (card IB);
A12: 0* (card IB) = 0. (TOP-REAL (card IB)) by EUCLID:66;
then (card IB) |-> 0 is Element of (TOP-REAL (card IB)) by EUCLID:def_4;
then reconsider P = {((card IB) |-> 0)} as Subset of (TOP-REAL (card IB)) by ZFMISC_1:31;
0* (card IB) = (card IB) |-> 0 by EUCLID:def_4;
then A13: P is closed by A12, PCOMPS_1:7;
set P1 = the Enumeration of Ia;
A14: rng the Enumeration of Ia = Ia by Def1;
set P2 = the Enumeration of IB;
set P12 = the Enumeration of IB ^ the Enumeration of Ia;
A15: rng the Enumeration of IB = IB by Def1;
Ia misses IB by XBOOLE_1:79;
then A16: the Enumeration of IB ^ the Enumeration of Ia is one-to-one by A14, A15, FINSEQ_3:91;
Ia \/ IB = Ia \/ IA by XBOOLE_1:39
.= IA by A4, XBOOLE_1:12 ;
then rng ( the Enumeration of IB ^ the Enumeration of Ia) = IA by A14, A15, FINSEQ_1:31;
then reconsider P12 = the Enumeration of IB ^ the Enumeration of Ia as Enumeration of IA by A16, Def1;
len the Enumeration of IB = card IB by A15, FINSEQ_4:62;
then A17: P12 .: (Seg (card IB)) = P12 .: (dom the Enumeration of IB) by FINSEQ_1:def_3
.= rng (P12 | (dom the Enumeration of IB)) by RELAT_1:115
.= rng the Enumeration of IB by FINSEQ_1:21
.= IB by Def1 ;
set B = { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } ;
A18: IA \ IB = IA /\ Ia by XBOOLE_1:48
.= Ia by A4, XBOOLE_1:28 ;
A19: Affin A c= { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Affin A or x in { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } )
assume A20: x in Affin A ; ::_thesis: x in { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P }
then reconsider v = x as Element of (TOP-REAL n) ;
set vP = v |-- P12;
A21: v |-- P12 = ((v |-- P12) | (card IB)) ^ ((v |-- P12) /^ (card IB)) by RFINSEQ:8;
v |-- P12 = ((card IB) |-> 0) ^ ((v |-- P12) /^ (card IB)) by A1, A3, A5, A8, A18, A17, A11, A20, Th22;
then (v |-- P12) | (card IB) = (card IB) |-> 0 by A21, FINSEQ_1:33;
then (v |-- P12) | (card IB) in P by TARSKI:def_1;
hence x in { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } ; ::_thesis: verum
end;
A22: card IB <= n by A10, NAT_1:13;
{ v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } c= Affin A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } or x in Affin A )
assume x in { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } ; ::_thesis: x in Affin A
then consider v being Element of (TOP-REAL n) such that
A23: x = v and
A24: (v |-- P12) | (card IB) in P ;
set vP = v |-- P12;
(v |-- P12) | (card IB) = (card IB) |-> 0 by A24, TARSKI:def_1;
then v |-- P12 = ((card IB) |-> 0) ^ ((v |-- P12) /^ (card IB)) by RFINSEQ:8;
hence x in Affin A by A1, A3, A5, A8, A18, A17, A11, A23, Th22; ::_thesis: verum
end;
then { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } = Affin A by A19, XBOOLE_0:def_10;
hence A is closed by A1, A9, A22, A13, Th26; ::_thesis: verum
end;
end;
end;
end;
theorem Th27: :: RLAFFIN3:27
for n, k being Nat
for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is open iff B is open )
proof
let n, k be Nat; ::_thesis: for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is open iff B is open )
let Affn be affinely-independent Subset of (TOP-REAL n); ::_thesis: for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is open iff B is open )
let Ak be Subset of (TOP-REAL k); ::_thesis: for EN being Enumeration of Affn
for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is open iff B is open )
let EN be Enumeration of Affn; ::_thesis: for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is open iff B is open )
set E = EN;
set Tn = TOP-REAL n;
set Tk = TOP-REAL k;
set A = Affn;
set cA = (card Affn) -' 1;
set TcA = TOP-REAL ((card Affn) -' 1);
set AA = Affin Affn;
let B be Subset of ((TOP-REAL n) | (Affin Affn)); ::_thesis: ( k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } implies ( Ak is open iff B is open ) )
assume that
A1: k < card Affn and
A2: B = { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- EN) | k in Ak } ; ::_thesis: ( Ak is open iff B is open )
set BB = { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ;
A3: [#] ((TOP-REAL n) | (Affin Affn)) = Affin Affn by PRE_TOPC:def_5;
A4: { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } or x in B )
assume x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ; ::_thesis: x in B
then consider u being Element of (TOP-REAL n) such that
A5: ( x = u & u in Affin Affn & (u |-- EN) | k in Ak ) ;
thus x in B by A2, A3, A5; ::_thesis: verum
end;
A6: not Affn is empty by A1;
B c= { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } )
assume x in B ; ::_thesis: x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) }
then consider u being Element of ((TOP-REAL n) | (Affin Affn)) such that
A7: ( x = u & (u |-- EN) | k in Ak ) by A2;
not Affin Affn is empty by A6;
then u in Affin Affn by A3;
hence x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } by A7; ::_thesis: verum
end;
then A8: { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } = B by A4, XBOOLE_0:def_10;
A9: rng EN = Affn by Def1;
then A10: len EN = card Affn by FINSEQ_4:62;
then A11: len EN >= 1 by A1, NAT_1:14;
then A12: len EN in dom EN by FINSEQ_3:25;
then EN . (len EN) in Affn by A9, FUNCT_1:def_3;
then reconsider EL = EN . (len EN) as Element of (TOP-REAL n) ;
len EN in Seg (card Affn) by A10, A11;
then A13: ((card Affn) |-> (- EL)) . (len EN) = - EL by FINSEQ_2:57;
A14: k < card ((- EL) + Affn) by A1, RLAFFIN1:7;
set T = transl ((- EL),(TOP-REAL n));
set TAA = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn);
A15: [#] ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) by PRE_TOPC:def_5;
A16: rng ((transl ((- EL),(TOP-REAL n))) | (Affin Affn)) = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) by RELAT_1:115;
A17: dom (transl ((- EL),(TOP-REAL n))) = [#] (TOP-REAL n) by FUNCT_2:52;
then dom ((transl ((- EL),(TOP-REAL n))) | (Affin Affn)) = Affin Affn by RELAT_1:62;
then reconsider TA = (transl ((- EL),(TOP-REAL n))) | (Affin Affn) as Function of ((TOP-REAL n) | (Affin Affn)),((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) by A3, A15, A16, FUNCT_2:1;
reconsider TAB = TA .: B as Subset of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) ;
A18: TA is being_homeomorphism by METRIZTS:2;
reconsider Ev = EN + ((card Affn) |-> (- EL)) as Enumeration of (- EL) + Affn by Th13;
A19: card ((- EL) + Affn) = card Affn by RLAFFIN1:7;
then A20: not (- EL) + Affn is empty by A1;
A21: rng Ev = (- EL) + Affn by Def1;
then len Ev = card Affn by A19, FINSEQ_4:62;
then dom EN = dom Ev by A10, FINSEQ_3:29;
then Ev . (len EN) = EL + (- EL) by A12, A13, FVSUM_1:17
.= 0. (TOP-REAL n) by RLVECT_1:5
.= 0* n by EUCLID:70 ;
then A22: Ev . (len Ev) = 0* n by A10, A19, A21, FINSEQ_4:62;
set Tab = { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } ;
A23: (- EL) + (Affin Affn) = Affin ((- EL) + Affn) by RLAFFIN1:53;
then A24: (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) = Affin ((- EL) + Affn) by RLTOPSP1:33;
TA .: B = (transl ((- EL),(TOP-REAL n))) .: B by A3, RELAT_1:129;
then A25: TAB = { w where w is Element of (TOP-REAL n) : ( w in Affin ((- EL) + Affn) & (w |-- Ev) | k in Ak ) } by A8, Lm6;
A26: TAB c= { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in TAB or x in { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } )
assume x in TAB ; ::_thesis: x in { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak }
then consider w being Element of (TOP-REAL n) such that
A27: x = w and
A28: w in Affin ((- EL) + Affn) and
A29: (w |-- Ev) | k in Ak by A25;
w in (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) by A23, A28, RLTOPSP1:33;
hence x in { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } by A15, A27, A29; ::_thesis: verum
end;
A30: not (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) is empty by A6, A17, RELAT_1:119;
{ w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } c= TAB
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } or x in TAB )
assume x in { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } ; ::_thesis: x in TAB
then consider w being Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) such that
A31: ( x = w & (w |-- Ev) | k in Ak ) ;
w in (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) by A15, A30;
hence x in TAB by A24, A25, A31; ::_thesis: verum
end;
then TAB = { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } by A26, XBOOLE_0:def_10;
then ( TAB is open iff Ak is open ) by A24, A22, A14, A20, Lm8;
hence ( Ak is open iff B is open ) by A6, A18, A30, TOPGRP_1:25; ::_thesis: verum
end;
theorem Th28: :: RLAFFIN3:28
for n, k being Nat
for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is closed iff B is closed )
proof
let n, k be Nat; ::_thesis: for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is closed iff B is closed )
let Affn be affinely-independent Subset of (TOP-REAL n); ::_thesis: for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is closed iff B is closed )
let Ak be Subset of (TOP-REAL k); ::_thesis: for EN being Enumeration of Affn
for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is closed iff B is closed )
let E be Enumeration of Affn; ::_thesis: for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- E) | k in Ak } holds
( Ak is closed iff B is closed )
set TRn = TOP-REAL n;
set A = Affn;
set AA = Affin Affn;
let B be Subset of ((TOP-REAL n) | (Affin Affn)); ::_thesis: ( k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- E) | k in Ak } implies ( Ak is closed iff B is closed ) )
assume that
A1: k < card Affn and
A2: B = { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak } ; ::_thesis: ( Ak is closed iff B is closed )
set B1 = { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } ;
A3: B ` c= { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B ` or x in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } )
assume A4: x in B ` ; ::_thesis: x in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` }
then reconsider v = x as Element of ((TOP-REAL n) | (Affin Affn)) ;
set vE = v |-- E;
len (v |-- E) = card Affn by Th16;
then len ((v |-- E) | k) = k by A1, FINSEQ_1:59;
then A5: (v |-- E) | k in [#] (TOP-REAL k) by TOPREAL3:46;
not v in B by A4, XBOOLE_0:def_5;
then not (v |-- E) | k in Ak by A2;
then (v |-- E) | k in Ak ` by A5, XBOOLE_0:def_5;
hence x in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } ; ::_thesis: verum
end;
A6: not Affn is empty by A1;
{ v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } c= B `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } or x in B ` )
assume x in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } ; ::_thesis: x in B `
then consider v being Element of ((TOP-REAL n) | (Affin Affn)) such that
A7: x = v and
A8: (v |-- E) | k in Ak ` ;
assume not x in B ` ; ::_thesis: contradiction
then v in B by A6, A7, XBOOLE_0:def_5;
then ex w being Element of ((TOP-REAL n) | (Affin Affn)) st
( w = v & (w |-- E) | k in Ak ) by A2;
hence contradiction by A8, XBOOLE_0:def_5; ::_thesis: verum
set vE = v |-- E;
end;
then { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } = B ` by A3, XBOOLE_0:def_10;
then ( Ak ` is open iff B ` is open ) by A1, Th27;
hence ( Ak is closed iff B is closed ) by TOPS_1:3; ::_thesis: verum
end;
registration
let n be Nat;
let p, q be Point of (TOP-REAL n);
cluster halfline (p,q) -> closed ;
coherence
halfline (p,q) is closed
proof
set pq = {p,q};
A1: n in NAT by ORDINAL1:def_12;
percases ( p = q or p <> q ) ;
supposeA2: p = q ; ::_thesis: halfline (p,q) is closed
{p} is closed by URYSOHN1:19;
hence halfline (p,q) is closed by A1, A2, TOPREAL9:29; ::_thesis: verum
end;
supposeA3: p <> q ; ::_thesis: halfline (p,q) is closed
A4: rng <*p,q*> = {p,q} by FINSEQ_2:127;
<*p,q*> is one-to-one by A3, FINSEQ_3:94;
then reconsider E = <*p,q*> as Enumeration of {p,q} by A4, Def1;
set Apq = Affin {p,q};
set TRn = TOP-REAL n;
set TR1 = TOP-REAL 1;
set L = ].-infty,1.];
A5: E . 1 = p by FINSEQ_1:44;
reconsider L = ].-infty,1.] as Subset of R^1 by TOPMETR:17;
consider h being Function of (TOP-REAL 1),R^1 such that
A6: for p being Point of (TOP-REAL 1) holds h . p = p /. 1 by JORDAN2B:1;
set B = { w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } ;
{ w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } c= [#] ((TOP-REAL n) | (Affin {p,q}))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } or x in [#] ((TOP-REAL n) | (Affin {p,q})) )
assume x in { w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } ; ::_thesis: x in [#] ((TOP-REAL n) | (Affin {p,q}))
then ex w being Element of ((TOP-REAL n) | (Affin {p,q})) st
( x = w & (w |-- E) | 1 in h " L ) ;
hence x in [#] ((TOP-REAL n) | (Affin {p,q})) ; ::_thesis: verum
end;
then reconsider B = { w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } as Subset of ((TOP-REAL n) | (Affin {p,q})) ;
A7: [#] ((TOP-REAL n) | (Affin {p,q})) = Affin {p,q} by PRE_TOPC:def_5;
A8: card {p,q} = 2 by A3, CARD_2:57;
A9: h is being_homeomorphism by A6, JORDAN2B:28;
then A10: dom h = [#] (TOP-REAL 1) by TOPGRP_1:24;
A11: halfline (p,q) c= B
proof
Carrier (q |-- {q}) c= {q} by RLVECT_2:def_6;
then not p in Carrier (q |-- {q}) by A3, TARSKI:def_1;
then A12: (q |-- {q}) . p = 0 by RLVECT_2:19;
{q} is Affine by RUSUB_4:23;
then A13: Affin {q} = {q} by RLAFFIN1:50;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in halfline (p,q) or x in B )
set W = x |-- {p,q};
set wE = x |-- E;
A14: p in {p,q} by TARSKI:def_2;
assume x in halfline (p,q) ; ::_thesis: x in B
then consider a being real number such that
A15: x = ((1 - a) * p) + (a * q) and
A16: 0 <= a by A1, TOPREAL9:26;
reconsider a = a as Real by XREAL_0:def_1;
( q in {q} & {q} c= {p,q} ) by TARSKI:def_1, ZFMISC_1:36;
then 0 = (q |-- {p,q}) . p by A12, A13, RLAFFIN1:77;
then A17: (a * (q |-- {p,q})) . p = a * 0 by RLVECT_2:def_11
.= 0 ;
{p,q} c= conv {p,q} by CONVEX1:41;
then A18: (p |-- {p,q}) . p = 1 by A14, RLAFFIN1:72;
A19: ( q in {p,q} & {p,q} c= Affin {p,q} ) by RLAFFIN1:49, TARSKI:def_2;
then x |-- {p,q} = ((1 - a) * (p |-- {p,q})) + (a * (q |-- {p,q})) by A15, A14, RLAFFIN1:70;
then (x |-- {p,q}) . p = (((1 - a) * (p |-- {p,q})) . p) + ((a * (q |-- {p,q})) . p) by RLVECT_2:def_10
.= ((1 - a) * ((p |-- {p,q}) . p)) + 0 by A17, RLVECT_2:def_11
.= 1 - a by A18 ;
then (x |-- {p,q}) . p <= 1 - 0 by A16, XREAL_1:10;
then A20: (x |-- {p,q}) . p in L by XXREAL_1:234;
(1 - a) + a = 1 ;
then reconsider w = x as Element of ((TOP-REAL n) | (Affin {p,q})) by A7, A15, A14, A19, RLAFFIN1:78;
len (x |-- E) = 2 by A8, Th16;
then A21: len ((x |-- E) | 1) = 1 by FINSEQ_1:59;
then reconsider wE1 = (x |-- E) | 1 as Point of (TOP-REAL 1) by TOPREAL3:46;
A22: 1 in dom wE1 by A21, FINSEQ_3:25;
then A23: ( wE1 /. 1 = wE1 . 1 & wE1 . 1 = (x |-- E) . 1 ) by FUNCT_1:47, PARTFUN1:def_6;
A24: 1 in dom (x |-- E) by A22, RELAT_1:57;
h . wE1 = wE1 /. 1 by A6;
then h . wE1 in L by A5, A20, A23, A24, FUNCT_1:12;
then wE1 in h " L by A10, FUNCT_1:def_7;
then w in B ;
hence x in B ; ::_thesis: verum
end;
L is closed by BORSUK_5:41;
then h " L is closed by A9, TOPGRP_1:24;
then A25: B is closed by A8, Th28;
B c= halfline (p,q)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in halfline (p,q) )
assume x in B ; ::_thesis: x in halfline (p,q)
then consider w being Element of ((TOP-REAL n) | (Affin {p,q})) such that
A26: x = w and
A27: (w |-- E) | 1 in h " L ;
set W = w |-- {p,q};
set wE = w |-- E;
reconsider wE1 = (w |-- E) | 1 as Point of (TOP-REAL 1) by A27;
A28: h . wE1 = wE1 /. 1 by A6;
len wE1 = 1 by CARD_1:def_7;
then A29: 1 in dom wE1 by FINSEQ_3:25;
then A30: ( wE1 /. 1 = wE1 . 1 & wE1 . 1 = (w |-- E) . 1 ) by FUNCT_1:47, PARTFUN1:def_6;
A31: 1 in dom (w |-- E) by A29, RELAT_1:57;
h . ((w |-- E) | 1) in L by A27, FUNCT_1:def_7;
then (w |-- {p,q}) . p in L by A5, A28, A30, A31, FUNCT_1:12;
then (w |-- {p,q}) . p <= 1 by XXREAL_1:234;
then A32: ((w |-- {p,q}) . p) - ((w |-- {p,q}) . p) <= 1 - ((w |-- {p,q}) . p) by XREAL_1:9;
A33: sum (w |-- {p,q}) = 1 by A7, RLAFFIN1:def_7;
Carrier (w |-- {p,q}) c= {p,q} by RLVECT_2:def_6;
then A34: sum (w |-- {p,q}) = ((w |-- {p,q}) . p) + ((w |-- {p,q}) . q) by A3, RLAFFIN1:33;
Sum (w |-- {p,q}) = w by A7, RLAFFIN1:def_7;
then w = ((1 - ((w |-- {p,q}) . q)) * p) + (((w |-- {p,q}) . q) * q) by A3, A34, A33, RLVECT_2:33;
hence x in halfline (p,q) by A1, A26, A34, A33, A32, TOPREAL9:26; ::_thesis: verum
end;
then halfline (p,q) = B by A11, XBOOLE_0:def_10;
hence halfline (p,q) is closed by A7, A25, TSEP_1:8; ::_thesis: verum
end;
end;
end;
end;
begin
definition
let V be RealLinearSpace;
let A be Subset of V;
let x be set ;
func |-- (A,x) -> Function of V,R^1 means :Def3: :: RLAFFIN3:def 3
for v being VECTOR of V holds it . v = (v |-- A) . x;
existence
ex b1 being Function of V,R^1 st
for v being VECTOR of V holds b1 . v = (v |-- A) . x
proof
deffunc H1( set ) -> set = ($1 |-- A) . x;
A1: for v being set st v in the carrier of V holds
H1(v) in the carrier of R^1
proof
let v be set ; ::_thesis: ( v in the carrier of V implies H1(v) in the carrier of R^1 )
assume v in the carrier of V ; ::_thesis: H1(v) in the carrier of R^1
set vA = v |-- A;
percases ( x in dom (v |-- A) or not x in dom (v |-- A) ) ;
suppose x in dom (v |-- A) ; ::_thesis: H1(v) in the carrier of R^1
then (v |-- A) . x in rng (v |-- A) by FUNCT_1:def_3;
hence H1(v) in the carrier of R^1 by TOPMETR:17; ::_thesis: verum
end;
suppose not x in dom (v |-- A) ; ::_thesis: H1(v) in the carrier of R^1
then (v |-- A) . x = 0 by FUNCT_1:def_2;
hence H1(v) in the carrier of R^1 by Lm5, TOPMETR:17; ::_thesis: verum
end;
end;
end;
consider f being Function of V,R^1 such that
A2: for v being set st v in the carrier of V holds
f . v = H1(v) from FUNCT_2:sch_2(A1);
take f ; ::_thesis: for v being VECTOR of V holds f . v = (v |-- A) . x
let v be Element of V; ::_thesis: f . v = (v |-- A) . x
thus f . v = (v |-- A) . x by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of V,R^1 st ( for v being VECTOR of V holds b1 . v = (v |-- A) . x ) & ( for v being VECTOR of V holds b2 . v = (v |-- A) . x ) holds
b1 = b2
proof
let F1, F2 be Function of V,R^1; ::_thesis: ( ( for v being VECTOR of V holds F1 . v = (v |-- A) . x ) & ( for v being VECTOR of V holds F2 . v = (v |-- A) . x ) implies F1 = F2 )
assume that
A3: for v being Element of V holds F1 . v = (v |-- A) . x and
A4: for v being Element of V holds F2 . v = (v |-- A) . x ; ::_thesis: F1 = F2
now__::_thesis:_for_v_being_set_st_v_in_the_carrier_of_V_holds_
F1_._v_=_F2_._v
let v be set ; ::_thesis: ( v in the carrier of V implies F1 . v = F2 . v )
assume A5: v in the carrier of V ; ::_thesis: F1 . v = F2 . v
hence F1 . v = (v |-- A) . x by A3
.= F2 . v by A4, A5 ;
::_thesis: verum
end;
hence F1 = F2 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines |-- RLAFFIN3:def_3_:_
for V being RealLinearSpace
for A being Subset of V
for x being set
for b4 being Function of V,R^1 holds
( b4 = |-- (A,x) iff for v being VECTOR of V holds b4 . v = (v |-- A) . x );
theorem Th29: :: RLAFFIN3:29
for x being set
for V being RealLinearSpace
for A being Subset of V st not x in A holds
|-- (A,x) = ([#] V) --> 0
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for A being Subset of V st not x in A holds
|-- (A,x) = ([#] V) --> 0
let V be RealLinearSpace; ::_thesis: for A being Subset of V st not x in A holds
|-- (A,x) = ([#] V) --> 0
let A be Subset of V; ::_thesis: ( not x in A implies |-- (A,x) = ([#] V) --> 0 )
set Ax = |-- (A,x);
assume A1: not x in A ; ::_thesis: |-- (A,x) = ([#] V) --> 0
A2: now__::_thesis:_for_y_being_set_st_y_in_dom_(|--_(A,x))_holds_
(|--_(A,x))_._y_=_0
let y be set ; ::_thesis: ( y in dom (|-- (A,x)) implies (|-- (A,x)) . b1 = 0 )
assume y in dom (|-- (A,x)) ; ::_thesis: (|-- (A,x)) . b1 = 0
then A3: (|-- (A,x)) . y = (y |-- A) . x by Def3;
Carrier (y |-- A) c= A by RLVECT_2:def_6;
then A4: not x in Carrier (y |-- A) by A1;
percases ( x in [#] V or not x in [#] V ) ;
suppose x in [#] V ; ::_thesis: (|-- (A,x)) . b1 = 0
hence (|-- (A,x)) . y = 0 by A3, A4, RLVECT_2:19; ::_thesis: verum
end;
suppose not x in [#] V ; ::_thesis: (|-- (A,x)) . b1 = 0
then not x in dom (y |-- A) ;
hence (|-- (A,x)) . y = 0 by A3, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
dom (|-- (A,x)) = [#] V by FUNCT_2:def_1;
hence |-- (A,x) = ([#] V) --> 0 by A2, FUNCOP_1:11; ::_thesis: verum
end;
theorem :: RLAFFIN3:30
for x being set
for V being RealLinearSpace
for A being affinely-independent Subset of V st |-- (A,x) = ([#] V) --> 0 holds
not x in A
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for A being affinely-independent Subset of V st |-- (A,x) = ([#] V) --> 0 holds
not x in A
let V be RealLinearSpace; ::_thesis: for A being affinely-independent Subset of V st |-- (A,x) = ([#] V) --> 0 holds
not x in A
let A be affinely-independent Subset of V; ::_thesis: ( |-- (A,x) = ([#] V) --> 0 implies not x in A )
set Ax = |-- (A,x);
assume A1: |-- (A,x) = ([#] V) --> 0 ; ::_thesis: not x in A
A2: A c= conv A by RLAFFIN1:2;
assume A3: x in A ; ::_thesis: contradiction
then 0 = (|-- (A,x)) . x by A1, FUNCOP_1:7
.= (x |-- A) . x by A3, Def3
.= 1 by A3, A2, RLAFFIN1:72 ;
hence contradiction ; ::_thesis: verum
end;
theorem Th31: :: RLAFFIN3:31
for x being set
for n being Nat
for Affn being affinely-independent Subset of (TOP-REAL n) holds (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1
proof
let x be set ; ::_thesis: for n being Nat
for Affn being affinely-independent Subset of (TOP-REAL n) holds (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1
let n be Nat; ::_thesis: for Affn being affinely-independent Subset of (TOP-REAL n) holds (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1
let Affn be affinely-independent Subset of (TOP-REAL n); ::_thesis: (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1
reconsider Z = 0 as Element of R^1 by Lm5, TOPMETR:17;
set TRn = TOP-REAL n;
set AA = Affin Affn;
set Ax = |-- (Affn,x);
set AxA = (|-- (Affn,x)) | (Affin Affn);
A1: ([#] (TOP-REAL n)) /\ (Affin Affn) = Affin Affn by XBOOLE_1:28;
A2: Affin Affn = [#] ((TOP-REAL n) | (Affin Affn)) by PRE_TOPC:def_5;
then reconsider AxA = (|-- (Affn,x)) | (Affin Affn) as Function of ((TOP-REAL n) | (Affin Affn)),R^1 by FUNCT_2:32;
A3: dom AxA = Affin Affn by A2, FUNCT_2:def_1;
percases ( not x in Affn or ( x in Affn & card Affn = 1 ) or ( x in Affn & card Affn <> 1 ) ) ;
suppose not x in Affn ; ::_thesis: (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1
then |-- (Affn,x) = ([#] (TOP-REAL n)) --> Z by Th29;
then AxA = ((TOP-REAL n) | (Affin Affn)) --> Z by A2, A1, FUNCOP_1:12;
hence (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1 ; ::_thesis: verum
end;
supposeA4: ( x in Affn & card Affn = 1 ) ; ::_thesis: (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1
A5: rng AxA c= the carrier of R^1 by RELAT_1:def_19;
consider y being set such that
A6: Affn = {y} by A4, CARD_2:42;
A7: x = y by A4, A6, TARSKI:def_1;
then Affn is Affine by A4, A6, RUSUB_4:23;
then A8: Affin Affn = Affn by RLAFFIN1:50;
then AxA . x in rng AxA by A3, A4, FUNCT_1:def_3;
then reconsider b = AxA . x as Element of R^1 by A5;
rng AxA = {(AxA . x)} by A3, A6, A7, A8, FUNCT_1:4;
then AxA = ((TOP-REAL n) | (Affin Affn)) --> b by A2, A3, FUNCOP_1:9;
hence (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1 ; ::_thesis: verum
end;
supposeA9: ( x in Affn & card Affn <> 1 ) ; ::_thesis: (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1
set P2 = the Enumeration of Affn \ {x};
set P1 = <*x*>;
set P12 = <*x*> ^ the Enumeration of Affn \ {x};
A10: ( rng <*x*> = {x} & rng the Enumeration of Affn \ {x} = Affn \ {x} ) by Def1, FINSEQ_1:39;
( <*x*> is one-to-one & {x} misses Affn \ {x} ) by FINSEQ_3:93, XBOOLE_1:79;
then A11: <*x*> ^ the Enumeration of Affn \ {x} is one-to-one by A10, FINSEQ_3:91;
rng (<*x*> ^ the Enumeration of Affn \ {x}) = (rng <*x*>) \/ (rng the Enumeration of Affn \ {x}) by FINSEQ_1:31;
then rng (<*x*> ^ the Enumeration of Affn \ {x}) = Affn by A9, A10, ZFMISC_1:116;
then reconsider P12 = <*x*> ^ the Enumeration of Affn \ {x} as Enumeration of Affn by A11, Def1;
set TR1 = TOP-REAL 1;
consider Pro being Function of (TOP-REAL 1),R^1 such that
A12: for p being Element of (TOP-REAL 1) holds Pro . p = p /. 1 by JORDAN2B:1;
A13: Pro is being_homeomorphism by A12, JORDAN2B:28;
card Affn >= 1 by A9, NAT_1:14;
then A14: card Affn > 1 by A9, XXREAL_0:1;
now__::_thesis:_for_P_being_Subset_of_R^1_st_P_is_closed_holds_
AxA_"_P_is_closed
A15: dom <*x*> c= dom P12 by FINSEQ_1:26;
let P be Subset of R^1; ::_thesis: ( P is closed implies AxA " P is closed )
set B = { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } ;
A16: 1 in {1} by FINSEQ_1:2;
assume P is closed ; ::_thesis: AxA " P is closed
then A17: Pro " P is closed by A13, TOPGRP_1:24;
A18: dom <*x*> = Seg 1 by FINSEQ_1:38;
then A19: P12 . 1 = <*x*> . 1 by A16, FINSEQ_1:2, FINSEQ_1:def_7
.= x by FINSEQ_1:40 ;
A20: not Affin Affn is empty by A9;
A21: { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } c= AxA " P
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } or y in AxA " P )
assume y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } ; ::_thesis: y in AxA " P
then consider v being Element of ((TOP-REAL n) | (Affin Affn)) such that
A22: y = v and
A23: (v |-- P12) | 1 in Pro " P ;
set vP = v |-- P12;
reconsider vP1 = (v |-- P12) | 1 as Element of (TOP-REAL 1) by A23;
A24: v in Affin Affn by A2, A20;
len vP1 = 1 by CARD_1:def_7;
then dom vP1 = Seg 1 by FINSEQ_1:def_3;
then A25: 1 in dom vP1 ;
then A26: 1 in dom (v |-- P12) by RELAT_1:57;
Pro . vP1 = vP1 /. 1 by A12
.= vP1 . 1 by A25, PARTFUN1:def_6
.= (v |-- P12) . 1 by A25, FUNCT_1:47
.= (v |-- Affn) . x by A19, A26, FUNCT_1:12
.= (|-- (Affn,x)) . v by A24, Def3 ;
then (|-- (Affn,x)) . v in P by A23, FUNCT_1:def_7;
then AxA . v in P by A2, A3, A9, FUNCT_1:47;
hence y in AxA " P by A2, A3, A9, A22, FUNCT_1:def_7; ::_thesis: verum
end;
A27: dom Pro = [#] (TOP-REAL 1) by A13, TOPGRP_1:24;
AxA " P c= { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in AxA " P or y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } )
set yP = y |-- P12;
len (y |-- P12) = card Affn by Th16;
then A28: len ((y |-- P12) | 1) = 1 by A9, FINSEQ_1:59, NAT_1:14;
then reconsider yP1 = (y |-- P12) | 1 as Element of (TOP-REAL 1) by TOPREAL3:46;
A29: dom yP1 = Seg 1 by A28, FINSEQ_1:def_3;
assume A30: y in AxA " P ; ::_thesis: y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P }
then A31: y in dom AxA by FUNCT_1:def_7;
then AxA . y = (|-- (Affn,x)) . y by FUNCT_1:47
.= (y |-- Affn) . (P12 . 1) by A19, A3, A31, Def3
.= (y |-- P12) . 1 by A18, A16, A15, FINSEQ_1:2, FUNCT_1:13
.= yP1 . 1 by A16, A29, FINSEQ_1:2, FUNCT_1:47
.= yP1 /. 1 by A16, A29, FINSEQ_1:2, PARTFUN1:def_6
.= Pro . yP1 by A12 ;
then Pro . yP1 in P by A30, FUNCT_1:def_7;
then yP1 in Pro " P by A27, FUNCT_1:def_7;
hence y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } by A30; ::_thesis: verum
end;
then { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } = AxA " P by A21, XBOOLE_0:def_10;
hence AxA " P is closed by A14, A17, Th28; ::_thesis: verum
end;
hence (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1 by PRE_TOPC:def_6; ::_thesis: verum
end;
end;
end;
theorem Th32: :: RLAFFIN3:32
for x being set
for n being Nat
for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds
|-- (Affn,x) is continuous
proof
let x be set ; ::_thesis: for n being Nat
for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds
|-- (Affn,x) is continuous
let n be Nat; ::_thesis: for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds
|-- (Affn,x) is continuous
let Affn be affinely-independent Subset of (TOP-REAL n); ::_thesis: ( card Affn = n + 1 implies |-- (Affn,x) is continuous )
set TRn = TOP-REAL n;
set AA = Affin Affn;
set Ax = |-- (Affn,x);
reconsider AxA = (|-- (Affn,x)) | (Affin Affn) as continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1 by Th31;
assume A1: card Affn = n + 1 ; ::_thesis: |-- (Affn,x) is continuous
dim (TOP-REAL n) = n by Th4;
then A2: Affin Affn = [#] (TOP-REAL n) by A1, Th6;
then A3: (TOP-REAL n) | (Affin Affn) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;
A4: dom (|-- (Affn,x)) = Affin Affn by A2, FUNCT_2:def_1;
now__::_thesis:_for_P_being_Subset_of_R^1_st_P_is_closed_holds_
(|--_(Affn,x))_"_P_is_closed
let P be Subset of R^1; ::_thesis: ( P is closed implies (|-- (Affn,x)) " P is closed )
assume P is closed ; ::_thesis: (|-- (Affn,x)) " P is closed
then AxA " P is closed by PRE_TOPC:def_6;
then A5: (AxA " P) ` in the topology of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by A3, PRE_TOPC:def_2;
(AxA " P) ` = ((|-- (Affn,x)) " P) ` by A4, A3, RELAT_1:69;
then ((|-- (Affn,x)) " P) ` is open by A5, PRE_TOPC:def_2;
hence (|-- (Affn,x)) " P is closed by TOPS_1:3; ::_thesis: verum
end;
hence |-- (Affn,x) is continuous by PRE_TOPC:def_6; ::_thesis: verum
end;
Lm9: for n being Nat
for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
conv A is closed
proof
let n be Nat; ::_thesis: for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
conv A is closed
set L = [.0,1.];
set TRn = TOP-REAL n;
let A be affinely-independent Subset of (TOP-REAL n); ::_thesis: ( card A = n + 1 implies conv A is closed )
assume A1: card A = n + 1 ; ::_thesis: conv A is closed
reconsider L = [.0,1.] as Subset of R^1 by TOPMETR:17;
set E = the Enumeration of A;
deffunc H1( set ) -> Element of bool the carrier of (TOP-REAL n) = (|-- (A,( the Enumeration of A . $1))) " L;
consider f being FinSequence such that
A2: len f = n + 1 and
A3: for k being Nat st k in dom f holds
f . k = H1(k) from FINSEQ_1:sch_2();
A4: dom f = Seg (len f) by FINSEQ_1:def_3;
then A5: not rng f is empty by A2, RELAT_1:42;
rng f c= bool the carrier of (TOP-REAL n)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in bool the carrier of (TOP-REAL n) )
assume y in rng f ; ::_thesis: y in bool the carrier of (TOP-REAL n)
then consider x being set such that
A6: x in dom f and
A7: f . x = y by FUNCT_1:def_3;
f . x = H1(x) by A3, A6;
hence y in bool the carrier of (TOP-REAL n) by A7; ::_thesis: verum
end;
then reconsider f = f as FinSequence of bool the carrier of (TOP-REAL n) by FINSEQ_1:def_4;
A8: rng the Enumeration of A = A by Def1;
then A9: len the Enumeration of A = card A by FINSEQ_4:62;
A10: meet (rng f) c= conv A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (rng f) or x in conv A )
assume A11: x in meet (rng f) ; ::_thesis: x in conv A
A12: now__::_thesis:_for_v_being_Element_of_(TOP-REAL_n)_st_v_in_A_holds_
(x_|--_A)_._v_>=_0
let v be Element of (TOP-REAL n); ::_thesis: ( v in A implies (x |-- A) . v >= 0 )
assume v in A ; ::_thesis: (x |-- A) . v >= 0
then consider k being set such that
A13: k in dom the Enumeration of A and
A14: the Enumeration of A . k = v by A8, FUNCT_1:def_3;
A15: k in dom f by A1, A2, A9, A4, A13, FINSEQ_1:def_3;
then f . k in rng f by FUNCT_1:def_3;
then A16: meet (rng f) c= f . k by SETFAM_1:3;
A17: (x |-- A) . v = (|-- (A,v)) . x by A11, Def3;
f . k = (|-- (A,v)) " L by A3, A14, A15;
then (x |-- A) . v in L by A11, A17, A16, FUNCT_1:def_7;
hence (x |-- A) . v >= 0 by XXREAL_1:1; ::_thesis: verum
end;
dim (TOP-REAL n) = n by Th4;
then [#] (TOP-REAL n) = Affin A by A1, Th6;
hence x in conv A by A11, A12, RLAFFIN1:73; ::_thesis: verum
end;
A18: dom the Enumeration of A = Seg (len the Enumeration of A) by FINSEQ_1:def_3;
A19: conv A c= meet (rng f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in conv A or x in meet (rng f) )
assume A20: x in conv A ; ::_thesis: x in meet (rng f)
now__::_thesis:_for_Y_being_set_st_Y_in_rng_f_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in rng f implies x in Y )
assume Y in rng f ; ::_thesis: x in Y
then consider k being set such that
A21: k in dom f and
A22: f . k = Y by FUNCT_1:def_3;
the Enumeration of A . k in A by A1, A2, A8, A9, A4, A18, A21, FUNCT_1:def_3;
then reconsider Ek = the Enumeration of A . k as Element of (TOP-REAL n) ;
A23: dom (|-- (A,Ek)) = [#] (TOP-REAL n) by FUNCT_2:def_1;
A24: ( 0 <= (x |-- A) . Ek & (x |-- A) . Ek <= 1 ) by A20, RLAFFIN1:71;
(x |-- A) . Ek = (|-- (A,Ek)) . x by A20, Def3;
then A25: (|-- (A,Ek)) . x in L by A24, XXREAL_1:1;
Y = (|-- (A,( the Enumeration of A . k))) " L by A3, A21, A22;
hence x in Y by A20, A25, A23, FUNCT_1:def_7; ::_thesis: verum
end;
hence x in meet (rng f) by A5, SETFAM_1:def_1; ::_thesis: verum
end;
now__::_thesis:_for_B_being_Subset_of_(TOP-REAL_n)_st_B_in_rng_f_holds_
B_is_closed
let B be Subset of (TOP-REAL n); ::_thesis: ( B in rng f implies B is closed )
assume B in rng f ; ::_thesis: B is closed
then consider k being set such that
A26: ( k in dom f & f . k = B ) by FUNCT_1:def_3;
( |-- (A,( the Enumeration of A . k)) is continuous & L is closed ) by A1, Th32, TREAL_1:1;
then (|-- (A,( the Enumeration of A . k))) " L is closed by PRE_TOPC:def_6;
hence B is closed by A3, A26; ::_thesis: verum
end;
then rng f is closed by TOPS_2:def_2;
then meet (rng f) is closed by TOPS_2:22;
hence conv A is closed by A19, A10, XBOOLE_0:def_10; ::_thesis: verum
end;
registration
let n be Nat;
let Affn be affinely-independent Subset of (TOP-REAL n);
cluster conv Affn -> closed ;
coherence
conv Affn is closed
proof
set TRn = TOP-REAL n;
consider I being affinely-independent Subset of (TOP-REAL n) such that
A1: Affn c= I and
I c= [#] (TOP-REAL n) and
A2: Affin I = Affin ([#] (TOP-REAL n)) by RLAFFIN1:60;
A3: dim (TOP-REAL n) = n by Th4;
[#] (TOP-REAL n) is Affine by RUSUB_4:22;
then Affin I = [#] (TOP-REAL n) by A2, RLAFFIN1:50;
then card I = n + 1 by A3, Th6;
then conv I is closed by Lm9;
then (conv I) /\ (Affin Affn) is closed ;
hence conv Affn is closed by A1, Th9; ::_thesis: verum
end;
end;
theorem :: RLAFFIN3:33
for n being Nat
for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds
Int Affn is open
proof
let n be Nat; ::_thesis: for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds
Int Affn is open
let Affn be affinely-independent Subset of (TOP-REAL n); ::_thesis: ( card Affn = n + 1 implies Int Affn is open )
set L = ].0,1.[;
set TRn = TOP-REAL n;
set A = Affn;
assume A1: card Affn = n + 1 ; ::_thesis: Int Affn is open
percases ( n <> 0 or n = 0 ) ;
supposeA2: n <> 0 ; ::_thesis: Int Affn is open
reconsider L = ].0,1.[ as Subset of R^1 by TOPMETR:17;
set E = the Enumeration of Affn;
deffunc H1( set ) -> Element of bool the carrier of (TOP-REAL n) = (|-- (Affn,( the Enumeration of Affn . $1))) " L;
consider f being FinSequence such that
A3: len f = n + 1 and
A4: for k being Nat st k in dom f holds
f . k = H1(k) from FINSEQ_1:sch_2();
A5: dom f = Seg (len f) by FINSEQ_1:def_3;
then A6: not rng f is empty by A3, RELAT_1:42;
rng f c= bool the carrier of (TOP-REAL n)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in bool the carrier of (TOP-REAL n) )
assume y in rng f ; ::_thesis: y in bool the carrier of (TOP-REAL n)
then consider x being set such that
A7: x in dom f and
A8: f . x = y by FUNCT_1:def_3;
f . x = H1(x) by A4, A7;
hence y in bool the carrier of (TOP-REAL n) by A8; ::_thesis: verum
end;
then reconsider f = f as FinSequence of bool the carrier of (TOP-REAL n) by FINSEQ_1:def_4;
A9: rng the Enumeration of Affn = Affn by Def1;
then A10: len the Enumeration of Affn = card Affn by FINSEQ_4:62;
A11: meet (rng f) c= Int Affn
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (rng f) or x in Int Affn )
dim (TOP-REAL n) = n by Th4;
then A12: [#] (TOP-REAL n) = Affin Affn by A1, Th6;
assume A13: x in meet (rng f) ; ::_thesis: x in Int Affn
A14: now__::_thesis:_for_v_being_Element_of_(TOP-REAL_n)_st_v_in_Affn_holds_
(x_|--_Affn)_._v_>_0
let v be Element of (TOP-REAL n); ::_thesis: ( v in Affn implies (x |-- Affn) . v > 0 )
assume v in Affn ; ::_thesis: (x |-- Affn) . v > 0
then consider k being set such that
A15: k in dom the Enumeration of Affn and
A16: the Enumeration of Affn . k = v by A9, FUNCT_1:def_3;
A17: k in dom f by A1, A3, A10, A5, A15, FINSEQ_1:def_3;
then f . k in rng f by FUNCT_1:def_3;
then A18: meet (rng f) c= f . k by SETFAM_1:3;
A19: (x |-- Affn) . v = (|-- (Affn,v)) . x by A13, Def3;
f . k = (|-- (Affn,v)) " L by A4, A16, A17;
then (x |-- Affn) . v in L by A13, A19, A18, FUNCT_1:def_7;
hence (x |-- Affn) . v > 0 by XXREAL_1:4; ::_thesis: verum
end;
A20: Affn c= Carrier (x |-- Affn)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Affn or y in Carrier (x |-- Affn) )
assume A21: y in Affn ; ::_thesis: y in Carrier (x |-- Affn)
then (x |-- Affn) . y > 0 by A14;
hence y in Carrier (x |-- Affn) by A21, RLVECT_2:19; ::_thesis: verum
end;
Carrier (x |-- Affn) c= Affn by RLVECT_2:def_6;
then A22: Carrier (x |-- Affn) = Affn by A20, XBOOLE_0:def_10;
for v being Element of (TOP-REAL n) st v in Affn holds
(x |-- Affn) . v >= 0 by A14;
then A23: x in conv Affn by A13, A12, RLAFFIN1:73;
Sum (x |-- Affn) = x by A13, A12, RLAFFIN1:def_7;
hence x in Int Affn by A23, A22, RLAFFIN1:71, RLAFFIN2:12; ::_thesis: verum
end;
A24: conv Affn c= Affin Affn by RLAFFIN1:65;
A25: Int Affn c= conv Affn by RLAFFIN2:5;
A26: dom the Enumeration of Affn = Seg (len the Enumeration of Affn) by FINSEQ_1:def_3;
A27: Int Affn c= meet (rng f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Int Affn or x in meet (rng f) )
assume A28: x in Int Affn ; ::_thesis: x in meet (rng f)
then consider K being Linear_Combination of Affn such that
A29: K is convex and
A30: x = Sum K by RLAFFIN2:10;
A31: x in conv Affn by A25, A28;
sum K = 1 by A29, RLAFFIN1:62;
then A32: K = x |-- Affn by A24, A30, A31, RLAFFIN1:def_7;
A33: Carrier K = Affn by A28, A29, A30, RLAFFIN2:11;
now__::_thesis:_for_Y_being_set_st_Y_in_rng_f_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in rng f implies x in Y )
assume Y in rng f ; ::_thesis: x in Y
then consider k being set such that
A34: k in dom f and
A35: f . k = Y by FUNCT_1:def_3;
A36: the Enumeration of Affn . k in Affn by A1, A3, A9, A10, A5, A26, A34, FUNCT_1:def_3;
then reconsider Ek = the Enumeration of Affn . k as Element of (TOP-REAL n) ;
(x |-- Affn) . Ek <> 0 by A32, A33, A36, RLVECT_2:19;
then A37: 0 < (x |-- Affn) . Ek by A29, A32, RLAFFIN1:62;
A38: (x |-- Affn) . Ek < 1
proof
assume A39: (x |-- Affn) . Ek >= 1 ; ::_thesis: contradiction
(x |-- Affn) . Ek <= 1 by A29, A32, RLAFFIN1:63;
then Affn = {Ek} by A29, A32, A33, A39, RLAFFIN1:64, XXREAL_0:1;
then card Affn = 1 by CARD_2:42;
hence contradiction by A1, A2; ::_thesis: verum
end;
(x |-- Affn) . Ek = (|-- (Affn,Ek)) . x by A30, Def3;
then A40: (|-- (Affn,Ek)) . x in L by A38, A37, XXREAL_1:4;
A41: dom (|-- (Affn,Ek)) = [#] (TOP-REAL n) by FUNCT_2:def_1;
Y = (|-- (Affn,( the Enumeration of Affn . k))) " L by A4, A34, A35;
hence x in Y by A28, A40, A41, FUNCT_1:def_7; ::_thesis: verum
end;
hence x in meet (rng f) by A6, SETFAM_1:def_1; ::_thesis: verum
end;
now__::_thesis:_for_B_being_Subset_of_(TOP-REAL_n)_st_B_in_rng_f_holds_
B_is_open
let B be Subset of (TOP-REAL n); ::_thesis: ( B in rng f implies B is open )
A42: not [#] R^1 is empty ;
assume B in rng f ; ::_thesis: B is open
then consider k being set such that
A43: ( k in dom f & f . k = B ) by FUNCT_1:def_3;
( |-- (Affn,( the Enumeration of Affn . k)) is continuous & L is open ) by A1, Th32, JORDAN6:35;
then (|-- (Affn,( the Enumeration of Affn . k))) " L is open by A42, TOPS_2:43;
hence B is open by A4, A43; ::_thesis: verum
end;
then rng f is open by TOPS_2:def_1;
then meet (rng f) is open by TOPS_2:20;
hence Int Affn is open by A27, A11, XBOOLE_0:def_10; ::_thesis: verum
end;
supposeA44: n = 0 ; ::_thesis: Int Affn is open
not Affn is empty by A1;
then A45: not Int Affn is empty by RLAFFIN2:20;
the carrier of (TOP-REAL n) = {(0. (TOP-REAL n))} by A44, EUCLID:22, EUCLID:77;
then Int Affn = [#] (TOP-REAL n) by A45, ZFMISC_1:33;
hence Int Affn is open ; ::_thesis: verum
end;
end;
end;