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
len (FinS2MX (Bn | c1)) = c1
by A11, FINSEQ_1:59;
then reconsider BnC = FinS2MX (Bn | c1) as Matrix of c1,n,F_Real ;
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)
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
object ;
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 A55:
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 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
object 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;
verum
end;
A63:
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 A67:
BF = { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum }
by A63;
A68:
{ v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } c= MT " B
proof
let x be
object ;
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 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;
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;
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; verum