let n, k be Nat; :: thesis: 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 An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is open iff An is open )

let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn

for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is open iff An is open )

let Ak be Subset of (TOP-REAL k); :: thesis: for EN being Enumeration of Affn

for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is open iff An is open )

set A = Affn;

set AA = Affin Affn;

set TRn = TOP-REAL n;

let EN be Enumeration of Affn; :: thesis: for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is open iff An is open )

let An be Subset of (TOP-REAL n); :: thesis: ( k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } implies ( Ak is open iff An is open ) )

assume that

A1: k <= n and

A2: card Affn = n + 1 and

A3: An = { v where v is Element of (TOP-REAL n) : (v |-- EN) | k in Ak } ; :: thesis: ( Ak is open iff An is open )

set E = EN;

A4: rng EN = Affn by Def1;

then A5: len EN = card Affn by FINSEQ_4:62;

then A6: len EN >= 1 by A2, NAT_1:14;

then A7: len EN in dom EN by FINSEQ_3:25;

then EN . (len EN) in Affn by A4, FUNCT_1:def 3;

then reconsider EL = EN . (len EN) as Element of (TOP-REAL n) ;

A8: card ((- EL) + Affn) = n + 1 by A2, RLAFFIN1:7;

set BB = { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ;

A9: { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } c= An

set TB = { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } ;

set T = transl ((- EL),(TOP-REAL n));

A10: dim (TOP-REAL n) = n by Th4;

then A11: [#] (TOP-REAL n) = Affin Affn by A2, Th6;

An c= { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) }

then A13: (transl ((- EL),(TOP-REAL n))) .: An = { w where w is Element of (TOP-REAL n) : ( w in Affin ((- EL) + Affn) & (w |-- Ev) | k in Ak ) } by Lm6;

A14: (transl ((- EL),(TOP-REAL n))) .: An c= { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak }

then A16: Affin ((- EL) + Affn) = [#] (TOP-REAL n) by A2, A10, Th6;

{ w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } c= (transl ((- EL),(TOP-REAL n))) .: An

len EN in Seg (card Affn) by A5, A6;

then A19: ((card Affn) |-> (- EL)) . (len EN) = - EL by FINSEQ_2:57;

A20: rng Ev = (- EL) + Affn by Def1;

then len Ev = card Affn by A15, FINSEQ_4:62;

then dom EN = dom Ev by A5, FINSEQ_3:29;

then Ev . (len EN) = EL + (- EL) by A7, A19, FVSUM_1:17

.= 0. (TOP-REAL n) by RLVECT_1:5

.= 0* n by EUCLID:70 ;

then A21: Ev . (len Ev) = 0* n by A5, A15, A20, FINSEQ_4:62;

not (- EL) + Affn is empty by A2, A15;

then ( (transl ((- EL),(TOP-REAL n))) .: An is open iff Ak is open ) by A1, A21, A8, A18, Lm7;

hence ( Ak is open iff An is open ) by TOPGRP_1:25; :: thesis: verum

set TAA = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn);

A22: rng ((transl ((- EL),(TOP-REAL n))) | (Affin Affn)) = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) by RELAT_1:115;

dom (transl ((- EL),(TOP-REAL n))) = [#] (TOP-REAL n) by FUNCT_2:52;

then A23: dom ((transl ((- EL),(TOP-REAL n))) | (Affin Affn)) = Affin Affn by RELAT_1:62;

( [#] ((TOP-REAL n) | (Affin Affn)) = Affin Affn & [#] ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) ) by PRE_TOPC:def 5;

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 A23, A22, FUNCT_2:1;

reconsider TAB = TA .: An as Subset of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) ;

reconsider TAB = TA .: An as Subset of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) ;

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn

for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is open iff An is open )

let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn

for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is open iff An is open )

let Ak be Subset of (TOP-REAL k); :: thesis: for EN being Enumeration of Affn

for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is open iff An is open )

set A = Affn;

set AA = Affin Affn;

set TRn = TOP-REAL n;

let EN be Enumeration of Affn; :: thesis: for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is open iff An is open )

let An be Subset of (TOP-REAL n); :: thesis: ( k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } implies ( Ak is open iff An is open ) )

assume that

A1: k <= n and

A2: card Affn = n + 1 and

A3: An = { v where v is Element of (TOP-REAL n) : (v |-- EN) | k in Ak } ; :: thesis: ( Ak is open iff An is open )

set E = EN;

A4: rng EN = Affn by Def1;

then A5: len EN = card Affn by FINSEQ_4:62;

then A6: len EN >= 1 by A2, NAT_1:14;

then A7: len EN in dom EN by FINSEQ_3:25;

then EN . (len EN) in Affn by A4, FUNCT_1:def 3;

then reconsider EL = EN . (len EN) as Element of (TOP-REAL n) ;

A8: card ((- EL) + Affn) = n + 1 by A2, RLAFFIN1:7;

set BB = { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ;

A9: { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } c= An

proof

reconsider Ev = EN + ((card Affn) |-> (- EL)) as Enumeration of (- EL) + Affn by Th13;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } or x in An )

assume x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ; :: thesis: x in An

then ex u being Element of (TOP-REAL n) st

( x = u & u in Affin Affn & (u |-- EN) | k in Ak ) ;

hence x in An by A3; :: thesis: verum

end;assume x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ; :: thesis: x in An

then ex u being Element of (TOP-REAL n) st

( x = u & u in Affin Affn & (u |-- EN) | k in Ak ) ;

hence x in An by A3; :: thesis: verum

set TB = { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } ;

set T = transl ((- EL),(TOP-REAL n));

A10: dim (TOP-REAL n) = n by Th4;

then A11: [#] (TOP-REAL n) = Affin Affn by A2, Th6;

An c= { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) }

proof

then
{ u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } = An
by A9;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in An or x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } )

assume x in An ; :: thesis: x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) }

then consider v being Element of (TOP-REAL n) such that

A12: ( x = v & (v |-- EN) | k in Ak ) by A3;

thus x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } by A11, A12; :: thesis: verum

end;assume x in An ; :: thesis: x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) }

then consider v being Element of (TOP-REAL n) such that

A12: ( x = v & (v |-- EN) | k in Ak ) by A3;

thus x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } by A11, A12; :: thesis: verum

then A13: (transl ((- EL),(TOP-REAL n))) .: An = { w where w is Element of (TOP-REAL n) : ( w in Affin ((- EL) + Affn) & (w |-- Ev) | k in Ak ) } by Lm6;

A14: (transl ((- EL),(TOP-REAL n))) .: An c= { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak }

proof

A15:
card ((- EL) + Affn) = card Affn
by RLAFFIN1:7;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (transl ((- EL),(TOP-REAL n))) .: An or x in { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } )

assume x in (transl ((- EL),(TOP-REAL n))) .: An ; :: thesis: x in { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak }

then ex w being Element of (TOP-REAL n) st

( x = w & w in Affin ((- EL) + Affn) & (w |-- Ev) | k in Ak ) by A13;

hence x in { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } ; :: thesis: verum

end;assume x in (transl ((- EL),(TOP-REAL n))) .: An ; :: thesis: x in { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak }

then ex w being Element of (TOP-REAL n) st

( x = w & w in Affin ((- EL) + Affn) & (w |-- Ev) | k in Ak ) by A13;

hence x in { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } ; :: thesis: verum

then A16: Affin ((- EL) + Affn) = [#] (TOP-REAL n) by A2, A10, Th6;

{ w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } c= (transl ((- EL),(TOP-REAL n))) .: An

proof

then A18:
(transl ((- EL),(TOP-REAL n))) .: An = { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak }
by A14;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } or x in (transl ((- EL),(TOP-REAL n))) .: An )

assume x in { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } ; :: thesis: x in (transl ((- EL),(TOP-REAL n))) .: An

then consider w being Element of (TOP-REAL n) such that

A17: ( x = w & (w |-- Ev) | k in Ak ) ;

thus x in (transl ((- EL),(TOP-REAL n))) .: An by A16, A13, A17; :: thesis: verum

end;assume x in { w where w is Element of (TOP-REAL n) : (w |-- Ev) | k in Ak } ; :: thesis: x in (transl ((- EL),(TOP-REAL n))) .: An

then consider w being Element of (TOP-REAL n) such that

A17: ( x = w & (w |-- Ev) | k in Ak ) ;

thus x in (transl ((- EL),(TOP-REAL n))) .: An by A16, A13, A17; :: thesis: verum

len EN in Seg (card Affn) by A5, A6;

then A19: ((card Affn) |-> (- EL)) . (len EN) = - EL by FINSEQ_2:57;

A20: rng Ev = (- EL) + Affn by Def1;

then len Ev = card Affn by A15, FINSEQ_4:62;

then dom EN = dom Ev by A5, FINSEQ_3:29;

then Ev . (len EN) = EL + (- EL) by A7, A19, FVSUM_1:17

.= 0. (TOP-REAL n) by RLVECT_1:5

.= 0* n by EUCLID:70 ;

then A21: Ev . (len Ev) = 0* n by A5, A15, A20, FINSEQ_4:62;

not (- EL) + Affn is empty by A2, A15;

then ( (transl ((- EL),(TOP-REAL n))) .: An is open iff Ak is open ) by A1, A21, A8, A18, Lm7;

hence ( Ak is open iff An is open ) by TOPGRP_1:25; :: thesis: verum

set TAA = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn);

A22: rng ((transl ((- EL),(TOP-REAL n))) | (Affin Affn)) = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) by RELAT_1:115;

dom (transl ((- EL),(TOP-REAL n))) = [#] (TOP-REAL n) by FUNCT_2:52;

then A23: dom ((transl ((- EL),(TOP-REAL n))) | (Affin Affn)) = Affin Affn by RELAT_1:62;

( [#] ((TOP-REAL n) | (Affin Affn)) = Affin Affn & [#] ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) ) by PRE_TOPC:def 5;

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 A23, A22, FUNCT_2:1;

reconsider TAB = TA .: An as Subset of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) ;

reconsider TAB = TA .: An as Subset of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) ;