:: 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-2018 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;
begin :: 1. Preliminaries
reserve i, j, m, n for Nat,
z, B0 for set,
f, x0 for real-valued FinSequence;
::$CT
theorem :: EUCLID_7:2
for R being Relation, Y being set st rng R c= Y holds R"Y = dom R;
theorem :: EUCLID_7:3
<* z *> * <* 1 *> = <* z *>;
theorem :: EUCLID_7:4
for x being Element of REAL 0 holds x = <*>REAL;
theorem :: EUCLID_7:5
for a,b,c being Element of REAL n holds a - b + c + b = a + c;
registration
let f1,f2 be FinSequence;
cluster <:f1,f2:> -> FinSequence-like;
end;
definition
let D be set, f1,f2 be FinSequence of D;
redefine func <:f1,f2:> -> FinSequence of [:D,D:];
end;
definition
let h be real-valued FinSequence;
redefine attr h is increasing means
:: EUCLID_7:def 1
for i being Nat st 1<=i & i FinSequence of D equals
:: EUCLID_7:def 2
F*h;
end;
theorem :: EUCLID_7:10
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;
theorem :: EUCLID_7:11
{} is Permutation of {};
theorem :: EUCLID_7:12
<* 1 *> is Permutation of {1};
theorem :: EUCLID_7:13
for h being FinSequence of REAL holds h is one-to-one iff sort_a
h is one-to-one;
theorem :: EUCLID_7:14
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;
begin :: 2. Orthogonal Basis of REAL n
definition
let B0 be set;
attr B0 is R-orthogonal means
:: EUCLID_7:def 3
for x, y being real-valued FinSequence
st x in B0 & y in B0 & x<>y holds |( x,y )| = 0;
end;
registration
cluster empty -> R-orthogonal for set;
end;
theorem :: EUCLID_7:15
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;
definition
let B0 be set;
attr B0 is R-normal means
:: EUCLID_7:def 4
for x being real-valued FinSequence st x in B0 holds |.x.| = 1;
end;
registration
cluster empty -> R-normal for set;
end;
registration
cluster R-normal for set;
end;
registration
let B0, B1 be R-normal set;
cluster B0 \/ B1 -> R-normal;
end;
theorem :: EUCLID_7:16
|.f.| = 1 implies {f} is R-normal;
theorem :: EUCLID_7:17
B0 is R-normal & |.x0.| = 1 implies B0 \/ {x0} is R-normal;
definition
let B0 be set;
attr B0 is R-orthonormal means
:: EUCLID_7:def 5
B0 is R-orthogonal R-normal;
end;
registration
cluster R-orthonormal -> R-orthogonal R-normal for set;
cluster R-orthogonal R-normal -> R-orthonormal for set;
end;
registration
cluster { <*1*> } -> R-orthonormal;
end;
registration
cluster R-orthonormal non empty for set;
end;
registration
let n;
cluster R-orthonormal for Subset of REAL n;
end;
definition
let n be Nat;
let B0 be Subset of REAL n;
attr B0 is complete means
:: EUCLID_7:def 6
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
:: EUCLID_7:def 7
B0 is R-orthonormal complete;
end;
registration
let n be Nat;
cluster orthogonal_basis -> R-orthonormal complete for Subset of REAL n;
cluster R-orthonormal complete -> orthogonal_basis for Subset of REAL n;
end;
theorem :: EUCLID_7:18
for B0 being Subset of REAL 0 st B0 is orthogonal_basis holds B0 = {};
theorem :: EUCLID_7:19
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;
begin :: 3. Linear Manifolds
definition
let n;
let X be Subset of REAL n;
attr X is linear_manifold means
:: EUCLID_7:def 8
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;
end;
theorem :: EUCLID_7:20
{ 0*n } is linear_manifold;
registration
let n;
cluster { 0*n } -> linear_manifold for Subset of REAL n;
end;
definition
let n;
let X be Subset of REAL n;
func L_Span X -> Subset of REAL n equals
:: EUCLID_7:def 9
meet {Y where Y is Subset of REAL n
: Y is linear_manifold & X c= Y};
end;
registration
let n;
let X be Subset of REAL n;
cluster L_Span X -> linear_manifold;
end;
definition
let n be Nat,f be FinSequence of REAL n;
func accum f -> FinSequence of REAL n means
:: EUCLID_7:def 10
len f = len it & f.1 = it.1 &
for i being Nat st 1<=i & i Element of REAL n equals
:: EUCLID_7:def 11
(accum f).len f if len f > 0 otherwise 0*n;
end;
theorem :: EUCLID_7:21
for F, F2 being FinSequence of REAL n, h being Permutation of
dom F st F2=F(*)h holds Sum F2=Sum F;
theorem :: EUCLID_7:22
for k being Element of NAT holds Sum(k |-> 0*n) = 0*n;
theorem :: EUCLID_7:23
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;
theorem :: EUCLID_7:24
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;
begin :: 4. Standard Basis
definition
let n, i be Nat;
redefine func Base_FinSeq(n,i) -> Element of REAL n;
end;
theorem :: EUCLID_7:25
for i1,i2 being Nat st 1<=i1 & i1<=n & Base_FinSeq(n,i1)=
Base_FinSeq(n,i2) holds i1=i2;
theorem :: EUCLID_7:26
sqr (Base_FinSeq(n,i)) = Base_FinSeq(n,i);
theorem :: EUCLID_7:27
1<=i & i<=n implies Sum Base_FinSeq(n,i)= 1;
theorem :: EUCLID_7:28
1<=i & i<=n implies |. Base_FinSeq(n,i) .| = 1;
theorem :: EUCLID_7:29
1<=i & i<=n & i<>j implies |( Base_FinSeq(n,i),Base_FinSeq(n,j))| = 0;
theorem :: EUCLID_7:30
for x being Element of REAL n st 1<=i & i<=n holds |( x,
Base_FinSeq(n,i) )| = x.i;
definition
let n be Nat;
let x0 be Element of REAL n;
func ProjFinSeq x0 -> FinSequence of REAL n means
:: EUCLID_7:def 12
len it = n & for i being Nat st 1<=i & i<=n holds
it.i = |( x0,Base_FinSeq(n,i) )| * Base_FinSeq(n,i);
end;
theorem :: EUCLID_7:31
for x0 being Element of REAL n holds x0 = Sum (ProjFinSeq x0);
definition
let n be Nat;
func RN_Base n -> Subset of REAL n equals
:: EUCLID_7:def 13
{ Base_FinSeq(n,i) where i is
Element of NAT: 1<=i & i<=n };
end;
theorem :: EUCLID_7:32
for n being non zero Nat holds RN_Base n <> {};
registration
cluster RN_Base 0 -> empty;
end;
registration
let n be non zero Nat;
cluster RN_Base n -> non empty;
end;
registration
let n;
cluster RN_Base n -> orthogonal_basis;
end;
registration
let n;
cluster orthogonal_basis for Subset of REAL n;
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;
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;
end;
registration
let n be Element of NAT;
cluster -> real-valued for Element of REAL-US n;
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;
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;
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;
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;
end;
theorem :: EUCLID_7:33
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);
theorem :: EUCLID_7:34
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;
registration
let A be set;
cluster RealVectSpace(A) -> constituted-Functions;
end;
registration
let n;
cluster RealVectSpace(Seg n) -> constituted-FinSeqs;
end;
registration
let A be set;
cluster -> real-valued for Element of RealVectSpace(A);
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;
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;
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;
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;
end;
theorem :: EUCLID_7:35
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;
theorem :: EUCLID_7:36
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;
theorem :: EUCLID_7:37
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;
theorem :: EUCLID_7:38
for u,v being Element of REAL n holds (Euclid_scalar n).(u,v) = |(u,v
)|;
theorem :: EUCLID_7:39
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);
registration
let n;
cluster R-orthonormal -> linearly-independent for
Subset of RealVectSpace(Seg n);
end;
registration
let n be Element of NAT;
cluster R-orthonormal -> linearly-independent for Subset of REAL-US n;
end;
theorem :: EUCLID_7:40
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;
begin :: 6. Finite Dimensionality of the Spaces
registration let n;
cluster RN_Base n -> finite;
end;
theorem :: EUCLID_7:41
card RN_Base n = n;
theorem :: EUCLID_7:42
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;
theorem :: EUCLID_7:43
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;
theorem :: EUCLID_7:44
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;
theorem :: EUCLID_7:45
for B being Subset of RealVectSpace(Seg n) st B=RN_Base n holds
B is Basis of RealVectSpace(Seg n);
registration
let n;
cluster RealVectSpace(Seg n) -> finite-dimensional;
end;
theorem :: EUCLID_7:46
dim (RealVectSpace(Seg n)) = n;
theorem :: EUCLID_7:47
for B being Subset of RealVectSpace(Seg n) st B is Basis of
RealVectSpace(Seg n) holds card B = n;
theorem :: EUCLID_7:48
{} is Basis of RealVectSpace(Seg 0);
theorem :: EUCLID_7:49
for n being Element of NAT holds RN_Base n is Basis of REAL-US n;
theorem :: EUCLID_7:50
for D being Orthogonal_Basis of n holds D is Basis of RealVectSpace(Seg n);
registration
let n be Element of NAT;
cluster REAL-US n -> finite-dimensional;
end;
theorem :: EUCLID_7:51
for n being Element of NAT holds dim (REAL-US n) = n;
theorem :: EUCLID_7:52
for B being Orthogonal_Basis of n holds card B = n;