let V be RealLinearSpace; for Af being finite Subset of V
for If being finite affinely-independent Subset of V
for L being Linear_Combination of Af st Af c= conv If & sum L = 1 holds
( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) )
let Af be finite Subset of V; for If being finite affinely-independent Subset of V
for L being Linear_Combination of Af st Af c= conv If & sum L = 1 holds
( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) )
let If be finite affinely-independent Subset of V; for L being Linear_Combination of Af st Af c= conv If & sum L = 1 holds
( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) )
defpred S1[ Nat] means for B being finite Subset of V st card B = $1 & B c= conv If holds
for L being Linear_Combination of B st Carrier L = B & sum L = 1 holds
( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) );
A1:
for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A2:
S1[
m]
;
S1[m + 1]
let B be
finite Subset of
V;
( card B = m + 1 & B c= conv If implies for L being Linear_Combination of B st Carrier L = B & sum L = 1 holds
( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) )
assume that A3:
card B = m + 1
and A4:
B c= conv If
;
for L being Linear_Combination of B st Carrier L = B & sum L = 1 holds
( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) )
conv If c= Affin If
by RLAFFIN1:65;
then A5:
B c= Affin If
by A4;
then A6:
Affin B c= Affin If
by RLAFFIN1:51;
let L be
Linear_Combination of
B;
( Carrier L = B & sum L = 1 implies ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) )
assume that A7:
Carrier L = B
and A8:
sum L = 1
;
( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) )
Sum L in { (Sum K) where K is Linear_Combination of B : sum K = 1 }
by A8;
then
Sum L in Affin B
by RLAFFIN1:59;
hence
Sum L in Affin If
by A6;
for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) )
per cases
( m = 0 or m > 0 )
;
suppose A9:
m = 0
;
for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) )let x be
Element of
V;
ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) )consider b being
object such that A10:
B = {b}
by A3, A9, CARD_2:42;
b in B
by A10, TARSKI:def 1;
then reconsider b =
b as
Element of
V ;
A11:
sum L = L . b
by A7, A10, RLAFFIN1:32;
set F =
<*((b |-- If) . x)*>;
set G =
<*b*>;
take
<*((b |-- If) . x)*>
;
ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum <*((b |-- If) . x)*> & len G = len <*((b |-- If) . x)*> & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom <*((b |-- If) . x)*> holds
<*((b |-- If) . x)*> . n = (L . (G . n)) * (((G . n) |-- If) . x) ) )take
<*b*>
;
( ((Sum L) |-- If) . x = Sum <*((b |-- If) . x)*> & len <*b*> = len <*((b |-- If) . x)*> & <*b*> is one-to-one & rng <*b*> = Carrier L & ( for n being Nat st n in dom <*((b |-- If) . x)*> holds
<*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x) ) )
Sum L = (L . b) * b
by A10, RLVECT_2:32;
then
(
len <*b*> = 1 &
Sum L = b )
by A8, A11, FINSEQ_1:39, RLVECT_1:def 8;
hence
(
((Sum L) |-- If) . x = Sum <*((b |-- If) . x)*> &
len <*b*> = len <*((b |-- If) . x)*> &
<*b*> is
one-to-one &
rng <*b*> = Carrier L )
by A7, A10, FINSEQ_1:39, FINSEQ_3:93, RVSUM_1:73;
for n being Nat st n in dom <*((b |-- If) . x)*> holds
<*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x)let n be
Nat;
( n in dom <*((b |-- If) . x)*> implies <*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x) )assume
n in dom <*((b |-- If) . x)*>
;
<*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x)then
n in Seg 1
by FINSEQ_1:38;
then A12:
n = 1
by FINSEQ_1:2, TARSKI:def 1;
then
<*b*> . n = b
by FINSEQ_1:40;
hence
<*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x)
by A8, A11, A12, FINSEQ_1:40;
verum end; suppose A13:
m > 0
;
for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) )
ex
v being
Element of
V st
(
L . v <> 1 &
v in Carrier L )
proof
consider F being
FinSequence of
V such that A14:
F is
one-to-one
and A15:
rng F = Carrier L
and A16:
1
= Sum (L * F)
by A8, RLAFFIN1:def 3;
dom F,
B are_equipotent
by A7, A14, A15, WELLORD2:def 4;
then A17:
card B =
card (dom F)
by CARD_1:5
.=
card (Seg (len F))
by FINSEQ_1:def 3
.=
len F
by FINSEQ_1:57
;
A18:
(
len F = len (L * F) &
len ((len F) |-> 1) = len F )
by CARD_1:def 7, FINSEQ_2:33;
Sum ((len F) |-> 1) = (len F) * 1
by RVSUM_1:80;
then
(len F) |-> 1
<> L * F
by A3, A13, A16, A17;
then consider k being
Nat such that A19:
( 1
<= k &
k <= len F )
and A20:
((len F) |-> 1) . k <> (L * F) . k
by A18, FINSEQ_1:14;
A21:
k in Seg (len F)
by A19, FINSEQ_1:1;
A22:
k in dom F
by A19, FINSEQ_3:25;
then A23:
F . k in Carrier L
by A15, FUNCT_1:def 3;
L . (F . k) = (L * F) . k
by A22, FUNCT_1:13;
then
L . (F . k) <> 1
by A20, A21, FINSEQ_2:57;
hence
ex
v being
Element of
V st
(
L . v <> 1 &
v in Carrier L )
by A23;
verum
end; then consider v being
Element of
V such that A24:
L . v <> 1
and A25:
v in Carrier L
;
set 1Lv = 1
- (L . v);
consider K being
Linear_Combination of
{v} such that A26:
K . v = L . v
by RLVECT_4:37;
set LK =
L - K;
A27:
1
- (L . v) <> 0
by A24;
set 1LK =
(1 / (1 - (L . v))) * (L - K);
A28:
Carrier K c= {v}
by RLVECT_2:def 6;
then
sum K = K . v
by RLAFFIN1:32;
then
sum (L - K) = 1
- (L . v)
by A8, A26, RLAFFIN1:36;
then A29:
sum ((1 / (1 - (L . v))) * (L - K)) = (1 / (1 - (L . v))) * (1 - (L . v))
by RLAFFIN1:35;
(L - K) . v = (L . v) - (K . v)
by RLVECT_2:54;
then A30:
not
v in Carrier (L - K)
by A26, RLVECT_2:19;
A31:
card (B \ {v}) = m
by A3, A7, A25, STIRL2_1:55;
A32:
Sum K = (L . v) * v
by A26, RLVECT_2:32;
B \ {v} c= B
by XBOOLE_1:36;
then A33:
B \ {v} c= conv If
by A4;
L . v <> 0
by A25, RLVECT_2:19;
then
v in Carrier K
by A26;
then A34:
Carrier K = {v}
by A28, ZFMISC_1:33;
A35:
B \ {v} c= Carrier (L - K)
let x be
Element of
V;
ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) )A38:
(1 / (1 - (L . v))) * (1 - (L . v)) =
(1 * (1 - (L . v))) / (1 - (L . v))
by XCMPLX_1:74
.=
1
by A27, XCMPLX_1:60
;
Sum ((1 / (1 - (L . v))) * (L - K)) = (1 / (1 - (L . v))) * (Sum (L - K))
by RLVECT_3:2;
then (1 - (L . v)) * (Sum ((1 / (1 - (L . v))) * (L - K))) =
((1 - (L . v)) * (1 / (1 - (L . v)))) * (Sum (L - K))
by RLVECT_1:def 7
.=
Sum (L - K)
by A38, RLVECT_1:def 8
;
then A39:
((1 - (L . v)) * (Sum ((1 / (1 - (L . v))) * (L - K)))) + ((L . v) * v) =
((Sum L) - ((L . v) * v)) + ((L . v) * v)
by A32, RLVECT_3:4
.=
Sum L
by RLVECT_4:1
;
B \/ {v} = B
by A7, A25, ZFMISC_1:40;
then
Carrier (L - K) c= B \ {v}
by A7, A34, A30, RLVECT_2:55, ZFMISC_1:34;
then
B \ {v} = Carrier (L - K)
by A35;
then A40:
Carrier ((1 / (1 - (L . v))) * (L - K)) = B \ {v}
by A27, RLVECT_2:42;
then A41:
(1 / (1 - (L . v))) * (L - K) is
Linear_Combination of
B \ {v}
by RLVECT_2:def 6;
then consider F being
FinSequence of
REAL ,
G being
FinSequence of
V such that A42:
((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If) . x = Sum F
and A43:
len G = len F
and A44:
G is
one-to-one
and A45:
rng G = Carrier ((1 / (1 - (L . v))) * (L - K))
and A46:
for
n being
Nat st
n in dom F holds
F . n = (((1 / (1 - (L . v))) * (L - K)) . (G . n)) * (((G . n) |-- If) . x)
by A2, A29, A38, A31, A33, A40;
Sum ((1 / (1 - (L . v))) * (L - K)) in Affin If
by A2, A29, A38, A31, A33, A40, A41;
then A47:
(Sum L) |-- If = ((1 - (L . v)) * ((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If)) + ((L . v) * (v |-- If))
by A5, A7, A25, A39, RLAFFIN1:70;
take F1 =
((1 - (L . v)) * F) ^ <*((L . v) * ((v |-- If) . x))*>;
ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F1 & len G = len F1 & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F1 holds
F1 . n = (L . (G . n)) * (((G . n) |-- If) . x) ) )take G1 =
G ^ <*v*>;
( ((Sum L) |-- If) . x = Sum F1 & len G1 = len F1 & G1 is one-to-one & rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds
F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) )thus Sum F1 =
(Sum ((1 - (L . v)) * F)) + ((L . v) * ((v |-- If) . x))
by RVSUM_1:74
.=
((1 - (L . v)) * (((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If) . x)) + ((L . v) * ((v |-- If) . x))
by A42, RVSUM_1:87
.=
(((1 - (L . v)) * ((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If)) . x) + ((L . v) * ((v |-- If) . x))
by RLVECT_2:def 11
.=
(((1 - (L . v)) * ((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If)) . x) + (((L . v) * (v |-- If)) . x)
by RLVECT_2:def 11
.=
((Sum L) |-- If) . x
by A47, RLVECT_2:def 10
;
( len G1 = len F1 & G1 is one-to-one & rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds
F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) )reconsider f =
F as
Element of
(len F) -tuples_on REAL by FINSEQ_2:92;
A48:
len F = len ((1 - (L . v)) * f)
by CARD_1:def 7;
then A49:
len F1 = (len F) + 1
by FINSEQ_2:16;
hence
len F1 = len G1
by A43, FINSEQ_2:16;
( G1 is one-to-one & rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds
F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) )A50:
rng <*v*> = {v}
by FINSEQ_1:38;
then
(
<*v*> is
one-to-one &
rng G misses rng <*v*> )
by A40, A45, FINSEQ_3:93, XBOOLE_1:79;
hence
G1 is
one-to-one
by A44, FINSEQ_3:91;
( rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds
F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) )thus rng G1 =
(B \ {v}) \/ {v}
by A40, A45, A50, FINSEQ_1:31
.=
Carrier L
by A7, A25, ZFMISC_1:116
;
for n being Nat st n in dom F1 holds
F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x)let n be
Nat;
( n in dom F1 implies F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) )assume A51:
n in dom F1
;
F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x)then A52:
n <= len F1
by FINSEQ_3:25;
per cases
( ( 1 <= n & n <= len F ) or n = (len F) + 1 )
by A49, A51, A52, FINSEQ_3:25, NAT_1:8;
suppose A53:
( 1
<= n &
n <= len F )
;
F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x)then
n in dom F
by FINSEQ_3:25;
then A54:
(
((1 - (L . v)) * f) . n = (1 - (L . v)) * (f . n) &
F . n = (((1 / (1 - (L . v))) * (L - K)) . (G . n)) * (((G . n) |-- If) . x) )
by A46, RVSUM_1:45;
A55:
n in dom G
by A43, A53, FINSEQ_3:25;
then A56:
G1 . n = G . n
by FINSEQ_1:def 7;
A57:
G . n in B \ {v}
by A40, A45, A55, FUNCT_1:def 3;
then
not
G . n in {v}
by XBOOLE_0:def 5;
then
K . (G . n) = 0
by A34, A57;
then
(L - K) . (G . n) = (L . (G . n)) - 0
by A57, RLVECT_2:54;
then
((1 / (1 - (L . v))) * (L - K)) . (G . n) = (1 / (1 - (L . v))) * (L . (G . n))
by A57, RLVECT_2:def 11;
then
(1 - (L . v)) * (((1 / (1 - (L . v))) * (L - K)) . (G1 . n)) = ((1 - (L . v)) * (1 / (1 - (L . v)))) * (L . (G . n))
by A56;
then A58:
(1 - (L . v)) * (((1 / (1 - (L . v))) * (L - K)) . (G1 . n)) = L . (G . n)
by A38;
n in dom ((1 - (L . v)) * F)
by A48, A53, FINSEQ_3:25;
hence
F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x)
by A54, A56, A58, FINSEQ_1:def 7;
verum end; end; end; end;
end;
let L be Linear_Combination of Af; ( Af c= conv If & sum L = 1 implies ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) )
assume that
A60:
Af c= conv If
and
A61:
sum L = 1
; ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) )
set C = Carrier L;
Carrier L c= Af
by RLVECT_2:def 6;
then A62:
Carrier L c= conv If
by A60;
reconsider L1 = L as Linear_Combination of Carrier L by RLVECT_2:def 6;
A63:
S1[ 0 ]
for m being Nat holds S1[m]
from NAT_1:sch 2(A63, A1);
then
( sum L = sum L1 & S1[ card (Carrier L)] )
;
hence
( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) )
by A61, A62; verum