:: The Real Vector Spaces of Finite Sequences Are Finite Dimensional
:: by Yatsuka Nakamura , Artur Korni{\l}owicz , Nagato Oya and Yasunari Shidama
::
:: Received September 23, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, SUBSET_1, FINSEQ_2, EUCLID, VALUED_0, FINSEQ_1,
FUNCT_1, RELAT_1, XBOOLE_0, TARSKI, FUNCT_2, CARD_1, ARYTM_1, ARYTM_3,
REAL_1, PARTFUN1, ZFMISC_1, ORDINAL2, XXREAL_0, RLVECT_1, RLSUB_1,
STRUCT_0, SUPINF_2, ALGSTR_0, REALSET1, MONOID_0, FUNCT_7, AFINSQ_1,
RFINSEQ2, CLASSES1, RVSUM_1, COMPLEX1, SQUARE_1, REWRITE1, SETFAM_1,
CARD_3, ORDINAL4, MATRIXR2, BINOP_2, XCMPLX_0, REAL_NS1, VALUED_1,
RLVECT_2, MATRIX_7, FUNCOP_1, FUNCSDOM, RLVECT_3, FINSET_1, RLVECT_5,
EUCLID_7, NUMBER09;
notations XBOOLE_0, TARSKI, RELAT_1, FUNCT_1, RVSUM_1, RELSET_1, PARTFUN1,
CARD_1, FUNCT_2, FUNCT_3, ORDINAL1, CLASSES1, NUMBERS, SUBSET_1,
XCMPLX_0, XREAL_0, COMPLEX1, FINSEQ_1, FINSEQ_2, VALUED_0, VALUED_1,
FINSET_1, BINOP_1, STRUCT_0, ALGSTR_0, FUNCSDOM, MONOID_0, BINOP_2,
RLVECT_1, EUCLID, SQUARE_1, XXREAL_0, SETFAM_1, RLSUB_1, RLVECT_2,
RLVECT_3, REAL_1, NAT_1, NAT_D, MATRIXR2, ZFMISC_1, RLVECT_5, REALSET1,
MATRIX_7, RFINSEQ2, FINSEQ_7, RUSUB_3, REAL_NS1, DOMAIN_1, RUSUB_4,
FUNCOP_1;
constructors REAL_1, SQUARE_1, BINOP_2, MONOID_0, RLVECT_2, RLVECT_3,
REAL_NS1, FUNCT_3, REALSET1, MATRIXR2, RLVECT_5, FINSOP_1, MATRIX_7,
RFINSEQ2, SETWISEO, FINSEQ_7, RUSUB_3, RUSUB_4, NAT_D, CLASSES1,
FUNCSDOM, RELSET_1, NUMBERS;
registrations FUNCT_1, MONOID_0, RELSET_1, NUMBERS, XREAL_0, STRUCT_0,
FINSET_1, XXREAL_0, CARD_1, NAT_1, MEMBERED, FINSEQ_2, EUCLID, VALUED_0,
FUNCT_2, SUBSET_1, XBOOLE_0, REAL_NS1, FINSEQ_1, RELAT_1, ORDINAL1,
SQUARE_1;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
definitions TARSKI, RLVECT_3, MONOID_0;
equalities SQUARE_1, FINSEQ_2, RVSUM_1, VALUED_1, RLVECT_1, BINOP_1, STRUCT_0,
ALGSTR_0, FUNCSDOM, EUCLID, ORDINAL1;
expansions TARSKI, RVSUM_1, STRUCT_0, MONOID_0;
theorems EUCLID, RVSUM_1, FINSEQ_2, FINSEQ_1, RFUNCT_1, FINSEQ_3, SQUARE_1,
ABSVALUE, JORDAN2C, XREAL_1, XXREAL_0, FUNCOP_1, XCMPLX_1, SUBSET_1,
XBOOLE_0, XBOOLE_1, EUCLID_2, TARSKI, EUCLID_4, ORDINAL1, CARD_1,
SETFAM_1, REAL_NS1, RLVECT_2, RLVECT_3, PARTFUN1, FUNCT_1, RLVECT_1,
NAT_1, RLSUB_1, RELAT_1, REALSET1, FUNCT_2, MATRIXR2, BINOP_2, FINSOP_1,
ZFMISC_1, FUNCT_3, FINSEQ_4, MATRPROB, MATRIX_7, RFINSEQ2, INTEGRA2,
FINSEQ_7, INT_5, EUCLIDLP, RLVECT_5, RUSUB_1, RUSUB_3, RUSUB_4, RLVECT_4,
VALUED_0, XREAL_0, VALUED_1, CLASSES1, RELSET_1, FUNCSDOM, EULER_1,
NUMBERS;
schemes NAT_1, CLASSES1, FUNCT_2, FINSEQ_1;
begin :: 1. Preliminaries
reserve i, j, m, n for Nat,
z, B0 for set,
f, x0 for real-valued FinSequence;
::$CT
theorem Th1:
for R being Relation, Y being set st rng R c= Y holds R"Y = dom R
proof
let R be Relation, Y be set;
assume rng R c= Y;
then rng R /\ Y = rng R by XBOOLE_1:28;
hence R"Y = R"rng R by RELAT_1:133
.= dom R by RELAT_1:134;
end;
Lm1: for X being set, Y being non empty set, f being Function of X,Y
st f is bijective holds card X = card Y by EULER_1:11;
theorem
<* z *> * <* 1 *> = <* z *>
proof
A1: dom <* z *>=Seg 1 by FINSEQ_1:38;
rng <* 1 *>= {1} by FINSEQ_1:38;
then
A2: dom (<* z *>*<* 1 *>)=dom <* 1 *> by A1,FINSEQ_1:2,RELAT_1:27;
A3: dom <* 1 *> = Seg 1 by FINSEQ_1:38;
then 1 in dom <* 1 *> by FINSEQ_1:2,TARSKI:def 1;
then (<* z *>*<* 1 *>).1 =<* z *>.((<* 1 *>).1) by FUNCT_1:13
.=<* z *>.1
.= z;
hence thesis by A3,A2,FINSEQ_1:def 8;
end;
theorem
for x being Element of REAL 0 holds x = <*>REAL;
theorem Th4:
for a,b,c being Element of REAL n holds a - b + c + b = a + c
proof
let a,b,c be Element of REAL n;
reconsider a2=a,b2=b,c2=c as Element of n-tuples_on REAL;
a2-b2+c2+b2=a2+-b2+b2+c2 by RFUNCT_1:8
.=a2+(b2+-b2)+c2 by RFUNCT_1:8
.=a2+(n|->In(0,REAL))+c2 by RVSUM_1:22
.=a2+c2 by RVSUM_1:16;
hence thesis;
end;
registration
let f1,f2 be FinSequence;
cluster <:f1,f2:> -> FinSequence-like;
coherence
proof
dom <:f1,f2:> = dom f1 /\ dom f2 by FUNCT_3:def 7;
hence thesis by VALUED_1:19;
end;
end;
definition
let D be set, f1,f2 be FinSequence of D;
redefine func <:f1,f2:> -> FinSequence of [:D,D:]; :: redefines <: (FUNCT_3, definition)
coherence
proof
A1: [: rng f1,rng f2 :] c= [:D,D:] by ZFMISC_1:96;
rng (<:f1,f2:>) c= [: rng f1,rng f2 :] by FUNCT_3:51;
then rng (<:f1,f2:>) c= [:D,D:] by A1;
hence thesis by FINSEQ_1:def 4;
end;
end;
Lm2: n<m implies ex k being Nat st m=n+1+k
proof
assume
A1: n<m;
then consider k1 be Nat such that
A2: m = n+k1 by NAT_1:10;
k1 <> 0 by A1,A2;
then consider n1 be Nat such that
A3: k1=n1+1 by NAT_1:6;
take n1;
thus m=n+1+n1 by A2,A3;
end;
definition
let h be real-valued FinSequence;
redefine attr h is increasing means :: redefines increasing (VALUED_0, definition)
for i being Nat st 1<=i & i<len h holds h.i < h.(i+1);
compatibility
proof
hereby
assume
A1: h is increasing;
let i be Nat such that
A2: 1<=i and
A3: i<len h;
A4: 1 <= i+1 by NAT_1:12;
i+1 <= len h by A3,NAT_1:13;
then
A5: i+1 in dom h by A4,FINSEQ_3:25;
A6: i < i+1 by NAT_1:16;
i in dom h by A2,A3,FINSEQ_3:25;
hence h.i < h.(i+1) by A1,A5,A6,VALUED_0:def 13;
end;
assume
A7: for i being Nat st 1<=i & i<len h holds h.i < h.(i+1);
now
let n, m be ExtReal;
assume
A8: n in dom h;
assume
A9: m in dom h;
then reconsider m1=m, n1=n as Element of NAT by A8;
defpred X[Nat] means n1+$1 < len h implies h.n < h.(n1+1+$1);
A10: now
let a be Nat such that
A11: X[a];
thus X[a+1]
proof
A12: n1+a+0 < n1+a+1 by XREAL_1:6;
assume
A13: n1+(a+1) < len h;
1 <= 1+(n1+a) by NAT_1:11;
then h.(n1+1+a)<h.(n1+1+a+1) by A7,A13;
hence thesis by A11,A13,A12,XXREAL_0:2;
end;
end;
1 <= n by A8,FINSEQ_3:25;
then
A14: X[0] by A7;
A15: for k being Nat holds X[k] from NAT_1:sch 2(A14,A10);
assume n < m;
then consider k being Nat such that
A16: m1 = n1+1+k by Lm2;
m <= len h by A9,FINSEQ_3:25;
then m1-1 < len h-0 by XREAL_1:15;
then n1+k < len h by A16;
hence h.n < h.m by A16,A15;
end;
hence thesis by VALUED_0:def 13;
end;
end;
theorem Th5:
for h being real-valued FinSequence st h is increasing holds for
i,j being Nat st i<j & 1<=i & j<=len h holds h.i < h.j
proof
let h be real-valued FinSequence;
assume
A1: h is increasing;
let i,j be Nat;
assume that
A2: i<j and
A3: 1<=i and
A4: j<=len h;
defpred P[Nat] means i+1+$1<=len h implies h.i<h.(i+1+$1);
A5: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A6: P[k];
i+1+(k+1)<=len h implies h.i<h.(i+1+(k+1))
proof
A7: i+1<=i+1+k by NAT_1:11;
i<i+1 by XREAL_1:29;
then i<i+1+k by A7,XXREAL_0:2;
then
A8: 1<i+1+k by A3,XXREAL_0:2;
k<k+1 by XREAL_1:29;
then
A9: i+1+k<i+1+(k+1) by XREAL_1:6;
assume
A10: i+1+(k+1)<=len h;
then i+1+k<len h by A9,XXREAL_0:2;
then h.(i+1+k)<h.(i+1+k+1) by A1,A8;
hence h.i<h.(i+1+(k+1)) by A6,A10,A9,XXREAL_0:2;
end;
hence P[k+1];
end;
i<len h by A2,A4,XXREAL_0:2;
then
A11: P[0] by A1,A3;
for k being Nat holds P[k] from NAT_1:sch 2(A11,A5);
then
A12: i+1+(j-'(i+1))<=len h implies h.i<h.(i+1+(j-'(i+1)));
i+1<=j by A2,NAT_1:13;
then j-'(i+1)=j-(i+1) by XREAL_1:233;
hence h.i<h.j by A4,A12;
end;
theorem Th6:
for h being real-valued FinSequence st h is increasing holds for
i,j being Nat st i<=j & 1<=i & j<=len h holds h.i <= h.j
proof
let h be real-valued FinSequence;
assume
A1: h is increasing;
let i,j be Nat;
assume that
A2: i<=j and
A3: 1<=i and
A4: j<=len h;
i<j or i=j by A2,XXREAL_0:1;
hence thesis by A1,A3,A4,Th5;
end;
theorem Th7:
for h being natural-valued FinSequence st h is increasing holds
for i being Nat st i<=len h & 1<=h.1 holds i <= h.i
proof
let h be natural-valued FinSequence;
assume
A1: h is increasing;
defpred P[Nat] means $1<=len h implies $1 <= h.$1;
let i be Nat;
assume that
A2: i<=len h and
A3: 1<=h.1;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A5: P[k];
k+1<=len h implies k+1 <= h.(k+1)
proof
A6: k<k+1 by XREAL_1:29;
assume
A7: k+1<=len h;
then
A8: k<len h by A6,XXREAL_0:2;
per cases;
suppose
k=0;
hence k+1<=h.(k+1) by A3;
end;
suppose
k>0;
then 0+1<=k by NAT_1:13;
then h.k < h.(k+1) by A1,A8;
then k<h.(k+1) by A5,A7,A6,XXREAL_0:2;
hence k+1<=h.(k+1) by NAT_1:13;
end;
end;
hence P[k+1];
end;
A9: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A9,A4);
hence i<=h.i by A2;
end;
theorem Th8:
for V being RealLinearSpace, X being Subspace of V st V is
strict & X is strict & the carrier of X = the carrier of V holds X = V
proof
let V be RealLinearSpace, X be Subspace of V;
assume that
A1: V is strict and
A2: X is strict and
A3: the carrier of X=the carrier of V;
A4: the Mult of X = (the Mult of V) | ( [:REAL,the carrier of V:] ) by A3,
RLSUB_1:def 2
.= the Mult of V;
A5: 0. X = 0. V by RLSUB_1:def 2;
the addF of X = (the addF of V) || (the carrier of V) by A3,RLSUB_1:def 2
.= (the addF of V) | ( [:the carrier of V,the carrier of V:] ) by
REALSET1:def 2
.=the addF of V;
hence X=V by A1,A2,A3,A5,A4;
end;
definition
let D be set;
let F be FinSequence of D;
let h be Permutation of dom F;
func F(*)h -> FinSequence of D equals
F*h;
coherence
proof
reconsider G=F as Function;
A1: h"(dom G)=h"(rng (h)) by FUNCT_2:def 3
.=dom (h) by RELAT_1:134;
dom (G*h) = h"(dom G) by RELAT_1:147
.=dom F by A1,FUNCT_2:52
.= Seg len F by FINSEQ_1:def 3;
then
A2: F*h is FinSequence by FINSEQ_1:def 2;
rng(F*h) c= D;
hence thesis by A2,FINSEQ_1:def 4;
end;
end;
theorem Th9:
for D being non empty set,f being FinSequence of D st 1<=i & i<=
len f & 1<=j & j<=len f holds (Swap(f,i,j)).i=f.j & (Swap(f,i,j)).j=f.i
proof
let D be non empty set,f be FinSequence of D;
assume that
A1: 1<=i and
A2: i<=len f and
A3: 1<=j and
A4: j<=len f;
A5: len Replace(f, i, f/.j)=len f by FINSEQ_7:5;
A6: len (Swap(f,i,j))=len f by FINSEQ_7:18;
then (Swap(f,i,j))/.j=(Swap(f,i,j)).j by A3,A4,FINSEQ_4:15;
then
A7: (Swap(f,i,j)).j =(Replace(Replace(f, i, f/.j), j, f/.i))/.j by A1,A2,A3,A4,
FINSEQ_7:def 2
.=f/.i by A3,A4,A5,FINSEQ_7:8
.=f.i by A1,A2,FINSEQ_4:15;
A8: Swap(f,i,j)=Swap(f,j,i) by FINSEQ_7:21;
A9: len Replace(f, j, f/.i)=len f by FINSEQ_7:5;
(Swap(f,i,j))/.i=(Swap(f,i,j)).i by A1,A2,A6,FINSEQ_4:15;
then
(Swap(f,i,j)).i =(Replace(Replace(f, j, f/.i), i, f/.j))/.i by A1,A2,A3,A4,A8
,FINSEQ_7:def 2
.=f/.j by A1,A2,A9,FINSEQ_7:8
.=f.j by A3,A4,FINSEQ_4:15;
hence thesis by A7;
end;
theorem Th10:
{} is Permutation of {}
proof
A1: rng {}={};
dom {}={};
then reconsider f={} as Function of {},{} by A1,FUNCT_2:1;
f is one-to-one onto Function of {},{} by A1,FUNCT_2:def 3;
hence thesis;
end;
theorem
<* 1 *> is Permutation of {1}
proof
set g=<* 1 *>;
A1: rng g={1} by FINSEQ_1:38;
dom g={1} by FINSEQ_1:2,38;
then reconsider f=g as Function of {1},{1} by A1,FUNCT_2:1;
f is one-to-one onto Function of {1},{1} by A1,FUNCT_2:def 3;
hence thesis;
end;
theorem Th12:
for h being FinSequence of REAL holds
h is one-to-one iff sort_a h is one-to-one
proof
let h be FinSequence of REAL;
A1: h,(sort_a h) are_fiberwise_equipotent by RFINSEQ2:def 6;
then ex H be Function st dom H = dom (sort_a h) & rng H = dom h & H is
one-to-one & (sort_a h) = h*H by CLASSES1:77;
hence h is one-to-one implies sort_a h is one-to-one;
ex G be Function st dom G = dom (h) & rng G = dom (sort_a h) & G is
one-to-one & (h) = (sort_a h) *G by A1,CLASSES1:77;
hence sort_a h is one-to-one implies h is one-to-one;
end;
theorem Th13:
for h being FinSequence of NAT st h is one-to-one ex h3 being
Permutation of dom h,h2 being FinSequence of NAT st h2=h*h3 & h2 is increasing
& dom h=dom h2 & rng h=rng h2
proof
let h be FinSequence of NAT;
assume
A1: h is one-to-one;
per cases;
suppose
A2: dom h <> {};
rng h c= REAL by NUMBERS:19;
then reconsider hr=h as FinSequence of REAL by FINSEQ_1:def 4;
A3: hr,(sort_a hr) are_fiberwise_equipotent by RFINSEQ2:def 6;
then consider H be Function such that
A4: dom H = dom (sort_a hr) and
A5: rng H = dom hr and
A6: H is one-to-one and
A7: (sort_a hr) = hr*H by CLASSES1:77;
rng (sort_a hr)=rng hr by A3,CLASSES1:75;
then reconsider h4=sort_a hr as FinSequence of NAT by FINSEQ_1:def 4;
A8: rng h=rng h4 by A5,A7,RELAT_1:28;
A9: dom h4=Seg len h4 by FINSEQ_1:def 3;
for i being Nat st 1<=i & i<len h4 holds h4.i < h4.(i+1)
proof
let i be Nat;
assume that
A10: 1<=i and
A11: i<len h4;
A12: i+1<=len h4 by A11,NAT_1:13;
A13: i in dom h4 by A9,A10,A11,FINSEQ_1:1;
1<i+1 by A10,XREAL_1:29;
then
A14: i+1 in dom h4 by A9,A12,FINSEQ_1:1;
A15: h4 is one-to-one by A1,Th12;
A16: now
assume h4.i=h4.(i+1);
then i=i+1 by A14,A13,A15,FUNCT_1:def 4;
hence contradiction;
end;
h4.i<=h4.(i+1) by A14,A13,INTEGRA2:def 1;
hence h4.i < h4.(i+1) by A16,XXREAL_0:1;
end;
then
A17: h4 is increasing;
dom (sort_a hr)=dom hr by RFINSEQ2:31;
then reconsider H2=H as Function of dom h,dom h by A4,A5,FUNCT_2:1;
H2 is onto by A5,FUNCT_2:def 3;
then reconsider h5=H as Permutation of dom h by A6;
A18: h4=h*h5 by A7;
dom h=dom h5 by A2,FUNCT_2:def 1
.= dom h4 by A4;
hence thesis by A18,A17,A8;
end;
suppose
A19: dom h={};
then rng h={} by RELAT_1:42;
then reconsider h5=h as Function of {},{} by A19,FUNCT_2:1;
reconsider h22=h*h5 as FinSequence of NAT;
h22 is increasing;
hence thesis by A19,Th10;
end;
end;
begin :: 2. Orthogonal Basis of REAL n
definition
let B0 be set;
attr B0 is R-orthogonal means
:Def3:
for x, y being real-valued FinSequence
st x in B0 & y in B0 & x<>y holds |( x,y )| = 0;
end;
registration
cluster empty -> R-orthogonal for set;
coherence;
end;
theorem
B0 is R-orthogonal iff for x,y being real-valued FinSequence st x in
B0 & y in B0 & x <> y holds x,y are_orthogonal
proof
thus B0 is R-orthogonal implies for x,y being real-valued FinSequence st x
in B0 & y in B0 & x <> y holds x,y are_orthogonal;
assume
A1: for x,y being real-valued FinSequence st x in B0 & y in B0 & x <> y
holds x,y are_orthogonal;
let x,y be real-valued FinSequence;
assume that
A2: x in B0 and
A3: y in B0 and
A4: x<>y;
x,y are_orthogonal by A1,A2,A3,A4;
hence |( x,y )|=0;
end;
definition
let B0 be set;
attr B0 is R-normal means
:Def4:
for x being real-valued FinSequence st x in B0 holds |.x.| = 1;
end;
registration
cluster empty -> R-normal for set;
coherence;
end;
registration
cluster R-normal for set;
existence
proof
take {};
thus thesis;
end;
end;
registration
let B0, B1 be R-normal set;
cluster B0 \/ B1 -> R-normal;
coherence
proof
let x be real-valued FinSequence;
assume x in B0 \/ B1;
then x in B0 or x in B1 by XBOOLE_0:def 3;
hence thesis by Def4;
end;
end;
theorem Th15:
|.f.| = 1 implies {f} is R-normal by TARSKI:def 1;
theorem Th16:
B0 is R-normal & |.x0.| = 1 implies B0 \/ {x0} is R-normal
proof
assume that
A1: B0 is R-normal and
A2: |.x0.| =1;
{x0} is R-normal by A2,Th15;
hence B0 \/ {x0} is R-normal by A1;
end;
definition
let B0 be set;
attr B0 is R-orthonormal means
B0 is R-orthogonal R-normal;
end;
registration
cluster R-orthonormal -> R-orthogonal R-normal for set;
coherence;
cluster R-orthogonal R-normal -> R-orthonormal for set;
coherence;
end;
registration
cluster { <*1*> } -> R-orthonormal;
coherence
proof
set B0 = { <*1*> };
thus for x, y being real-valued FinSequence st x in B0 & y in B0 & x<>y
holds |( x,y )| = 0
proof
let x, y be real-valued FinSequence;
assume that
A1: x in B0 and
A2: y in B0;
x = <*1*> by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
let x be real-valued FinSequence;
assume x in B0;
then x = <*1*> by TARSKI:def 1;
then sqr x = <*1^2*> by RVSUM_1:55;
hence thesis by RVSUM_1:73,SQUARE_1:18;
end;
end;
registration
cluster R-orthonormal non empty for set;
existence
proof
take {<*1*>};
thus thesis;
end;
end;
registration
let n;
cluster R-orthonormal for Subset of REAL n;
existence
proof
{}(REAL n) is R-orthonormal;
hence thesis;
end;
end;
definition
let n be Nat;
let B0 be Subset of REAL n;
attr B0 is complete means
:Def6:
for B being R-orthonormal Subset of REAL n st B0 c= B holds B = B0;
end;
definition
let n be Nat, B0 be Subset of REAL n;
attr B0 is orthogonal_basis means
B0 is R-orthonormal complete;
end;
registration
let n be Nat;
cluster orthogonal_basis -> R-orthonormal complete for Subset of REAL n;
coherence;
cluster R-orthonormal complete -> orthogonal_basis for Subset of REAL n;
coherence;
end;
theorem Th17:
for B0 being Subset of REAL 0 st B0 is orthogonal_basis holds B0 = {}
proof
let B0 be Subset of REAL 0;
assume that
A1: B0 is orthogonal_basis and
A2: B0 <> {};
set x = the Element of B0;
x in B0 by A2;
then reconsider x0=x as Element of REAL 0;
|( (0*(len x0)),0*(len x0) )| =0 by EUCLID_2:9; then
|. 0*(len x0) .| =0;
hence contradiction by A1,A2,Def4;
end;
theorem
for B0 being Subset of REAL n,y being Element of REAL n st B0 is
orthogonal_basis & (for x being Element of REAL n st x in B0 holds |(x,y)|=0)
holds y=0*n
proof
let B0 be Subset of REAL n,y be Element of REAL n;
assume that
A1: B0 is orthogonal_basis and
A2: for x being Element of REAL n st x in B0 holds |(x,y)|=0;
now
reconsider y1=(1/(|.y.|))*y as Element of REAL n;
reconsider B1=B0 \/ {y1} as Subset of REAL n;
y1 in {y1} by TARSKI:def 1;
then
A3: y1 in B1 by XBOOLE_0:def 3;
A4: len y=n by CARD_1:def 7;
for x2,y2 being real-valued FinSequence st x2 in B1 & y2 in B1 & x2<>
y2 holds |(x2,y2)|=0
proof
let x2,y2 be real-valued FinSequence;
assume that
A5: x2 in B1 and
A6: y2 in B1 and
A7: x2<>y2;
reconsider X2=x2, Y2=y2 as Element of REAL n by A5,A6;
A8: len Y2=n by CARD_1:def 7;
per cases by A5,XBOOLE_0:def 3;
suppose
A9: x2 in B0;
per cases by A6,XBOOLE_0:def 3;
suppose
y2 in B0;
hence |(x2,y2)|=0 by A1,A7,A9,Def3;
end;
suppose
A10: y2 in {y1};
A11: len X2=n by CARD_1:def 7;
|(x2,y)|=0 by A2,A9;
then
A12: (1/(|.y.|))*|(x2,y)|=0;
y2=y1 by A10,TARSKI:def 1;
hence |(x2,y2)|=0 by A4,A11,A12,RVSUM_1:121;
end;
end;
suppose
A13: x2 in {y1};
then x2=y1 by TARSKI:def 1;
then not y2 in {y1} by A7,TARSKI:def 1;
then y2 in B0 by A6,XBOOLE_0:def 3;
then |(y2,y)|=0 by A2;
then (1/(|.y.|))*|(y2,y)|=0;
then |(Y2,(1/(|.y.|))*y)|=0 by A4,A8,RVSUM_1:121;
hence |(x2,y2)|=0 by A13,TARSKI:def 1;
end;
end;
then
A14: B1 is R-orthogonal;
assume
A15: y <> 0*n;
A16: |.y1.|= (|.1/(|.y.|).|)*(|.y.|) by EUCLID:11
.= (1/(|.y.|))*(|.y.|) by ABSVALUE:def 1
.=1 by A15,EUCLID:8,XCMPLX_1:106;
for x being real-valued FinSequence st x in B1 holds |.x.|=1
proof
let x be real-valued FinSequence;
assume x in B1;
then x in B0 or x in {y1} by XBOOLE_0:def 3;
hence |.x.|=1 by A1,A16,Def4,TARSKI:def 1;
end;
then
A17: B1 is R-normal;
A18: len y1=n by CARD_1:def 7;
A19: now
assume y1 in B0;
then |(y1,y)|=0 by A2;
then (1/(|.y.|))*|(y1,y)|=0;
then |(y1,(1/(|.y.|))*y)|=0 by A4,A18,RVSUM_1:121;
hence contradiction by A16;
end;
B0 c= B1 by XBOOLE_1:7;
hence contradiction by A1,A19,A3,A14,A17,Def6;
end;
hence y=0*n;
end;
begin :: 3. Linear Manifolds
definition
let n;
let X be Subset of REAL n;
attr X is linear_manifold means
for x, y being Element of REAL n, a,b
being Element of REAL st x in X & y in X holds a*x+b*y in X;
end;
registration
let n;
cluster [#](REAL n) -> linear_manifold;
coherence
proof
let x,y be Element of REAL n, a,b be Element of REAL;
assume that
x in [#](REAL n) and
y in [#](REAL n);
a*x+b*y in REAL n;
hence thesis by SUBSET_1:def 3;
end;
end;
theorem Th19:
{ 0*n } is linear_manifold
proof
let x, y be Element of REAL n, a,b be Element of REAL;
assume that
A1: x in {0*n} and
A2: y in {0*n};
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
A3: y=0*n by A2,TARSKI:def 1;
x= 0*n by A1,TARSKI:def 1;
then a*x+b*y =0*nn + b*(0*nn) by A3,EUCLID_4:2
.=0*nn + (0*nn) by EUCLID_4:2
.= 0*nn by EUCLID_4:1;
hence a*x+b*y in { 0*n} by TARSKI:def 1;
end;
registration
let n;
cluster { 0*n } -> linear_manifold for Subset of REAL n;
coherence by Th19;
end;
definition
let n;
let X be Subset of REAL n;
func L_Span X -> Subset of REAL n equals
meet {Y where Y is Subset of REAL n
: Y is linear_manifold & X c= Y};
correctness
proof
X c= REAL n;
then X c= [#](REAL n) by SUBSET_1:def 3;
then
[#](REAL n) in {Y where Y is Subset of REAL n: Y is linear_manifold &
X c= Y};
hence thesis by SETFAM_1:7;
end;
end;
registration
let n;
let X be Subset of REAL n;
cluster L_Span X -> linear_manifold;
coherence
proof
X c= REAL n;
then X c= [#](REAL n) by SUBSET_1:def 3;
then
[#](REAL n) in {Y where Y is Subset of REAL n: Y is linear_manifold &
X c= Y};
then reconsider
Z={Y where Y is Subset of REAL n: Y is linear_manifold & X c= Y
} as non empty set;
let x,y be Element of REAL n, a,b be Element of REAL;
assume that
A1: x in (L_Span X) and
A2: y in (L_Span X);
A3: for Y4 being set st Y4 in {Y where Y is Subset of REAL n: Y is
linear_manifold & X c= Y} holds a*x+b*y in Y4
proof
let Y4 be set;
assume
A4: Y4 in {Y where Y is Subset of REAL n: Y is linear_manifold & X c= Y};
then
A5: ex Y0 being Subset of REAL n st Y4=Y0 & Y0 is linear_manifold & X c= Y0;
A6: y in Y4 by A2,A4,SETFAM_1:def 1;
x in Y4 by A1,A4,SETFAM_1:def 1;
hence a*x+b*y in Y4 by A6,A5;
end;
Z <>{};
hence a*x+b*y in (L_Span X) by A3,SETFAM_1:def 1;
end;
end;
definition
let n be Nat,f be FinSequence of REAL n;
func accum f -> FinSequence of REAL n means :Def10:
len f = len it & f.1 = it.1 &
for i being Nat st 1<=i & i<len f holds it.(i+1) = (it/.i) + (f/.(i+1));
existence
proof
per cases;
suppose
A1: len f>0;
reconsider q=<* f/.1 *> as FinSequence of REAL n;
A2: 0+1<=len f by A1,NAT_1:13;
then f/.1=f.1 by FINSEQ_4:15;
then
A3: q.1=f.1;
defpred P[Nat] means $1+1<=len f implies ex g being FinSequence of REAL
n st $1+1 =len g & f.1=g.1 & (for i being Nat st 1<=i & i<$1+1 holds g.(i+1)=(g
/.i)+(f/.(i+1)));
A4: for i being Nat st 1<=i & i<0+1 holds q.(i+1)=(q/.i)+(f/.(i+1));
A5: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A6: P[k];
now
per cases;
case
A7: k+1+1<=len f;
k+1<k+1+1 by XREAL_1:29;
then consider g being FinSequence of REAL n such that
A8: k+1 =len g and
A9: f.1=g.1 and
A10: for i being Nat st 1<=i & i< k+1 holds g.(i+1)=(g/.i)+(f
/.(i+1)) by A6,A7,XXREAL_0:2;
reconsider g2=g^(<* g/.(k+1)+(f/.(k+1+1)) *>) as FinSequence of
REAL n;
A11: Seg len g = dom g by FINSEQ_1:def 3;
A12: len g2=len g+ len (<* g/.(k+1)+(f/.(k+1+1)) *>) by FINSEQ_1:22
.= k+1+1 by A8,FINSEQ_1:40;
A13: for i being Nat st 1<=i & i< k+1+1 holds g2.(i+1)=(g2/.i)+(f
/.(i+1))
proof
let i be Nat;
assume that
A14: 1<=i and
A15: i< k+1+1;
A16: i<=k+1 by A15,NAT_1:13;
per cases by A16,XXREAL_0:1;
suppose
A17: i<k+1;
A18: 1<=i+1 by NAT_1:12;
i+1<=k+1 by A17,NAT_1:13;
then i+1 in Seg len g by A8,A18,FINSEQ_1:1;
then
A19: g2.(i+1)=g.(i+1) by A11,FINSEQ_1:def 7;
i in Seg len g by A8,A14,A16,FINSEQ_1:1;
then
A20: g2.i=g.i by A11,FINSEQ_1:def 7;
A21: g/.i=g.i by A8,A14,A17,FINSEQ_4:15;
g2/.i=g2.i by A12,A14,A15,FINSEQ_4:15;
hence thesis by A10,A14,A17,A19,A20,A21;
end;
suppose
A22: i=k+1;
A23: g2/.i=g2.i by A12,A14,A15,FINSEQ_4:15;
i in Seg len g by A8,A14,A16,FINSEQ_1:1;
then
A24: g.i=g2.i by A11,FINSEQ_1:def 7;
g/.i=g.i by A8,A14,A16,FINSEQ_4:15;
hence thesis by A8,A22,A24,A23,FINSEQ_1:42;
end;
end;
1<=k+1 by NAT_1:11;
then 1 in Seg len g by A8,FINSEQ_1:1;
then g2.1=f.1 by A9,A11,FINSEQ_1:def 7;
hence P[k+1] by A12,A13;
end;
case
k+1+1>len f;
hence P[k+1];
end;
end;
hence P[k + 1];
end;
len f-'1=len f -1 by A2,XREAL_1:233;
then
A25: len f-'1+1=len f;
len q=1 by FINSEQ_1:40;
then
A26: P[0] by A3,A4;
for k being Nat holds P[k] from NAT_1:sch 2(A26,A5);
hence thesis by A25;
end;
suppose
A27: len f <= 0;
take f;
thus len f = len f & f.1 = f.1;
let i be Nat;
thus thesis by A27;
end;
end;
uniqueness
proof
let g1,g2 be FinSequence of REAL n;
assume that
A28: len f=len g1 and
A29: f.1=g1.1 and
A30: for i being Nat st 1<=i & i<len f holds g1.(i+1)=(g1/.i)+(f/.(i+1 ));
defpred P[Nat] means 1<=$1 & $1<=len f implies g1.$1=g2.$1;
assume that
A31: len f=len g2 and
A32: f.1=g2.1 and
A33: for i being Nat st 1<=i & i<len f holds g2.(i+1)=(g2/.i)+(f/.(i+1 ));
A34: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A35: P[k];
1<=k+1 & k+1<=len f implies g1.(k+1)=g2.(k+1)
proof
assume that
1<=k+1 and
A36: k+1<=len f;
A37: k<k+1 by XREAL_1:29;
then
A38: k< len f by A36,XXREAL_0:2;
per cases;
suppose
A39: 1<=k;
then
A40: g2.(k+1)=(g2/.k)+(f/.(k+1)) by A33,A38;
A41: k<=len g2 by A31,A36,A37,XXREAL_0:2;
A42: g1/.k=g1.k by A28,A38,A39,FINSEQ_4:15;
g1.(k+1)=(g1/.k)+(f/.(k+1)) by A30,A38,A39;
hence thesis by A35,A36,A37,A39,A40,A42,A41,FINSEQ_4:15,XXREAL_0:2;
end;
suppose
1>k;
then 0+1>k;
then k=0 by NAT_1:13;
hence g1.(k+1)=g2.(k+1) by A29,A32;
end;
end;
hence P[k+1];
end;
A43: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A43,A34);
hence g1=g2 by A28,A31,FINSEQ_1:14;
end;
end;
definition
let n be Nat;
let f be FinSequence of REAL n;
func Sum f -> Element of REAL n equals :Def11:
(accum f).len f if len f > 0 otherwise 0*n;
coherence
proof
A1: len f = len accum f by Def10;
now per cases;
case len f > 0;
then 0+1 <= len f by NAT_1:13;
then len f in dom accum f by A1,FINSEQ_3:25;
then (accum f).len f in rng accum f by FUNCT_1:def 3;
hence (accum f).len f is Element of REAL n;
end;
case len f <= 0;
hence thesis;
end;
end;
hence thesis;
end;
consistency;
end;
theorem Th20:
for F, F2 being FinSequence of REAL n,
h being Permutation of dom F st F2=F(*)h holds Sum F2=Sum F
proof
let F,F2 be FinSequence of REAL n, h be Permutation of dom F;
assume
A1: F2=F(*)h;
per cases;
suppose
A2: len F>0; then
A3: 0+1<=len F by NAT_1:13; then
A4: 1 in Seg len F by FINSEQ_1:1; then
A5: 1 in dom F by FINSEQ_1:def 3; then
A6: dom h=dom F by FUNCT_2:def 1;
then rng h=dom h by FUNCT_2:def 3; then
A7: dom F2=dom h by A1,RELAT_1:27; then
A8: Seg len F2=dom F by A6,FINSEQ_1:def 3;
set gF = accum F;
A9: len F = len gF by Def10;
A10: for i being Nat st 1<=i & i<len F holds gF.(i+1)=(gF/.i)+(F/.(i+1))
by Def10;
defpred P[Nat] means
for h2 being Permutation of dom F st $1<len F &
(for i being Nat st $1+1<i & i<=len F holds h2.i=i) holds
gF.($1+1)=(accum (F(*)h2)).($1+1);
A11: dom F=Seg len F by FINSEQ_1:def 3;
1 in Seg len F2 by A5,A6,A7,FINSEQ_1:def 3;
then
A12: 1<=len F2 by FINSEQ_1:1;
A13: len F-'1=len F-1 by A3,XREAL_1:233;
then
A14: for i being Nat st len F -'1+1<i & i<=len F holds h.i=i;
A15: dom F <> {} by A4,FINSEQ_1:def 3;
A16: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A17: P[k];
for h2 being Permutation of dom F st k+1<len F & (for i being Nat
st k+1+1<i & i<=len F holds h2.i=i) holds gF.(k+1+1)=(accum (F(*)h2)).(k+1+1)
proof
A18: 1<=k+1 by NAT_1:11;
A19: k+1<k+1+1 by XREAL_1:29;
let h2 be Permutation of dom F;
assume that
A20: k+1<len F and
A21: for i being Nat st k+1+1<i & i<=len F holds h2.i=i;
A22: k+1+1<=len F by A20,NAT_1:13;
k<k+1 by XREAL_1:29;
then
A23: k<len F by A20,XXREAL_0:2;
A24: 1<k+1+1 by XREAL_1:29;
then
A25: k+1+1 in Seg len F by A22,FINSEQ_1:1;
then
A26: k+1+1 in dom F by FINSEQ_1:def 3;
A27: dom h2=dom F by A5,FUNCT_2:def 1;
then
A28: rng h2=dom h2 by FUNCT_2:def 3;
then
A29: dom (F(*)h2)=dom h2 by RELAT_1:27
.=dom F by A5,FUNCT_2:def 1;
then
A30: Seg len (F(*)h2)=dom F by FINSEQ_1:def 3;
then
A31: Seg len (F(*)h2)=Seg len F by FINSEQ_1:def 3;
A32: len (F(*)h2)=len F by A30,FINSEQ_1:def 3;
h2 is FinSequence by A11,A27,FINSEQ_1:def 2;
then reconsider h2r=h2 as FinSequence of NAT by A27,A28,FINSEQ_1:def 4;
dom h2=Seg len F by A2,A11,FUNCT_2:def 1;
then
A33: len h2r=len F by FINSEQ_1:def 3;
consider x being object such that
A34: x in dom h2 and
A35: k+1+1=h2.x by A11,A27,A28,A25,FUNCT_1:def 3;
reconsider nx=x as Element of NAT by A27,A34;
A36: nx<=len F by A11,A34,FINSEQ_1:1;
reconsider h2b=Swap (h2r,nx,k+1+1) as FinSequence of NAT;
A37: rng h2b =rng h2 by FINSEQ_7:22
.=dom F by FUNCT_2:def 3;
A38: len h2b=len h2r by FINSEQ_7:18;
then dom h2b=Seg len h2r by FINSEQ_1:def 3;
then
A39: dom h2b=dom h2 by FINSEQ_1:def 3
.= dom F by A15,FUNCT_2:def 1;
then reconsider h2d=h2b as Function of dom F,dom F by A37,FUNCT_2:1;
A40: h2d is one-to-one by INT_5:39;
h2d is onto by A37,FUNCT_2:def 3;
then reconsider h4=h2d as Permutation of dom F by A40;
A41: 1<=nx by A11,A34,FINSEQ_1:1;
then
A42: h4.nx=h2r.(k+1+1) by A22,A24,A36,A33,Th9;
A43: dom h4=dom F by A5,FUNCT_2:def 1;
rng h4 c= dom F;
then
A44: dom (F(*)h4)=dom h4 by RELAT_1:27
.=dom F by A5,FUNCT_2:def 1;
then Seg len (F(*)h4)=dom F by FINSEQ_1:def 3;
then
A45: len (F(*)h4)=len F by FINSEQ_1:def 3;
per cases;
suppose
A46: nx<=k+1;
A47: k+1+1<=len h2r by A20,A33,NAT_1:13;
A48: nx<=len h2r by A11,A34,A33,FINSEQ_1:1;
A49: F.(k+1+1)=(F(*)h2).nx by A34,A35,FUNCT_1:13;
A50: len (accum (F(*)h4))=len (F(*)h4) by Def10;
A51: 1<=nx by A11,A34,FINSEQ_1:1;
A52: 1<=k+1+1 by NAT_1:11;
then
A53: h2b.(k+1+1)=k+1+1 by A35,A51,A48,A47,Th9;
A54: for i being Nat st k+1<i & i<=len F holds h4.i=i
proof
let i be Nat;
assume that
A55: k+1<i and
A56: i<=len F;
A57: k+1+1<=i by A55,NAT_1:13;
per cases;
suppose
A58: k+1+1<i;
1<=k+1 by NAT_1:11;
then
A59: 1<i by A55,XXREAL_0:2;
then h4.i=h2b/.i by A33,A38,A56,FINSEQ_4:15
.=h2r/.i by A33,A46,A55,A56,A58,A59,FINSEQ_7:30
.=h2.i by A33,A56,A59,FINSEQ_4:15
.=i by A21,A56,A58;
hence h4.i=i;
end;
suppose
k+1+1>=i;
then i=k+1+1 by A57,XXREAL_0:1;
hence h4.i=i by A35,A51,A48,A52,A47,Th9;
end;
end;
A60: F/.(k+1+1)=F.(k+1+1) by A22,A24,FINSEQ_4:15;
A61: 1<=k+1 by NAT_1:11;
A62: len (accum (F(*)h2))=len (F(*)h2) by Def10;
A63: nx<k+1+1 by A19,A46,XXREAL_0:2;
A64: for i4 being Nat st 1<=i4 & i4<nx holds (accum (F(*)h2)).i4=(
accum (F(*)h4)).i4
proof
defpred T[Nat] means 1+$1<nx implies (accum (F(*)h2)).(1+$1)=(
accum (F(*)h4)).(1+$1);
let i4 be Nat;
assume that
A65: 1<=i4 and
A66: i4<nx;
A67: 1+(i4-'1)=i4-1+1 by A65,XREAL_1:233
.=i4;
A68: for k3 being Nat st T[k3] holds T[k3+1]
proof
let k3 be Nat;
A69: 1<=k3+1 by NAT_1:11;
assume
A70: T[k3];
1+(k3+1)<nx implies (accum (F(*)h2)).(1+(k3+1))=(accum (F
(*)h4)).(1+(k3+1))
proof
assume
A71: 1+(k3+1)<nx;
then
A72: 1+(k3+1) <len F by A36,XXREAL_0:2;
then
A73: h2r/.(k3+1+1)=h2r.(k3+1+1) by A33,FINSEQ_4:15,NAT_1:11;
A74: (k3+1+1)<k+1+1 by A63,A71,XXREAL_0:2;
A75: h2b/.(k3+1+1)=h2b.(k3+1+1) by A33,A38,A72,FINSEQ_4:15,NAT_1:11;
1<=1+(k3+1) by NAT_1:11;
then k3+1+1 in Seg len F by A72,FINSEQ_1:1;
then
A76: k3+1+1 in dom (F(*)h2) by A29,FINSEQ_1:def 3;
then
A77: (F(*)h2).(k3+1+1)= F.(h2.(k3+1+1)) by FUNCT_1:12
.=F.(h4.(k3+1+1)) by A33,A71,A72,A74,A73,A75,FINSEQ_7:30
,NAT_1:11
.= (F(*)h4).(k3+1+1) by A44,A29,A76,FUNCT_1:12;
A78: (F(*)h4)/.(k3+1+1)=(F(*)h4).(k3+1+1) by A45,A72,FINSEQ_4:15
,NAT_1:11;
A79: k3+1<1+(k3+1) by XREAL_1:29;
then
A80: k3+1<nx by A71,XXREAL_0:2;
then
A81: k3+1<len F by A36,XXREAL_0:2;
k3+1<len (F(*)h2) by A36,A32,A80,XXREAL_0:2;
then
A82: (accum (F(*)h4))/.(1+k3)=(accum (F(*)h4)).(1+k3) by A45,A32,A50
,FINSEQ_4:15,NAT_1:11;
(accum (F(*)h2))/.(1+k3)=(accum (F(*)h2)).(1+k3) by A32,A62,A81
,FINSEQ_4:15,NAT_1:11;
then (accum (F(*)h2)).(1+(k3+1))= (accum (F(*)h4))/.(k3+1)+(F
(*)h2)/.(k3+1+1) by A32,A70,A69,A71,A79,A81,A82,Def10,XXREAL_0:2
.=(accum (F(*)h4))/.(k3+1)+(F(*)h4)/.(k3+1+1) by A32,A72,A77
,A78,FINSEQ_4:15,NAT_1:11;
hence (accum (F(*)h2)).(1+(k3+1))=(accum (F(*)h4)).(1+(k3+1))
by A45,A69,A81,Def10;
end;
hence T[k3+1];
end;
0<k+1;
then
A83: 1<>k+1+1;
A84: h2b/.1=h2b.1 by A3,A33,A38,FINSEQ_4:15;
A85: h2r/.1=h2r.1 by A3,A33,FINSEQ_4:15;
(F(*)h2).1= F.(h2.1) by A5,A29,FUNCT_1:12
.=F.(h4.1) by A3,A33,A65,A66,A83,A85,A84,FINSEQ_7:30
.= (F(*)h4).1 by A5,A44,FUNCT_1:12;
then (accum (F(*)h2)).(1+0)=(F(*)h4).1 by Def10
.=(accum (F(*)h4)).(1+0) by Def10;
then
A86: T[0];
for k3 being Nat holds T[k3] from NAT_1:sch 2(A86,A68);
hence (accum (F(*)h2)).i4=(accum (F(*)h4)).i4 by A66,A67;
end;
A87: for i being Nat st nx<=i & i<k+1+1 holds (accum (F(*)h2)).i= (
accum (F(*)h4))/.i-(F(*)h2)/.(k+1+1)+(F(*)h2)/.nx
proof
defpred S[Nat] means nx<=nx+$1 & nx+$1<k+1+1 implies (accum (F(*)
h2)).(nx+$1) =(accum (F(*)h4))/.(nx+$1)-(F(*)h2)/.(k+1+1)+(F(*)h2)/.nx;
let i be Nat;
assume that
A88: nx<=i and
A89: i<k+1+1;
A90: len (accum (F(*)h4))=len (F(*)h4) by Def10;
A91: len (accum (F(*)h2))=len (F(*)h2) by Def10;
A92: for k3 being Nat st S[k3] holds S[k3+1]
proof
let k3 be Nat;
assume
A93: S[k3];
nx<=nx+(k3+1) & nx+(k3+1)<k+1+1 implies (accum (F(*)h2)).(
nx+(k3+1)) =(accum (F(*)h4))/.(nx+(k3+1))-(F(*)h2)/.(k+1+1)+(F(*)h2)/.nx
proof
reconsider f3 = (F(*)h2)/.(nx+k3+1) as Element of REAL n;
A94: nx<=nx+k3 by NAT_1:11;
reconsider f2 = (F(*)h2)/.(k+1+1) as Element of REAL n;
A95: nx+k3<nx+k3+1 by XREAL_1:29;
reconsider f4 = (F(*)h2)/.nx as Element of REAL n;
reconsider f1 = (accum (F(*)h4))/.(nx+k3) as Element of REAL n;
assume that
nx<=nx+(k3+1) and
A96: nx+(k3+1)<k+1+1;
A97: nx+(k3+1)<len (accum (F(*)h4)) by A22,A45,A90,A96,XXREAL_0:2;
A98: nx+k3<nx+k3+1 by XREAL_1:29;
then nx+k3<k+1+1 by A96,XXREAL_0:2;
then
A99: nx+k3< len (F(*)h2) by A33,A32,A47,XXREAL_0:2;
then
A100: nx+k3+1<=len (F(*)h2) by NAT_1:13;
nx+k3>=0+1 by A41,NAT_1:13;
then
A101: 1<nx+(k3+1) by A98,XXREAL_0:2;
then
A102: (F(*)h4)/.(nx+k3+1)=(F(*)h4).(nx+k3+1) by A45,A32,A100,
FINSEQ_4:15;
nx+k3+1 in Seg len (F(*)h2) by A101,A100,FINSEQ_1:1;
then
A103: nx+k3+1 in dom (F(*)h2) by FINSEQ_1:def 3;
then
A104: (F(*)h4).(nx+k3+1)=F.(h4.(nx+k3+1)) by A44,A29,FUNCT_1:12
.=F.(h2b/.(nx+k3+1)) by A33,A38,A32,A101,A100,FINSEQ_4:15
.=F.(h2r/.(nx+k3+1)) by A33,A32,A96,A101,A100,A95,A94,
FINSEQ_7:30
.=F.(h2r.(nx+k3+1)) by A33,A32,A101,A100,FINSEQ_4:15
.=(F(*)h2).(nx+k3+1) by A103,FUNCT_1:12;
nx<=nx+k3 by NAT_1:11;
then
A105: 1<=nx+k3 by A51,XXREAL_0:2;
then (accum (F(*)h4)).(nx+(k3+1))=(accum (F(*)h4))/.(nx+k3) +
(F(*)h4)/.(nx+k3+1) by A45,A32,A99,Def10
.=(accum (F(*)h4))/.(nx+k3) +(F(*)h2)/.(nx+k3+1) by A101,A100
,A104,A102,FINSEQ_4:15;
then
A106: (accum (F(*)h4))/.(nx+(k3+1))-(F(*)h2)/.(k+1+1)+ (F(*)h2
)/.nx = f1 + f3 - f2 + f4 by A101,A97,FINSEQ_4:15
.= f1 - f2 + f3 + f4 by RFUNCT_1:8
.= f1 - f2 + f4 + f3 by RFUNCT_1:8;
(accum (F(*)h2)).(nx+(k3+1))=(accum (F(*)h2))/.(nx+k3) +
(F(*)h2)/.(nx+k3+1) by A105,A99,Def10
.=(accum (F(*)h4))/.(nx+k3)-(F(*)h2)/.(k+1+1) +(F(*)h2)/.
nx +(F(*)h2)/.(nx+k3+1) by A91,A93,A96,A98,A105,A99,FINSEQ_4:15,NAT_1:11
,XXREAL_0:2;
hence
(accum (F(*)h2)).(nx+(k3+1)) =(accum (F(*)h4))/.(nx+(k3+1
))-(F(*)h2)/.(k+1+1)+ (F(*)h2)/.nx by A106;
end;
hence S[k3+1];
end;
now
per cases by A41,XXREAL_0:1;
case
A107: 1=nx;
(accum (F(*)h4))/.(nx+0)=(accum (F(*)h4)).1 by A3,A45,A90,A107,
FINSEQ_4:15
.=(F(*)h4).1 by Def10
.=F.(h2.(k+1+1)) by A5,A43,A42,A107,FUNCT_1:13
.=(F(*)h2).(k+1+1) by A27,A26,FUNCT_1:13
.=(F(*)h2)/.(k+1+1) by A22,A24,A32,FINSEQ_4:15;
then
A108: (accum (F(*)h4))/.(nx+0)-(F(*)h2)/.(k+1+1)+(F(*)h2)/.nx
= 0*n +(F(*)h2)/.nx by EUCLIDLP:2
.=(F(*)h2)/.nx by EUCLID_4:1;
(accum (F(*)h2)).(nx+0) =(F(*)h2).1 by A107,Def10
.=(F(*)h2)/.nx by A36,A32,A107,FINSEQ_4:15;
hence
(accum (F(*)h2)).(nx+0) =(accum (F(*)h4))/.(nx+0)-(F(*)h2
)/.(k+1+1)+(F(*)h2)/.nx by A108;
end;
case
A109: 1<nx;
A110: (F(*)h4)/.(nx)=(F(*)h4).nx by A41,A36,A45,FINSEQ_4:15
.=F.(h2.(k+1+1)) by A34,A43,A42,FUNCT_1:13
.=(F(*)h2).(k+1+1) by A27,A26,FUNCT_1:13
.=(F(*)h2)/.(k+1+1) by A22,A24,A32,FINSEQ_4:15;
A111: nx-'1=nx-1 by A109,XREAL_1:233;
then nx-'1>0 by A109,XREAL_1:50;
then
A112: nx-'1>=0+1 by NAT_1:13;
nx<nx+1 by XREAL_1:29;
then
A113: nx-1<nx+1-1 by XREAL_1:9;
then
A114: nx-'1<len (F(*)h2) by A33,A32,A48,A111,XXREAL_0:2;
then
A115: (accum (F(*)h2))/.(nx-'1)=(accum (F(*)h2)).(nx-'1) by A91,A112,
FINSEQ_4:15;
(accum (F(*)h4)).(nx+0)=(accum (F(*)h4))/.(nx-'1) +(F(*)
h4)/.(nx-'1+1) by A45,A32,A111,A112,A114,Def10
.=(accum (F(*)h4))/.(nx-'1)+(F(*)h2)/.(k+1+1) by A111,A110;
then
A116: (accum (F(*)h4))/.(nx+0)-(F(*)h2)/.(k+1+1) =(accum (F(*)
h4))/.(nx-'1) +(F(*)h2)/.(k+1+1) -(F(*)h2)/.(k+1+1) by A33,A45,A51,A48,A90,
FINSEQ_4:15
.=(accum (F(*)h4))/.(nx-'1) by RVSUM_1:42;
A117: (accum (F(*)h4))/.(nx-'1)=(accum (F(*)h4)).(nx-'1) by A45,A32
,A90,A112,A114,FINSEQ_4:15;
(accum (F(*)h2)).(nx+0)=(accum (F(*)h2))/.(nx-'1) +(F(*)
h2)/.(nx-'1+1) by A111,A112,A114,Def10
.=(accum (F(*)h4))/.(nx-'1) +(F(*)h2)/.(nx) by A64,A111,A112
,A113,A115,A117;
hence
(accum (F(*)h2)).(nx+0) =(accum (F(*)h4))/.(nx+0)-(F(*)h2
)/.(k+1+1)+(F(*)h2)/.nx by A116;
end;
end;
then
A118: S[0];
A119: for k3 being Nat holds S[k3] from NAT_1:sch 2(A118,A92);
A120: i-'nx=i-nx by A88,XREAL_1:233;
then nx<=nx+(i-'nx) by A88;
hence (accum (F(*)h2)).i =(accum (F(*)h4))/.i-(F(*)h2)/.(k+1+1)+(F
(*)h2)/.nx by A89,A119,A120;
end;
A121: (F(*)h2)/.nx=(F(*)h2).nx by A41,A36,A32,FINSEQ_4:15;
A122: k+1+1 in dom h4 by A25,A39,FINSEQ_1:def 3;
A123: (F(*)h4)/.(k+1+1)=(F(*)h4).(k+1+1) by A22,A24,A45,FINSEQ_4:15;
A124: for i being Nat st k+1+1<=i & i<=len F holds (accum (F(*)h2)).
i=(accum (F(*)h4)).i
proof
defpred Y[Nat] means k+1+1+$1<=len F implies (accum (F(*)h2)).(k+1
+1+$1)=(accum (F(*)h4)).(k+1+1+$1);
let i be Nat;
assume that
A125: k+1+1<=i and
A126: i<=len F;
A127: for k3 being Nat st Y[k3] holds Y[k3+1]
proof
let k3 be Nat;
assume
A128: Y[k3];
k+1+1+(k3+1)<=len F implies (accum (F(*)h2)).(k+1+1+(k3+1)
)=(accum (F(*)h4)).(k+1+1+(k3+1))
proof
A129: k+1+1<=k+1+1+k3 by NAT_1:11;
A130: k+1+1+k3<k+1+1+k3+1 by XREAL_1:29;
then
A131: k+1+1<k+1+1+k3+1 by A129,XXREAL_0:2;
assume
A132: k+1+1+(k3+1)<=len F;
then
A133: (
F(*)h4)/.(k+1+1+k3+1)=(F(*)h4).(k+1+1+k3+1) by A45,FINSEQ_4:15,NAT_1:11;
1<=k+1+1+k3+1 by NAT_1:11;
then k+1+1+k3+1 in Seg len (F(*)h2) by A31,A132,FINSEQ_1:1;
then
A134: k+1+1+k3+1 in dom (F(*)h2) by FINSEQ_1:def 3;
then
A135: (F(*)h4).(k+1+1+k3+1)=F.(h4.(k+1+1+k3+1)) by A44,A29,FUNCT_1:12
.=F.(h2b/.(k+1+1+k3+1)) by A33,A38,A132,FINSEQ_4:15,NAT_1:11
.=F.(h2r/.(k+1+1+k3+1)) by A33,A63,A132,A131,FINSEQ_7:30
,NAT_1:11
.=F.(h2r.(k+1+1+k3+1)) by A33,A132,FINSEQ_4:15,NAT_1:11
.=(F(*)h2).(k+1+1+k3+1) by A134,FUNCT_1:12;
1<=k+1+1 by NAT_1:11;
then
A136: 1<=k+1+1+k3 by A129,XXREAL_0:2;
A137: k+1+1+k3<len F by A132,A130,XXREAL_0:2;
then
A138: (accum (F(*)h4))/.(k+1+1+k3)=(accum (F(*)h4)).(k+1+1+k3)
by A45,A50,A136,FINSEQ_4:15;
(accum (F(*)h2)).(k+1+1+(k3+1)) =(accum (F(*)h2))/.(k+1+
1+k3)+((F(*)h2)/.(k+1+1+k3+1)) by A32,A137,A136,Def10
.=(accum (F(*)h4))/.(k+1+1+k3)+((F(*)h2)/.(k+1+1+k3+1)) by
A32,A62,A128,A137,A136,A138,FINSEQ_4:15
.=(accum (F(*)h4))/.(k+1+1+k3)+((F(*)h4)/.(k+1+1+k3+1)) by
A32,A132,A135,A133,FINSEQ_4:15,NAT_1:11;
hence
(accum (F(*)h2)).(k+1+1+(k3+1)) =(accum (F(*)h4)).(k+1+1+
(k3+1)) by A45,A137,A136,Def10;
end;
hence Y[k3+1];
end;
A139: len (accum (F(*)h2))=len (F(*)h2) by Def10;
A140: (accum (F(*)h2)).(k+1) =(accum (F(*)h4))/.(k+1)-(F(*)h2)/.(k
+1+1)+(F(*)h2)/.nx by A19,A46,A87;
A141: 1<=k+1 by NAT_1:11;
k+1<len (F(*)h2) by A20,A30,FINSEQ_1:def 3;
then (accum (F(*)h2)).(k+1+1) =((accum (F(*)h2))/.(k+1))+((F(*)h2
)/.(k+1+1)) by A141,Def10
.=(accum (F(*)h4))/.(k+1)-((F(*)h2)/.(k+1+1))+(F(*)h2)/.nx +((
F(*)h2)/.(k+1+1)) by A20,A32,A139,A140,FINSEQ_4:15,NAT_1:11
.= (accum (F(*)h4))/.(k+1) +(F(*)h2)/.nx by Th4
.= ((accum (F(*)h4))/.(k+1))+((F(*)h4)/.(k+1+1)) by A122,A53,A49
,A123,A121,FUNCT_1:13;
then
A142: Y[0] by A20,A18,A45,Def10;
A143: for k3 being Nat holds Y[k3] from NAT_1:sch 2(A142,A127);
k+1+1+(i-'(k+1+1))=i-(k+1+1)+(k+1+1) by A125,XREAL_1:233
.=i;
hence (accum (F(*)h2)).i=(accum (F(*)h4)).i by A126,A143;
end;
A144: gF/.(k+1)=gF.(k+1) by A9,A20,FINSEQ_4:15,NAT_1:11;
A145: dom h4=dom F by A5,FUNCT_2:def 1;
rng h4 c= dom F;
then
A146: dom (F(*)h4)=dom h4 by RELAT_1:27;
then Seg len (F(*)h4)=dom h4 by FINSEQ_1:def 3;
then
A147: k+1<len (F(*)h4) by A20,A145,FINSEQ_1:def 3;
Seg len (F(*)h4)=dom F by A145,A146,FINSEQ_1:def 3;
then len (F(*)h4)=len F by FINSEQ_1:def 3;
then
A148: (F(*)h4)/.(k+1+1)=(F(*)h4).(k+1+1) by A22,A24,FINSEQ_4:15;
len (accum (F(*)h4))=len (F(*)h4) by Def10;
then
A149: (accum (F(*)h4))/.(k+1)=(accum (F(*)h4)).(k+1) by A147,FINSEQ_4:15
,NAT_1:11;
gF.(k+1+1)=gF/.(k+1) + F/.(k+1+1) by A10,A20,NAT_1:11
.=(accum (F(*)h4))/.(k+1)+F/.(k+1+1) by A17,A23,A54,A149,A144
.=(accum (F(*)h4))/.(k+1) + (F(*)h4)/.(k+1+1) by A122,A53,A148,A60,
FUNCT_1:13
.=(accum (F(*)h4)).(k+1+1) by A61,A147,Def10;
hence gF.(k+1+1)=(accum (F(*)h2)).(k+1+1) by A22,A124;
end;
suppose
nx>k+1;
then
A150: k+1+1<=nx by NAT_1:13;
per cases by A150,XXREAL_0:1;
suppose
A151: k+1+1=nx;
A152: for i being Nat st k+1<i & i<=len F holds h2.i=i
proof
let i be Nat;
assume that
A153: k+1<i and
A154: i<=len F;
A155: k+1+1<=i by A153,NAT_1:13;
per cases by A155,XXREAL_0:1;
suppose
k+1+1<i;
hence h2.i=i by A21,A154;
end;
suppose
k+1+1=i;
hence h2.i=i by A35,A151;
end;
end;
A156: k+1<len (F(*)h2) by A20,A30,FINSEQ_1:def 3;
len (accum (F(*)h2))=len (F(*)h2) by Def10;
then
A157: (accum (F(*)h2))/.(k+1)=(accum (F(*)h2)).(k+1) by A20,A32,
FINSEQ_4:15,NAT_1:11;
A158: 1<=k+1 by NAT_1:11;
A159: F.(k+1+1)=(F(*)h2).nx by A34,A35,FUNCT_1:13;
A160: gF/.(k+1)=gF.(k+1) by A9,A20,FINSEQ_4:15,NAT_1:11;
A161: F/.(k+1+1)=F.(k+1+1) by A22,A24,FINSEQ_4:15;
gF.(k+1+1)=gF/.(k+1) + F/.(k+1+1) by A10,A20,NAT_1:11
.=(accum (F(*)h2))/.(k+1)+F/.(k+1+1) by A17,A23,A152,A157,A160
.=(accum (F(*)h2))/.(k+1) + (F(*)h2)/.(k+1+1) by A22,A24,A32,A151
,A161,A159,FINSEQ_4:15
.=(accum (F(*)h2)).(k+1+1) by A158,A156,Def10;
hence gF.(k+1+1)=(accum (F(*)h2)).(k+1+1);
end;
suppose
k+1+1<nx;
hence gF.(k+1+1)=(accum (F(*)h2)).(k+1+1) by A21,A35,A36;
end;
end;
end;
hence P[k+1];
end;
for h2 being Permutation of dom F st for i being Nat st 0+1<i & i<=
len F holds h2.i=i holds gF.(0+1)=(accum (F(*)h2)).(0+1)
proof
let h2 be Permutation of dom F;
A162: rng h2=dom F by FUNCT_2:def 3;
A163: dom h2=dom F by A5,FUNCT_2:def 1;
assume
A164: for i being Nat st 0+1<i & i<=len F holds h2.i=i;
A165: now
assume
A166: h2.1<>1;
consider x being object such that
A167: x in dom h2 and
A168: h2.x=1 by A5,A162,FUNCT_1:def 3;
reconsider nx=x as Element of NAT by A163,A167;
1<=nx by A11,A167,FINSEQ_1:1;
then nx=1 or 1<nx & nx<=len F by A11,A167,FINSEQ_1:1,XXREAL_0:1;
hence contradiction by A164,A166,A168;
end;
(accum (F(*)h2)).1=(F(*)h2).1 by Def10
.=F.1 by A5,A163,A165,FUNCT_1:13;
hence gF.(0+1)=(accum (F(*)h2)).(0+1) by Def10;
end;
then
A169: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A169,A16);
then gF.(len F)=(accum (F(*)h)).(len F) by A13,A14,XREAL_1:44
.=(accum F2).(len F2) by A1,A8,FINSEQ_1:def 3
.= Sum F2 by A12,Def11;
hence Sum F2=Sum F by A2,Def11;
end;
suppose
A170: len F<=0;
rng h c= dom F;
then
A171: dom (F(*)h)=dom h by RELAT_1:27;
Seg len F = {} by A170;
then dom F={} by FINSEQ_1:def 3;
then Seg len F=dom F2 by A1,A171,FINSEQ_1:def 3;
then
A172: len F=len F2 by FINSEQ_1:def 3;
Sum F=0*n by A170,Def11;
hence Sum F2=Sum F by A170,A172,Def11;
end;
end;
theorem Th21:
for k being Nat holds Sum(k |-> 0*n) = 0*n
proof
let k be Nat;
set g = k |-> 0*n;
A1: for i being Nat st i in dom g holds g.i= 0*n
proof
let i be Nat;
assume i in dom g;
then i in Seg k by FUNCOP_1:13;
hence thesis by FINSEQ_2:57;
end;
per cases;
suppose
A2: len g>0;
set g3 = accum g;
A3: len g=len g3 by Def10;
A4: g.1=g3.1 by Def10;
defpred P[Nat] means $1<len g implies g3.($1+1)=0*n;
A5: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A6: P[k];
A7: k<k+1 by XREAL_1:29;
per cases;
suppose
A8: k+1<len g; then
A9: k+1+1<=len g by NAT_1:13;
per cases;
suppose
A10: 1<=k+1;
A11: 1<=k+1+1 by XREAL_1:29;
then k+1+1 in Seg len g by A9,FINSEQ_1:1;
then k+1+1 in dom g by FINSEQ_1:def 3;
then
A12: g.(k+1+1)=0*n by A1;
A13: g3/.(k+1)=g3.(k+1) by A3,A8,A10,FINSEQ_4:15;
g3.(k+1+1)=(g3/.(k+1))+(g/.(k+1+1)) by Def10,A8,A10;
then g3.(k+1+1)=0*n + 0*n by A6,A7,A8,A9,A13,A11,A12,FINSEQ_4:15
,XXREAL_0:2
.= 0*n by EUCLID_4:1;
hence P[k+1];
end;
suppose
1>k+1;
hence P[k+1] by NAT_1:14;
end;
end;
suppose
k+1>=len g;
hence P[k+1];
end;
end;
A14: 0+1<=len g by A2,NAT_1:13;
then 1 in Seg len g by FINSEQ_1:1;
then 1 in dom g by FINSEQ_1:def 3;
then
A15: P[0] by A1,A4;
for k being Nat holds P[k] from NAT_1:sch 2(A15,A5);
then
A16: P[ len g3 -'1];
len g3-'1=len g3-1 by A3,A14,XREAL_1:233;
hence Sum g= 0*n by A3,Def11,A16,XREAL_1:44;
end;
suppose len g<=0;
hence Sum g= 0*n by Def11;
end;
end;
theorem Th22:
for g being FinSequence of REAL n, h being FinSequence of NAT,
F being FinSequence of REAL n st
h is increasing & rng h c= dom g & F=g*h &
(for i being Element of NAT st i in dom g & not i in rng h holds g.i= 0*n)
holds Sum g=Sum F
proof
let g be FinSequence of REAL n, h be FinSequence of NAT,
F be FinSequence of REAL n;
assume that
A1: h is increasing and
A2: rng h c= dom g and
A3: F=g*h and
A4: for i being Element of NAT st i in dom g & not i in rng h holds g.i= 0*n;
A5: dom((h qua Relation)*(g qua Relation))=dom h by A2,RELAT_1:27;
dom (g*h)=dom h by A2,RELAT_1:27;
then
A6: dom F=Seg len h by A3,FINSEQ_1:def 3;
then
A7: len F=len h by FINSEQ_1:def 3;
dom h c=dom g
proof
let x be object;
assume
A8: x in dom h;
then reconsider nx=x as Element of NAT;
A9: h.x in rng h by A8,FUNCT_1:def 3;
then reconsider nhx=h.x as Element of NAT;
A10: nx in Seg len h by A8,FINSEQ_1:def 3;
then
A11: 1<=nx by FINSEQ_1:1;
A12: nx<=len h by A10,FINSEQ_1:1;
then 1<=len h by A11,XXREAL_0:2;
then 1 in Seg len h by FINSEQ_1:1;
then 1 in dom h by FINSEQ_1:def 3;
then h.1 in rng h by FUNCT_1:def 3;
then h.1 in dom g by A2;
then h.1 in Seg len g by FINSEQ_1:def 3;
then 1<=h.1 by FINSEQ_1:1;
then
A13: nx<=nhx by A1,A12,Th7;
h.x in dom g by A2,A9;
then h.x in Seg len g by FINSEQ_1:def 3;
then nhx <=len g by FINSEQ_1:1;
then nx <=len g by A13,XXREAL_0:2;
then nx in Seg len g by A11,FINSEQ_1:1;
hence x in dom g by FINSEQ_1:def 3;
end;
then dom h c= Seg len g by FINSEQ_1:def 3;
then Seg len h c= Seg len g by FINSEQ_1:def 3;
then
A14: len h <= len g by FINSEQ_1:5;
per cases;
suppose
A15: len F>0;
then
A16: 0+1<=len F by NAT_1:13;
then 1 in Seg len F by FINSEQ_1:1;
then
A17: 1 in dom F by FINSEQ_1:def 3;
then
A18: 1 in Seg len h by A3,A5,FINSEQ_1:def 3;
then
A19: 1<=len h by FINSEQ_1:1;
then len h in Seg len h by FINSEQ_1:1;
then len h in dom h by FINSEQ_1:def 3;
then h.(len h) in rng h by FUNCT_1:def 3;
then h.(len h) in dom g by A2;
then
A20: h.(len h) in Seg len g by FINSEQ_1:def 3;
reconsider j=h.1 as Nat;
dom((h qua Relation)*(g qua Relation))=dom h by A2,RELAT_1:27;
then
A21: Seg len F=dom h by A3,FINSEQ_1:def 3;
then
A22: len F=len h by FINSEQ_1:def 3;
A23: h.1 in rng h by A3,A5,A17,FUNCT_1:def 3;
then
A24: h.1 in dom g by A2;
then
A25: h.1 in Seg len g by FINSEQ_1:def 3;
then
A26: 1<=h.1 by FINSEQ_1:1;
then
A27: j-'1=j-1 by XREAL_1:233;
Seg len g <> {} by A2,A23,FINSEQ_1:def 3;
then 0<len g;
then
A28: 0+1<=len g by NAT_1:13;
then
A29: len g -'1=len g-1 by XREAL_1:233;
then
A30: h.(len h)<=len g-'1+1 by A20,FINSEQ_1:1;
A31: 1<=j by A25,FINSEQ_1:1;
set g4 = accum g;
A32: len g=len g4 by Def10;
A33: g.1=g4.1 by Def10;
A34: for i being Nat st 1<=i & i<len g holds g4.(i+1)=(g4/.i)+(g/.(i+1) )
by Def10;
A35: Sum g=g4.(len g) by A7,A14,A15,Def11;
set g2 = accum F;
A36: len F=len g2 by Def10;
A37: F.1=g2.1 by Def10;
A38: for i being Nat st 1<=i & i<len F holds g2.(i+1)=(g2/.i)+(F/.(i+1) )
by Def10;
A39: Sum F=g2.(len F) by A15,Def11;
defpred Q[Nat] means 1<=$1+1 & $1+1<j implies g4.($1+1)= 0*n;
A40: for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume
A41: Q[k];
1<=k+1+1 & k+1+1<j implies g4.(k+1+1)= 0*n
proof
assume that
A42: 1<=k+1+1 and
A43: k+1+1<j;
per cases by A42,XXREAL_0:1;
suppose
A44: 1<k+1+1;
j in Seg len g by A24,FINSEQ_1:def 3;
then
A45: j<=len g by FINSEQ_1:1;
then k+1+1<len g by A43,XXREAL_0:2;
then
A46: g/.(k+1+1)=g.(k+1+1) by A44,FINSEQ_4:15;
A47: now
assume k+1+1 in rng h;
then consider x0 being object such that
A48: x0 in dom h and
A49: h.x0=k+1+1 by FUNCT_1:def 3;
reconsider nx0=x0 as Element of NAT by A48;
A50: x0 in Seg len h by A48,FINSEQ_1:def 3;
then
A51: nx0<=len h by FINSEQ_1:1;
1<=nx0 by A50,FINSEQ_1:1;
hence contradiction by A1,A43,A49,A51,Th6;
end;
A52: k+1<k+1+1 by XREAL_1:29;
then k+1<j by A43,XXREAL_0:2;
then
A53: k+1<len g by A45,XXREAL_0:2;
then
A54: g4/.(k+1)=g4.(k+1) by A32,FINSEQ_4:15,NAT_1:11;
k+1+1<=len g by A53,NAT_1:13;
then k+1+1 in Seg len g by A42,FINSEQ_1:1;
then k+1+1 in dom g by FINSEQ_1:def 3;
then
A55: g.(k+1+1)= 0*n by A4,A47;
g4.(k+1+1)=(g4/.(k+1))+(g/.(k+1+1)) by A34,A53,NAT_1:11;
hence g4.(k+1+1)= 0*n by A41,A43,A52,A55,A54,A46,EUCLID_4:1,NAT_1:11
,XXREAL_0:2;
end;
suppose
1=k+1+1;
hence g4.(k+1+1)= 0*n;
end;
end;
hence Q[k+1];
end;
defpred P[Nat] means 1<=$1+1 & $1+1<=len g2 implies g4.(h.($1+1))=g2.($1+1
);
A56: 1 in Seg len g by A28,FINSEQ_1:1;
1<j implies 1 in dom g & not 1 in rng h
proof
assume
A57: 1<j;
thus 1 in dom g by A56,FINSEQ_1:def 3;
hereby
assume 1 in rng h;
then consider x0 being object such that
A58: x0 in dom h and
A59: h.x0=1 by FUNCT_1:def 3;
reconsider nx0=x0 as Element of NAT by A58;
A60: x0 in Seg len h by A58,FINSEQ_1:def 3;
then
A61: nx0<=len h by FINSEQ_1:1;
1<=nx0 by A60,FINSEQ_1:1;
hence contradiction by A1,A57,A59,A61,Th6;
end;
end;
then
A62: Q[0] by A4,A33;
A63: for k being Nat holds Q[k] from NAT_1:sch 2(A62,A40);
A64: now
per cases by A26,XXREAL_0:1;
case
1<j;
then 1+1<=j by NAT_1:13;
then
A65: 1+1-1<=j-1 by XREAL_1:9;
then 1<=j-'1 by A31,XREAL_1:233;
then
A66: j-'1-'1+1=j-'1-1+1 by XREAL_1:233
.=j-'1;
A67: g.j=g2.1 by A3,A5,A37,A17,FUNCT_1:13;
A68: Q[j-'1-'1] by A63;
A69: j in Seg len g by A24,FINSEQ_1:def 3;
then
A70: j<=len g by FINSEQ_1:1;
1<=j by A69,FINSEQ_1:1;
then
A71: g/.j=g.j by A70,FINSEQ_4:15;
A72: g2/.1=g2.1 by A36,A16,FINSEQ_4:15;
A73: j-'1<j-'1+1 by XREAL_1:29;
then
A74: j-'1<len g by A27,A70,XXREAL_0:2;
then g4/.(j-'1)=g4.(j-'1) by A32,A27,A65,FINSEQ_4:15;
then g4.j= 0*n + g2/.1 by Def10,A27,A65,A73,A74,A68,A66,A71,A72,A67
.=g2/.1 by EUCLID_4:1;
hence P[0] by FINSEQ_4:15;
end;
case
j=1;
hence P[0] by A3,A5,A37,A33,A17,FUNCT_1:13;
end;
end;
A75: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A76: P[k];
1<=k+1+1 & k+1+1<=len g2 implies g4.(h.(k+1+1))=g2.(k+1+1)
proof
defpred R[Nat] means h.(k+1)<= $1+1 & $1+1<h.(k+1+1) implies g4.($1+1)
= g2.(k+1);
assume that
A77: 1<=k+1+1 and
A78: k+1+1<=len g2;
A79: k+1+1 in Seg len g2 by A77,A78,FINSEQ_1:1;
then h.(k+1+1) in rng h by A36,A21,FUNCT_1:def 3;
then h.(k+1+1) in dom g by A2;
then
A80: h.(k+1+1) in Seg len g by FINSEQ_1:def 3;
then
A81: 1<=h.(k+1+1) by FINSEQ_1:1;
A82: k+1<k+1+1 by XREAL_1:29;
then
A83: k+1<len g2 by A78,XXREAL_0:2;
now
per cases;
case
A84: 1<=k;
k<k+1 by XREAL_1:29;
then
A85: k<len h by A36,A22,A83,XXREAL_0:2;
then k<=h.k by A1,A26,Th7;
then
A86: 1<=h.k by A84,XXREAL_0:2;
h.k<h.(k+1) by A1,A84,A85;
hence R[0] by A86,XXREAL_0:2;
end;
case
k<1;
hence R[0] by A15,A36,A64,NAT_1:14;
end;
end;
then
A87: R[0];
A88: h.(k+1+1)<=len g by A80,FINSEQ_1:1;
1<=k+1 by NAT_1:11;
then
A89: h.(k+1)<h.(k+1+1) by A1,A36,A22,A83;
A90: for k2 being Nat st R[k2] holds R[k2+1]
proof
let k2 be Nat;
assume
A91: R[k2];
h.(k+1)<= k2+1+1 & k2+1+1<h.(k+1+1) implies g4.(k2+1+1)= g2.(k +1)
proof
assume that
A92: h.(k+1)<= k2+1+1 and
A93: k2+1+1<h.(k+1+1);
per cases by A92,XXREAL_0:1;
suppose
A94: h.(k+1)< k2+1+1;
A95: now
assume k2+1+1 in rng h;
then consider x0 being object such that
A96: x0 in dom h and
A97: h.x0=k2+1+1 by FUNCT_1:def 3;
reconsider nx0=x0 as Element of NAT by A96;
A98: x0 in Seg len h by A96,FINSEQ_1:def 3;
then nx0<=len h by FINSEQ_1:1;
then
A99: nx0>=k+1+1 implies h.nx0>=h.(k+1+1) by A1,A77,Th6;
1<=nx0 by A98,FINSEQ_1:1;
then nx0<=k+1 implies h.nx0<=h.(k+1) by A1,A36,A22,A83,Th6;
hence contradiction by A93,A94,A97,A99,NAT_1:13;
end;
h.(k+1+1) in rng h by A36,A21,A79,FUNCT_1:def 3;
then h.(k+1+1) in dom g by A2;
then h.(k+1+1) in Seg len g by FINSEQ_1:def 3;
then h.(k+1+1)<=len g by FINSEQ_1:1;
then
A100: k2+1+1< len g by A93,XXREAL_0:2;
A101: 1<k2+1+1 by XREAL_1:29;
then
A102: g/.(k2+1+1)=g.(k2+1+1) by A100,FINSEQ_4:15;
A103: k2+1<k2+1+1 by XREAL_1:29;
then
A104: k2+1<len g by A100,XXREAL_0:2;
k2+1+1 in Seg len g by A100,A101,FINSEQ_1:1;
then k2+1+1 in dom g by FINSEQ_1:def 3;
then
A105: g.(k2+1+1)= 0*n by A4,A95;
k2+1< len g by A103,A100,XXREAL_0:2;
then g4.(k2+1+1)=(g4/.(k2+1))+(g/.(k2+1+1)) by A34,NAT_1:11
.=(g4/.(k2+1)) by A105,A102,EUCLID_4:1
.= g4.(k2+1) by A32,A104,FINSEQ_4:15,NAT_1:11;
hence g4.(k2+1+1)= g2.(k+1) by A91,A93,A94,NAT_1:13;
end;
suppose
h.(k+1)=k2+1+1;
hence g4.(k2+1+1)=g2.(k+1) by A76,A78,A82,NAT_1:11,XXREAL_0:2;
end;
end;
hence R[k2+1];
end;
A106: for k2 being Nat holds R[k2] from NAT_1:sch 2(A87,A90);
then
A107: h.(k+1)<= h.(k+1+1)-'1-'1+1 & h.(k+1+1)-'1-'1+1<h.(k+1+1)
implies g4.(h.(k+1+1)-'1-'1+1)= g2.(k+1);
now
per cases;
case
A108: 1<=k;
k<k+1 by XREAL_1:29;
then
A109: k<len h by A36,A22,A83,XXREAL_0:2;
then k<=h.k by A1,A26,Th7;
then
A110: 1<=h.k by A108,XXREAL_0:2;
A111: 1+h.(k+1)<=h.(k+1+1) by A89,NAT_1:13;
then
A112: h.(k+1)+1-1<=h.(k+1+1)-1 by XREAL_1:9;
h.k<h.(k+1) by A1,A108,A109;
then 1<h.(k+1) by A110,XXREAL_0:2;
then 1+1<h.(k+1)+1 by XREAL_1:6;
then 1+1<h.(k+1+1) by A111,XXREAL_0:2;
then
A113: 1+1-1<h.(k+1+1)-1 by XREAL_1:9;
then
A114: h.(k+1+1)-'1=h.(k+1+1)-1 by XREAL_0:def 2;
then
A115: h.(k+1+1)-'1-'1=h.(k+1+1)-1-1 by A113,XREAL_1:233;
A116: g/.(h.(k+1+1))=g.(h.(k+1+1)) by A81,A88,FINSEQ_4:15;
A117: F.(k+1+1)=g.(h.(k+1+1)) by A3,A36,A21,A79,FUNCT_1:13;
A118: k+1<=len g2 by A78,A82,XXREAL_0:2;
h.(k+1+1)<h.(k+1+1)+1 by XREAL_1:29;
then
A119: h.(k+1+1)-1 <h.(k+1+1)+1-1 by XREAL_1:9;
then
A120: h.(k+1+1)-'1<len g by A88,A114,XXREAL_0:2;
then
A121: g4
/.(h.(k+1+1)-'1)=g4.((h.(k+1+1)-'1)) by A32,A113,A114,FINSEQ_4:15;
g2.(k+1+1)=(g2/.(k+1))+(F/.(k+1+1)) by A36,A38,A83,NAT_1:11
.= g4/.(h.(k+1+1)-'1) +(F/.(k+1+1)) by A107,A114,A115,A112,A119
,A121,A118,FINSEQ_4:15,NAT_1:11
.= g4/.(h.(k+1+1)-'1) +g/.(h.(k+1+1)) by A36,A77,A78,A117,A116,
FINSEQ_4:15
.=g4.(h.(k+1+1)-'1+1) by Def10,A113,A114,A120;
hence g4.(h.(k+1+1))=g2.(k+1+1) by A114;
end;
case
k<1;
then
A122: k=0 by NAT_1:14;
then 1<len h by A36,A22,A78,NAT_1:13;
then
A123: h.1<h.(1+1) by A1;
then
A124: h.(1+1)-'1=h.(1+1)-1 by A31,XREAL_1:233,XXREAL_0:2;
then
A125: h.(k+1+1)-'1+1=h.(k+1+1) by A122;
A126: F/.1=F.1 by A19,A22,FINSEQ_4:15;
k+1<len F by A36,A78,NAT_1:13;
then
A127: g2.(k+1+1)=(g2/.(k+1))+(F/.(k+1+1)) by A38,NAT_1:11
.=F/.1 +F/.(1+1) by A36,A37,A19,A22,A122,A126,FINSEQ_4:15;
A128: F/.(1+1)=F.(1+1) by A36,A78,A122,FINSEQ_4:15;
h.1+1<=h.(1+1) by A123,NAT_1:13;
then h.1+1-1<=h.(1+1)-1 by XREAL_1:9;
then
A129: h.1<=h.(1+1)-'1 by A26,A123,XREAL_1:233,XXREAL_0:2;
h.(1+1)<h.(1+1)+1 by XREAL_1:29;
then
A130: h.(1+1)-1<h.(1+1)+1-1 by XREAL_1:9;
then
A131: h.(1+1)-'1<h.(1+1) by A26,A123,XREAL_1:233,XXREAL_0:2;
A132: 1<h.(1+1) by A26,A123,XXREAL_0:2;
then 1+1<=h.(1+1) by NAT_1:13;
then
A133: 1+1-1<=h.(1+1)-1 by XREAL_1:9;
then h.(1+1)-'1-'1=h.(1+1)-'1-1 by A124,XREAL_1:233;
then
A134: h.(1+1)-'1-'1+1=h.(1+1)-'1;
1+1 in Seg len h by A36,A22,A78,A122,FINSEQ_1:1;
then 1+1 in dom h by FINSEQ_1:def 3;
then h.(1+1) in rng h by FUNCT_1:def 3;
then h.(1+1) in dom g by A2;
then
A135: h.(1+1) in Seg len g by FINSEQ_1:def 3;
then h.(1+1)<=len g by FINSEQ_1:1;
then
A136: g/.(h.(k+1+1)) =g.(h.(1+1)) by A122,A132,FINSEQ_4:15
.=F.(1+1) by A3,A36,A21,A79,A122,FUNCT_1:13;
h.(1+1)<=len g by A135,FINSEQ_1:1;
then h.(1+1)-'1<len g4 by A32,A124,A130,XXREAL_0:2;
then
A137: g4/.(h.(k+1+1)-'1)=g4.((h.(1+1)-'1)) by A122,A124,A133,FINSEQ_4:15
.=F.1 by A37,A106,A122,A134,A131,A129;
h.(1+1)<=len g by A135,FINSEQ_1:1;
then
A138: h.(k+1+1)-'1<len g by A122,A125,NAT_1:13;
1<=h.(k+1+1)-'1 by A122,A132,A125,NAT_1:13;
then g4.(h.(k+1+1)-'1+1)=g4/.(h.(k+1+1)-'1) +g/.(h.(k+1+1))
by Def10,A122,A124,A138
.=F/.1 +F/.(1+1) by A19,A22,A128,A137,A136,FINSEQ_4:15;
hence g4.(h.(k+1+1))=g2.(k+1+1) by A122,A124,A127;
end;
end;
hence g4.(h.(k+1+1))=g2.(k+1+1);
end;
hence P[k+1];
end;
defpred R[Nat] means h.(len h)<= $1+1 & $1+1<=len g implies g4.($1+1)= g2.
(len g2);
A139: P[0] by A64;
A140: for k being Nat holds P[k] from NAT_1:sch 2(A139,A75);
A141: for k being Nat st R[k] holds R[k+1]
proof
let k be Nat;
assume
A142: R[k];
h.(len h)<= k+1+1 & k+1+1<=len g implies g4.(k+1+1)= g2.(len g2)
proof
assume that
A143: h.(len h)<= k+1+1 and
A144: k+1+1<=len g;
per cases by A143,XXREAL_0:1;
suppose
A145: h.(len h)<k+1+1;
A146: now
assume k+1+1 in rng h;
then consider x being object such that
A147: x in dom h and
A148: h.x=k+1+1 by FUNCT_1:def 3;
reconsider nx=x as Element of NAT by A147;
A149: x in Seg len h by A147,FINSEQ_1:def 3;
then
A150: nx<=len h by FINSEQ_1:1;
1<=nx by A149,FINSEQ_1:1;
hence contradiction by A1,A145,A148,A150,Th6;
end;
1<=k+1+1 by NAT_1:11;
then k+1+1 in Seg len g by A144,FINSEQ_1:1;
then
A151: k+1+1 in dom g by FINSEQ_1:def 3;
k+1<k+1+1 by XREAL_1:29;
then
A152: k+1<len g by A144,XXREAL_0:2;
then
A153: g4.(k+1+1)=(g4/.(k+1))+(g/.(k+1+1)) by A34,NAT_1:11;
1<=k+1 by NAT_1:11;
then
A154: g4/.(k+1)= g2.(len g2) by A32,A142,A145,A152,FINSEQ_4:15,NAT_1:13;
1<k+1+1 by XREAL_1:29;
then g/.(k+1+1)= g.(k+1+1) by A144,FINSEQ_4:15
.=0*n by A4,A146,A151;
hence g4.(k+1+1)= g2.(len g2) by A154,A153,EUCLID_4:1;
end;
suppose
A155: h.(len h)=k+1+1;
A156: len h-'1=len h -1 by A19,XREAL_1:233;
1<=len h-'1+1 & len h-'1+1<=len g2 implies g4.(h.(len h-'1+1))
=g2.(len h-'1+1) by A140;
hence g4.(k+1+1)= g2.(len g2) by A36,A18,A21,A155,A156,FINSEQ_1:1
,def 3;
end;
end;
hence R[k+1];
end;
A157: 1<=h.(len h) by A20,FINSEQ_1:1;
h.(len h)<=1 & 1<=len g implies g4.(0+1)= g2.(len g2)
proof
assume that
A158: h.(len h)<=1 and
1<=len g;
h.(len h)=1 by A157,A158,XXREAL_0:1;
then len h<=1 by A1,A26,Th7;
then
A159: len h=1 by A19,XXREAL_0:1;
g2.1=g.(h.1) by A3,A5,A37,A17,FUNCT_1:13
.=g.1 by A157,A158,A159,XXREAL_0:1;
hence g4.(0+1)= g2.(len g2) by A6,A36,A33,A159,FINSEQ_1:def 3;
end;
then
A160: R[0];
for k being Nat holds R[k] from NAT_1:sch 2(A160,A141);
hence Sum g =Sum F by A36,A39,A35,A29,A30;
end;
suppose
A161: len F <=0;
then
A162: Sum F= 0*n by Def11;
A163: dom g = Seg len g by FINSEQ_1:def 3;
Seg len F = {} by A161;
then dom F= {} by FINSEQ_1:def 3;
then
A164: rng h= {} by A3,A5,RELAT_1:42;
A165: now
let z be object;
assume
A166: z in dom g;
hence g.z = 0*n by A4,A164
.= (len g |-> 0*n).z by A163,A166,FINSEQ_2:57;
end;
Seg len g = dom(len g |-> 0*n) by FUNCOP_1:13;
then g = len g |-> 0*n by A163,A165,FUNCT_1:2;
hence Sum g =Sum F by A162,Th21;
end;
end;
theorem Th23:
for g being FinSequence of REAL n, h being FinSequence of NAT,
F being FinSequence of REAL n st
h is one-to-one & rng h c= dom g & F=g*h &
(for i being Element of NAT st i in dom g & not i in rng h holds g.i= 0*n)
holds Sum g = Sum F
proof
let g be FinSequence of REAL n, h be FinSequence of NAT,
F be FinSequence of REAL n;
assume that
A1: h is one-to-one and
A2: rng h c= dom g and
A3: F=g*h and
A4: for i being Element of NAT st i in dom g & not i in rng h holds g.i= 0*n;
consider h3 being Permutation of dom h,h2 being FinSequence of NAT such that
A5: h2=h*h3 and
A6: h2 is increasing and
A7: dom h=dom h2 and
A8: rng h=rng h2 by A1,Th13;
dom (g*h)=dom h by A2,RELAT_1:27;
then reconsider h33=h3 as Permutation of dom F by A3;
reconsider F22=g*h2 as Function;
dom F22 =dom h by A2,A7,A8,RELAT_1:27
.=Seg len h by FINSEQ_1:def 3;
then reconsider F23=F22 as FinSequence by FINSEQ_1:def 2;
rng F22 c= rng g by RELAT_1:26;
then rng F23 c= REAL n by XBOOLE_1:1;
then reconsider F2=F23 as FinSequence of REAL n by FINSEQ_1:def 4;
F2=F(*)h33 by A3,A5,RELAT_1:36;
then Sum F=Sum F2 by Th20;
hence Sum g =Sum F by A2,A4,A6,A8,Th22;
end;
begin :: 4. Standard Basis
definition
let n, i be Nat;
redefine func Base_FinSeq(n,i) -> Element of REAL n; :: redefines Base_FinSeq (MATRIXR2, definition)
coherence
proof
len (Base_FinSeq(n,i))=n by MATRIXR2:74;
hence thesis by FINSEQ_2:92;
end;
end;
theorem Th24:
for i1,i2 being Nat st 1<=i1 & i1<=n &
Base_FinSeq(n,i1) = Base_FinSeq(n,i2) holds i1=i2
proof
let i1,i2 be Nat;
assume that
A1: 1<=i1 and
A2: i1<=n and
A3: Base_FinSeq(n,i1)=Base_FinSeq(n,i2);
Base_FinSeq(n,i1).i1=1 by A1,A2,MATRIXR2:75;
hence thesis by A1,A2,A3,MATRIXR2:76;
end;
theorem Th25:
sqr Base_FinSeq(n,i) = Base_FinSeq(n,i)
proof
A1: dom (sqrreal * Base_FinSeq(n,i)) = (Base_FinSeq(n,i))"(dom sqrreal) by
RELAT_1:147;
A2: rng (Base_FinSeq(n,i)) c= REAL;
A3: for x being object st x in dom Base_FinSeq(n,i) holds (sqrreal * (
Base_FinSeq(n,i) qua Function)).x=(Base_FinSeq(n,i)).x
proof
let x be object;
assume
A4: x in dom Base_FinSeq(n,i);
then reconsider nx=x as Element of NAT;
A5: (sqrreal * ( Base_FinSeq(n,i) qua Function)).x =sqrreal.((Base_FinSeq
(n,i)).x) by A4,FUNCT_1:13;
A6: x in Seg len (Base_FinSeq(n,i)) by A4,FINSEQ_1:def 3;
then
A7: 1<=nx by FINSEQ_1:1;
len (Base_FinSeq(n,i))=n by MATRIXR2:74;
then
A8: nx<=n by A6,FINSEQ_1:1;
per cases;
suppose
A9: nx=i;
hence
(sqrreal * ( Base_FinSeq(n,i) qua Function)).x =sqrreal.1 by A7,A8,A5,
MATRIXR2:75
.=1^2 by RVSUM_1:def 2
.= (Base_FinSeq(n,i)).x by A7,A8,A9,MATRIXR2:75;
end;
suppose
A10: nx<>i;
hence
(sqrreal * ( Base_FinSeq(n,i) qua Function)).x =sqrreal.0 by A7,A8,A5,
MATRIXR2:76
.=0^2 by RVSUM_1:def 2
.= (Base_FinSeq(n,i)).x by A7,A8,A10,MATRIXR2:76;
end;
end;
(Base_FinSeq(n,i))"(dom sqrreal) =(Base_FinSeq(n,i))"REAL by FUNCT_2:def 1
.=dom (Base_FinSeq(n,i)) by A2,Th1;
hence thesis by A1,A3,FUNCT_1:2;
end;
Lm3: 0 in REAL by XREAL_0:def 1;
theorem Th26:
1<=i & i<=n implies Sum Base_FinSeq(n,i) = 1
proof
assume that
A1: 1<=i and
A2: i<=n;
defpred P[object,object] means (not ($1 in i) implies $2=1)&
($1 in i implies $2=0);
:: !!! ??? funckja charakterystyczna
set F=Base_FinSeq(n,i);
A3: for x being object st x in NAT ex y being object st y in REAL & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider nx=x as Element of NAT;
per cases;
suppose
nx>=i;
then
A4: not nx in Segm i by NAT_1:44;
take y = 1;
thus y in REAL by XREAL_0:def 1;
thus P[x,y] by A4;
end;
suppose
nx<i;
then nx in Segm i by NAT_1:44;
hence ex y being object st y in REAL & P[x,y] by Lm3;
end;
end;
consider f0 being sequence of REAL such that
A5: for x being object st x in NAT holds P[x,f0.x] from FUNCT_2:sch 1(A3);
A6: len Base_FinSeq(n,i) = n by MATRIXR2:74;
A7: for n2 being Nat st 0 <> n2 & n2 < len F holds f0.(n2 + 1) =
addreal.(f0.n2,F.(n2 + 1))
proof
let n2 be Nat;
assume that
0 <> n2 and
A8: n2 < len F;
A9: n2+1<=n by A6,A8,NAT_1:13;
A10: n2 in NAT by ORDINAL1:def 12;
per cases;
suppose
A11: n2+1<i;
then n2<i by NAT_1:13;
then n2 in Segm i by NAT_1:44;
then
A12: f0.n2=0 by A5,A10;
A13: 1<=n2+1 by NAT_1:11;
A14: (n2+1) in Segm i by A11,NAT_1:44;
n2+1<=len F by A8,NAT_1:13;
then addreal.(f0.n2,F.(n2+1))=addreal.(0,0) by A6,A11,A12,A13,MATRIXR2:76
.= 0+0 by BINOP_2:def 9;
hence f0.(n2 + 1) = addreal.(f0.n2,F.(n2 + 1)) by A5,A14;
end;
suppose
A15: i<=n2+1;
per cases by A15,XXREAL_0:1;
suppose
A16: i<n2+1;
then i<=n2 by NAT_1:13;
then
A17: not n2 in Segm i by NAT_1:44;
A18: not n2+1 in Segm i by A16,NAT_1:44;
1<=n2+1 by A1,A16,XXREAL_0:2;
then F.(n2 + 1)=0 by A9,A16,MATRIXR2:76;
then addreal.(f0.n2,F.(n2 + 1))=addreal.(1,0) by A5,A17,A10
.= 1+0 by BINOP_2:def 9;
hence f0.(n2 + 1) = addreal.(f0.n2,F.(n2 + 1)) by A5,A18;
end;
suppose
A19: i=n2+1;
n2<n2+1 by XREAL_1:29;
then n2 in Segm i by A19,NAT_1:44;
then f0.n2=0 by A5,A10;
then
A20: addreal.(f0.n2,F.(n2 + 1))=addreal.(0,1) by A1,A2,A19,MATRIXR2:75
.=0+1 by BINOP_2:def 9;
not n2+1 in i by A19;
hence f0.(n2 + 1) = addreal.(f0.n2,F.(n2 + 1)) by A5,A20;
end;
end;
end;
A21: f0.1=F.1
proof
per cases;
suppose
A22: 1<i;
then 1 in Segm i by NAT_1:44;
then
A23: f0.1=0 by A5;
1<=n by A1,A2,XXREAL_0:2;
hence f0.1=F.1 by A22,A23,MATRIXR2:76;
end;
suppose
A24: 1>=i;
then not 1 in Segm i by NAT_1:44;
then
A25: f0.1=1 by A5;
1=i by A1,A24,XXREAL_0:1;
hence f0.1=F.1 by A2,A25,MATRIXR2:75;
end;
end;
A26: f0.(len F)=1
proof
per cases;
suppose
len F<i;
hence f0.(len F)=1 by A2,MATRIXR2:74;
end;
suppose
len F >=i;
then not len F in Segm i by NAT_1:44;
hence f0.(len F)=1 by A5;
end;
end;
len (Base_FinSeq(n,i)) >=1 by A1,A2,A6,XXREAL_0:2;
hence thesis by A21,A26,A7,FINSOP_1:def 1;
end;
theorem Th27:
1<=i & i<=n implies |. Base_FinSeq(n,i) .| = 1
proof
assume that
A1: 1<=i and
A2: i<=n;
sqrt Sum (Base_FinSeq(n,i))=1 by A1,A2,Th26,SQUARE_1:18;
hence thesis by Th25;
end;
theorem Th28:
1<=i & i<=n & i<>j implies |( Base_FinSeq(n,i),Base_FinSeq(n,j))| = 0
proof
assume that
A1: 1<=i and
A2: i<=n and
A3: i<>j;
set x1=Base_FinSeq(n,i),x2=Base_FinSeq(n,j);
A4: dom (0*n)=Seg len (n |-> (0 qua Real)) by FINSEQ_1:def 3
.=Seg n by CARD_1:def 7;
A5: dom x2=Seg len x2 by FINSEQ_1:def 3
.=Seg n by MATRIXR2:74;
A6: dom x1=Seg len x1 by FINSEQ_1:def 3
.=Seg n by MATRIXR2:74;
A7: dom (<:x1,x2:>)=(dom x1) /\ dom x2 by FUNCT_3:def 7;
dom (multreal)=[:REAL,REAL:] by FUNCT_2:def 1;
then
A8: dom (multreal* (<:x1,x2:>)) = (<:x1,x2:>)"([:REAL,REAL:]) by RELAT_1:147
.=Seg n by A7,A6,A5,RELSET_1:22;
for x being object st x in dom (0*n)
holds (multreal* <:x1,x2:>).x= (0*n). x
proof
let x be object;
assume
A9: x in dom (0*n);
then reconsider nx=x as Element of NAT;
A10: (multreal* <:x1,x2:>).x=multreal.((<:x1,x2:>).x) by A4,A8,A9,FUNCT_1:12
.=multreal.([x1.nx,x2.nx]) by A4,A7,A6,A5,A9,FUNCT_3:def 7;
A11: nx<=n by A4,A9,FINSEQ_1:1;
A12: 1<=nx by A4,A9,FINSEQ_1:1;
per cases;
suppose
A13: nx=i;
then
A14: x1.nx=1 by A1,A2,MATRIXR2:75;
A15: x2.nx=0 by A1,A2,A3,A13,MATRIXR2:76;
multreal.([x1.nx,x2.nx])= multreal.(x1.nx,x2.nx)
.=1*0 by A15,A14,BINOP_2:def 11
.=0;
hence (multreal* <:x1,x2:>).x= (0*n).x by A10;
end;
suppose
A16: nx<>i;
reconsider r=x2.nx as Element of REAL by XREAL_0:def 1;
A17: x1.nx=0 by A12,A11,A16,MATRIXR2:76;
multreal.([x1.nx,x2.nx])= multreal.(x1.nx,x2.nx)
.=0 * r by A17,BINOP_2:def 11
.=0;
hence (multreal* <:x1,x2:>).x= (0*n).x by A10;
end;
end;
then multreal* <:x1,x2:>= 0*n by A4,A8,FUNCT_1:2;
then multreal .: (x1,x2)=0*n by FUNCOP_1:def 3;
hence |( Base_FinSeq(n,i),Base_FinSeq(n,j) )|=0 by RVSUM_1:81;
end;
theorem Th29:
for x being Element of REAL n st 1<=i & i<=n holds
|( x,Base_FinSeq(n,i) )| = x.i
proof
let x be Element of REAL n;
assume that
A1: 1<=i and
A2: i<=n;
set x2=Base_FinSeq(n,i);
A3: len x=n by CARD_1:def 7;
A4: len x2=n by MATRIXR2:74;
then
A5: len (mlt(x,x2))=n by A3,MATRPROB:30;
A6: for j being Nat st 1<=j & j<=n holds (mlt(x,x2)).j=((x/.i)*(Base_FinSeq(
n,i))).j
proof
let j be Nat;
assume that
A7: 1<=j and
A8: j<=n;
reconsider j0=j as Element of NAT by ORDINAL1:def 12;
A9: now
per cases;
case i=j;
hence ((x/.i)*(Base_FinSeq(n,i))).j=(x/.j)*((Base_FinSeq(n,i)).j) by
RVSUM_1:44;
end;
case i<>j;
then
A10: (Base_FinSeq(n,i)).j0=0 by A7,A8,MATRIXR2:76;
((x/.i)*(Base_FinSeq(n,i))).j=(x/.i)*((Base_FinSeq(n,i)).j) by
RVSUM_1:44
.= (x/.j)*((Base_FinSeq(n,i)).j) by A10;
hence ((x/.i)*(Base_FinSeq(n,i))).j=(x/.j)*((Base_FinSeq(n,i)).j);
end;
end;
(mlt(x,x2)).j=(x.j)*(x2.j) by RVSUM_1:59;
hence (mlt(x,x2)).j=((x/.i)*(Base_FinSeq(n,i))).j by A3,A7,A8,A9,
FINSEQ_4:15;
end;
len ((x/.i)*(Base_FinSeq(n,i)))=n by A4,RVSUM_1:117;
then (mlt(x,x2))= (x/.i)*(Base_FinSeq(n,i)) by A5,A6,FINSEQ_1:14;
then Sum mlt(x,x2)=(x/.i)*(Sum (Base_FinSeq(n,i))) by RVSUM_1:87
.=(x/.i)*1 by A1,A2,Th26
.=x.i by A1,A2,A3,FINSEQ_4:15;
hence |( x, Base_FinSeq(n,i) )| = x.i;
end;
definition
let n be Nat;
let x0 be Element of REAL n;
func ProjFinSeq x0 -> FinSequence of REAL n means :Def12:
len it = n & for i being Nat st 1<=i & i<=n holds
it.i = |( x0,Base_FinSeq(n,i) )| * Base_FinSeq(n,i);
existence
proof
defpred P[set,set] means for i being Nat st i=$1 & 1<=i & i<=n holds $2=
|( x0,Base_FinSeq(n,i) )|*Base_FinSeq(n,i);
A1: for k being Nat st k in Seg n ex x being Element of REAL n st P[k,x]
proof
reconsider n0=n as Element of NAT by ORDINAL1:def 12;
let k be Nat;
assume k in Seg n;
reconsider k0=k as Element of NAT by ORDINAL1:def 12;
reconsider x00=(|( x0,Base_FinSeq(n0,k0) )|)*(Base_FinSeq(n0,k0) ) as
Element of REAL n;
for i being Nat st i=k & 1<=i & i<=n holds x00 = (|( x0,Base_FinSeq(
n,i) )|)*(Base_FinSeq(n,i));
hence ex x being Element of REAL n st P[k,x];
end;
consider p being FinSequence of REAL n such that
A2: dom p = Seg n & for k being Nat st k in Seg n holds P[k,p.k] from
FINSEQ_1:sch 5(A1);
A3: for i being Nat st 1<=i & i<=n holds p.i= (|( x0,Base_FinSeq(n,i) )|)*
(Base_FinSeq(n,i) ) by FINSEQ_1:1,A2;
Seg n=Seg len p by A2,FINSEQ_1:def 3;
hence thesis by A3,FINSEQ_1:6;
end;
uniqueness
proof
let r1,r2 be FinSequence of REAL n;
assume that
A4: len r1=n and
A5: for i being Nat st 1<=i & i<=n holds r1.i= (|( x0, Base_FinSeq(n,
i) )|)*(Base_FinSeq(n,i) ) and
A6: len r2=n and
A7: for i being Nat st 1<=i & i<=n holds r2.i= (|( x0, Base_FinSeq(n,
i) )|)*(Base_FinSeq(n,i) );
for k being Nat st 1<=k & k<=n holds r1.k=r2.k
proof
reconsider n22=n as Element of NAT by ORDINAL1:def 12;
let k be Nat;
assume that
A8: 1<=k and
A9: k<=n;
reconsider k0=k as Element of NAT by ORDINAL1:def 12;
r1.k0= (|( x0,Base_FinSeq(n22,k0) )|)*(Base_FinSeq(n22,k0) ) by A5,A8
,A9;
hence r1.k=r2.k by A7,A8,A9;
end;
hence r1=r2 by A4,A6,FINSEQ_1:14;
end;
end;
theorem Th30:
for x0 being Element of REAL n holds x0 = Sum (ProjFinSeq x0)
proof
let x0 be Element of REAL n;
set f=ProjFinSeq x0;
reconsider n2=n as Element of NAT by ORDINAL1:def 12;
now
per cases;
case
A1: len f>0;
set g2 = accum f;
A2: len f=len g2 by Def10;
A3: f.1=g2.1 by Def10;
defpred P[Nat] means for i being Nat st 1<=i & i<=len f & 1<=$1 & $1<=
len f holds (i<= $1 implies (g2/.$1).i= x0.i)& (i> $1 implies (g2/.$1).i=0);
A4: len f=n by Def12;
A5: 0+1<=len f by A1,NAT_1:13;
A6: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
reconsider k2=k as Element of NAT by ORDINAL1:def 12;
assume
A7: P[k];
for i being Nat st 1<=i & i<=len f & 1<=k+1 & k+1<=len f holds (i
<= k+1 implies (g2/.(k+1)).i= x0.i)& (i> k+1 implies (g2/.(k+1)).i=0)
proof
let i be Nat;
assume that
A8: 1<=i and
A9: i<=len f and
A10: 1<=k+1 and
A11: k+1<=len f;
g2/.(k+1) is Element of REAL n;
then reconsider r=g2.(k+1) as Element of REAL n by A2,A10,A11,
FINSEQ_4:15;
reconsider i2=i as Element of NAT by ORDINAL1:def 12;
A12: g2/.(k+1)=g2.(k+1) by A2,A10,A11,FINSEQ_4:15;
now
per cases;
case
A13: 1<=k;
reconsider r3=f/.(k+1) as Element of REAL n;
reconsider r2=g2/.k as Element of REAL n;
A14: (ProjFinSeq x0)/.(k+1)=(ProjFinSeq x0).(k+1) by A10,A11,
FINSEQ_4:15
.=(|( x0,Base_FinSeq(n2,k+1) )|)*(Base_FinSeq(n2,k+1) ) by A4
,A10,A11,Def12;
A15: k<k+1 by XREAL_1:29;
then
A16: k<len f by A11,XXREAL_0:2;
then r=g2/.k + f/.(k+1) by Def10,A13;
then
A17: r.i=r2.i+r3.i by RVSUM_1:11;
A18: now
assume
A19: i<=k+1;
per cases by A19,XXREAL_0:1;
suppose
A20: i<k+1;
then
A21: i<=k by NAT_1:13;
(f/.(k+1)).i = |(x0,Base_FinSeq(n2,k+1))|*((Base_FinSeq
(n2,k2+1) ).i2) by A14,RVSUM_1:44
.= |( x0,Base_FinSeq(n2,k+1) )|* 0 by A4,A8,A9,A20,
MATRIXR2:76;
hence
(g2/.(k+1)).i= x0.i by A7,A8,A9,A12,A13,A16,A17,A21;
end;
suppose
A22: i=k+1;
then
A23: (g2/.k).i= 0 by A7,A8,A9,A13,A15,A16;
(f/.(k+1)).i = |(x0,Base_FinSeq(n2,k+1))|*((Base_FinSeq
(n2,k2+1) ).i2) by A14,RVSUM_1:44
.= (|( x0,Base_FinSeq(n2,k+1) )|)* 1 by A4,A8,A9,A22,
MATRIXR2:75
.= x0.(k+1) by A4,A10,A11,Th29;
hence (g2/.(k+1)).i= x0.i by A2,A8,A9,A17,A22,A23,FINSEQ_4:15
;
end;
end;
now
assume
A24: i>k+1; then
A25: i>k by A15,XXREAL_0:2;
(f/.(k+1)).i = (|( x0,Base_FinSeq(n2,k+1) )|)*((
Base_FinSeq(n2,k2+1) ).i2) by A14,RVSUM_1:44
.= (|( x0,Base_FinSeq(n2,k+1) )|)* 0 by A4,A8,A9,A24,
MATRIXR2:76
.= 0;
hence (g2/.(k+1)).i=0 by A7,A8,A9,A12,A13,A16,A17,A25;
end;
hence (i<= k+1 implies (g2/.(k+1)).i= x0.i)& (i> k+1 implies (g2
/.(k+1)).i= 0) by A18;
end;
case
k<1;
then
A26: k+1<= 0+1 by NAT_1:13;
then
A27: k=0 by XREAL_1:6;
A28: now
assume
A29: i> 0+1;
(g2/.1)=f.1 by A5,A2,A3,FINSEQ_4:15;
then
(g2/.1).i= ((|( x0,Base_FinSeq(n2,1) )|)*(Base_FinSeq(n2,
1) )).i by A5,A4,Def12
.= (|( x0,Base_FinSeq(n2,1) )|)*((Base_FinSeq(n2,1) ).i2)
by RVSUM_1:44
.= (|( x0,Base_FinSeq(n2,1) )|)* 0 by A4,A9,A29,MATRIXR2:76
.= 0;
hence (g2/.(k+1)).i= 0 by A27;
end;
A30: now
assume i<= 0+1; then
A31: i=1 by A8,XXREAL_0:1;
(g2/.1)=f.1 by A5,A2,A3,FINSEQ_4:15;
then
(g2/.1).1= ((|( x0,Base_FinSeq(n2,1) )|)*(Base_FinSeq(n2,
1) )).1 by A5,A4,Def12
.= (|( x0,Base_FinSeq(n2,1) )|)*((Base_FinSeq(n2,1) ).1)
by RVSUM_1:44
.= (|( x0,Base_FinSeq(n2,1) )|)* 1 by A5,A4,MATRIXR2:75
.= x0.1 by A5,A4,Th29;
hence (g2/.(0+1)).i= x0.i by A31;
end;
k<=0 by A26,XREAL_1:6;
hence (i<= k+1 implies (g2/.(k+1)).i= x0.i)& (i> k+1 implies (g2
/.(k+1)).i= 0) by A30,A28;
end;
end;
hence thesis;
end;
hence P[k+1];
end;
reconsider r4=g2/.(len f) as Element of REAL n;
A32: len x0=n by CARD_1:def 7;
then
A33: len x0 = len r4 by CARD_1:def 7;
A34: P[0];
A35: for k being Nat holds P[k] from NAT_1:sch 2(A34,A6);
for i being Nat st 1<=i & i<=len (r4) holds (g2/.(len f)).i=x0.i
proof
let i be Nat;
assume that
A36: 1<=i and
A37: i<=len r4;
A38: i<=len f by A4,A37,CARD_1:def 7;
1<=len f by A4,A32,A33,A36,A37,XXREAL_0:2;
hence (g2/.(len f)).i=x0.i by A35,A36,A38;
end;
then x0=g2/.(len f) by A33,FINSEQ_1:14;
hence x0=g2.(len f) by A5,A2,FINSEQ_4:15;
end;
case len f<=0; then
A39: n=0 by Def12;
then x0=<*>REAL;
hence x0 = 0*n by A39;
end;
end;
hence x0=Sum (ProjFinSeq x0) by Def11;
end;
definition
let n be Nat;
func RN_Base n -> Subset of REAL n equals
{ Base_FinSeq(n,i) where i is
Element of NAT: 1<=i & i<=n };
coherence
proof
{ Base_FinSeq(n,i) where i is Element of NAT: 1<=i & i<=n} c= REAL n
proof
let x be object;
assume x in { Base_FinSeq(n,i) where i is Element of NAT: 1<=i & i<=n};
then ex i being Element of NAT st x=Base_FinSeq(n,i) & 1<=i & i<=n;
hence x in REAL n;
end;
hence thesis;
end;
end;
theorem Th31:
for n being non zero Nat holds RN_Base n <> {}
proof
let n be non zero Nat;
0+1 <= n by NAT_1:13;
then
Base_FinSeq(n,1) in { Base_FinSeq(n,i) where i is Element of NAT: 1<=i &
i<=n};
hence thesis;
end;
registration
cluster RN_Base 0 -> empty;
coherence
proof
assume not thesis;
then consider x being object such that
A1: x in RN_Base 0 by XBOOLE_0:def 1;
ex i being Element of NAT st x = Base_FinSeq(0,i) & 1<=i & i<=0 by A1;
hence thesis;
end;
end;
registration
let n be non zero Nat;
cluster RN_Base n -> non empty;
coherence by Th31;
end;
registration
let n;
cluster RN_Base n -> orthogonal_basis;
coherence
proof
set B=RN_Base n;
A1: {x where x is Element of REAL n: ex i being Element of NAT st 1<=i & i
<=n & x=Base_FinSeq(n,i)} c= B
proof
let y be object;
assume y in {x where x is Element of REAL n: ex i being Element of NAT
st 1<=i & i<=n & x=Base_FinSeq(n,i)};
then
ex x being Element of REAL n st y=x & ex i being Element of NAT st 1
<=i & i<=n & x=Base_FinSeq(n,i);
hence y in B;
end;
B c= {x where x is Element of REAL n: ex i being Element of NAT st 1<=
i & i<=n & x=Base_FinSeq(n,i)}
proof
let y be object;
assume y in B;
then
ex i2 being Element of NAT st y=Base_FinSeq(n,i2) & 1<= i2 & i2<= n;
hence y in {x where x is Element of REAL n: ex i being Element of NAT st
1<=i & i<=n & x=Base_FinSeq(n,i)};
end;
then
A2: B={x where x is Element of REAL n: ex i being Element of NAT st 1<=i
& i<=n & x=Base_FinSeq(n,i)} by A1,XBOOLE_0:def 10;
thus B is R-orthogonal
proof
let x,y be real-valued FinSequence;
assume that
A3: x in B and
A4: y in B and
A5: x<>y;
A6: ex y0 being Element of REAL n st y=y0 & ex i being Element of NAT
st 1<=i & i<=n & y0=Base_FinSeq(n,i) by A2,A4;
ex x0 being Element of REAL n st x=x0 & ex i being Element of NAT
st 1<=i & i<=n & x0=Base_FinSeq(n,i) by A2,A3;
hence |( x,y )|=0 by A5,A6,Th28;
end;
thus B is R-normal
proof
let x be real-valued FinSequence;
assume x in B;
then ex x0 being Element of REAL n st x=x0 & ex i being Element of NAT
st 1<=i & i<=n & x0=Base_FinSeq(n,i) by A2;
hence |.x.|=1 by Th27;
end;
let B2 be R-orthonormal Subset of REAL n;
assume
A7: B c= B2;
now
assume not B2 c= B;
then consider x being object such that
A8: x in B2 and
A9: not x in B;
reconsider rx=x as Element of REAL n by A8;
A10: now
assume rx<> 0*n;
then consider i being Element of NAT such that
A11: 1<=i and
A12: i<=n and
A13: rx.i<>0 by JORDAN2C:46;
Base_FinSeq(n,i) in B by A11,A12;
then |( rx,Base_FinSeq(n,i) )|=0 by A7,A8,A9,Def3;
hence contradiction by A11,A12,A13,Th29;
end;
|. 0*n .|=0 by EUCLID:7;
hence contradiction by A8,A10,Def4;
end;
hence thesis by A7,XBOOLE_0:def 10;
end;
end;
registration
let n;
cluster orthogonal_basis for Subset of REAL n;
existence
proof
take RN_Base n;
thus thesis;
end;
end;
definition
let n;
mode Orthogonal_Basis of n is orthogonal_basis Subset of REAL n;
end;
registration
let n be non zero Nat;
cluster -> non empty for Orthogonal_Basis of n;
coherence
proof
let B be Orthogonal_Basis of n;
assume
A1: B is empty;
then B c= RN_Base n;
hence contradiction by A1,Def6;
end;
end;
begin :: 5. Finite Real Unitary Spaces and Finite Real Linear Spaces
registration
let n be Element of NAT;
cluster REAL-US n -> constituted-FinSeqs;
coherence
proof
let a be Element of REAL-US n;
reconsider a as Element of REAL n by REAL_NS1:def 6;
a is FinSequence of REAL;
hence thesis;
end;
end;
registration
let n be Element of NAT;
cluster -> real-valued for Element of REAL-US n;
coherence
proof
let a be Element of REAL-US n;
reconsider a as Element of REAL n by REAL_NS1:def 6;
a is FinSequence of REAL;
hence thesis;
end;
end;
registration
let n be Element of NAT;
let x, y be VECTOR of REAL-US n, a, b be real-valued Function;
identify x+y with a+b when x = a, y = b;
compatibility
proof
assume that
A1: x=a and
A2: y=b;
reconsider a1=a, b1=b as Element of REAL n by A1,A2,REAL_NS1:def 6;
thus x+y = (Euclid_add n).(a1,b1) by A1,A2,REAL_NS1:def 6
.= a+b by REAL_NS1:def 1;
end;
end;
registration
let n be Element of NAT,
x be VECTOR of REAL-US n, y be real-valued Function,
a, b be Element of REAL;
identify a*x with b(#)y when x = y, a = b;
compatibility
proof
assume that
A1: x = y and
A2: a = b;
reconsider y1=y as Element of REAL n by A1,REAL_NS1:def 6;
thus a * x =(Euclid_mult n).(b,y1) by A1,A2,REAL_NS1:def 6
.= b (#) y by REAL_NS1:def 2;
end;
end;
registration
let n be Element of NAT;
let x be VECTOR of REAL-US n, a be real-valued Function;
identify -x with -a when x = a;
compatibility
proof
x is Element of REAL n by REAL_NS1:def 6;
then reconsider xn=x as Element of REAL-NS n by REAL_NS1:def 4;
assume
A1: x = a;
then reconsider a1=a as Element of REAL n by REAL_NS1:def 6;
thus -x = -xn by REAL_NS1:13
.= -a1 by A1,REAL_NS1:4
.= -a;
end;
end;
registration
let n be Element of NAT;
let x, y be VECTOR of REAL-US n, a, b be real-valued Function;
identify x-y with a-b when x = a, y = b;
compatibility;
end;
theorem Th32:
for n,j being Element of NAT,
F being FinSequence of the carrier of REAL-US n,
Bn being Subset of REAL-US n, v0 being Element of REAL-US n,
l being Linear_Combination of Bn st
F is one-to-one & Bn is R-orthogonal &
rng F = Carrier l & v0 in Bn & j in dom (l (#) F) &
v0=F.j holds (Euclid_scalar n).(v0,Sum (l(#)F)) =
(Euclid_scalar n).(v0,(l.(F/.j))*v0)
proof
let n,j be Element of NAT, F be FinSequence of the carrier of (REAL-US n),
Bn be Subset of REAL-US n, v0 be Element of REAL-US n,
l be Linear_Combination of Bn;
assume that
A1: F is one-to-one and
A2: Bn is R-orthogonal and
A3: rng F= Carrier l and
A4: v0 in Bn and
A5: j in dom (l (#) F) and
A6: v0=F.j;
A7: ( len (l (#) F) ) = len F by RLVECT_2:def 7;
then
A8: dom (l(#)F)=Seg len F by FINSEQ_1:def 3
.=dom F by FINSEQ_1:def 3;
reconsider F2= l(#) F as FinSequence of the carrier of (REAL-US n);
reconsider rv0=v0 as Element of REAL n by REAL_NS1:def 6;
A9: Carrier l c= Bn by RLVECT_2:def 6;
A10: dom (l(#)F)=Seg len (l(#)F) by FINSEQ_1:def 3;
then
A11: j<=len F by A5,A7,FINSEQ_1:1;
consider f being sequence of the carrier of (REAL-US n) such that
A12: Sum(F2) = f . (len F2) and
A13: f.0 = 0.(REAL-US n) and
A14: for j2 being Nat for v being Element of REAL-US n st j2
< len F2 & v = F2 . (j2 + 1) holds f . (j2 + 1) = (f . j2) + v by
RLVECT_1:def 12;
defpred Q[Nat] means $1>=j & $1<=len F implies (Euclid_scalar n).(v0,f.$1) =
(Euclid_scalar n).(v0,(l.(F/.j))*v0);
defpred P[Nat] means $1<j implies (Euclid_scalar n).(v0,f.$1)=0;
0.(REAL-US n)= 0*n by REAL_NS1:def 6;
then (Euclid_scalar n).(v0,f.0) = |( rv0, 0*n )| by A13,REAL_NS1:def 5
.= 0 by EUCLID_4:18;
then
A15: P[0];
A16: j in Seg len F by A5,A7,FINSEQ_1:def 3;
then
A17: j<=len F2 by A7,FINSEQ_1:1;
A18: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A19: P[k];
now
per cases;
case
A20: k<len F2;
A21: 1<=k+1 by NAT_1:11;
k+1<= len F2 by A20,NAT_1:13;
then k+1 in Seg len F2 by A21,FINSEQ_1:1;
then k+1 in dom F2 by FINSEQ_1:def 3;
then F2.(k+1) in rng F2 by FUNCT_1:def 3;
then reconsider v=F2 . (k + 1) as Element of REAL-US n;
A22: f . (k + 1) = (f . k) + v by A14,A20;
reconsider rv=v as Element of REAL n by REAL_NS1:def 6;
reconsider fk=f.k as Element of REAL n by REAL_NS1:def 6;
per cases;
suppose
A23: k+1<j;
A24: 1<=k+1 by NAT_1:11;
k+1<len F by A11,A23,XXREAL_0:2;
then k+1 in Seg len F by A24,FINSEQ_1:1;
then
A25: k+1 in dom F by FINSEQ_1:def 3;
then
A26: F/.(k+1)=F.(k+1) by PARTFUN1:def 6;
then
A27: rv0<>F/.(k+1) by A1,A5,A6,A8,A23,A25,FUNCT_1:def 4;
reconsider fk1=F/.(k+1) as Element of REAL n by REAL_NS1:def 6;
A28: k<k+1 by XREAL_1:29;
A29: |(rv0,fk+rv)|= |(rv0,fk)| +|(rv0,rv)| by EUCLID_4:28;
A30: F/.(k+1) in rng F by A25,A26,FUNCT_1:def 3;
v=(l . (F /. (k+1))) * (F /. (k+1)) by A8,A25,RLVECT_2:def 7;
then |(rv0,rv)|= (l . (F /. (k+1))) * (|(rv0,fk1)|) by EUCLID_4:22
.= (l . (F /. (k+1))) * 0 by A2,A3,A4,A9,A30,A27
.=0;
then |( rv0, fk+rv )| = 0 by A19,A23,A28,A29,REAL_NS1:def 5
,XXREAL_0:2;
hence P[k+1] by A22,REAL_NS1:def 5;
end;
suppose
k+1>=j;
hence P[k+1];
end;
end;
case
A31: k>=len F2;
k+1>k by XREAL_1:29;
then k+1>len F2 by A31,XXREAL_0:2;
hence P[k+1] by A17,XXREAL_0:2;
end;
end;
hence P[k+1];
end;
A32: for i being Nat holds P[i] from NAT_1:sch 2(A15,A18);
A33: for i being Nat st i<j holds (Euclid_scalar n).(v0,f.i)=0 by A32;
A34: for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume
A35: Q[k];
per cases;
suppose
k+1<j;
hence Q[k+1];
end;
suppose
A36: k+1>=j;
per cases by A36,XXREAL_0:1;
suppose
A37: k+1>j;
per cases;
suppose
A38: k+1<=len F2;
1<=k+1 by NAT_1:11;
then
A39: k+1 in Seg len F2 by A38,FINSEQ_1:1;
then
A40: k+1 in dom F by A7,FINSEQ_1:def 3;
then
A41: F/.(k+1)=F.(k+1) by PARTFUN1:def 6;
then
A42: F/.(k+1) in rng F by A40,FUNCT_1:def 3;
k+1 in dom F2 by A39,FINSEQ_1:def 3;
then F2.(k+1) in rng F2 by FUNCT_1:def 3;
then reconsider v=F2 . (k + 1) as Element of REAL-US n;
reconsider fk1=F/.(k+1) as Element of REAL n by REAL_NS1:def 6;
reconsider fk=f.k as Element of REAL n by REAL_NS1:def 6;
k<k+1 by XREAL_1:29;
then
A43: k<len F2 by A38,XXREAL_0:2;
then
A44: f . (k + 1) = (f . k) + v by A14;
A45: rv0<>F/.(k+1) by A1,A5,A6,A8,A37,A40,A41,FUNCT_1:def 4;
reconsider rv=v as Element of REAL n by REAL_NS1:def 6;
v=(l . (F /. (k+1))) * (F /. (k+1)) by A8,A40,RLVECT_2:def 7;
then
A46: |(rv0,rv)|= (l . (F /. (k+1))) * (|(rv0,fk1)|) by EUCLID_4:22
.= (l . (F /. (k+1))) * 0 by A2,A3,A4,A9,A42,A45
.=0;
|(rv0,fk+rv)|= |(rv0,fk)| +|(rv0,rv)| by EUCLID_4:28;
then
|( rv0, fk+rv )| = (Euclid_scalar n).(v0,(l.(F/.j))*v0) by A35,A37
,A43,A46,NAT_1:13,REAL_NS1:def 5,RLVECT_2:def 7;
hence Q[k+1] by A44,REAL_NS1:def 5;
end;
suppose
k+1>len F2;
hence Q[k+1] by RLVECT_2:def 7;
end;
end;
suppose
A47: k+1=j;
then F2.(k+1) in rng F2 by A5,FUNCT_1:def 3;
then reconsider v=F2 . (k + 1) as Element of REAL-US n;
reconsider rv=v as Element of REAL n by REAL_NS1:def 6;
A48: v=(l . (F /. (k+1))) * (F /. (k+1)) by A5,A47,RLVECT_2:def 7;
k+1 in dom F by A5,A10,A7,A47,FINSEQ_1:def 3;
then
A49: |(rv0,rv)|= |(rv0,(l . (F /. (j))) *rv0 )| by A6,A47,A48,PARTFUN1:def 6
.=(Euclid_scalar n).(v0,(l.(F/.j))*v0) by REAL_NS1:def 5;
k<k+1 by XREAL_1:29;
then k<len F2 by A7,A11,A47,XXREAL_0:2;
then
A50: f . (k + 1) = (f . k) + v by A14;
reconsider fk=f.k as Element of REAL n by REAL_NS1:def 6;
(Euclid_scalar n).(v0,f.k) =0 by A33,A47,XREAL_1:29;
then
A51: |(rv0,fk)|=0 by REAL_NS1:def 5;
|(rv0,fk+rv)|= |(rv0,fk)| +|(rv0,rv)| by EUCLID_4:28;
hence Q[k+1] by A50,A51,A49,REAL_NS1:def 5;
end;
end;
end;
A52: Q[0] by A16,FINSEQ_1:1;
A53: for i being Nat holds Q[i] from NAT_1:sch 2(A52,A34);
for i being Nat st i>=j & i<=len F holds (Euclid_scalar n).(v0,f.i) = (
Euclid_scalar n).(v0,(l.(F/.j))*v0)by A53;
hence thesis by A12,A7,A11;
end;
theorem Th33:
for n being Element of NAT, f being FinSequence of REAL n, g
being FinSequence of the carrier of (REAL-US n) st f=g holds Sum f=Sum g
proof
let n be Element of NAT, f be FinSequence of REAL n, g be FinSequence of the
carrier of (REAL-US n);
set V=REAL-US n;
assume
A1: f=g;
now
per cases;
case
A2: len f>0;
set g2 = accum f;
A3: len f=len g2 by Def10;
A4: f.1=g2.1 by Def10;
A5: Sum f=g2.(len f) by A2,Def11;
deffunc F(set)=IFIN($1,len f+1,IFEQ($1,0, 0.V, g2/.$1),0.V);
A6: for x being set st x in NAT holds F(x) in the carrier of V
proof
let x be set;
assume x in NAT;
then reconsider nx=x as Element of NAT;
per cases;
suppose
nx in len f+1;
then
A7: F(x)=IFEQ(x,0, 0.V, g2/.nx) by MATRIX_7:def 1;
per cases;
suppose
x=0;
then F(x)=0.V by A7,FUNCOP_1:def 8;
hence F(x) in the carrier of V;
end;
suppose
A8: x<>0;
A9: the carrier of V=REAL n by REAL_NS1:def 6;
F(x)=g2/.nx by A7,A8,FUNCOP_1:def 8;
hence F(x) in the carrier of V by A9;
end;
end;
suppose
not nx in len f +1;
then F(x)=0.V by MATRIX_7:def 1;
hence F(x) in the carrier of V;
end;
end;
consider f3 being sequence of the carrier of V such that
A10: for x being set st x in NAT holds f3.x = F(x) from FUNCT_2:sch
11( A6);
A11: for j being Nat for v being Element of V st j < len g &
v = g . (j + 1) holds f3 . (j + 1) = (f3 . j) + v
proof
let j be Nat;
A12: j in NAT by ORDINAL1:def 12;
let v be Element of V;
assume that
A13: j < len g and
A14: v = g . (j + 1);
A15: j+1<=len f by A1,A13,NAT_1:13;
per cases;
suppose
A16: j=0;
then j+1<len f+1 by A2,XREAL_1:6;
then
A17: (j+1) in Segm(len f+1) by NAT_1:44;
A18: 0 in Segm(len f +1) by NAT_1:44;
A19: f3.j=IFIN(j,len f+1,IFEQ(j,0, 0.V, g2/.j),0.V) by A10,A12
.= IFEQ(j,0, 0.V, g2/.j) by A16,A18,MATRIX_7:def 1
.= 0.V by A16,FUNCOP_1:def 8;
thus f3.(j+1)=IFIN(j+1,len f+1,IFEQ(j+1,0, 0.V, g2/.(j+1)),0.V) by
A10
.=IFEQ(j+1,0, 0.V, g2/.(j+1)) by A17,MATRIX_7:def 1
.=g2/.1 by A16,FUNCOP_1:def 8
.=g.(j+1) by A1,A3,A4,A15,A16,FINSEQ_4:15
.= (f3.j)+v by A14,A19,RLVECT_1:4;
end;
suppose
A20: j<>0;
len f<len f+1 by XREAL_1:29;
then j< len f+1 by A1,A13,XXREAL_0:2;
then
A21: j in Segm(len f +1) by NAT_1:44;
A22: f3.j=IFIN(j,len f+1,IFEQ(j,0, 0.V, g2/.j),0.V) by A10,A12
.= IFEQ(j,0, 0.V, g2/.j) by A21,MATRIX_7:def 1
.= g2/.j by A20,FUNCOP_1:def 8;
A23: 0+1<=j+1 by NAT_1:13;
A24: 0+1<=j by A20,NAT_1:13;
j+1<len f+1 by A1,A13,XREAL_1:6;
then
A25: (j+1) in Segm(len f+1) by NAT_1:44;
thus f3.(j+1)=IFIN(j+1,len f+1,IFEQ(j+1,0, 0.V, g2/.(j+1)),0.V) by
A10
.=IFEQ(j+1,0, 0.V, g2/.(j+1)) by A25,MATRIX_7:def 1
.=g2/.(j+1) by FUNCOP_1:def 8
.=g2.(j+1) by A3,A15,A23,FINSEQ_4:15
.=(g2/.j)+(f/.(j+1)) by A1,Def10,A13,A24
.=(f3.j)+v by A1,A14,A15,A23,A22,FINSEQ_4:15;
end;
end;
len f <len f+1 by XREAL_1:29;
then
A26: len f in Segm(len f+1) by NAT_1:44;
A27: 0+1<=len f by A2,NAT_1:13;
A28: 0 in Segm(len f +1) by NAT_1:44;
A29: f3.0=IFIN(0,len f+1,IFEQ(0,0, 0.V, g2/.0),0.V) by A10
.=IFEQ(0,0, 0.V, g2/.0) by A28,MATRIX_7:def 1
.=0.V by FUNCOP_1:def 8;
f3.(len g)=F(len f) by A1,A10
.=IFEQ(len f,0,0.V,g2/.(len f)) by A26,MATRIX_7:def 1
.=g2/.(len f) by A2,FUNCOP_1:def 8
.=Sum f by A3,A5,A27,FINSEQ_4:15;
hence
ex f2 being sequence of the carrier of V st Sum f = f2 . (len g
) & f2 . 0 = 0. V & for j being Nat for v being Element of V st j <
len g & v = g . (j + 1) holds f2 . (j + 1) = (f2 . j) + v by A29,A11;
end;
case
A30: len f<=0;
set f3 = NAT --> 0.V;
A31: for j being Nat for v being Element of V st j < len g &
v = g . (j + 1) holds f3 . (j + 1) = (f3 . j) + v by A1,A30;
A32: f3.(len g)=0.V by FUNCOP_1:7
.= 0*n by REAL_NS1:def 6;
A33: f3.0=0.V by FUNCOP_1:7;
Sum f = 0*n by A30,Def11;
hence
ex f2 being sequence of the carrier of V st Sum f = f2 . (len g
) & f2 . 0 = 0. V & for j being Nat for v being Element of V st j <
len g & v = g . (j + 1) holds f2 . (j + 1) = (f2 . j) + v by A32,A33,A31;
end;
end;
hence Sum f=Sum g by RLVECT_1:def 12;
end;
registration
let A be set;
cluster RealVectSpace(A) -> constituted-Functions;
coherence;
end;
registration
let n;
cluster RealVectSpace(Seg n) -> constituted-FinSeqs;
coherence
proof
let a be Element of RealVectSpace(Seg n);
a is Element of REAL n by FINSEQ_2:93;
hence thesis;
end;
end;
registration
let A be set;
cluster -> real-valued for Element of RealVectSpace(A);
coherence
proof
let a be Element of RealVectSpace(A);
a is Function of A,REAL or a is empty by FUNCT_2:66;
hence thesis;
end;
end;
registration
let A be set;
let x, y be VECTOR of RealVectSpace(A), a, b be real-valued Function;
identify x+y with a+b when x = a, y = b;
compatibility
proof
A1: dom y = A by FUNCT_2:92;
assume that
A2: x = a and
A3: y = b;
dom(x+y) = A by FUNCT_2:92;
then
A4: for c being object st c in dom(x+y) holds (x+y).c = a.c + b.c by A2,A3,
FUNCSDOM:1;
dom x = A by FUNCT_2:92;
then dom(x+y) = dom a /\ dom b by A2,A3,A1,FUNCT_2:92;
hence thesis by A4,VALUED_1:def 1;
end;
end;
registration
let A be set;
let x be VECTOR of RealVectSpace(A), y be real-valued Function, a, b be
Element of REAL;
identify a*x with b(#)y when x = y, a = b;
compatibility
proof
A1: dom x = A by FUNCT_2:92;
assume that
A2: x = y and
A3: a = b;
A4: dom(a*x) = A by FUNCT_2:92;
then for c being object st c in dom(a*x) holds (a*x).c = b * y.c by A2,A3,
FUNCSDOM:4;
hence thesis by A2,A4,A1,VALUED_1:def 5;
end;
end;
registration
let A be set;
let x be VECTOR of RealVectSpace(A), a be real-valued Function;
identify -x with -a when x = a;
compatibility
proof
assume
A1: x = a;
A2: now
let c be object;
assume c in dom a;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
thus (-x).c = ((-jj)*x).c by RLVECT_1:16
.= (-jj)*a.c by A1,VALUED_1:6
.= -(a.c);
end;
dom -x = A by FUNCT_2:92;
hence thesis by A1,A2,FUNCT_2:92,VALUED_1:9;
end;
end;
registration
let A be set;
let x, y be VECTOR of RealVectSpace(A), a, b be real-valued Function;
identify x-y with a-b when x = a, y = b;
compatibility;
end;
theorem Th34:
for X being Subspace of RealVectSpace(Seg n), x being Element of
REAL n, a being Real st x in the carrier of X holds a*x in the carrier of X
proof
let X be Subspace of RealVectSpace(Seg n), x be Element of REAL n,a be Real;
reconsider x1=x as Element of RealVectSpace(Seg n) by FINSEQ_2:93;
assume x in the carrier of X;
then
A1: x in X;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
aa*x=aa*x1;
then a*x in X by A1,RLSUB_1:21;
hence a*x in the carrier of X;
end;
theorem Th35:
for X being Subspace of RealVectSpace(Seg n), x,y being Element of REAL n st
x in the carrier of X & y in the carrier of X holds
x+y in the carrier of X
proof
let X be Subspace of RealVectSpace(Seg n), x,y be Element of REAL n;
assume that
A1: x in the carrier of X and
A2: y in the carrier of X;
A3: y in X by A2;
reconsider x1=x,y1=y as Element of RealVectSpace(Seg n) by FINSEQ_2:93;
A4: x1+y1=x+y;
x in X by A1;
then x+y in X by A3,A4,RLSUB_1:20;
hence x+y in the carrier of X;
end;
theorem
for X being Subspace of RealVectSpace(Seg n), x,y being Element of
REAL n,a,b being Real st x in the carrier of X & y in the carrier of X holds a*
x+b*y in the carrier of X
proof
let X be Subspace of RealVectSpace(Seg n), x,y be Element of REAL n,a,b
being Real;
assume that
A1: x in the carrier of X and
A2: y in the carrier of X;
A3: b*y in the carrier of X by A2,Th34;
a*x in the carrier of X by A1,Th34;
hence a*x+b*y in the carrier of X by A3,Th35;
end;
Lm4: for X being Subspace of RealVectSpace(Seg n), x,y being Element of REAL n
,a being Real st x in the carrier of X & y in the carrier of X holds a*x+y in
the carrier of X
proof
let X be Subspace of RealVectSpace(Seg n), x,y be Element of REAL n,
a be Real;
assume that
A1: x in the carrier of X and
A2: y in the carrier of X;
a*x in the carrier of X by A1,Th34;
hence a*x+y in the carrier of X by A2,Th35;
end;
theorem
for u,v being Element of REAL n holds (Euclid_scalar n).(u,v) = |(u,v
)| by REAL_NS1:def 5;
theorem Th38:
for F being FinSequence of the carrier of RealVectSpace(Seg n),
Bn being Subset of RealVectSpace(Seg n), v0 being Element of RealVectSpace(Seg
n),l being Linear_Combination of Bn st F is one-to-one & Bn is R-orthogonal &
rng F = Carrier l & v0 in Bn & j in dom (l (#) F) & v0=F.j holds (Euclid_scalar
n).(v0,Sum (l(#)F)) = (Euclid_scalar n).(v0,(l.(F/.j))*v0)
proof
let F be FinSequence of the carrier of RealVectSpace(Seg n), Bn be Subset of
RealVectSpace(Seg n), v0 be Element of RealVectSpace(Seg n),l be
Linear_Combination of Bn;
assume that
A1: F is one-to-one and
A2: Bn is R-orthogonal and
A3: rng F= Carrier l and
A4: v0 in Bn and
A5: j in dom (l (#) F) and
A6: v0=F.j;
A7: ( len (l (#) F) ) = len F by RLVECT_2:def 7;
then
A8: dom (l(#)F)=Seg len F by FINSEQ_1:def 3
.=dom F by FINSEQ_1:def 3;
reconsider F2= l(#) F as FinSequence of the carrier of RealVectSpace(Seg n);
reconsider rv0=v0 as Element of REAL n by FINSEQ_2:93;
consider f being sequence of the carrier of RealVectSpace(Seg n) such
that
A9: Sum(F2) = f . (len F2) and
A10: f.0 = 0.(RealVectSpace(Seg n)) and
A11: for j2 being Nat for v being Element of RealVectSpace(Seg n) st
j2 < len F2 & v = F2 . (j2 + 1) holds f . (j2 + 1) = (f . j2) + v
by RLVECT_1:def 12;
defpred Q[Nat] means $1>=j & $1<=len F implies (Euclid_scalar n).(v0,f.$1) =
(Euclid_scalar n).(v0,(l.(F/.j))*v0);
defpred P[Nat] means $1<j implies (Euclid_scalar n).(v0,f.$1)=0;
(Euclid_scalar n).(v0,f.0) = |( rv0, 0*n )| by A10,REAL_NS1:def 5
.= 0 by EUCLID_4:18;
then
A12: P[0];
A13: dom (l(#)F)=Seg len (l(#)F) by FINSEQ_1:def 3;
then
A14: j<=len F by A5,A7,FINSEQ_1:1;
A15: Carrier l c= Bn by RLVECT_2:def 6;
A16: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A17: P[k];
now
per cases;
case
A18: k<len F2;
A19: 1<=k+1 by NAT_1:11;
k+1<= len F2 by A18,NAT_1:13;
then k+1 in Seg len F2 by A19,FINSEQ_1:1;
then k+1 in dom F2 by FINSEQ_1:def 3;
then F2.(k+1) in rng F2 by FUNCT_1:def 3;
then reconsider v=F2 . (k + 1) as Element of RealVectSpace(Seg n);
reconsider rv=v as Element of REAL n by FINSEQ_2:93;
reconsider fk=f.k as Element of REAL n by FINSEQ_2:93;
per cases;
suppose
A20: k+1<j;
A21: 1<=k+1 by NAT_1:11;
k+1<len F by A14,A20,XXREAL_0:2;
then k+1 in Seg len F by A21,FINSEQ_1:1;
then
A22: k+1 in dom F by FINSEQ_1:def 3;
then
A23: F/.(k+1)=F.(k+1) by PARTFUN1:def 6;
then
A24: rv0<>F/.(k+1) by A1,A5,A6,A8,A20,A22,FUNCT_1:def 4;
k<k+1 by XREAL_1:29;
then
A25: |(rv0,fk)|=0 by A17,A20,REAL_NS1:def 5,XXREAL_0:2;
reconsider fk1=F/.(k+1) as Element of REAL n by FINSEQ_2:93;
A26: |(rv0,fk+rv)|= |(rv0,fk)| +|(rv0,rv)| by EUCLID_4:28;
A27: F/.(k+1) in rng F by A22,A23,FUNCT_1:def 3;
v=(l . (F /. (k+1))) * (F /. (k+1)) by A8,A22,RLVECT_2:def 7;
then |(rv0,rv)|= (l . (F /. (k+1))) * (|(rv0,fk1)|) by EUCLID_4:22
.= (l . (F /. (k+1))) * 0 by A2,A3,A4,A15,A27,A24
.=0;
then (Euclid_scalar n).(v0,(f.k) + v)=0 by A25,A26,REAL_NS1:def 5;
hence P[k+1] by A11,A18;
end;
suppose
k+1>=j;
hence P[k+1];
end;
end;
case
A28: k>=len F2;
k+1>k by XREAL_1:29;
then k+1>len F2 by A28,XXREAL_0:2;
hence P[k+1] by A7,A14,XXREAL_0:2;
end;
end;
hence P[k+1];
end;
A29: for i being Nat holds P[i] from NAT_1:sch 2(A12,A16);
A30: for i being Nat st i<j holds (Euclid_scalar n).(v0,f.i)=0 by A29;
A31: for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume
A32: Q[k];
per cases;
suppose
k+1<j;
hence Q[k+1];
end;
suppose
A33: k+1>=j;
per cases by A33,XXREAL_0:1;
suppose
A34: k+1>j;
per cases;
suppose
A35: k+1<=len F2;
1<=k+1 by NAT_1:11;
then
A36: k+1 in Seg len F2 by A35,FINSEQ_1:1;
then
A37: k+1 in dom F by A7,FINSEQ_1:def 3;
then
A38: F/.(k+1)=F.(k+1) by PARTFUN1:def 6;
then
A39: F/.(k+1) in rng F by A37,FUNCT_1:def 3;
k+1 in dom F2 by A36,FINSEQ_1:def 3;
then F2.(k+1) in rng F2 by FUNCT_1:def 3;
then reconsider v=F2 . (k + 1) as Element of RealVectSpace(Seg n);
reconsider rv=v as Element of REAL n by FINSEQ_2:93;
reconsider fk1=F/.(k+1) as Element of REAL n by FINSEQ_2:93;
reconsider fk=f.k as Element of REAL n by FINSEQ_2:93;
A40: |(rv0,fk+rv)|= |(rv0,fk)| +|(rv0,rv)| by EUCLID_4:28;
A41: rv0<>F/.(k+1) by A1,A5,A6,A8,A34,A37,A38,FUNCT_1:def 4;
v=(l . (F /. (k+1))) * (F /. (k+1)) by A8,A37,RLVECT_2:def 7;
then
A42: |(rv0,rv)| = (l . (F /. (k+1))) * (|(rv0,fk1)|) by EUCLID_4:22
.= (l . (F /. (k+1))) * 0 by A2,A3,A4,A15,A39,A41
.=0;
k<k+1 by XREAL_1:29;
then
A43: k<len F2 by A35,XXREAL_0:2;
then |(rv0,fk)|=(Euclid_scalar n).(v0,(l.(F/.j))*v0) by A32,A34,
NAT_1:13,REAL_NS1:def 5,RLVECT_2:def 7;
then
(Euclid_scalar n).(v0,(f.k) + v) =(Euclid_scalar n).(v0,(l.(F/.
j))*v0) by A40,A42,REAL_NS1:def 5;
hence Q[k+1] by A11,A43;
end;
suppose
k+1>len F2;
hence Q[k+1] by RLVECT_2:def 7;
end;
end;
suppose
A44: k+1=j;
then F2.(k+1) in rng F2 by A5,FUNCT_1:def 3;
then reconsider v=F2 . (k + 1) as Element of RealVectSpace(Seg n);
A45: v=(l . (F /. (k+1))) * (F /. (k+1)) by A5,A44,RLVECT_2:def 7;
reconsider rv=v as Element of REAL n by FINSEQ_2:93;
k+1 in dom F by A5,A13,A7,A44,FINSEQ_1:def 3;
then
A46: |(rv0,rv)|= |(rv0,(l . (F /. (j))) *rv0 )| by A6,A44,A45,PARTFUN1:def 6
.=(Euclid_scalar n).(v0,(l.(F/.j))*v0) by REAL_NS1:def 5;
reconsider fk=f.k as Element of REAL n by FINSEQ_2:93;
(Euclid_scalar n).(v0,f.k) =0 by A30,A44,XREAL_1:29;
then
A47: |(rv0,fk)|=0 by REAL_NS1:def 5;
k<k+1 by XREAL_1:29;
then
A48: k<len F2 by A7,A14,A44,XXREAL_0:2;
|(rv0,fk+rv)|= |(rv0,fk)| +|(rv0,rv)| by EUCLID_4:28;
then
(Euclid_scalar n).(v0,(f.k) + v) =(Euclid_scalar n).(v0,(l.(F/.j)
)*v0) by A47,A46,REAL_NS1:def 5;
hence Q[k+1] by A11,A48;
end;
end;
end;
A49: Q[0] by A5,A13,FINSEQ_1:1;
A50: for i being Nat holds Q[i] from NAT_1:sch 2(A49,A31);
for i being Nat st i>=j & i<=len F holds (Euclid_scalar n).(v0,f.i) = (
Euclid_scalar n).(v0,(l.(F/.j))*v0)by A50;
hence thesis by A9,A7,A14;
end;
registration
let n;
cluster R-orthonormal -> linearly-independent for
Subset of RealVectSpace(Seg n);
coherence
proof
let Bn be Subset of RealVectSpace(Seg n);
assume
A1: Bn is R-orthonormal;
let l be Linear_Combination of Bn;
assume
A2: Sum l = 0.(RealVectSpace(Seg n));
set v0 = the Element of Carrier l;
consider F being FinSequence of the carrier of RealVectSpace(Seg n) such
that
A3: F is one-to-one and
A4: rng F = Carrier l and
A5: Sum l = Sum (l(#)F) by RLVECT_2:def 8;
assume
A6: Carrier l <> {};
then
A7: v0 in Carrier l;
then
v0 in {v2 where v2 is Element of RealVectSpace(Seg n) : l.v2 <> 0} by
RLVECT_2:def 4;
then consider v being Element of RealVectSpace(Seg n) such that
A8: v0=v and
l.v <> 0;
reconsider xv=v as Element of REAL n by FINSEQ_2:93;
A9: (Euclid_scalar n).(v,(Sum (l (#) F))) = |( xv,0*n )| by A2,A5,
REAL_NS1:def 5
.= 0 by EUCLID_4:18;
consider x0 being object such that
A10: x0 in dom F and
A11: v0=F.x0 by A6,A4,FUNCT_1:def 3;
reconsider nx0=x0 as Element of NAT by A10;
F.x0=F/.x0 by A10,PARTFUN1:def 6;
then F/.nx0 in rng F by A10,FUNCT_1:def 3;
then
F/.nx0 in {v3 where v3 is Element of RealVectSpace(Seg n) : l.v3 <> 0
} by A4,RLVECT_2:def 4;
then
A12: ex v3 being Element of RealVectSpace(Seg n) st v3=F/.nx0 & l.v3 <> 0;
A13: dom F=Seg len F by FINSEQ_1:def 3;
A14: Carrier l c= Bn by RLVECT_2:def 6;
len (l (#) F) = len F by RLVECT_2:def 7;
then nx0 in dom (l (#) F) by A10,A13,FINSEQ_1:def 3;
then (Euclid_scalar n).(v,(Sum (l (#) F))) =(Euclid_scalar n).(v,(l . (F
/. nx0)) *v) by A1,A14,A7,A8,A3,A4,A11,Th38
.= |(xv,(l . (F /. nx0)) *xv )| by REAL_NS1:def 5
.= (l . (F /. nx0))* ( |(xv,xv)| ) by EUCLID_4:22
.= (l . (F /. nx0))* ((|.xv .|)^2) by EUCLID_2:4
.= (l . (F /. nx0))* (1^2) by A1,A14,A7,A8,Def4
.= (l . (F /. nx0));
hence contradiction by A12,A9;
end;
end;
registration
let n be Element of NAT;
cluster R-orthonormal -> linearly-independent for Subset of REAL-US n;
coherence
proof
let Bn be Subset of REAL-US n;
assume
A1: Bn is R-orthonormal;
let l be Linear_Combination of Bn;
assume
A2: Sum l = 0.(REAL-US n);
set v0 = the Element of Carrier l;
consider F being FinSequence of the carrier of (REAL-US n) such that
A3: F is one-to-one and
A4: rng F = Carrier l and
A5: Sum l = Sum (l (#) F) by RLVECT_2:def 8;
assume
A6: Carrier l <> {};
then
A7: v0 in Carrier l;
then v0 in {v2 where v2 is Element of REAL-US n : l.v2 <> 0} by
RLVECT_2:def 4;
then consider v being Element of REAL-US n such that
A8: v0=v and
l.v <> 0;
reconsider xv=v as Element of REAL n by REAL_NS1:def 6;
0.(REAL-US n)= 0*n by REAL_NS1:def 6;
then
A9: (Euclid_scalar n).(v,(Sum (l (#) F))) =|( xv,0*n )| by A2,A5,REAL_NS1:def 5
.= 0 by EUCLID_4:18;
consider x0 being object such that
A10: x0 in dom F and
A11: v0=F.x0 by A6,A4,FUNCT_1:def 3;
reconsider nx0=x0 as Element of NAT by A10;
F.x0=F/.x0 by A10,PARTFUN1:def 6;
then F/.nx0 in rng F by A10,FUNCT_1:def 3;
then F/.nx0 in {v3 where v3 is Element of REAL-US n : l.v3 <> 0} by A4,
RLVECT_2:def 4;
then
A12: ex v3 being Element of REAL-US n st v3=F/.nx0 & l.v3 <> 0;
A13: dom F=Seg len F by FINSEQ_1:def 3;
A14: (Carrier l) c= Bn by RLVECT_2:def 6;
( len (l (#) F) ) = len F by RLVECT_2:def 7;
then nx0 in dom (l (#) F) by A10,A13,FINSEQ_1:def 3;
then (Euclid_scalar n).(v,(Sum (l (#) F))) =(Euclid_scalar n).(v,(l . (F
/. nx0)) *v) by A1,A14,A7,A8,A3,A4,A11,Th32
.= |(xv,(l . (F /. nx0)) *xv )| by REAL_NS1:def 5
.= (l . (F /. nx0))* ( |(xv,xv)| ) by EUCLID_4:22
.= (l . (F /. nx0))* ((|.xv .|)^2) by EUCLID_2:4
.= (l . (F /. nx0))* (1^2) by A1,A14,A7,A8,Def4
.= (l . (F /. nx0));
hence contradiction by A12,A9;
end;
end;
theorem Th39:
for Bn being Subset of RealVectSpace(Seg n), x,y being Element
of REAL n,a being Real st Bn is linearly-independent & x in Bn & y in Bn & y=a*
x holds x=y
proof
let Bn be Subset of RealVectSpace(Seg n), x,y be Element of REAL n,a be Real;
assume that
A1: Bn is linearly-independent and
A2: x in Bn and
A3: y in Bn and
A4: y=a*x;
reconsider x0=x,y0=y as Element of RealVectSpace(Seg n) by FINSEQ_2:93;
reconsider A={y0,x0} as Subset of RealVectSpace(Seg n);
A c= Bn
by A2,A3,TARSKI:def 2;
then
A5: A is linearly-independent by A1,RLVECT_3:5;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
y0=aa*x0 by A4;
hence x=y by A5,RLVECT_3:12;
end;
Lm5: now
let n;
thus RN_Base n is finite & card RN_Base n = n
proof
per cases;
suppose n is zero;
hence thesis;
end;
suppose n is non zero;
then reconsider n as non zero Nat;
defpred P[object,object] means
for i being Element of NAT st i=$1 holds $2=
Base_FinSeq(n,i);
A1: for x being object st x in Seg n ex y being object st P[x,y]
proof
let x be object;
assume x in Seg n;
then reconsider j=x as Element of NAT;
for i being Element of NAT st i=j holds Base_FinSeq(n,j)=
Base_FinSeq(n,i);
hence ex y being object st P[x,y];
end;
consider f being Function such that
A2: dom f = Seg n & for x2 being object st x2 in Seg n holds P[x2,f.x2]
from CLASSES1:sch 1(A1);
A3: rng f c= RN_Base n
proof
let y be object;
assume y in rng f;
then consider x being object such that
A4: x in dom f and
A5: y=f.x by FUNCT_1:def 3;
reconsider nx=x as Element of NAT by A2,A4;
A6: nx<=n by A2,A4,FINSEQ_1:1;
A7: f.x=Base_FinSeq(n,nx) by A2,A4;
1<=nx by A2,A4,FINSEQ_1:1;
hence y in RN_Base n by A5,A6,A7;
end;
then reconsider f2=f as Function of Seg n,RN_Base n by A2,FUNCT_2:2;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1=f.x2
holds x1=x2
proof
let x1,x2 be object;
assume that
A8: x1 in dom f and
A9: x2 in dom f and
A10: f.x1=f.x2;
reconsider nx1=x1,nx2=x2 as Element of NAT by A2,A8,A9;
A11: nx1<=n by A2,A8,FINSEQ_1:1;
A12: f.x2=Base_FinSeq(n,nx2) by A2,A9;
A13: f.x1=Base_FinSeq(n,nx1) by A2,A8;
1<=nx1 by A2,A8,FINSEQ_1:1;
hence x1=x2 by A10,A11,A13,A12,Th24;
end;
then
A14: f2 is one-to-one by FUNCT_1:def 4;
RN_Base n c= rng f
proof
let y be object;
assume y in RN_Base n;
then consider i being Element of NAT such that
A15: y=Base_FinSeq(n,i) and
A16: 1<=i and
A17: i<=n;
A18: i in Seg n by A16,A17,FINSEQ_1:1;
then f.i=Base_FinSeq(n,i) by A2;
hence y in rng f by A2,A15,A18,FUNCT_1:def 3;
end;
then rng f = RN_Base n by A3,XBOOLE_0:def 10;
then f2 is onto by FUNCT_2:def 3;
then card Seg n = card RN_Base n by A14,Lm1;
hence thesis by FINSEQ_1:57;
end;
end;
end;
begin :: 6. Finite Dimensionality of the Spaces
registration let n;
cluster RN_Base n -> finite;
coherence by Lm5;
end;
theorem
card RN_Base n = n by Lm5;
theorem Th41:
for f being FinSequence of REAL n, g being FinSequence of the
carrier of RealVectSpace(Seg n) st f=g holds Sum f=Sum g
proof
let f be FinSequence of REAL n, g be FinSequence of the carrier of
RealVectSpace(Seg n);
assume
A1: f=g;
set V=RealVectSpace(Seg n);
A2: REAL(n) = the carrier of V by FINSEQ_2:93;
now
per cases;
case
A3: len f>0;
set g2 = accum f;
A4: len f=len g2 by Def10;
A5: f.1=g2.1 by Def10;
A6: Sum f=g2.(len f) by Def11,A3;
deffunc F(set)=IFIN($1,len f+1,IFEQ($1,0, 0.V, g2/.$1),0.V);
A7: for x being set st x in NAT holds F(x) in the carrier of V
proof
let x be set;
assume x in NAT;
then reconsider nx=x as Element of NAT;
per cases;
suppose
nx in (len f+1);
then
A8: F(x)=IFEQ(x,0, 0.V, g2/.nx) by MATRIX_7:def 1;
per cases;
suppose x=0;
then F(x)=0.V by A8,FUNCOP_1:def 8;
hence F(x) in the carrier of V;
end;
suppose x<>0;
then F(x)=g2/.nx by A8,FUNCOP_1:def 8;
hence F(x) in the carrier of V by A2;
end;
end;
suppose not nx in (len f +1);
then F(x)=0.V by MATRIX_7:def 1;
hence F(x) in the carrier of V;
end;
end;
consider f3 being sequence of the carrier of V such that
A9: for x being set st x in NAT holds f3.x = F(x) from FUNCT_2:sch
11(A7);
A10: for j being Nat for v being Element of V st j < len g &
v = g . (j + 1) holds f3 . (j + 1) = (f3 . j) + v
proof
let j be Nat;
A11: j in NAT by ORDINAL1:def 12;
let v be Element of V;
assume that
A12: j < len g and
A13: v = g . (j + 1);
A14: j+1<=len f by A1,A12,NAT_1:13;
per cases;
suppose
A15: j=0;
then j+1<len f+1 by A3,XREAL_1:6;
then
A16: (j+1) in Segm(len f+1) by NAT_1:44;
A17: 0 in Segm(len f +1) by NAT_1:44;
A18: f3.j=IFIN(j,len f+1,IFEQ(j,0, 0.V, g2/.j),0.V) by A9,A11
.= IFEQ(j,0, 0.V, g2/.j) by A15,A17,MATRIX_7:def 1
.= 0.V by A15,FUNCOP_1:def 8;
thus f3.(j+1)=IFIN(j+1,len f+1,IFEQ(j+1,0, 0.V, g2/.(j+1)),0.V) by A9
.=IFEQ(j+1,0, 0.V, g2/.(j+1)) by A16,MATRIX_7:def 1
.=g2/.1 by A15,FUNCOP_1:def 8
.=g.(j+1) by A1,A4,A5,A14,A15,FINSEQ_4:15
.= (f3.j)+v by A13,A18,RLVECT_1:4;
end;
suppose
A19: j<>0;
len f<len f+1 by XREAL_1:29;
then j< len f+1 by A1,A12,XXREAL_0:2;
then
A20: j in Segm(len f +1) by NAT_1:44;
A21: f3.j=IFIN(j,len f+1,IFEQ(j,0, 0.V, g2/.j),0.V) by A9,A11
.= IFEQ(j,0, 0.V, g2/.j) by A20,MATRIX_7:def 1
.= g2/.j by A19,FUNCOP_1:def 8;
A22: 0+1<=j+1 by NAT_1:13;
A23: 0+1<=j by A19,NAT_1:13;
j+1<len f+1 by A1,A12,XREAL_1:6;
then
A24: (j+1) in Segm(len f+1) by NAT_1:44;
thus f3.(j+1)=IFIN(j+1,len f+1,IFEQ(j+1,0, 0.V, g2/.(j+1)),0.V) by A9
.=IFEQ(j+1,0, 0.V, g2/.(j+1)) by A24,MATRIX_7:def 1
.=g2/.(j+1) by FUNCOP_1:def 8
.=g2.(j+1) by A4,A14,A22,FINSEQ_4:15
.=(g2/.j)+(f/.(j+1)) by A1,Def10,A12,A23
.=(f3.j)+v by A1,A13,A14,A22,A21,FINSEQ_4:15;
end;
end;
len f <len f+1 by XREAL_1:29;
then
A25: len f in Segm(len f+1) by NAT_1:44;
A26: 0+1<=len f by A3,NAT_1:13;
A27: 0 in Segm(len f +1) by NAT_1:44;
A28: f3.0=IFIN(0,len f+1,IFEQ(0,0, 0.V, g2/.0),0.V) by A9
.=IFEQ(0,0, 0.V, g2/.0) by A27,MATRIX_7:def 1
.=0.V by FUNCOP_1:def 8;
f3.(len g)=F(len f) by A1,A9
.=IFEQ(len f,0,0.V,g2/.(len f)) by A25,MATRIX_7:def 1
.=g2/.(len f) by A3,FUNCOP_1:def 8
.=Sum f by A4,A6,A26,FINSEQ_4:15;
hence
ex f2 being sequence of the carrier of V st Sum f = f2 . (len g
) & f2 . 0 = 0. V & for j being Nat for v being Element of V st j <
len g & v = g . (j + 1) holds f2 . (j + 1) = (f2 . j) + v by A28,A10;
end;
case
A29: len f<=0;
set f3 = NAT --> 0.V;
A30: for j being Nat for v being Element of V st j < len g &
v = g . (j + 1) holds f3 . (j + 1) = (f3 . j) + v by A1,A29;
A31: f3.(len g)= 0*n by FUNCOP_1:7;
A32: f3.0=0.V by FUNCOP_1:7;
Sum f = 0*n by A29,Def11;
hence
ex f2 being sequence of the carrier of V st Sum f = f2 . (len g
) & f2 . 0 = 0. V & for j being Nat for v being Element of V st j <
len g & v = g . (j + 1) holds f2 . (j + 1) = (f2 . j) + v by A31,A32,A30;
end;
end;
hence Sum f=Sum g by RLVECT_1:def 12;
end;
theorem Th42:
for x0 being Element of RealVectSpace(Seg n), B being Subset of
RealVectSpace(Seg n) st B=RN_Base n holds ex l being Linear_Combination of B st
x0=Sum l
proof
let x0 be Element of RealVectSpace(Seg n), B be Subset of RealVectSpace(Seg
n);
reconsider x1=x0 as Element of REAL n by FINSEQ_2:93;
A1: REAL(n) = the carrier of RealVectSpace(Seg n) by FINSEQ_2:93;
assume
A2: B=RN_Base n;
A3: {x where x is Element of REAL n: ex i being Element of NAT st 1<=i & i<=
n & x=Base_FinSeq(n,i)} c= B
proof
let y be object;
assume y in {x where x is Element of REAL n: ex i being Element of NAT st
1<=i & i<=n & x=Base_FinSeq(n,i)};
then
ex x being Element of REAL n st y=x & ex i being Element of NAT st 1<=
i & i<=n & x=Base_FinSeq(n,i);
hence y in B by A2;
end;
B c= {x where x is Element of REAL n: ex i being Element of NAT st 1<=i
& i<=n & x=Base_FinSeq(n,i)}
proof
let y be object;
assume y in B;
then
ex i2 being Element of NAT st y=Base_FinSeq(n,i2) & 1<= i2 & i2<=n by A2;
hence y in {x where x is Element of REAL n: ex i being Element of NAT st 1
<=i & i<=n & x=Base_FinSeq(n,i)};
end;
then
A4: B={x where x is Element of REAL n: ex i being Element of NAT st 1<=i &
i<=n & x=Base_FinSeq(n,i)} by A3,XBOOLE_0:def 10;
A5: {x where x is Element of REAL n: ex i being Element of NAT st 1<=i & i<=
n & x=Base_FinSeq(n,i) & |(x1,x)| <>0} c=B
proof
let x2 be object;
assume x2 in {x where x is Element of REAL n: ex i being Element of NAT
st 1<=i & i<=n & x=Base_FinSeq(n,i) & |(x1,x)| <>0};
then
ex x being Element of REAL n st x=x2 & ex i being Element of NAT st 1
<=i & i<=n & x=Base_FinSeq(n,i) & |(x1,x)| <>0;
hence x2 in B by A4;
end;
then reconsider
B0={x where x is Element of REAL n: ex i being Element of NAT st
1<=i & i<=n & x=Base_FinSeq(n,i) & |(x1,x)| <>0} as Subset of RealVectSpace(Seg
n) by XBOOLE_1:1;
A6: dom (ProjFinSeq x1)=Seg len (ProjFinSeq x1) by FINSEQ_1:def 3
.=Seg n by Def12;
defpred R[object,object] means
$1 in B0 implies ex i being Element of NAT st $2=i
& 1<=i & i<=n & $1=Base_FinSeq(n,i);
A7: for x being object st x in B0 ex y being object st y in Seg n & R[x,y]
proof
let x be object;
assume x in B0;
then consider x2 being Element of REAL n such that
A8: x=x2 and
A9: ex i being Element of NAT st 1<=i & i<=n & x2=Base_FinSeq(n,i) &
|( x1,x2)| <>0;
consider i0 being Element of NAT such that
A10: 1<=i0 and
A11: i0<=n and
A12: x2=Base_FinSeq(n,i0) and
|(x1,x2)| <>0 by A9;
i0 in Seg n by A10,A11,FINSEQ_1:1;
hence ex y being object st y in Seg n & R[x,y] by A8,A10,A11,A12;
end;
consider f being Function of B0,Seg n such that
A13: for x being object st x in B0 holds R[x,f.x] from FUNCT_2:sch 1(A7);
defpred Q[object,object] means
($1 in B0 implies (for i being Element of NAT st 1
<=i & i<=n & $1=Base_FinSeq(n,i) holds $2=|( x1, Base_FinSeq(n,i) )|))& (not $1
in B0 implies $2=0);
A14: for x being object st x in the carrier of RealVectSpace(Seg n)
ex y being object st y in REAL & Q[x,y]
proof
let x be object;
assume x in the carrier of RealVectSpace(Seg n);
per cases;
suppose
A15: x in B0;
then consider x2 being Element of REAL n such that
A16: x2=x and
ex i being Element of NAT st 1<=i & i<=n & x2=Base_FinSeq(n,i) & |(
x1,x2)| <>0;
reconsider y0=|(x1,x2)| as Element of REAL;
for i2 being Element of NAT st 1<=i2 & i2<=n & x=Base_FinSeq(n,i2)
holds y0=|( x1, Base_FinSeq(n,i2) )| by A16;
hence ex y being object st y in REAL & Q[x,y] by A15;
end;
suppose
not x in B0;
hence ex y being object st y in REAL & Q[x,y] by Lm3;
end;
end;
consider l2 being Function of the carrier of RealVectSpace(Seg n),REAL such
that
A17: for x being object st x in the carrier of RealVectSpace(Seg n) holds Q
[x,l2.x] from FUNCT_2:sch 1(A14);
A18: l2 is Element of Funcs(the carrier of RealVectSpace(Seg n),REAL) by
FUNCT_2:8;
for v being Element of RealVectSpace(Seg n) st not v in B0 holds l2.v =
0 by A17;
then reconsider
l3=l2 as Linear_Combination of RealVectSpace(Seg n) by A2,A5,A18,
RLVECT_2:def 3;
Carrier l3 c= B0
proof
let x be object;
assume x in Carrier l3;
then x in { v where v is Element of RealVectSpace(Seg n) : l3.v <> 0 } by
RLVECT_2:def 4;
then ex v being Element of RealVectSpace(Seg n) st x=v & l3.v <> 0;
hence x in B0 by A17;
end;
then reconsider l0=l3 as Linear_Combination of B0 by RLVECT_2:def 6;
A19: Carrier l0 c= B0 by RLVECT_2:def 6;
then Carrier l0 c= B by A5;
then reconsider l2=l0 as Linear_Combination of B by RLVECT_2:def 6;
A20: B0 c= Carrier l0
proof
let x be object;
assume
A21: x in B0;
then consider x6 being Element of REAL n such that
A22: x=x6 and
A23: ex i being Element of NAT st 1<=i & i<=n & x6=Base_FinSeq(n,i)&
|( x1,x6)| <>0;
reconsider x66=x6 as Element of RealVectSpace(Seg n) by FINSEQ_2:93;
consider i8 being Element of NAT such that
1<=i8 and
i8<=n and
A24: x6=Base_FinSeq(n,i8) and
|(x1,x6)| <>0 by A23;
l0.x66=|( x1, Base_FinSeq(n,i8) )| by A17,A21,A22,A23,A24;
then
x in { v where v is Element of RealVectSpace(Seg n) : l0 . v <> 0} by A22
,A23,A24;
hence x in Carrier l0 by RLVECT_2:def 4;
end;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1=f.x2 holds x1= x2
proof
let x1,x2 be object;
assume that
A25: x1 in dom f and
A26: x2 in dom f and
A27: f.x1=f.x2;
A28: ex i2 being Element of NAT st f.x2=i2 & 1<=i2 & i2<=n & x2=
Base_FinSeq(n,i2) by A13,A26;
ex i1 being Element of NAT st f.x1=i1 & 1<=i1 & i1<=n & x1=
Base_FinSeq(n,i1) by A13,A25;
hence x1=x2 by A27,A28;
end;
then
A29: f is one-to-one by FUNCT_1:def 4;
A30: Seg n={} implies B0={}
proof
assume
A31: Seg n={};
now
set y = the Element of B0;
assume B0 <> {};
then y in B0;
then ex x being Element of REAL n st x=y & ex i being Element of NAT st
1<=i & i<=n & x=Base_FinSeq(n,i) & |(x1,x)| <>0;
hence contradiction by A31;
end;
hence B0={};
end;
aaa: rng f is included_in_Seg by FINSEQ_1:def 13;
then
bbb: rng (Sgm (rng f)) = rng f by FINSEQ_1:def 14;
A32: for i3 being Element of NAT st i3 in dom (ProjFinSeq x1) & not i3 in
rng (Sgm (rng f)) holds (ProjFinSeq x1).i3= 0*n
proof
let i3 be Element of NAT;
assume that
A33: i3 in dom (ProjFinSeq x1) and
A34: not i3 in rng (Sgm (rng f));
A35: i3 in Seg len (ProjFinSeq x1) by A33,FINSEQ_1:def 3;
then
A36: 1<=i3 by FINSEQ_1:1;
len (ProjFinSeq x1)=n by Def12;
then
A37: i3<=n by A35,FINSEQ_1:1;
A38: not i3 in rng f by A34,bbb;
A39: now
assume |( x1,Base_FinSeq(n,i3) )| <> 0;
then
A40: Base_FinSeq(n,i3) in B0 by A36,A37;
then consider i5 being Element of NAT such that
A41: f.(Base_FinSeq(n,i3))=i5 and
1<=i5 and
i5<=n and
A42: Base_FinSeq(n,i3)=Base_FinSeq(n,i5) by A13;
A43: Base_FinSeq(n,i3) in dom f by A30,A40,FUNCT_2:def 1;
i3=i5 by A36,A37,A42,Th24;
hence contradiction by A38,A41,A43,FUNCT_1:def 3;
end;
(ProjFinSeq x1).i3 =(|( x1,Base_FinSeq(n,i3) )|)*(Base_FinSeq(n,i3) )
by A36,A37,Def12;
hence (ProjFinSeq x1).i3= 0*n by A39,EUCLID_4:3;
end;
A44: dom ((Sgm (rng f))qua Function) = Seg len (Sgm (rng f)) by FINSEQ_1:def 3;
A45: rng (((ProjFinSeq x1)qua Function)*((Sgm (rng f))qua Function)) c= REAL n;
A46: rng (Sgm (rng f))= rng f by bbb;
dom (((ProjFinSeq x1)qua Function)*((Sgm (rng f))qua Function)) = ((Sgm
(rng f))qua Function)"(dom (ProjFinSeq x1)) by RELAT_1:147
.= dom (Sgm (rng f)) by A46,A6,Th1;
then ((ProjFinSeq x1)qua Function)*((Sgm (rng f))qua Function) is
FinSequence by A44,FINSEQ_1:def 2;
then reconsider
F2=((ProjFinSeq x1)qua Function)* ((Sgm rng f)qua Function) as
FinSequence of the carrier of RealVectSpace(Seg n) by A1,A45,FINSEQ_1:def 4;
dom F2= ((Sgm (rng f))qua Function)"(Seg n) by A6,RELAT_1:147
.= dom (Sgm (rng f)) by A46,Th1;
then
A47: dom F2=Seg len (Sgm (rng f)) by FINSEQ_1:def 3;
then
A48: Seg len F2=Seg len (Sgm (rng f)) by FINSEQ_1:def 3;
reconsider F3=F2 as FinSequence of REAL n by FINSEQ_2:93;
A49: x0= Sum (ProjFinSeq x1) by Th30
.= Sum F3 by aaa,A46,A6,A32,Th23,FINSEQ_3:92
.= Sum F2 by Th41;
A50: rng (((f qua Function)")*((Sgm (rng f))qua Function)) c= rng (((f qua
Function)")qua Function) by RELAT_1:26;
A51: dom ((Sgm rng f)qua Function) = Seg len (Sgm rng f) by FINSEQ_1:def 3;
A52: len F2=len (Sgm (rng f)) by A47,FINSEQ_1:def 3;
A53: dom f=B0 by A30,FUNCT_2:def 1;
then rng ((f qua Function)") = B0 by A29,FUNCT_1:33;
then
A54: rng ((f qua Function)" *((Sgm (rng f))qua Function)) c= the carrier of
RealVectSpace(Seg n) by A50,XBOOLE_1:1;
dom ((((f qua Function)") qua Function)*((Sgm (rng f))qua Function)) =
((Sgm (rng f))qua Function)"(dom ((f qua Function)")) by RELAT_1:147
.= ((Sgm (rng f))qua Function)"(rng f) by A29,FUNCT_1:33
.= dom (Sgm rng f) by A46,Th1;
then (((f qua Function)")qua Function)* ((Sgm (rng f))qua Function) is
FinSequence by A51,FINSEQ_1:def 2;
then reconsider
F0=(f qua Function)" *((Sgm (rng f))qua Function) as FinSequence
of the carrier of RealVectSpace(Seg n) by A54,FINSEQ_1:def 4;
dom F0= ((Sgm (rng f))qua Function)"(dom ((f qua Function)")) by RELAT_1:147
.= ((Sgm (rng f))qua Function)"(rng f) by A29,FUNCT_1:33
.= dom ((Sgm (rng f))qua Function) by A46,Th1;
then
A55: dom F0=Seg len (Sgm (rng f)) by FINSEQ_1:def 3;
dom ((f qua Function)")=rng f by A29,FUNCT_1:33;
then rng F0=rng ((f qua Function)") by A46,RELAT_1:28
.=dom f by A29,FUNCT_1:33;
then
A56: rng F0 =Carrier l0 by A53,A19,A20,XBOOLE_0:def 10;
A57: for i being Nat st i in dom F2 holds F2 . i = (l0 .(F0 /. i)) * (F0 /. i)
proof
let i be Nat;
A58: Sgm (rng f) is one-to-one by aaa,FINSEQ_3:92;
assume i in dom F2; then
A59: i in Seg len F2 by FINSEQ_1:def 3;
then
A60: i in dom (Sgm (rng f)) by A52,FINSEQ_1:def 3;
then (Sgm (rng f)).i in rng (Sgm (rng f)) by FUNCT_1:def 3;
then reconsider i2=(Sgm (rng f)).i as Element of NAT;
reconsider r=Base_FinSeq(n,i2) as Element of RealVectSpace(
Seg n) by FINSEQ_2:93;
i2 in rng (Sgm (rng f)) by A60,FUNCT_1:def 3;
then consider x2 being object such that
A61: x2 in dom f and
A62: f.x2=i2 by A46,FUNCT_1:def 3;
dom f=B0 by A30,FUNCT_2:def 1;
then reconsider r2=x2 as Element of RealVectSpace(Seg n) by A61;
A63: ex i22 being Element of NAT st f.r2=i22 & 1<=i22 & i22 <=n & r2=
Base_FinSeq(n,i22) by A13,A61;
then consider i4 being Element of NAT such that
A64: f.r=i4 and
1<=i4 and
i4<=n and
A65: r=Base_FinSeq(n,i4) by A62;
A66: dom f=B0 by A30,FUNCT_2:def 1;
F0.i= ((f qua Function)").((((Sgm (rng f))qua Function)).i) by A60,
FUNCT_1:13
.= Base_FinSeq(n,i2) by A29,A61,A62,A63,FUNCT_1:32;
then Base_FinSeq(n,i2) in rng F0 by A55,A48,A59,FUNCT_1:def 3;
then Base_FinSeq(n,i2) in { v where v is Element of RealVectSpace(Seg n)
: l0 . v <> 0 } by A56,RLVECT_2:def 4;
then
A67: ex v0 being Element of RealVectSpace(Seg n) st Base_FinSeq(n,i2)=v0
& l0.v0 <>0;
then Base_FinSeq(n,i2) in B0 by A17;
then
A68: ((f qua Function)").( (f.(Base_FinSeq(n,i2)))) =Base_FinSeq(n,i2) by A29
,A66,FUNCT_1:34;
then
A69: ((f qua Function)"*(Sgm (rng f))).i=Base_FinSeq(n,i2) by A60,A62,A63,
FUNCT_1:13;
A70: i2 in rng f by A46,A60,FUNCT_1:def 3;
then
A71: 1<=i2 by FINSEQ_1:1;
A72: i2<=n by A70,FINSEQ_1:1;
then i4=i2 by A71,A65,Th24;
then
A73: ((Sgm (rng f)) qua Function)". (f.(Base_FinSeq(n,i2)))=i by A60,A64,A58,
FUNCT_1:32;
A74: f.(Base_FinSeq(n,i2)) in rng (Sgm (rng f)) by A46,A61,A62,A63,
FUNCT_1:def 3;
then
A75: ((f qua Function)").((Sgm (rng f)). (((Sgm (rng f)) qua Function)".
(f.(Base_FinSeq(n,i2))))) =Base_FinSeq(n,i2) by A58,A68,FUNCT_1:35;
dom (((Sgm (rng f)) qua Function)")=rng (Sgm (rng f)) by A58,FUNCT_1:33;
then ((Sgm (rng f)) qua Function)". (f.(Base_FinSeq(n,i2))) in rng (((Sgm
(rng f)) qua Function)") by A74,FUNCT_1:def 3;
then
A76: ((Sgm (rng f)) qua Function)". (f.(Base_FinSeq(n,i2))) in dom (Sgm (
rng f)) by A58,FUNCT_1:33;
l0 . (F0 /. i)=l0.((((f qua Function)")*(Sgm (rng f))).i) by A55,A52,A59,
PARTFUN1:def 6
.=l0.(Base_FinSeq(n,i2)) by A73,A76,A75,FUNCT_1:13
.=|( x1,Base_FinSeq(n,i2) )| by A17,A71,A72,A67;
then (l0 . (F0 /. i)) * (F0 /. i) =( |( x1,Base_FinSeq(n,i2) )| )*(
Base_FinSeq(n,i2)) by A55,A52,A59,A69,PARTFUN1:def 6
.=(ProjFinSeq x1).((Sgm (rng f)).i) by A71,A72,Def12
.=(((ProjFinSeq x1) qua Function) *((Sgm (rng f))qua Function)).i by A60,
FUNCT_1:13;
hence F2 . i = (l0 . (F0 /. i)) * (F0 /. i);
end;
A77: ((Sgm (rng f))qua Function) is one-to-one by aaa,FINSEQ_3:92;
len F2 = len F0 by A55,A48,FINSEQ_1:def 3;
then x1=Sum (l0 (#) F0) by A49,A57,RLVECT_2:def 7;
then x1=Sum l2 by A29,A77,A56,RLVECT_2:def 8;
hence ex l being Linear_Combination of B st x0=Sum l;
end;
theorem Th43:
for n being Element of NAT,x0 being Element of REAL-US n, B
being Subset of REAL-US n st B=RN_Base n holds ex l being Linear_Combination of
B st x0=Sum l
proof
let n be Element of NAT,x0 be Element of REAL-US n, B be Subset of REAL-US n;
reconsider x1=x0 as Element of REAL n by REAL_NS1:def 6;
A1: REAL n=the carrier of (REAL-US n) by REAL_NS1:def 6;
assume
A2: B=RN_Base n;
A3: {x where x is Element of REAL n: ex i being Element of NAT st 1<=i & i<=
n & x=Base_FinSeq(n,i)} c= B
proof
let y be object;
assume y in {x where x is Element of REAL n: ex i being Element of NAT st
1<=i & i<=n & x=Base_FinSeq(n,i)};
then
ex x being Element of REAL n st y=x & ex i being Element of NAT st 1
<=i & i<=n & x=Base_FinSeq(n,i);
hence y in B by A2;
end;
B c= {x where x is Element of REAL n: ex i being Element of NAT st 1<=i
& i<=n & x=Base_FinSeq(n,i)}
proof
let y be object;
assume y in B; then
ex i2 being Element of NAT st y=Base_FinSeq(n,i2) & 1<= i2 & i2<=n by A2;
hence y in {x where x is Element of REAL n: ex i being Element of NAT st 1
<=i & i<=n & x=Base_FinSeq(n,i)};
end;
then
A4: B={x where x is Element of REAL n: ex i being Element of NAT st 1<=i &
i<=n & x=Base_FinSeq(n,i)} by A3,XBOOLE_0:def 10;
A5: {x where x is Element of REAL n: ex i being Element of NAT st 1<=i & i<=
n & x=Base_FinSeq(n,i) & |(x1,x)| <>0} c=B
proof
let x2 being object;
assume x2 in {x where x is Element of REAL n: ex i being Element of NAT
st 1<=i & i<=n & x=Base_FinSeq(n,i) & |(x1,x)| <>0};
then
ex x being Element of REAL n st x=x2 & ex i being Element of NAT st 1
<=i & i<=n & x=Base_FinSeq(n,i) & |(x1,x)| <>0;
hence x2 in B by A4;
end;
then reconsider
B0={x where x is Element of REAL n: ex i being Element of NAT st
1<=i & i<=n & x=Base_FinSeq(n,i) & |(x1,x)| <>0} as Subset of REAL-US n by
XBOOLE_1:1;
defpred R[object,object] means
$1 in B0 implies ex i being Element of NAT st $2=i
& 1<=i & i<=n & $1=Base_FinSeq(n,i);
A6: for x being object st x in B0 ex y being object st y in Seg n & R[x,y]
proof
let x be object;
assume x in B0;
then consider x2 being Element of REAL n such that
A7: x=x2 and
A8: ex i being Element of NAT st 1<=i & i<=n & x2=Base_FinSeq(n,i) &
|( x1,x2)| <>0;
consider i0 being Element of NAT such that
A9: 1<=i0 and
A10: i0<=n and
A11: x2=Base_FinSeq(n,i0) and
|(x1,x2)| <>0 by A8;
i0 in Seg n by A9,A10,FINSEQ_1:1;
hence ex y being object st y in Seg n & R[x,y] by A7,A9,A10,A11;
end;
consider f being Function of B0,Seg n such that
A12: for x being object st x in B0 holds R[x,f.x] from FUNCT_2:sch 1(A6);
defpred Q[object,object] means
($1 in B0 implies (for i being Element of NAT st 1
<=i & i<=n & $1=Base_FinSeq(n,i) holds $2=|( x1, Base_FinSeq(n,i) )|))& (not $1
in B0 implies $2=0);
A13: for x being object st x in the carrier of REAL-US n
ex y being object st y in REAL & Q[x,y]
proof
let x be object;
assume x in the carrier of (REAL-US n);
per cases;
suppose
A14: x in B0;
then consider x2 being Element of REAL n such that
A15: x2=x and
ex i being Element of NAT st 1<=i & i<=n & x2=Base_FinSeq(n,i) & |(
x1,x2)| <>0;
reconsider y0=|(x1,x2)| as Element of REAL;
for i2 being Element of NAT st 1<=i2 & i2<=n & x=Base_FinSeq(n,i2)
holds y0=|( x1, Base_FinSeq(n,i2) )| by A15;
hence ex y being object st y in REAL & Q[x,y] by A14;
end;
suppose
not x in B0;
hence ex y being object st y in REAL & Q[x,y] by Lm3;
end;
end;
consider l2 being Function of the carrier of (REAL-US n),REAL such that
A16: for x being object st x in the carrier of (REAL-US n) holds Q[x,l2.x]
from FUNCT_2:sch 1(A13);
A17: l2 is Element of Funcs(the carrier of (REAL-US n),REAL) by FUNCT_2:8;
for v being Element of REAL-US n st not v in B0 holds l2.v = 0 by A16;
then reconsider l3=l2 as Linear_Combination of REAL-US n by A2,A5,A17,
RLVECT_2:def 3;
Carrier l3 c= B0
proof
let x be object;
assume x in Carrier l3;
then x in { v where v is Element of REAL-US n : l3 . v <> 0 } by
RLVECT_2:def 4;
then ex v being Element of REAL-US n st x=v & l3 . v <> 0;
hence x in B0 by A16;
end;
then reconsider l0=l3 as Linear_Combination of B0 by RLVECT_2:def 6;
A18: Carrier l0 c= B0 by RLVECT_2:def 6;
then Carrier l0 c= B by A5;
then reconsider l2=l0 as Linear_Combination of B by RLVECT_2:def 6;
A19: B0 c= Carrier l0
proof
let x be object;
assume
A20: x in B0;
then consider x6 being Element of REAL n such that
A21: x=x6 and
A22: ex i being Element of NAT st 1<=i & i<=n & x6=Base_FinSeq(n,i)&
|( x1,x6)| <>0;
reconsider x66=x6 as Element of REAL-US n by REAL_NS1:def 6;
consider i8 being Element of NAT such that
1<=i8 and
i8<=n and
A23: x6=Base_FinSeq(n,i8) and
|(x1,x6)| <>0 by A22;
l0.x66=|( x1, Base_FinSeq(n,i8) )| by A16,A20,A21,A22,A23;
then x in { v where v is Element of REAL-US n : l0 . v <> 0 } by A21,A22
,A23;
hence x in Carrier l0 by RLVECT_2:def 4;
end;
A24: dom ((Sgm (rng f))qua Function) = Seg len (Sgm (rng f)) by FINSEQ_1:def 3;
A25: rng (((f qua Function)")*((Sgm (rng f))qua Function)) c= rng (((f qua
Function)")qua Function) by RELAT_1:26;
A26: dom ((Sgm (rng f))qua Function) = Seg len (Sgm (rng f)) by FINSEQ_1:def 3;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1=f.x2 holds x1= x2
proof
let x1,x2 be object;
assume that
A27: x1 in dom f and
A28: x2 in dom f and
A29: f.x1=f.x2;
A30: ex i2 being Element of NAT st f.x2=i2 & 1<=i2 & i2<=n & x2=
Base_FinSeq(n,i2) by A12,A28;
ex i1 being Element of NAT st f.x1=i1 & 1<=i1 & i1<=n & x1=
Base_FinSeq(n,i1) by A12,A27;
hence x1=x2 by A29,A30;
end;
then
A31: f is one-to-one by FUNCT_1:def 4;
A32: Seg n={} implies B0={}
proof
set y = the Element of B0;
assume
A33: Seg n={};
assume B0 <> {};
then y in B0;
then ex x being Element of REAL n st x=y & ex i being Element of NAT st 1
<=i & i<=n & x=Base_FinSeq(n,i) & |(x1,x)| <>0;
hence contradiction by A33;
end;
iii: rng f is included_in_Seg by FINSEQ_1:def 13;
then
A47: rng (Sgm (rng f))= rng f by FINSEQ_1:def 14;
A34: for i3 being Element of NAT st i3 in dom (ProjFinSeq x1) & not i3 in
rng (Sgm (rng f)) holds (ProjFinSeq x1).i3= 0*n
proof
let i3 be Element of NAT;
assume that
A35: i3 in dom (ProjFinSeq x1) and
A36: not i3 in rng (Sgm (rng f));
A37: i3 in Seg len (ProjFinSeq x1) by A35,FINSEQ_1:def 3;
then
A38: 1<=i3 by FINSEQ_1:1;
len (ProjFinSeq x1)=n by Def12;
then
A39: i3<=n by A37,FINSEQ_1:1;
A40: not i3 in rng f by A36,A47;
A41: now
assume |( x1,Base_FinSeq(n,i3) )| <> 0; then
A42: Base_FinSeq(n,i3) in B0 by A38,A39;
then consider i5 being Element of NAT such that
A43: f.(Base_FinSeq(n,i3))=i5 and
1<=i5 and
i5<=n and
A44: Base_FinSeq(n,i3)=Base_FinSeq(n,i5) by A12;
A45: Base_FinSeq(n,i3) in dom f by A32,A42,FUNCT_2:def 1;
i3=i5 by A38,A39,A44,Th24;
hence contradiction by A40,A43,A45,FUNCT_1:def 3;
end;
(ProjFinSeq x1).i3 =(|( x1,Base_FinSeq(n,i3) )|)*(Base_FinSeq(n,i3) )
by A38,A39,Def12;
hence (ProjFinSeq x1).i3= 0*n by A41,EUCLID_4:3;
end;
A46: rng (((ProjFinSeq x1)qua Function)*((Sgm (rng f))qua Function)) c= REAL n;
A48: dom f=B0 by A32,FUNCT_2:def 1;
then rng ((f qua Function)") = B0 by A31,FUNCT_1:33;
then
A49: rng ((f qua Function)" *((Sgm (rng f))qua Function)) c= the carrier of
(REAL-US n) by A25,XBOOLE_1:1;
dom ((((f qua Function)") qua Function)*((Sgm (rng f))qua Function)) =
((Sgm (rng f))qua Function)"(dom ((f qua Function)")) by RELAT_1:147
.= ((Sgm (rng f))qua Function)"(rng f) by A31,FUNCT_1:33
.= dom (Sgm (rng f)) by A47,Th1;
then (((f qua Function)")qua Function)* ((Sgm (rng f))qua Function) is
FinSequence by A26,FINSEQ_1:def 2;
then reconsider
F0=(f qua Function)" *((Sgm (rng f))qua Function) as FinSequence
of the carrier of (REAL-US n) by A49,FINSEQ_1:def 4;
dom F0= ((Sgm (rng f))qua Function)"(dom ((f qua Function)")) by RELAT_1:147
.= ((Sgm (rng f))qua Function)"(rng f) by A31,FUNCT_1:33
.= dom ((Sgm (rng f))qua Function) by A47,Th1;
then
A50: dom F0=Seg len (Sgm (rng f)) by FINSEQ_1:def 3;
A51: dom (ProjFinSeq x1)=Seg len (ProjFinSeq x1) by FINSEQ_1:def 3
.=Seg n by Def12;
then dom (((ProjFinSeq x1)qua Function)* ((Sgm (rng f))qua Function)) = ((
Sgm (rng f))qua Function)"(Seg n) by RELAT_1:147
.= dom (Sgm (rng f)) by A47,Th1;
then ((ProjFinSeq x1)qua Function)*((Sgm (rng f))qua Function) is
FinSequence by A24,FINSEQ_1:def 2;
then reconsider
F2=((ProjFinSeq x1)qua Function)* ((Sgm (rng f))qua Function) as
FinSequence of the carrier of (REAL-US n) by A1,A46,FINSEQ_1:def 4;
dom F2= ((Sgm (rng f))qua Function)"(Seg n) by A51,RELAT_1:147
.= dom (Sgm (rng f)) by A47,Th1;
then
A52: dom F2=Seg len (Sgm (rng f)) by FINSEQ_1:def 3;
then
A53: Seg len F2=Seg len (Sgm (rng f)) by FINSEQ_1:def 3;
A54: len F2=len (Sgm (rng f)) by A52,FINSEQ_1:def 3;
dom ((f qua Function)")=rng f by A31,FUNCT_1:33;
then rng F0=rng ((f qua Function)") by A47,RELAT_1:28
.=dom f by A31,FUNCT_1:33;
then
A55: rng F0 =Carrier l0 by A48,A18,A19,XBOOLE_0:def 10;
A56: for i being Nat st i in dom F2 holds F2 . i = (l0 . (F0 /. i
)) * (F0 /. i)
proof
let i be Nat;
A57: Sgm (rng f) is one-to-one by iii,FINSEQ_3:92;
assume i in dom F2; then
A58: i in Seg len F2 by FINSEQ_1:def 3; then
A59: i in dom (Sgm (rng f)) by A54,FINSEQ_1:def 3;
then (Sgm (rng f)).i in rng (Sgm (rng f)) by FUNCT_1:def 3;
then reconsider i2=(Sgm (rng f)).i as Element of NAT;
reconsider r=Base_FinSeq(n,i2) as Element of (REAL-US n) by REAL_NS1:def 6;
i2 in rng (Sgm (rng f)) by A59,FUNCT_1:def 3;
then consider x2 being object such that
A60: x2 in dom f and
A61: f.x2=i2 by A47,FUNCT_1:def 3;
dom f=B0 by A32,FUNCT_2:def 1;
then reconsider r2=x2 as Element of REAL-US n by A60;
A62: ex i22 being Element of NAT st f.r2=i22 & 1<=i22 & i22 <=n & r2=
Base_FinSeq(n,i22) by A12,A60;
then consider i4 being Element of NAT such that
A63: f.r=i4 and
1<=i4 and
i4<=n and
A64: r=Base_FinSeq(n,i4) by A61;
A65: dom f=B0 by A32,FUNCT_2:def 1;
F0.i= ((f qua Function)").((((Sgm (rng f))qua Function)).i) by A59,
FUNCT_1:13
.= Base_FinSeq(n,i2) by A31,A60,A61,A62,FUNCT_1:32;
then Base_FinSeq(n,i2) in rng F0 by A50,A53,A58,FUNCT_1:def 3;
then Base_FinSeq(n,i2) in { v where v is Element of REAL-US n : l0 . v <>
0 } by A55,RLVECT_2:def 4;
then
A66: ex v0 being Element of REAL-US n st Base_FinSeq(n,i2)=v0 & l0.v0 <>0;
then Base_FinSeq(n,i2) in B0 by A16;
then
A67: ((f qua Function)").( (f.(Base_FinSeq(n,i2)))) =Base_FinSeq(n,i2) by A31
,A65,FUNCT_1:34;
then
A68: ((f qua Function)"*(Sgm (rng f))).i=Base_FinSeq(n,i2) by A59,A61,A62,
FUNCT_1:13;
A69: i2 in rng f by A47,A59,FUNCT_1:def 3;
then
A70: 1<=i2 by FINSEQ_1:1;
A71: i2<=n by A69,FINSEQ_1:1;
then i4=i2 by A70,A64,Th24;
then
A72: ((Sgm (rng f)) qua Function)". (f.(Base_FinSeq(n,i2)))=i by A59,A63,A57,
FUNCT_1:32;
A73: f.(Base_FinSeq(n,i2)) in rng (Sgm (rng f)) by A47,A60,A61,A62,
FUNCT_1:def 3;
then
A74: ((f qua Function)").((Sgm (rng f)). (((Sgm (rng f)) qua Function)".
(f.(Base_FinSeq(n,i2))))) =Base_FinSeq(n,i2) by A57,A67,FUNCT_1:35;
dom (((Sgm (rng f)) qua Function)")=rng (Sgm (rng f)) by A57,FUNCT_1:33;
then ((Sgm (rng f)) qua Function)". (f.(Base_FinSeq(n,i2))) in rng (((Sgm
(rng f)) qua Function)") by A73,FUNCT_1:def 3;
then
A75: ((Sgm (rng f)) qua Function)". (f.(Base_FinSeq(n,i2))) in dom (Sgm (
rng f)) by A57,FUNCT_1:33;
l0 . (F0 /. i)=l0.((((f qua Function)")*(Sgm (rng f))).i) by A50,A54,A58,
PARTFUN1:def 6
.=l0.(Base_FinSeq(n,i2)) by A72,A75,A74,FUNCT_1:13
.=|( x1,Base_FinSeq(n,i2) )| by A16,A70,A71,A66;
then (l0 . (F0 /. i)) * (F0 /. i) =( |( x1,Base_FinSeq(n,i2) )| )*(
Base_FinSeq(n,i2)) by A50,A54,A58,A68,PARTFUN1:def 6
.=(ProjFinSeq x1).((Sgm (rng f)).i) by A70,A71,Def12
.=(((ProjFinSeq x1) qua Function) *((Sgm (rng f))qua Function)).i by A59,
FUNCT_1:13;
hence F2 . i = (l0 . (F0 /. i)) * (F0 /. i);
end;
A76: ((Sgm (rng f))qua Function) is one-to-one by iii,FINSEQ_3:92;
reconsider F3=F2 as FinSequence of REAL n by REAL_NS1:def 6;
A77: x0= Sum (ProjFinSeq x1) by Th30
.= Sum F3 by A47,A51,A34,iii,Th23,FINSEQ_3:92
.= Sum F2 by Th33;
len F2 = len F0 by A50,A53,FINSEQ_1:def 3;
then x1=Sum (l0 (#) F0) by A77,A56,RLVECT_2:def 7;
then x1=Sum l2 by A31,A76,A55,RLVECT_2:def 8;
hence ex l being Linear_Combination of B st x0=Sum l;
end;
theorem Th44:
for B being Subset of RealVectSpace(Seg n) st B=RN_Base n holds
B is Basis of RealVectSpace(Seg n)
proof
let B be Subset of RealVectSpace(Seg n);
set V= RealVectSpace(Seg n);
assume
A1: B=RN_Base n;
then reconsider B1 = B as R-orthonormal Subset of V;
A2: the carrier of Lin B = the set of all
(Sum l) where l is Linear_Combination of B by RLVECT_3:def 2;
A3: now
assume not the carrier of V c= the carrier of Lin B;
then consider x being object such that
A4: x in the carrier of V and
A5: not x in the carrier of Lin B;
reconsider x0=x as Element of V by A4;
ex l being Linear_Combination of B st x0=Sum l by A1,Th42;
hence contradiction by A2,A5;
end;
the carrier of Lin B c= the carrier of V
proof
let x be object;
assume x in the carrier of Lin B;
then ex l being Linear_Combination of B st x=(Sum l) by A2;
hence x in the carrier of V;
end;
then the carrier of Lin B=the carrier of V by A3,XBOOLE_0:def 10;
then Lin B = V by Th8;
then B1 is Basis of RealVectSpace(Seg n) by RLVECT_3:def 3;
hence thesis;
end;
registration
let n;
cluster RealVectSpace(Seg n) -> finite-dimensional;
coherence
proof
reconsider B=RN_Base n as Subset of RealVectSpace(Seg n) by FINSEQ_2:93;
B is Basis of RealVectSpace(Seg n) by Th44;
hence thesis by RLVECT_5:def 1;
end;
end;
theorem
dim (RealVectSpace(Seg n)) = n
proof
reconsider B=RN_Base n as Subset of RealVectSpace(Seg n) by FINSEQ_2:93;
A1: for I being Basis of RealVectSpace(Seg n) holds n = card I
proof
let I be Basis of RealVectSpace(Seg n);
B is Basis of RealVectSpace(Seg n) by Th44;
then card B=card I by RLVECT_5:25;
hence n = card I by Lm5;
end;
n in NAT by ORDINAL1:def 12;
hence thesis by A1,RLVECT_5:def 2;
end;
theorem Th46:
for B being Subset of RealVectSpace(Seg n) st B is Basis of
RealVectSpace(Seg n) holds card B = n
proof
let B be Subset of RealVectSpace(Seg n);
assume
A1: B is Basis of RealVectSpace(Seg n);
reconsider Br=RN_Base n as Subset of RealVectSpace(Seg n) by FINSEQ_2:93;
Br is Basis of RealVectSpace(Seg n) by Th44;
then card Br=card B by A1,RLVECT_5:25;
hence card B=n by Lm5;
end;
theorem Th47:
{} is Basis of RealVectSpace(Seg 0)
proof
consider A being finite Subset of RealVectSpace(Seg 0) such that
A1: A is Basis of RealVectSpace(Seg 0) by RLVECT_5:def 1;
card A=0 by A1,Th46;
then A={};
hence thesis by A1;
end;
theorem Th48:
for n being Element of NAT holds RN_Base n is Basis of REAL-US n
proof
let n be Element of NAT;
reconsider B = RN_Base n as Subset of REAL-US n by REAL_NS1:def 6;
set V = REAL-US n;
A1: the carrier of Lin B = the set of all
Sum l where l is Linear_Combination of B by RUSUB_3:def 1;
A2: now
assume not the carrier of V c= the carrier of Lin B;
then consider x being object such that
A3: x in the carrier of V and
A4: not x in the carrier of Lin B;
reconsider x0=x as Element of V by A3;
ex l being Linear_Combination of B st x0=Sum l by Th43;
hence contradiction by A1,A4;
end;
the carrier of Lin B c= the carrier of V
proof
let x be object;
assume x in the carrier of Lin B;
then ex l being Linear_Combination of B st x = Sum l by A1;
hence x in the carrier of V;
end;
then the carrier of Lin B=the carrier of V by A2,XBOOLE_0:def 10;
then Lin B = V by RUSUB_1:26;
hence thesis by RUSUB_3:def 2;
end;
theorem Th49:
for D being Orthogonal_Basis of n holds D is Basis of RealVectSpace(Seg n)
proof
let D being Orthogonal_Basis of n;
set V = RealVectSpace(Seg n);
reconsider B = D as R-orthonormal Subset of V by FINSEQ_2:93;
per cases;
suppose
n=0;
hence thesis by Th17,Th47;
end;
suppose
A1: n<>0;
reconsider D0=D as R-orthonormal Subset of REAL n;
consider I being Basis of V such that
A2: B c= I by RLVECT_5:2;
card I=n by Th46;
then
A3: I is finite;
A4: for D2 being R-orthonormal Subset of REAL n st D0 c= D2 holds D2=D0 by Def6
;
A5: now
assume that
B <>I and
A6: not I c= the carrier of Lin B;
consider x0 being object such that
A7: x0 in I and
A8: not x0 in the carrier of Lin B by A6;
reconsider z0=x0 as Element of REAL n by A7,FINSEQ_2:93;
not x0 in Lin B by A8;
then
A9: not x0 in B by RLVECT_3:15;
consider p being FinSequence such that
A10: rng p=B and
A11: p is one-to-one by A2,A3,FINSEQ_4:58;
A12: 1<=len p+1 by NAT_1:12;
reconsider p0 =p as FinSequence of REAL n by A10,FINSEQ_1:def 4;
defpred P[Nat] means 1<=$1 & $1<=len p+1 implies ex q being FinSequence
of REAL n st len q=$1 & ($1<=len p implies for d being Real holds not q.$1=d*(
p0/.$1))& q.1=z0 & for i being Nat,a,b being Element of REAL n st 1<=i & i< $1
& a=q/.i & b=p0/.i holds (q/.(i+1))<> 0*n & q.(i+1)=(q/.i)-( |( a,b )| )*(p0/.i
);
A13: I is linearly-independent by RLVECT_3:def 3;
A14: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A15: P[k];
per cases;
suppose
A16: 1<=k+1 & k+1<=len p+1;
k<k+1 by XREAL_1:29;
then
A17: k<len p+1 by A16,XXREAL_0:2;
A18: k<=len p by A16,XREAL_1:6;
per cases;
suppose
1<=k;
then consider q0 being FinSequence of REAL n such that
A19: len q0=k and
A20: 1<=k and
k<=len p+1 and
A21: k<=len p implies for d being Real holds not q0.(k)=d*(p0 /.(k)) and
A22: q0.1=z0 and
A23: for i being Nat,a,b being Element of REAL n st 1<=i & i<
k & a=q0/. i & b=p0/.i holds (q0/.(i+1))<> 0*n & q0.(i+1)=(q0/.i)-( |( a,b )| )
*(p0/.i) by A15,A17;
reconsider a2=q0/.k,b2=p0/.k as Element of REAL n;
reconsider q3=<* (q0/.k)-( |( a2,b2 )| )*(p0/.k) *> as FinSequence
of REAL n;
reconsider q1=q0^q3 as FinSequence of REAL n;
1 in Seg len q0 by A19,A20,FINSEQ_1:1;
then
A24: 1 in dom q0 by FINSEQ_1:def 3;
then
A25: q1.1=z0 by A22,FINSEQ_1:def 7;
A26: 1<=k+1 by NAT_1:12;
A27: k+1<=len p implies p0/.(k+1) in B
proof
assume
A28: k+1<=len p;
then k+1 in dom p by A26,FINSEQ_3:25;
then p.(k+1) in rng p by FUNCT_1:def 3;
hence p0/.(k+1) in B by A10,A28,FINSEQ_4:15,NAT_1:12;
end;
A29: len q1=len q0+len q3 by FINSEQ_1:22
.=k+1 by A19,FINSEQ_1:40;
A30: for i being Nat,a,b being Element of REAL n st 1<=i & i< k+1
& a=q1/.i & b=p0/.i holds (q1/.(i+1))<> 0*n & q1.(i+1)=(q1/.i)-( |( a,b )| )*(
p0/.i)
proof
let i be Nat,a,b be Element of REAL n;
assume that
A31: 1<=i and
A32: i< k+1 and
A33: a=q1/.i and
A34: b=p0/.i;
A35: i<=k by A32,NAT_1:13;
A36: i+1<=k+1 by A32,NAT_1:13;
A37: 1<=i+1 by NAT_1:12;
per cases by A35,XXREAL_0:1;
suppose
A38: i<k;
then
A39: i+1<=k by NAT_1:13;
then
A40: q1.(i+1) = q0.(i+1) by A19,FINSEQ_1:64,NAT_1:12;
A41: q1/.(i+1)=q1.(i+1) by A29,A37,A36,FINSEQ_4:15;
A42: q0/.(i+1)=q0.(i+1) by A19,A39,FINSEQ_4:15,NAT_1:12;
q1/.i=q1.i by A29,A31,A32,FINSEQ_4:15
.=q0.i by A19,A31,A35,FINSEQ_1:64
.= q0/.i by A19,A31,A35,FINSEQ_4:15;
hence
(q1/.(i+1))<> 0*n & q1.(i+1)=(q1/.i)-( |( a,b )| )*(p0/.i
) by A23,A31,A33,A34,A38,A40,A41,A42;
end;
suppose
A43: i=k;
then
A44: q1/.(i+1)=q1.(k+1) by A29,A26,FINSEQ_4:15
.=q3.(k+1-len q0) by A19,A29,FINSEQ_1:24,XREAL_1:29
.=(q0/.k)-( |( a2,b2 )| )*(p0/.k) by A19;
A45: now
assume (q1/.(i+1)) = 0*n;
then (q0/.k)-( |( a2,b2 )| )*(p0/.k)+ ( |( a2,b2 )| )*(p0/.
k) =( |( a2,b2 )| )*(p0/.k) by A44,EUCLID_4:1;
then
A46: q0/.k=( |( a2,b2 )| )*(p0/.k) by RVSUM_1:43;
q0/.k=q0.k by A19,A20,FINSEQ_4:15;
hence contradiction by A16,A21,A46,XREAL_1:6;
end;
k<k+1 by XREAL_1:29;
then
A47: q1/.k=q1.k by A20,A29,FINSEQ_4:15;
A48: q0/.k=q0.k by A19,A20,FINSEQ_4:15;
q1.k=q0.k by A19,A20,FINSEQ_1:64;
hence
(q1/.(i+1))<> 0*n & q1.(i+1)=(q1/.i)-( |( a,b )| )*(p0/.i
) by A29,A33,A34,A37,A43,A48,A47,A44,A45,FINSEQ_4:15;
end;
end;
A49: for s1 being Element of RealVectSpace(Seg n),a01 being Real
st s1 in B holds a01*s1 in the carrier of Lin B
proof
let s1 be Element of RealVectSpace(Seg n),a01 be Real;
assume
A50: s1 in B;
{s1} c= B
by A50,TARSKI:def 1;
then Lin {s1} is Subspace of Lin B by RLVECT_3:20;
then
A51: the carrier of Lin {s1} c= the carrier of Lin B by RLSUB_1:def 2;
a01*s1 in Lin {s1} by RLVECT_4:8;
then a01*s1 in the carrier of Lin {s1};
hence a01*s1 in the carrier of Lin B by A51;
end;
A52: for s1 being Element of REAL n,a01 being Real st s1 in B
holds a01*s1 in the carrier of Lin B
proof
let s1 be Element of REAL n,a01 be Real;
reconsider s10=s1 as Element of RealVectSpace(Seg n) by
FINSEQ_2:93;
reconsider aa=a01 as Element of REAL by XREAL_0:def 1;
A53: aa*s1=aa*s10;
assume s1 in B;
hence a01*s1 in the carrier of Lin B by A49,A53;
end;
defpred G[Nat] means $1+1<=k+1 implies not q1.($1+1) in the
carrier of Lin B;
A54: for j being Nat st G[j] holds G[j+1]
proof
let j be Nat;
assume
A55: G[j];
j+1+1<=k+1 implies not q1.(j+1+1) in the carrier of Lin B
proof
A56: B c= the carrier of Lin B
proof
let z be object;
assume z in B;
then z in Lin B by RLVECT_3:15;
hence z in the carrier of Lin B;
end;
assume j+1+1<=k+1;
then
A57: j+1<=k by XREAL_1:6;
per cases by A57,XXREAL_0:1;
suppose
A58: j+1=k;
1<=j+1 by NAT_1:12;
then j+1 in dom p0 by A18,A58,FINSEQ_3:25;
then
A59: p0.(j+1) in rng p by FUNCT_1:def 3;
A60: p0/.(j+1)=p0.(j+1) by A18,A58,FINSEQ_4:15,NAT_1:12;
1<=j+1+1 by NAT_1:12;
then
A61: q1/.(j+1+1)=q1.(j+1+1) by A29,A58,FINSEQ_4:15;
A62: q1.(j+1+1)=(q0/.k)-( |( a2,b2 )| )*(p0/.k) by A19,A58,
FINSEQ_1:42;
now
assume
A63: q1.(j+1+1) in the carrier of Lin B;
q1/.(j+1+1)+( |( a2,b2 )| )*(p0/.(j+1)) =(q0/.(j+1))
by A58,A62,A61,RVSUM_1:43;
then (q0/.(j+1)) in the carrier of Lin B by A10,A56,A61,A59
,A60,A63,Lm4;
then
A64: (q0/.(j+1)) in Lin B;
A65: not q1.(j+1) in Lin B by A55,A58,XREAL_1:29;
q1.(j+1)=q0.(j+1) by A19,A20,A58,FINSEQ_1:64;
hence contradiction by A19,A20,A58,A64,A65,FINSEQ_4:15;
end;
hence not q1.(j+1+1) in the carrier of Lin B;
end;
suppose
A66: j+1<k;
reconsider a11=q0/.(j+1),b11=p0/.(j+1) as Element of REAL n;
A67: j+1+1<=k by A66,NAT_1:13;
then
A68: q0/.(j+1+1)=q0.(j+1+1) by A19,FINSEQ_4:15,NAT_1:12;
A69: j+1<=len p0 by A18,A66,XXREAL_0:2;
then
A70: p0/.(j+1)=p0.(j+1) by FINSEQ_4:15,NAT_1:12;
A71: 1<=j+1 by NAT_1:12;
then j+1 in dom p0 by A69,FINSEQ_3:25;
then
A72: p0.(j+1) in rng p by FUNCT_1:def 3;
A73: q1.(j+1+1)=q0.(j+1+1) by A19,A67,FINSEQ_1:64,NAT_1:12;
A74: q0.(j+1+1)=(q0/.(j+1))-( |( a11,b11 )| )*(p0/.(j+1)) by A23
,A66,A71;
now
assume
A75: q1.(j+1+1) in the carrier of Lin B;
q0/.(j+1+1)+( |( a11,b11 )| )*(p0/.(j+1)) =(q0/.(j+1)
) by A74,A68,RVSUM_1:43;
then (q0/.(j+1)) in the carrier of Lin B by A10,A56,A68,A72
,A70,A73,A75,Lm4;
then
A76: (q0/.(j+1)) in Lin B;
k<k+1 by XREAL_1:29;
then
A77: not q1.(j+1) in Lin B by A55,A66,XXREAL_0:2;
q1.(j+1)=q0.(j+1) by A19,A66,FINSEQ_1:64,NAT_1:12;
hence contradiction by A19,A66,A76,A77,FINSEQ_4:15,NAT_1:12
;
end;
hence not q1.(j+1+1) in the carrier of Lin B;
end;
end;
hence G[j+1];
end;
A78: G[0] by A8,A22,A24,FINSEQ_1:def 7;
for j being Nat holds G[j] from NAT_1:sch 2(A78,A54);
then k+1<=len p implies for d being Real holds not q1.(k+1)=d*(p0
/.(k+1)) by A52,A27;
hence P[k+1] by A29,A25,A30;
end;
suppose
A79: 1>k;
reconsider q1=<* z0 *> as FinSequence of REAL n;
A80: len q1=1 by FINSEQ_1:40;
A81: q1.1=z0;
A82: 1<=len p implies for d being Real holds not q1.(1)=d*(p0/.(1 ))
proof
assume
A83: 1<=len p;
thus for d being Real holds not q1.(1)=d*(p0/.(1))
proof
let d be Real;
1 in dom p0 by A83,FINSEQ_3:25;
then
A85: p0.1 in B by A10,FUNCT_1:def 3;
p0/.1=p0.1 by A83,FINSEQ_4:15;
hence not q1.(1)=d*(p0/.(1)) by A2,A7,A9,A13,A85,Th39;
end;
end;
A86: for i being Nat,a,b being Element of REAL n st 1<=i & i< 1 &
a=q1/.i & b=p0/.i holds (q1/.(i+1))<> 0*n & q1.(i+1)=(q1/.i)-( |( a,b )| )*(p0
/.i);
k=0 by A79,NAT_1:14;
hence P[k+1] by A80,A81,A82,A86;
end;
end;
suppose
not (1<=k+1 & k+1<=len p+1);
hence P[k+1];
end;
end;
A87: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A87,A14);
then consider q being FinSequence of REAL n such that
A88: len q=len p+1 and
len p+1<=len p implies for d being Real holds not q.(len p+1)=d*( p0
/.(len p+1)) and
q.1=z0 and
A89: for i being Nat,a,b being Element of REAL n st 1<=i & i< len p
+1 & a=q/.i & b=p0/.i holds (q/.(i+1))<> 0*n & q.(i+1)=(q/.i)-( |( a,b )| )*(p0
/.i) by A12;
reconsider u4=q/.(len q) as Element of REAL n;
A90: len p<len p +1 by XREAL_1:29;
set u0=(1/(|.u4.|))*u4;
reconsider B3=B \/ {u0} as Subset of REAL n by XBOOLE_1:8;
A91: for i being Nat,s being Element of REAL n st 1<=i & i<=len p & p0
/.i=s holds |( s,u4 )| = 0
proof
defpred Q[Nat] means for s2 being Element of REAL n, u2 being Element
of REAL n,k being Nat st u2=q/.$1 & 1<=k & k< $1 & $1<=len p+1 & p0/.k=s2 holds
|( s2,u2 )| =0;
let i be Nat,s be Element of REAL n;
assume that
A92: 1<=i and
A93: i<=len p and
A94: p0/.i=s;
A95: for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume
A96: Q[k];
for s2 being Element of REAL n, u2 being Element of REAL n,k2
being Nat st u2=q/.(k+1) & 1<=k2 & k2<k+1 & k+1<=len p+1 & p0/.k2=s2 holds |(
s2,u2 )| =0
proof
A97: k<k+1 by XREAL_1:29;
let s2 be Element of REAL n, u2 being Element of REAL n,k2 being
Nat;
assume that
A98: u2=q/.(k+1) and
A99: 1<=k2 and
A100: k2<k+1 and
A101: k+1<=len p+1 and
A102: p0/.k2=s2;
A103: k2<=k by A100,NAT_1:13;
per cases;
suppose
k=0;
hence |( s2,u2 )| =0 by A99,A100;
end;
suppose
A104: k<>0;
reconsider a=q/.k, b=p0/.k as Element of REAL n;
A105: k<len p+1 by A101,A97,XXREAL_0:2;
then
A106: k<=len p by NAT_1:13;
1<=k+1 by A99,A100,XXREAL_0:2;
then
A107: u2= q.(k+1) by A88,A98,A101,FINSEQ_4:15;
A108: 0+1<=k by A104,NAT_1:13;
then q.(k+1)=(q/.k)-( |( a,b )| )*(p0/.k) by A89,A105;
then
A109: |( s2,u2 )| = |(s2,a)| - |(s2,( |( a,b )| )*b )| by A107,
EUCLID_4:26
.= |(s2,a)| - ( |( a,b )| )* ( |( s2,b )| ) by EUCLID_4:21;
per cases by A103,XXREAL_0:1;
suppose
A110: k2<k;
then
A111: 1<k by A99,XXREAL_0:2;
then
A112: p0/.k=p0.k by A106,FINSEQ_4:15;
k in Seg len p0 by A106,A111,FINSEQ_1:1;
then
A113: k in dom p0 by FINSEQ_1:def 3;
then
A114: b in D by A10,A112,FUNCT_1:def 3;
A115: k<len p+1 by A101,A97,XXREAL_0:2;
A116: k2<len p by A106,A110,XXREAL_0:2;
then
A117: p0/.k2=p0.k2 by A99,FINSEQ_4:15;
k2 in Seg len p0 by A99,A116,FINSEQ_1:1;
then
A118: k2 in dom p0 by FINSEQ_1:def 3;
then
A119: s2 in rng p by A102,A117,FUNCT_1:def 3;
s2<>b by A11,A102,A110,A117,A118,A112,A113,FUNCT_1:def 4;
then |( s2,b)| =0 by A10,A119,A114,Def3;
hence |( s2,u2 )| =0 by A96,A99,A102,A109,A110,A115;
end;
suppose
A120: k2=k;
k in Seg len p0 by A108,A106,FINSEQ_1:1;
then
A121: k in dom p0 by FINSEQ_1:def 3;
p0/.k=p0.k by A108,A106,FINSEQ_4:15;
then b in rng p0 by A121,FUNCT_1:def 3;
then |.b.| =1 by A10,Def4;
then (|.b.|)^2=1;
hence
|( s2,u2 )| =|(b,a)| - ( |( a,b )| )* 1 by A102,A109,A120,
EUCLID_2:4
.=0;
end;
end;
end;
hence Q[k+1];
end;
A122: Q[0];
A123: for k being Nat holds Q[k] from NAT_1:sch 2(A122,A95);
len p<len p+1 by XREAL_1:29;
then i<len q by A88,A93,XXREAL_0:2;
hence |( s,u4 )| =0 by A88,A92,A94,A123;
end;
A124: for i being Nat,s being Element of REAL n st 1<=i & i<=len p & p0
/.i=s holds |( s,u0 )| = 0
proof
let i be Nat,s be Element of REAL n;
assume that
A125: 1<=i and
A126: i<=len p and
A127: p0/.i=s;
A128: |( s,u0 )| = (1/(|.u4.|))*( |( s,u4 )|) by EUCLID_4:22;
|( s,u4 )| = 0 by A91,A125,A126,A127;
hence |( s,u0 )| = 0 by A128;
end;
for x,y being real-valued FinSequence st x in B3 & y in B3 & x<>y
holds |( x,y )|=0
proof
let x,y be real-valued FinSequence;
assume that
A129: x in B3 and
A130: y in B3 and
A131: x<>y;
per cases by A129,A130,XBOOLE_0:def 3;
suppose
x in B & y in B;
hence |( x,y )|=0 by A131,Def3;
end;
suppose
A132: x in B & y in {u0};
then consider x3 being object such that
A133: x3 in dom p0 and
A134: x=p0.x3 by A10,FUNCT_1:def 3;
reconsider j=x3 as Element of NAT by A133;
A135: x3 in Seg len p0 by A133,FINSEQ_1:def 3;
then
A136: j<=len p0 by FINSEQ_1:1;
A137: y=u0 by A132,TARSKI:def 1;
A138: 1<=j by A135,FINSEQ_1:1;
then p0.x3=p0/.j by A136,FINSEQ_4:15;
hence |( x,y )|=0 by A124,A137,A134,A138,A136;
end;
suppose
A139: x in {u0} & y in B;
then consider y3 being object such that
A140: y3 in dom p0 and
A141: y=p0.y3 by A10,FUNCT_1:def 3;
reconsider j=y3 as Element of NAT by A140;
A142: y3 in Seg len p0 by A140,FINSEQ_1:def 3;
then
A143: j<=len p0 by FINSEQ_1:1;
A144: x=u0 by A139,TARSKI:def 1;
A145: 1<=j by A142,FINSEQ_1:1;
then p0.y3=p0/.j by A143,FINSEQ_4:15;
hence |( x,y )|=0 by A124,A144,A141,A145,A143;
end;
suppose
A146: x in {u0} & y in {u0};
then y=u0 by TARSKI:def 1;
hence |( x,y )|=0 by A131,A146,TARSKI:def 1;
end;
end;
then
A147: B3 is R-orthogonal;
1 in dom p by A1,A10,FINSEQ_3:32;
then
A148: 1<= len p by FINSEQ_3:25;
set aq=q/.(len p), bq=p0/.(len p);
A149: bq=p0/.(len p);
aq=q/.(len p);
then
A150: |.u4.| <> 0 by A148,A88,A89,A149,A90,EUCLID:8;
A151: |.1/|. u4 .|.|=1/(|. u4 .|) by ABSVALUE:def 1;
A152: u0 in {u0} by TARSKI:def 1;
A153: |. u0 .| = (|.1/(|.u4.|).|)*(|. u4 .|) by EUCLID:11
.= 1 by A150,A151,XCMPLX_1:106;
then B3 is R-normal by Th16;
then D0=B3 by A4,A147,XBOOLE_1:7;
then u0 in B by A152,XBOOLE_0:def 3;
then consider x3 being object such that
A154: x3 in dom p0 and
A155: u0=p0.x3 by A10,FUNCT_1:def 3;
reconsider j=x3 as Element of NAT by A154;
A156: x3 in Seg len p0 by A154,FINSEQ_1:def 3;
then
A157: j<=len p0 by FINSEQ_1:1;
A158: 1<=j by A156,FINSEQ_1:1;
then p0.x3=p0/.j by A157,FINSEQ_4:15;
then |(u0,u0)|=0 by A124,A155,A158,A157;
hence B is Basis of RealVectSpace(Seg n) by A153;
end;
Lin B is Subspace of Lin I by A2,RLVECT_3:20;
then
A159: the carrier of Lin B c= the carrier of (Lin I) by RLSUB_1:def 2;
A160: Lin I=V by RLVECT_3:def 3;
now
assume I c= the carrier of Lin B;
then Lin I is Subspace of Lin B by RLVECT_5:19;
then the carrier of (Lin I) c= the carrier of Lin B by RLSUB_1:def 2;
then the carrier of (Lin I)=the carrier of Lin B by A159,XBOOLE_0:def 10;
then Lin B=Lin I by RLSUB_1:30;
hence B is Basis of RealVectSpace(Seg n) by A160,RLVECT_3:def 3;
end;
hence thesis by A5;
end;
end;
registration
let n be Element of NAT;
cluster REAL-US n -> finite-dimensional;
coherence
proof
reconsider B=RN_Base n as Subset of REAL-US n by REAL_NS1:def 6;
B is Basis of REAL-US n by Th48;
hence thesis by RUSUB_4:def 1;
end;
end;
theorem
for n being Element of NAT holds dim (REAL-US n) = n
proof
let n be Element of NAT;
reconsider B=RN_Base n as Subset of REAL-US n by REAL_NS1:def 6;
for I being Basis of REAL-US n holds n = card I
proof
let I be Basis of REAL-US n;
B is Basis of REAL-US n by Th48;
then card B=card I by RUSUB_4:5;
hence n = card I by Lm5;
end;
hence thesis by RUSUB_4:def 2;
end;
theorem
for B being Orthogonal_Basis of n holds card B = n
proof
let B be Orthogonal_Basis of n;
reconsider B0=B as Subset of RealVectSpace(Seg n) by FINSEQ_2:93;
B0 is Basis of RealVectSpace(Seg n) by Th49;
hence card B = n by Th46;
end;