let n, k be 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 )
set TRn = TOP-REAL n;
let A be non empty finite affinely-independent Subset of (TOP-REAL n); ( 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
; 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; ( 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
; 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); 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)); ( 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 }
; ( 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 ;
A20:
c1 + 1 = card A
;
A21: len F =
card (A \ {(0. (TOP-REAL n))})
by A14, A15, FINSEQ_4:62
.=
c1
by A9, A20, STIRL2_1:55
;
set MBc = Mx2Tran BnC;
set TRc = TOP-REAL c1;
A22:
( 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 A23:
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;
A24:
rng MBC = BF
by A21, MATRTOP2:18;
consider M being Matrix of n,F_Real such that
A25:
M is invertible
and
A26:
M | (len F) = F
by A10, A14, A15, MATRTOP2:19;
set MTI = Mx2Tran (M ~);
A27:
[#] ((TOP-REAL n) | BF) = BF
by PRE_TOPC:def 5;
M ~ is invertible
by A25, MATRIX_6:16;
then A28:
Det (M ~) <> 0. F_Real
by LAPLACE:34;
then A29:
the_rank_of (M ~) = n
by MATRIX13:83;
then reconsider MTe = (Mx2Tran (M ~)) * E as Enumeration of (Mx2Tran (M ~)) .: A by Th15;
A30:
rng MTe = (Mx2Tran (M ~)) .: A
by Def1;
( dom (Mx2Tran (M ~)) = [#] (TOP-REAL n) & Mx2Tran (M ~) is one-to-one )
by A28, FUNCT_2:def 1, MATRTOP1:40;
then
A,(Mx2Tran (M ~)) .: A are_equipotent
by CARD_1:33;
then A31:
card A = card ((Mx2Tran (M ~)) .: A)
by CARD_1:5;
then
len MTe = len E
by A4, A30, FINSEQ_4:62;
then
len E in dom MTe
by A5, FINSEQ_3:25;
then A32: 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 A33:
(Mx2Tran M) .: BF = Affin A
by A10, A14, A15, A25, A26, MATRTOP2:21;
then A34:
rng ((Mx2Tran M) | BF) = Affin A
by RELAT_1:115;
A35:
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, A27, A34, FUNCT_2:1;
reconsider MT = Mx2Tran M as Function ;
A36:
Det M <> 0. F_Real
by A25, LAPLACE:34;
then A37:
MT " = Mx2Tran (M ~)
by MATRTOP1:43;
MT1 is being_homeomorphism
by A25, A33, METRIZTS:2;
then A38:
( 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 } ;
A39:
n -' c1 = n - c1
by A11, XREAL_1:233;
then A40:
n = c1 + (n -' c1)
;
A41:
MT is one-to-one
by A36, MATRTOP1:40;
then A42:
MT " (Affin A) = BF
by A33, A35, FUNCT_1:94;
A43:
MT " A c= MT " (Affin A)
by RELAT_1:143, RLAFFIN1:49;
then A44:
(Mx2Tran (M ~)) .: A c= BF
by A37, A41, A42, FUNCT_1:85;
Bn is one-to-one
by MATRLIN:def 2;
then
Bn | c1 is one-to-one
by FUNCT_1:52;
then A45:
the_rank_of BnC = c1
by A23, MATRIX13:121;
then A46:
MBC is one-to-one
by MATRTOP1:39;
then A47:
dom (MBC ") = rng MBC
by FUNCT_1:33;
then reconsider MBCe = (MBC ") * MTe as FinSequence by A24, A30, A44, FINSEQ_1:16;
A48:
rng MBCe = (MBC ") .: ((Mx2Tran (M ~)) .: A)
by A30, RELAT_1:127;
(Mx2Tran (M ~)) .: A is affinely-independent
by A29, MATRTOP2:24;
then
(Mx2Tran BnC) " ((Mx2Tran (M ~)) .: A) is affinely-independent
by A45, MATRTOP2:27;
then reconsider R = rng MBCe as finite affinely-independent Subset of (TOP-REAL c1) by A46, A48, FUNCT_1:85;
reconsider MBCe = MBCe as Enumeration of R by A46, Def1;
reconsider MBCeE = (Mx2Tran BnC) * MBCe as Enumeration of (Mx2Tran BnC) .: R by A45, Th15;
MBC * (MBC ") = id (rng MBC)
by A46, FUNCT_1:39;
then A49: MBCeE =
(id (rng MBC)) * MTe
by RELAT_1:36
.=
MTe
by A24, A30, A44, RELAT_1:53
;
set PPP = { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } ;
A50:
{ v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } c= [#] (TOP-REAL c1)
A51:
(Mx2Tran (M ~)) .: A = MT " A
by A37, A41, FUNCT_1:85;
A52:
MT " B c= MT " (Affin A)
by A13, RELAT_1:143;
A53:
(Mx2Tran (M ~)) .: A,R are_equipotent
by A24, A46, A47, A44, A48, CARD_1:33;
then A54:
c1 + 1 = card R
by A31, CARD_1:5;
then A55:
( 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 A50;
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 A56:
Affin R = [#] (TOP-REAL c1)
by A54, Th6;
A57: (Mx2Tran BnC) .: R =
MBC .: ((MBC ") .: ((Mx2Tran (M ~)) .: A))
by A30, RELAT_1:127
.=
(MBC * (MBC ")) .: ((Mx2Tran (M ~)) .: A)
by RELAT_1:126
.=
(id (rng MBC)) .: ((Mx2Tran (M ~)) .: A)
by A46, FUNCT_1:39
.=
(Mx2Tran (M ~)) .: A
by A51, A42, A43, A24, FUNCT_1:92
;
A58:
MT " B c= { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) }
proof
let x be
set ;
TARSKI:def 3 ( 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 A59:
x in MT " B
;
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 A33, A27, A35, A41, A52, FUNCT_1:94;
MT . x in B
by A59, FUNCT_1:def 7;
then consider v being
Element of
((TOP-REAL n) | (Affin A)) such that A60:
MT . x = v
and A61:
(v |-- E) | k in P
by A12;
x in dom MT
by A59, FUNCT_1:def 7;
then A62:
(Mx2Tran (M ~)) . v = x
by A37, A41, A60, FUNCT_1:34;
x in BF
by A42, A52, A59;
then reconsider W =
x as
Element of
(TOP-REAL n) ;
A63:
v in Affin A
by A13;
consider u being
set such that A64:
u in dom (Mx2Tran BnC)
and A65:
(Mx2Tran BnC) . u = w
by A42, A52, A24, A59, FUNCT_1:def 3;
A66:
W | c1 = u
by A64, A65, MATRTOP1:38;
reconsider u =
u as
Element of
(TOP-REAL c1) by A64;
u |-- MBCe =
w |-- MTe
by A65, A57, A49, A45, A56, Th19
.=
v |-- E
by A29, A62, A63, Th19
;
then
u in PPP
by A61;
hence
x in { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) }
by A42, A52, A59, A66;
verum
end;
A67:
BF c= { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum }
{ (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } c= BF
then A71:
BF = { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum }
by A67, XBOOLE_0:def 10;
A72:
{ v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } c= MT " B
proof
let x be
set ;
TARSKI:def 3 ( 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 ) }
;
x in MT " B
then consider v being
Element of
(TOP-REAL n) such that A73:
x = v
and A74:
v | c1 in PPP
and A75:
v in BF
;
consider v1 being
Element of
(TOP-REAL c1) such that A76:
v = v1 ^ ((n -' c1) |-> 0)
by A71, A75;
consider u being
Element of
(TOP-REAL c1) such that A77:
u = v | c1
and A78:
(u |-- MBCe) | k in P
by A74;
set w =
(Mx2Tran BnC) . u;
A79:
(Mx2Tran BnC) . u = (Mx2Tran (M ~)) . (MT . ((Mx2Tran BnC) . u))
by A35, A37, A41, FUNCT_1:34;
dom (Mx2Tran BnC) = [#] (TOP-REAL c1)
by FUNCT_2:def 1;
then A80:
(Mx2Tran BnC) . u in BF
by A24, FUNCT_1:def 3;
then A81:
MT . ((Mx2Tran BnC) . u) in Affin A
by A33, A35, FUNCT_1:def 6;
u |-- MBCe =
((Mx2Tran BnC) . u) |-- MBCeE
by A45, A56, Th19
.=
(MT . ((Mx2Tran BnC) . u)) |-- E
by A29, A79, A81, Th19, A57, A49
;
then A82:
MT . ((Mx2Tran BnC) . u) in B
by A12, A13, A78, A81;
consider w1 being
Element of
(TOP-REAL c1) such that A83:
(Mx2Tran BnC) . u = w1 ^ ((n -' c1) |-> 0)
by A71, A80;
w1 =
((Mx2Tran BnC) . u) | (dom w1)
by A83, 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 A77, MATRTOP1:38
.=
v | (Seg (len v1))
by CARD_1:def 7
.=
v | (dom v1)
by FINSEQ_1:def 3
.=
v1
by A76, FINSEQ_1:21
;
hence
x in MT " B
by A35, A73, A83, A76, A82, FUNCT_1:def 7;
verum
end;
A84:
len MBCe = len E
by A4, A54, FINSEQ_4:62;
then
len E in dom MBCe
by A5, FINSEQ_3:25;
then MBCe . (len E) =
(MBC ") . (0. (TOP-REAL n))
by A32, FUNCT_1:12
.=
0. (TOP-REAL c1)
by A46, A22, FUNCT_1:34
;
then A85:
MBCe . (len MBCe) = 0* c1
by A84, EUCLID:70;
MT1 " B =
BF /\ (MT " B)
by FUNCT_1:70
.=
MT " B
by A13, A42, 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 A58, A72, XBOOLE_0:def 10;
then A86:
( PPP is open iff B is open )
by A38, A71, A40, Th8;
card R = c1 + 1
by A31, A53, CARD_1:5;
hence
( P is open iff B is open )
by A85, A86, A55, Lm6; verum