:: 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-2011 Association of Mizar Users

begin

theorem :: EUCLID_7:1

for f, g being Function holds dom (f * g) = (dom g) /\ (g " (dom f))

proof end;

theorem Th2: :: EUCLID_7:2

for R being Relation
for Y being set st rng R c= Y holds
R " Y = dom R

proof end;

theorem :: EUCLID_7:3

canceled;

Lm1: for X being set
for Y being non empty set
for f being Function of X,Y st f is bijective holds
card X = card Y
by EULER_1:12;

theorem :: EUCLID_7:4

for z being set holds <*z*> * <*1*> = <*z*>

proof end;

theorem :: EUCLID_7:5

for x being Element of REAL 0 holds x = <*> REAL ;

theorem Th6: :: EUCLID_7:6

for n being Nat
for a, b, c being Element of REAL n holds ((a - b) + c) + b = a + c

proof end;

registration

let f1, f2 be FinSequence;
cluster <:f1,f2:> -> FinSequence-like ;
coherence
<:f1,f2:> is FinSequence-like

proof end;

end;

definition

let D be set ;
let f1, f2 be FinSequence of D;
:: original: <:
redefine func <:f1,f2:> -> FinSequence of [:D,D:];
coherence
<:f1,f2:> is FinSequence of [:D,D:]

proof end;

end;

Lm2: for n, m being Nat st n < m holds
ex k being Nat st m = (n + 1) + k

proof end;

definition

let h be real-valued FinSequence;
redefine attr h is increasing means :Def1: :: EUCLID_7:def 1
for i being Nat st 1 <= i & i < len h holds
h . i < h . (i + 1);
compatibility
( h is increasing iff for i being Nat st 1 <= i & i < len h holds
h . i < h . (i + 1) )

proof end;

end;

:: deftheorem Def1 defines increasing EUCLID_7:def 1 :
for h being real-valued FinSequence holds
( h is increasing iff for i being Nat st 1 <= i & i < len h holds
h . i < h . (i + 1) );

theorem Th7: :: EUCLID_7:7

for h being real-valued FinSequence st h is increasing holds
for i, j being Nat st i < j & 1 <= i & j <= len h holds
h . i < h . j

proof end;

theorem Th8: :: EUCLID_7:8

for h being real-valued FinSequence st h is increasing holds
for i, j being Nat st i <= j & 1 <= i & j <= len h holds
h . i <= h . j

proof end;

theorem Th9: :: EUCLID_7:9

for h being natural-valued FinSequence st h is increasing holds
for i being Nat st i <= len h & 1 <= h . 1 holds
i <= h . i

proof end;

theorem Th10: :: EUCLID_7:10

for V being RealLinearSpace
for X being Subspace of V st V is strict & X is strict & the carrier of X = the carrier of V holds
X = V

proof end;

definition

let D be set ;
let F be FinSequence of D;
let h be Permutation of (dom F);
func F (*) h -> FinSequence of D equals :: EUCLID_7:def 2
F * h;
coherence
F * h is FinSequence of D

proof end;

end;

:: deftheorem defines (*) EUCLID_7:def 2 :
for D being set
for F being FinSequence of D
for h being Permutation of (dom F) holds F (*) h = F * h;

theorem Th11: :: EUCLID_7:11

for i, j being Nat
for D being non empty set
for 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 end;

theorem Th12: :: EUCLID_7:12

{} is Permutation of {}

proof end;

theorem :: EUCLID_7:13

<*1*> is Permutation of {1}

proof end;

theorem Th14: :: EUCLID_7:14

for h being FinSequence of REAL holds
( h is one-to-one iff sort_a h is one-to-one )

proof end;

theorem Th15: :: EUCLID_7:15

for h being FinSequence of NAT st h is one-to-one holds
ex h3 being Permutation of (dom h) ex h2 being FinSequence of NAT st
( h2 = h * h3 & h2 is increasing & dom h = dom h2 & rng h = rng h2 )

proof end;

begin

definition

let B0 be set ;
attr B0 is R-orthogonal means :Def3: :: 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;

:: deftheorem Def3 defines R-orthogonal EUCLID_7:def 3 :
for B0 being set holds
( B0 is R-orthogonal iff for x, y being real-valued FinSequence st x in B0 & y in B0 & x <> y holds
|(x,y)| = 0 );

registration

cluster empty -> R-orthogonal set ;
coherence
for b₁ being set st b₁ is empty holds
b₁ is R-orthogonal

proof end;

end;

theorem :: EUCLID_7:16

for B0 being set holds
( 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 end;

definition

let B0 be set ;
attr B0 is R-normal means :Def4: :: EUCLID_7:def 4
for x being real-valued FinSequence st x in B0 holds
|.x.| = 1;

end;

:: deftheorem Def4 defines R-normal EUCLID_7:def 4 :
for B0 being set holds
( B0 is R-normal iff for x being real-valued FinSequence st x in B0 holds
|.x.| = 1 );

registration

cluster empty -> R-normal set ;
coherence
for b₁ being set st b₁ is empty holds
b₁ is R-normal

proof end;

end;

registration

cluster R-normal set ;
existence
ex b₁ being set st b₁ is R-normal

proof end;

end;

registration

let B0, B1 be R-normal set ;
cluster B0 \/ B1 -> R-normal ;
coherence
B0 \/ B1 is R-normal

proof end;

end;

theorem Th17: :: EUCLID_7:17

for f being real-valued FinSequence st |.f.| = 1 holds
{f} is R-normal

proof end;

theorem Th18: :: EUCLID_7:18

for B0 being set
for x0 being real-valued FinSequence st B0 is R-normal & |.x0.| = 1 holds
B0 \/ {x0} is R-normal

proof end;

definition

let B0 be set ;
attr B0 is R-orthonormal means :Def5: :: EUCLID_7:def 5
( B0 is R-orthogonal & B0 is R-normal );

end;

:: deftheorem Def5 defines R-orthonormal EUCLID_7:def 5 :
for B0 being set holds
( B0 is R-orthonormal iff ( B0 is R-orthogonal & B0 is R-normal ) );

registration

cluster R-orthonormal -> R-orthogonal R-normal set ;
coherence
for b₁ being set st b₁ is R-orthonormal holds
( b₁ is R-orthogonal & b₁ is R-normal ) by Def5;
cluster R-orthogonal R-normal -> R-orthonormal set ;
coherence
for b₁ being set st b₁ is R-orthogonal & b₁ is R-normal holds
b₁ is R-orthonormal by Def5;

end;

registration

cluster {<*1*>} -> R-orthonormal ;
coherence
{<*1*>} is R-orthonormal

proof end;

end;

registration

cluster non empty R-orthonormal set ;
existence
ex b₁ being set st
( b₁ is R-orthonormal & not b₁ is empty )

proof end;

end;

registration

let n be Nat;
cluster functional FinSequence-membered R-orthonormal Element of bool (REAL n);
existence
ex b₁ being Subset of (REAL n) st b₁ is R-orthonormal

proof end;

end;

definition

let n be Nat;
let B0 be Subset of (REAL n);
attr B0 is complete means :Def6: :: EUCLID_7:def 6
for B being R-orthonormal Subset of (REAL n) st B0 c= B holds
B = B0;

end;

:: deftheorem Def6 defines complete EUCLID_7:def 6 :
for n being Nat
for B0 being Subset of (REAL n) holds
( B0 is complete iff for B being R-orthonormal Subset of (REAL n) st B0 c= B holds
B = B0 );

definition

let n be Nat;
let B0 be Subset of (REAL n);
attr B0 is orthogonal_basis means :Def7: :: EUCLID_7:def 7
( B0 is R-orthonormal & B0 is complete );

end;

:: deftheorem Def7 defines orthogonal_basis EUCLID_7:def 7 :
for n being Nat
for B0 being Subset of (REAL n) holds
( B0 is orthogonal_basis iff ( B0 is R-orthonormal & B0 is complete ) );

registration

let n be Nat;
cluster orthogonal_basis -> R-orthonormal complete Element of bool (REAL n);
coherence
for b₁ being Subset of (REAL n) st b₁ is orthogonal_basis holds
( b₁ is R-orthonormal & b₁ is complete ) by Def7;
cluster R-orthonormal complete -> orthogonal_basis Element of bool (REAL n);
coherence
for b₁ being Subset of (REAL n) st b₁ is R-orthonormal & b₁ is complete holds
b₁ is orthogonal_basis by Def7;

end;

theorem Th19: :: EUCLID_7:19

for B0 being Subset of (REAL 0) st B0 is orthogonal_basis holds
B0 = {}

proof end;

theorem :: EUCLID_7:20

for n being Nat
for B0 being Subset of (REAL n)
for 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 end;

begin

definition

let n be Nat;
let X be Subset of (REAL n);
attr X is linear_manifold means :Def8: :: EUCLID_7:def 8
for x, y being Element of REAL n
for a, b being Element of REAL st x in X & y in X holds
(a * x) + (b * y) in X;

end;

:: deftheorem Def8 defines linear_manifold EUCLID_7:def 8 :
for n being Nat
for X being Subset of (REAL n) holds
( X is linear_manifold iff for x, y being Element of REAL n
for a, b being Element of REAL st x in X & y in X holds
(a * x) + (b * y) in X );

registration

let n be Nat;
cluster [#] (REAL n) -> linear_manifold ;
coherence
[#] (REAL n) is linear_manifold

proof end;

end;

theorem Th21: :: EUCLID_7:21

for n being Nat holds {(0* n)} is linear_manifold

proof end;

registration

let n be Nat;
cluster {(0* n)} -> linear_manifold Subset of (REAL n);
coherence
for b₁ being Subset of (REAL n) st b₁ = {(0* n)} holds
b₁ is linear_manifold by Th21;

end;

definition

let n be Nat;
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 ) } ;
correctness
coherence
meet { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } is Subset of (REAL n);

proof end;

end;

:: deftheorem defines L_Span EUCLID_7:def 9 :
for n being Nat
for X being Subset of (REAL n) holds L_Span X = meet { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } ;

registration

let n be Nat;
let X be Subset of (REAL n);
cluster L_Span X -> linear_manifold ;
coherence
L_Span X is linear_manifold

proof end;

end;

definition

let n be Nat;
let f be FinSequence of REAL n;
func accum f -> FinSequence of REAL n means :Def10: :: EUCLID_7:def 10
( len f = len it & f . 1 = it . 1 & ( for i being Nat st 1 <= i & i < len f holds
it . (i + 1) = (it /. i) + (f /. (i + 1)) ) );
existence
ex b₁ being FinSequence of REAL n st
( len f = len b₁ & f . 1 = b₁ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₁ . (i + 1) = (b₁ /. i) + (f /. (i + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of REAL n st len f = len b₁ & f . 1 = b₁ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₁ . (i + 1) = (b₁ /. i) + (f /. (i + 1)) ) & len f = len b₂ & f . 1 = b₂ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₂ . (i + 1) = (b₂ /. i) + (f /. (i + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines accum EUCLID_7:def 10 :
for n being Nat
for f, b₃ being FinSequence of REAL n holds
( b₃ = accum f iff ( len f = len b₃ & f . 1 = b₃ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₃ . (i + 1) = (b₃ /. i) + (f /. (i + 1)) ) ) );

definition

let n be Nat;
let f be FinSequence of REAL n;
func Sum f -> Element of REAL n equals :Def11: :: EUCLID_7:def 11
(accum f) . (len f) if len f > 0
otherwise 0* n;
coherence
( ( len f > 0 implies (accum f) . (len f) is Element of REAL n ) & ( not len f > 0 implies 0* n is Element of REAL n ) )

proof end;

consistency
for b₁ being Element of REAL n holds verum ;

end;

:: deftheorem Def11 defines Sum EUCLID_7:def 11 :
for n being Nat
for f being FinSequence of REAL n holds
( ( len f > 0 implies Sum f = (accum f) . (len f) ) & ( not len f > 0 implies Sum f = 0* n ) );

theorem :: EUCLID_7:22

canceled;

theorem Th23: :: EUCLID_7:23

for n being Nat
for F, F2 being FinSequence of REAL n
for h being Permutation of (dom F) st F2 = F (*) h holds
Sum F2 = Sum F

proof end;

theorem Th24: :: EUCLID_7:24

for n being Nat
for k being Element of NAT holds Sum (k |-> (0* n)) = 0* n

proof end;

theorem Th25: :: EUCLID_7:25

for n being Nat
for g being FinSequence of REAL n
for h being FinSequence of NAT
for 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 end;

theorem Th26: :: EUCLID_7:26

for n being Nat
for g being FinSequence of REAL n
for h being FinSequence of NAT
for 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 end;

begin

definition

let n, i be Nat;
:: original: Base_FinSeq
redefine func Base_FinSeq (n,i) -> Element of REAL n;
coherence
Base_FinSeq (n,i) is Element of REAL n

proof end;

end;

theorem Th27: :: EUCLID_7:27

for n, i1, i2 being Nat st 1 <= i1 & i1 <= n & Base_FinSeq (n,i1) = Base_FinSeq (n,i2) holds
i1 = i2

proof end;

theorem Th28: :: EUCLID_7:28

for n, i being Nat holds sqr (Base_FinSeq (n,i)) = Base_FinSeq (n,i)

proof end;

theorem Th29: :: EUCLID_7:29

for i, n being Nat st 1 <= i & i <= n holds
Sum (Base_FinSeq (n,i)) = 1

proof end;

theorem Th30: :: EUCLID_7:30

for i, n being Nat st 1 <= i & i <= n holds
|.(Base_FinSeq (n,i)).| = 1

proof end;

theorem Th31: :: EUCLID_7:31

for i, n, j being Nat st 1 <= i & i <= n & i <> j holds
|((Base_FinSeq (n,i)),(Base_FinSeq (n,j)))| = 0

proof end;

theorem Th32: :: EUCLID_7:32

for n, i being Nat
for x being Element of REAL n st 1 <= i & i <= n holds
|(x,(Base_FinSeq (n,i)))| = x . i

proof end;

definition

let n be Nat;
let x0 be Element of REAL n;
func ProjFinSeq x0 -> FinSequence of REAL n means :Def12: :: 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)) ) );
existence
ex b₁ being FinSequence of REAL n st
( len b₁ = n & ( for i being Nat st 1 <= i & i <= n holds
b₁ . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of REAL n st len b₁ = n & ( for i being Nat st 1 <= i & i <= n holds
b₁ . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) & len b₂ = n & ( for i being Nat st 1 <= i & i <= n holds
b₂ . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines ProjFinSeq EUCLID_7:def 12 :
for n being Nat
for x0 being Element of REAL n
for b₃ being FinSequence of REAL n holds
( b₃ = ProjFinSeq x0 iff ( len b₃ = n & ( for i being Nat st 1 <= i & i <= n holds
b₃ . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) ) );

theorem Th33: :: EUCLID_7:33

for n being Nat
for x0 being Element of REAL n holds x0 = Sum (ProjFinSeq x0)

proof end;

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 ) } ;
coherence
{ (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n ) } is Subset of (REAL n)

proof end;

end;

:: deftheorem defines RN_Base EUCLID_7:def 13 :
for n being Nat holds RN_Base n = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n ) } ;

theorem Th34: :: EUCLID_7:34

for n being non zero Nat holds RN_Base n <> {}

proof end;

registration

cluster RN_Base 0 -> empty ;
coherence
RN_Base 0 is empty

proof end;

end;

registration

let n be non zero Nat;
cluster RN_Base n -> non empty ;
coherence
not RN_Base n is empty by Th34;

end;

registration

let n be Nat;
cluster RN_Base n -> orthogonal_basis ;
coherence
RN_Base n is orthogonal_basis

proof end;

end;

registration

let n be Nat;
cluster functional FinSequence-membered orthogonal_basis Element of bool (REAL n);
existence
ex b₁ being Subset of (REAL n) st b₁ is orthogonal_basis

proof end;

end;

definition

let n be Nat;
mode Orthogonal_Basis of n is orthogonal_basis Subset of (REAL n);

end;

registration

let n be non zero Nat;
cluster orthogonal_basis -> non empty Element of bool (REAL n);
coherence
for b₁ being Orthogonal_Basis of n holds not b₁ is empty

proof end;

end;

begin

registration

let n be Element of NAT ;
cluster REAL-US n -> constituted-FinSeqs ;
coherence
REAL-US n is constituted-FinSeqs

proof end;

end;

registration

let n be Element of NAT ;
cluster -> real-valued Element of the carrier of (REAL-US n);
coherence
for b₁ being Element of (REAL-US n) holds b₁ is real-valued

proof end;

end;

registration

let n be Element of NAT ;
let x, y be VECTOR of (REAL-US n);
let a, b be real-valued Function;
identify x + y with a + b when x = a, y = b;
compatibility
( x = a & y = b implies x + y = a + b )

proof end;

end;

registration

let n be Element of NAT ;
let x be VECTOR of (REAL-US n);
let y be real-valued Function;
let a, b be Element of REAL ;
identify a * x with b * y when x = y, a = b;
compatibility
( x = y & a = b implies a * x = b * y )

proof end;

end;

registration

let n be Element of NAT ;
let x be VECTOR of (REAL-US n);
let a be real-valued Function;
identify - x with - a when x = a;
compatibility
( x = a implies - x = - a )

proof end;

end;

registration

let n be Element of NAT ;
let x, y be VECTOR of (REAL-US n);
let a, b be real-valued Function;
identify x - y with a - b when x = a, y = b;
compatibility
( x = a & y = b implies x - y = a - b ) ;

end;

theorem :: EUCLID_7:35

canceled;

theorem Th36: :: EUCLID_7:36

for n, j being Element of NAT
for F being FinSequence of the carrier of (REAL-US n)
for Bn being Subset of (REAL-US n)
for v0 being Element of (REAL-US n)
for 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 end;

theorem Th37: :: EUCLID_7:37

for n being Element of NAT
for f being FinSequence of REAL n
for g being FinSequence of the carrier of (REAL-US n) st f = g holds
Sum f = Sum g

proof end;

registration

let A be set ;
cluster RealVectSpace A -> constituted-Functions ;
coherence
RealVectSpace A is constituted-Functions

proof end;

end;

registration

let n be Nat;
cluster RealVectSpace (Seg n) -> constituted-FinSeqs ;
coherence
RealVectSpace (Seg n) is constituted-FinSeqs

proof end;

end;

registration

let A be set ;
cluster -> real-valued Element of the carrier of (RealVectSpace A);
coherence
for b₁ being Element of (RealVectSpace A) holds b₁ is real-valued

proof end;

end;

registration

let A be set ;
let x, y be VECTOR of (RealVectSpace A);
let a, b be real-valued Function;
identify x + y with a + b when x = a, y = b;
compatibility
( x = a & y = b implies x + y = a + b )

proof end;

end;

registration

let A be set ;
let x be VECTOR of (RealVectSpace A);
let y be real-valued Function;
let a, b be Element of REAL ;
identify a * x with b * y when x = y, a = b;
compatibility
( x = y & a = b implies a * x = b * y )

proof end;

end;

registration

let A be set ;
let x be VECTOR of (RealVectSpace A);
let a be real-valued Function;
identify - x with - a when x = a;
compatibility
( x = a implies - x = - a )

proof end;

end;

registration

let A be set ;
let x, y be VECTOR of (RealVectSpace A);
let a, b be real-valued Function;
identify x - y with a - b when x = a, y = b;
compatibility
( x = a & y = b implies x - y = a - b ) ;

end;

theorem Th38: :: EUCLID_7:38

for n being Nat
for X being Subspace of RealVectSpace (Seg n)
for x being Element of REAL n
for a being Real st x in the carrier of X holds
a * x in the carrier of X

proof end;

theorem Th39: :: EUCLID_7:39

for n being Nat
for X being Subspace of RealVectSpace (Seg n)
for 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 end;

theorem :: EUCLID_7:40

for n being Nat
for X being Subspace of RealVectSpace (Seg n)
for x, y being Element of REAL n
for 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 end;

Lm3: for n being Nat
for X being Subspace of RealVectSpace (Seg n)
for x, y being Element of REAL n
for 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 end;

theorem :: EUCLID_7:41

for n being Nat
for u, v being Element of REAL n holds (Euclid_scalar n) . (u,v) = |(u,v)| by REAL_NS1:def 5;

theorem Th42: :: EUCLID_7:42

for n, j being Nat
for F being FinSequence of the carrier of (RealVectSpace (Seg n))
for Bn being Subset of (RealVectSpace (Seg n))
for v0 being Element of (RealVectSpace (Seg n))
for 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 end;

registration

let n be Nat;
cluster R-orthonormal -> linearly-independent Element of bool the carrier of (RealVectSpace (Seg n));
coherence
for b₁ being Subset of (RealVectSpace (Seg n)) st b₁ is R-orthonormal holds
b₁ is linearly-independent

proof end;

end;

registration

let n be Element of NAT ;
cluster R-orthonormal -> linearly-independent Element of bool the carrier of (REAL-US n);
coherence
for b₁ being Subset of (REAL-US n) st b₁ is R-orthonormal holds
b₁ is linearly-independent

proof end;

end;

theorem Th43: :: EUCLID_7:43

for n being Nat
for Bn being Subset of (RealVectSpace (Seg n))
for x, y being Element of REAL n
for a being Real st Bn is linearly-independent & x in Bn & y in Bn & y = a * x holds
x = y

proof end;

Lm4: now

let n be Nat; :: thesis: ( RN_Base n is finite & card (RN_Base n) = n )
thus ( RN_Base n is finite & card (RN_Base n) = n ) :: thesis: verum

proof

per cases ( n is empty or not n is empty ) ;

suppose n is empty ; :: thesis: ( RN_Base n is finite & card (RN_Base n) = n )

hence ( RN_Base n is finite & card (RN_Base n) = n ) ; :: thesis: verum

end;

suppose not n is empty ; :: thesis: ( RN_Base n is finite & card (RN_Base n) = n )

then reconsider n = n as non empty Nat ;
defpred S₁[ set , set ] means for i being Element of NAT st i = $1 holds
$2 = Base_FinSeq (n,i);
A1: for x being set st x in Seg n holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in Seg n implies ex y being set st S₁[x,y] )
assume x in Seg n ; :: thesis: ex y being set st S₁[x,y]
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 set st S₁[x,y] ; :: thesis: verum

end;

consider f being Function such that
A2: ( dom f = Seg n & ( for x2 being set st x2 in Seg n holds
S₁[x2,f . x2] ) ) from CLASSES1:sch 1(A1);
A3: rng f c= RN_Base n

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in RN_Base n )
assume y in rng f ; :: thesis: y in RN_Base n
then consider x being set such that
A4: x in dom f and
A5: y = f . x by FUNCT_1:def 5;
reconsider nx = x as Element of NAT by A2, A4;
A6: nx <= n by A2, A4, FINSEQ_1:3;
A7: f . x = Base_FinSeq (n,nx) by A2, A4;
1 <= nx by A2, A4, FINSEQ_1:3;
hence y in RN_Base n by A5, A6, A7; :: thesis: verum

end;

then reconsider f2 = f as Function of (Seg n),(RN_Base n) by A2, FUNCT_2:4;
for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A8: x1 in dom f and
A9: x2 in dom f and
A10: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider nx1 = x1, nx2 = x2 as Element of NAT by A2, A8, A9;
A11: nx1 <= n by A2, A8, FINSEQ_1:3;
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:3;
hence x1 = x2 by A10, A11, A13, A12, Th27; :: thesis: verum

end;

then A14: f2 is one-to-one by FUNCT_1:def 8;
RN_Base n c= rng f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in RN_Base n or y in rng f )
assume y in RN_Base n ; :: thesis: y in rng f
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:3;
then f . i = Base_FinSeq (n,i) by A2;
hence y in rng f by A2, A15, A18, FUNCT_1:def 5; :: thesis: verum

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 ( RN_Base n is finite & card (RN_Base n) = n ) by FINSEQ_1:78; :: thesis: verum

end;

end;

end;

end;

begin

registration

let n be Nat;
cluster RN_Base n -> finite ;
coherence
RN_Base n is finite by Lm4;

end;

theorem :: EUCLID_7:44

for n being Nat holds card (RN_Base n) = n by Lm4;

theorem Th45: :: EUCLID_7:45

for n being Nat
for f being FinSequence of REAL n
for g being FinSequence of the carrier of (RealVectSpace (Seg n)) st f = g holds
Sum f = Sum g

proof end;

theorem Th46: :: EUCLID_7:46

for n being Nat
for x0 being Element of (RealVectSpace (Seg n))
for 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 end;

theorem Th47: :: EUCLID_7:47

for n being Element of NAT
for x0 being Element of (REAL-US n)
for 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 end;

theorem Th48: :: EUCLID_7:48

for n being Nat
for B being Subset of (RealVectSpace (Seg n)) st B = RN_Base n holds
B is Basis of RealVectSpace (Seg n)

proof end;

registration

let n be Nat;
cluster RealVectSpace (Seg n) -> finite-dimensional ;
coherence
RealVectSpace (Seg n) is finite-dimensional

proof end;

end;

theorem :: EUCLID_7:49

for n being Nat holds dim (RealVectSpace (Seg n)) = n

proof end;

theorem Th50: :: EUCLID_7:50

for n being Nat
for B being Subset of (RealVectSpace (Seg n)) st B is Basis of RealVectSpace (Seg n) holds
card B = n

proof end;

theorem Th51: :: EUCLID_7:51

{} is Basis of RealVectSpace (Seg 0)

proof end;

theorem Th52: :: EUCLID_7:52

for n being Element of NAT holds RN_Base n is Basis of REAL-US n

proof end;

theorem Th53: :: EUCLID_7:53

for n being Nat
for D being Orthogonal_Basis of n holds D is Basis of RealVectSpace (Seg n)

proof end;

registration

let n be Element of NAT ;
cluster REAL-US n -> finite-dimensional ;
coherence
REAL-US n is finite-dimensional

proof end;

end;

theorem :: EUCLID_7:54

for n being Element of NAT holds dim (REAL-US n) = n

proof end;

theorem :: EUCLID_7:55

for n being Nat
for B being Orthogonal_Basis of n holds card B = n

proof end;