let n, k be 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 )
let Affn be 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 Ak be 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 EN be 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 )
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)); ( 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 }
; ( 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
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 ) }
then A8:
{ u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } = B
by A4;
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 }
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
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;
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; verum