let n, k be Nat; ( 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
; 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); ( 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
; 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; ( 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
; 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); 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); ( 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)
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 }
; ( 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
object ;
TARSKI:def 3 ( not x in B or x in (Mx2Tran M) .: PP )
assume
x in B
;
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;
verum
end;
(Mx2Tran M) .: PP c= B
proof
let y be
object ;
TARSKI:def 3 ( not y in (Mx2Tran M) .: PP or y in B )
assume
y in (Mx2Tran M) .: PP
;
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;
verum
end;
then A26:
(Mx2Tran M) .: PP = B
by A17;
( P is open iff PP is open )
by A1, Th7;
hence
( P is open iff B is open )
by A15, A26, TOPGRP_1:25; verum