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