let x be set ; for n being Nat
for Affn being affinely-independent Subset of (TOP-REAL n) holds (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1
let n be Nat; for Affn being affinely-independent Subset of (TOP-REAL n) holds (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1
let Affn be affinely-independent Subset of (TOP-REAL n); (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1
reconsider Z = 0 as Element of R^1 by Lm5, TOPMETR:17;
set TRn = TOP-REAL n;
set AA = Affin Affn;
set Ax = |-- (Affn,x);
set AxA = (|-- (Affn,x)) | (Affin Affn);
A1:
([#] (TOP-REAL n)) /\ (Affin Affn) = Affin Affn
by XBOOLE_1:28;
A2:
Affin Affn = [#] ((TOP-REAL n) | (Affin Affn))
by PRE_TOPC:def 5;
then reconsider AxA = (|-- (Affn,x)) | (Affin Affn) as Function of ((TOP-REAL n) | (Affin Affn)),R^1 by FUNCT_2:32;
A3:
dom AxA = Affin Affn
by A2, FUNCT_2:def 1;
per cases
( not x in Affn or ( x in Affn & card Affn = 1 ) or ( x in Affn & card Affn <> 1 ) )
;
suppose A4:
(
x in Affn &
card Affn = 1 )
;
(|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1A5:
rng AxA c= the
carrier of
R^1
by RELAT_1:def 19;
consider y being
object such that A6:
Affn = {y}
by A4, CARD_2:42;
A7:
x = y
by A4, A6, TARSKI:def 1;
then
Affn is
Affine
by A4, A6, RUSUB_4:23;
then A8:
Affin Affn = Affn
by RLAFFIN1:50;
then
AxA . x in rng AxA
by A3, A4, FUNCT_1:def 3;
then reconsider b =
AxA . x as
Element of
R^1 by A5;
rng AxA = {(AxA . x)}
by A3, A6, A7, A8, FUNCT_1:4;
then
AxA = ((TOP-REAL n) | (Affin Affn)) --> b
by A2, A3, FUNCOP_1:9;
hence
(|-- (Affn,x)) | (Affin Affn) is
continuous Function of
((TOP-REAL n) | (Affin Affn)),
R^1
;
verum end; suppose A9:
(
x in Affn &
card Affn <> 1 )
;
(|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1set P2 = the
Enumeration of
Affn \ {x};
set P1 =
<*x*>;
set P12 =
<*x*> ^ the
Enumeration of
Affn \ {x};
A10:
(
rng <*x*> = {x} &
rng the
Enumeration of
Affn \ {x} = Affn \ {x} )
by Def1, FINSEQ_1:39;
(
<*x*> is
one-to-one &
{x} misses Affn \ {x} )
by FINSEQ_3:93, XBOOLE_1:79;
then A11:
<*x*> ^ the
Enumeration of
Affn \ {x} is
one-to-one
by A10, FINSEQ_3:91;
rng (<*x*> ^ the Enumeration of Affn \ {x}) = (rng <*x*>) \/ (rng the Enumeration of Affn \ {x})
by FINSEQ_1:31;
then
rng (<*x*> ^ the Enumeration of Affn \ {x}) = Affn
by A9, A10, ZFMISC_1:116;
then reconsider P12 =
<*x*> ^ the
Enumeration of
Affn \ {x} as
Enumeration of
Affn by A11, Def1;
set TR1 =
TOP-REAL 1;
consider Pro being
Function of
(TOP-REAL 1),
R^1 such that A12:
for
p being
Element of
(TOP-REAL 1) holds
Pro . p = p /. 1
by JORDAN2B:1;
A13:
Pro is
being_homeomorphism
by A12, JORDAN2B:28;
card Affn >= 1
by A9, NAT_1:14;
then A14:
card Affn > 1
by A9, XXREAL_0:1;
now for P being Subset of R^1 st P is closed holds
AxA " P is closed A15:
dom <*x*> c= dom P12
by FINSEQ_1:26;
let P be
Subset of
R^1;
( P is closed implies AxA " P is closed )set B =
{ v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } ;
A16:
1
in {1}
by FINSEQ_1:2;
assume
P is
closed
;
AxA " P is closed then A17:
Pro " P is
closed
by A13, TOPGRP_1:24;
A18:
dom <*x*> = Seg 1
by FINSEQ_1:38;
then A19:
P12 . 1 =
<*x*> . 1
by A16, FINSEQ_1:2, FINSEQ_1:def 7
.=
x
;
A20:
not
Affin Affn is
empty
by A9;
A21:
{ v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } c= AxA " P
proof
let y be
object ;
TARSKI:def 3 ( not y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } or y in AxA " P )
assume
y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P }
;
y in AxA " P
then consider v being
Element of
((TOP-REAL n) | (Affin Affn)) such that A22:
y = v
and A23:
(v |-- P12) | 1
in Pro " P
;
set vP =
v |-- P12;
reconsider vP1 =
(v |-- P12) | 1 as
Element of
(TOP-REAL 1) by A23;
A24:
v in Affin Affn
by A2, A20;
len vP1 = 1
by CARD_1:def 7;
then
dom vP1 = Seg 1
by FINSEQ_1:def 3;
then A25:
1
in dom vP1
;
then A26:
1
in dom (v |-- P12)
by RELAT_1:57;
Pro . vP1 =
vP1 /. 1
by A12
.=
vP1 . 1
by A25, PARTFUN1:def 6
.=
(v |-- P12) . 1
by A25, FUNCT_1:47
.=
(v |-- Affn) . x
by A19, A26, FUNCT_1:12
.=
(|-- (Affn,x)) . v
by A24, Def3
;
then
(|-- (Affn,x)) . v in P
by A23, FUNCT_1:def 7;
then
AxA . v in P
by A2, A3, A9, FUNCT_1:47;
hence
y in AxA " P
by A2, A3, A9, A22, FUNCT_1:def 7;
verum
end; A27:
dom Pro = [#] (TOP-REAL 1)
by A13, TOPGRP_1:24;
AxA " P c= { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P }
proof
let y be
object ;
TARSKI:def 3 ( not y in AxA " P or y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } )
set yP =
y |-- P12;
len (y |-- P12) = card Affn
by Th16;
then A28:
len ((y |-- P12) | 1) = 1
by A9, FINSEQ_1:59, NAT_1:14;
then reconsider yP1 =
(y |-- P12) | 1 as
Element of
(TOP-REAL 1) by TOPREAL3:46;
A29:
dom yP1 = Seg 1
by A28, FINSEQ_1:def 3;
assume A30:
y in AxA " P
;
y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P }
then A31:
y in dom AxA
by FUNCT_1:def 7;
then AxA . y =
(|-- (Affn,x)) . y
by FUNCT_1:47
.=
(y |-- Affn) . (P12 . 1)
by A19, A3, A31, Def3
.=
(y |-- P12) . 1
by A18, A16, A15, FINSEQ_1:2, FUNCT_1:13
.=
yP1 . 1
by A16, A29, FINSEQ_1:2, FUNCT_1:47
.=
yP1 /. 1
by A16, A29, FINSEQ_1:2, PARTFUN1:def 6
.=
Pro . yP1
by A12
;
then
Pro . yP1 in P
by A30, FUNCT_1:def 7;
then
yP1 in Pro " P
by A27, FUNCT_1:def 7;
hence
y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P }
by A30;
verum
end; then
{ v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } = AxA " P
by A21;
hence
AxA " P is
closed
by A14, A17, Th28;
verum end; hence
(|-- (Affn,x)) | (Affin Affn) is
continuous Function of
((TOP-REAL n) | (Affin Affn)),
R^1
by PRE_TOPC:def 6;
verum end;