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 len (FinS2MX (e | n)) = n by A2, A6, FINSEQ_1:59;

then reconsider M = FinS2MX (e | n) as Matrix of n,F_Real ;

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)

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

( 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

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 len (FinS2MX (e | n)) = n by A2, A6, FINSEQ_1:59;

then reconsider M = FinS2MX (e | n) as Matrix of n,F_Real ;

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

then reconsider PP = { v where v is Element of (TOP-REAL n) : v | k in P } as Subset of (TOP-REAL n) ;
let x be object ; :: 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;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

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

(Mx2Tran M) .: PP c= B
let x be object ; :: 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 object 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;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 object 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

proof

then A26:
(Mx2Tran M) .: PP = B
by A17;
let y be object ; :: 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 object 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;assume y in (Mx2Tran M) .: PP ; :: thesis: y in B

then consider x being object 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

( 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