:: 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-2016 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;
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, RVSUM_1, RLVECT_3, MONOID_0;
equalities SQUARE_1, FINSEQ_2, RVSUM_1, VALUED_1, RLVECT_1, BINOP_1, STRUCT_0,
ALGSTR_0, FUNCSDOM, EUCLID, CARD_1, 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 by FINSEQ_1:40
.= z by FINSEQ_1:40;
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:];
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 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
for i being Nat st 1<=i & i0;
then 0+1<=k by NAT_1:13;
then h.k < h.(k+1) by A1,A8;
then k 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 & iy 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 by EUCLID_2:8;
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,EUCLID_2:8;
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 & i0;
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 by FINSEQ_1:40;
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) 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: ilen 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 & ik;
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 {} 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=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: nxk+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=0+1 by A41,NAT_1:13;
then
A101: 10 by A109,XREAL_1:50;
then
A112: nx-'1>=0+1 by NAT_1:13;
nxk+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*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 0*n) = 0*n
proof
let k be Element of 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 $1k+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=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 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;
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** 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 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;
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: kk+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 $1F/.(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=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;
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;
kF/.(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=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
12( 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+10;
len f 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 $1F/.(k+1) by A1,A5,A6,A8,A20,A22,FUNCT_1:def 4;
k=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;
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;
klen 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=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
12(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+10;
len f 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;
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,FINSEQ_1:def 13;
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 FINSEQ_1:def 13;
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 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 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 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;
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,FINSEQ_1:def 13;
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;
A47: rng (Sgm (rng f))= rng f by FINSEQ_1:def 13;
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 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 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,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 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 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,FINSEQ_1:40;
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 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+1k;
reconsider q1=<* z0 *> as FinSequence of REAL n;
A80: len q1=1 by FINSEQ_1:40;
A81: q1.1=z0 by FINSEQ_1:40;
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;
A84: q1.1=z0 by FINSEQ_1:40;
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,A84,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 p0;
reconsider a=q/.k, b=p0/.k as Element of REAL n;
A105: kb 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 py
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,EUCLID_4:16;
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;
*