:: by Yatsuka Nakamura , Artur Korni{\l}owicz , Nagato Oya and Yasunari Shidama

::

:: Received September 23, 2008

:: Copyright (c) 2008-2012 Association of Mizar Users

begin

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:11;

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:]

end;
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;

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;

( h is increasing iff for i being Nat st 1 <= i & i < len h holds

h . i < h . (i + 1) )

end;
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 for i being Nat st 1 <= i & i < len h holds

h . i < h . (i + 1);

( h is increasing iff for i being Nat st 1 <= i & i < len h holds

h . i < h . (i + 1) )

proof 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) );

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 Th6: :: EUCLID_7:6

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

for i, j being Nat st i < j & 1 <= i & j <= len h holds

h . i < h . j

proof end;

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

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 natural-valued FinSequence st h is increasing holds

for i being Nat st i <= len h & 1 <= h . 1 holds

i <= h . i

for i being Nat st i <= len h & 1 <= h . 1 holds

i <= h . i

proof end;

theorem Th9: :: EUCLID_7:9

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

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);

coherence

F * h is FinSequence of D

end;
let F be FinSequence of D;

let h be Permutation of (dom F);

coherence

F * h is FinSequence of D

proof 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;

for D being set

for F being FinSequence of D

for h being Permutation of (dom F) holds F (*) h = F * h;

theorem Th10: :: EUCLID_7:10

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 )

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 Th14: :: EUCLID_7:14

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 )

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 ;

end;
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 ;

for x, y being real-valued FinSequence st x in B0 & y in B0 & x <> y holds

|(x,y)| = 0 ;

:: 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 );

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
end;

theorem :: EUCLID_7:15

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 )

( 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 ;

end;
attr B0 is R-normal means :Def4: :: EUCLID_7:def 4

for x being real-valued FinSequence st x in B0 holds

|.x.| = 1;

for x being real-valued FinSequence st x in B0 holds

|.x.| = 1;

:: 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 );

for B0 being set holds

( B0 is R-normal iff for x being real-valued FinSequence st x in B0 holds

|.x.| = 1 );

registration
end;

registration
end;

theorem Th17: :: EUCLID_7:17

for B0 being set

for x0 being real-valued FinSequence st B0 is R-normal & |.x0.| = 1 holds

B0 \/ {x0} is R-normal

for x0 being real-valued FinSequence st B0 is R-normal & |.x0.| = 1 holds

B0 \/ {x0} is R-normal

proof 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 ) );

for B0 being set holds

( B0 is R-orthonormal iff ( B0 is R-orthogonal & B0 is R-normal ) );

registration

coherence

for b_{1} being set st b_{1} is R-orthonormal holds

( b_{1} is R-orthogonal & b_{1} is R-normal )
by Def5;

coherence

for b_{1} being set st b_{1} is R-orthogonal & b_{1} is R-normal holds

b_{1} is R-orthonormal
by Def5;

end;
for b

( b

coherence

for b

b

registration
end;

registration
end;

definition

let n be Nat;

let B0 be Subset of (REAL n);

end;
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;

for B being R-orthonormal Subset of (REAL n) st B0 c= B holds

B = B0;

:: 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 );

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 );

:: 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 ) );

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;

coherence

for b_{1} being Subset of (REAL n) st b_{1} is orthogonal_basis holds

( b_{1} is R-orthonormal & b_{1} is complete )
by Def7;

coherence

for b_{1} being Subset of (REAL n) st b_{1} is R-orthonormal & b_{1} is complete holds

b_{1} is orthogonal_basis
by Def7;

end;
coherence

for b

( b

coherence

for b

b

theorem :: EUCLID_7:19

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

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

:: 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 );

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;

coherence

for b_{1} being Subset of (REAL n) st b_{1} = {(0* n)} holds

b_{1} is linear_manifold
by Th20;

end;
coherence

for b

b

definition

let n be Nat;

let X be Subset of (REAL n);

coherence

meet { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } is Subset of (REAL n);

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

coherence

meet { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } is Subset of (REAL n);

proof 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 ) } ;

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
end;

definition

let n be Nat;

let f be FinSequence of REAL n;

ex b_{1} being FinSequence of REAL n st

( len f = len b_{1} & f . 1 = b_{1} . 1 & ( for i being Nat st 1 <= i & i < len f holds

b_{1} . (i + 1) = (b_{1} /. i) + (f /. (i + 1)) ) )

for b_{1}, b_{2} being FinSequence of REAL n st len f = len b_{1} & f . 1 = b_{1} . 1 & ( for i being Nat st 1 <= i & i < len f holds

b_{1} . (i + 1) = (b_{1} /. i) + (f /. (i + 1)) ) & len f = len b_{2} & f . 1 = b_{2} . 1 & ( for i being Nat st 1 <= i & i < len f holds

b_{2} . (i + 1) = (b_{2} /. i) + (f /. (i + 1)) ) holds

b_{1} = b_{2}

end;
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 ( 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)) ) );

ex b

( len f = len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def10 defines accum EUCLID_7:def 10 :

for n being Nat

for f, b_{3} being FinSequence of REAL n holds

( b_{3} = accum f iff ( len f = len b_{3} & f . 1 = b_{3} . 1 & ( for i being Nat st 1 <= i & i < len f holds

b_{3} . (i + 1) = (b_{3} /. i) + (f /. (i + 1)) ) ) );

for n being Nat

for f, b

( b

b

definition

let n be Nat;

let f be FinSequence of REAL n;

( ( 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 ) )

for b_{1} being Element of REAL n holds verum
;

end;
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 (accum f) . (len f) if len f > 0

otherwise 0* n;

( ( 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

:: 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 ) );

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 Th21: :: EUCLID_7:21

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

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 Th23: :: EUCLID_7:23

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

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 Th24: :: EUCLID_7:24

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

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

end;
:: 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;

theorem Th25: :: EUCLID_7:25

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

i1 = i2

i1 = i2

proof end;

theorem Th29: :: EUCLID_7:29

for i, n, j being Nat st 1 <= i & i <= n & i <> j holds

|((Base_FinSeq (n,i)),(Base_FinSeq (n,j)))| = 0

|((Base_FinSeq (n,i)),(Base_FinSeq (n,j)))| = 0

proof end;

theorem Th30: :: EUCLID_7:30

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

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;

ex b_{1} being FinSequence of REAL n st

( len b_{1} = n & ( for i being Nat st 1 <= i & i <= n holds

b_{1} . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) )

for b_{1}, b_{2} being FinSequence of REAL n st len b_{1} = n & ( for i being Nat st 1 <= i & i <= n holds

b_{1} . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) & len b_{2} = n & ( for i being Nat st 1 <= i & i <= n holds

b_{2} . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) holds

b_{1} = b_{2}

end;
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 ( len it = n & ( for i being Nat st 1 <= i & i <= n holds

it . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def12 defines ProjFinSeq EUCLID_7:def 12 :

for n being Nat

for x0 being Element of REAL n

for b_{3} being FinSequence of REAL n holds

( b_{3} = ProjFinSeq x0 iff ( len b_{3} = n & ( for i being Nat st 1 <= i & i <= n holds

b_{3} . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) ) );

for n being Nat

for x0 being Element of REAL n

for b

( b

b

definition

let n be Nat;

{ (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n ) } is Subset of (REAL n)

end;
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 ) } ;

{ (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n ) } is Subset of (REAL n)

proof 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 ) } ;

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

registration
end;

registration
end;

registration

let n be non zero Nat;

coherence

for b_{1} being Orthogonal_Basis of n holds not b_{1} is empty

end;
coherence

for b

proof end;

begin

registration

let n be Element of NAT ;

coherence

for b_{1} being Element of (REAL-US n) holds b_{1} is real-valued

end;
coherence

for b

proof end;

registration

let n be Element of NAT ;

let x, y be VECTOR of (REAL-US n);

let a, b be real-valued Function;

compatibility

( x = a & y = b implies x + y = a + b )

end;
let x, y be VECTOR of (REAL-US n);

let a, b be real-valued Function;

compatibility

( x = a & y = b implies x + y = a + b )

proof 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 ;

compatibility

( x = y & a = b implies a * x = b * y )

end;
let x be VECTOR of (REAL-US n);

let y be real-valued Function;

let a, b be Element of REAL ;

compatibility

( x = y & a = b implies a * x = b * y )

proof end;

registration

let n be Element of NAT ;

let x be VECTOR of (REAL-US n);

let a be real-valued Function;

compatibility

( x = a implies - x = - a )

end;
let x be VECTOR of (REAL-US n);

let a be real-valued Function;

compatibility

( x = a implies - x = - a )

proof end;

registration

let n be Element of NAT ;

let x, y be VECTOR of (REAL-US n);

let a, b be real-valued Function;

compatibility

( x = a & y = b implies x - y = a - b ) ;

end;
let x, y be VECTOR of (REAL-US n);

let a, b be real-valued Function;

compatibility

( x = a & y = b implies x - y = a - b ) ;

theorem Th33: :: EUCLID_7:33

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))

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 Th34: :: EUCLID_7:34

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

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 ;

coherence

for b_{1} being Element of (RealVectSpace A) holds b_{1} is real-valued

end;
coherence

for b

proof end;

registration

let A be set ;

let x, y be VECTOR of (RealVectSpace A);

let a, b be real-valued Function;

compatibility

( x = a & y = b implies x + y = a + b )

end;
let x, y be VECTOR of (RealVectSpace A);

let a, b be real-valued Function;

compatibility

( x = a & y = b implies x + y = a + b )

proof 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 ;

compatibility

( x = y & a = b implies a * x = b * y )

end;
let x be VECTOR of (RealVectSpace A);

let y be real-valued Function;

let a, b be Element of REAL ;

compatibility

( x = y & a = b implies a * x = b * y )

proof end;

registration

let A be set ;

let x be VECTOR of (RealVectSpace A);

let a be real-valued Function;

compatibility

( x = a implies - x = - a )

end;
let x be VECTOR of (RealVectSpace A);

let a be real-valued Function;

compatibility

( x = a implies - x = - a )

proof end;

registration

let A be set ;

let x, y be VECTOR of (RealVectSpace A);

let a, b be real-valued Function;

compatibility

( x = a & y = b implies x - y = a - b ) ;

end;
let x, y be VECTOR of (RealVectSpace A);

let a, b be real-valued Function;

compatibility

( x = a & y = b implies x - y = a - b ) ;

theorem Th35: :: EUCLID_7:35

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

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 Th36: :: EUCLID_7:36

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

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:37

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

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:38

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;

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

theorem Th39: :: EUCLID_7:39

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))

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;

for b_{1} being Subset of (RealVectSpace (Seg n)) st b_{1} is R-orthonormal holds

b_{1} is linearly-independent

end;
cluster R-orthonormal -> linearly-independent for Element of bool the carrier of (RealVectSpace (Seg n));

coherence for b

b

proof end;

registration

let n be Element of NAT ;

coherence

for b_{1} being Subset of (REAL-US n) st b_{1} is R-orthonormal holds

b_{1} is linearly-independent

end;
coherence

for b

b

proof end;

theorem Th40: :: EUCLID_7:40

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

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 :: thesis: for n being Nat holds

( RN_Base n is finite & card (RN_Base n) = n )

( RN_Base n is finite & card (RN_Base n) = n )

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

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

proof
end;

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

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_{1}[ 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_{1}[x,y]

A2: ( dom f = Seg n & ( for x2 being set st x2 in Seg n holds

S_{1}[x2,f . x2] ) )
from CLASSES1:sch 1(A1);

A3: rng f c= RN_Base n

for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2

RN_Base n c= rng f

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:57; :: thesis: verum

end;
defpred S

$2 = Base_FinSeq (n,i);

A1: for x being set st x in Seg n holds

ex y being set st S

proof

consider f being Function such that
let x be set ; :: thesis: ( x in Seg n implies ex y being set st S_{1}[x,y] )

assume x in Seg n ; :: thesis: ex y being set st S_{1}[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_{1}[x,y]
; :: thesis: verum

end;
assume x in Seg n ; :: thesis: ex y being set st S

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

A2: ( dom f = Seg n & ( for x2 being set st x2 in Seg n holds

S

A3: rng f c= RN_Base n

proof

then reconsider f2 = f as Function of (Seg n),(RN_Base n) by A2, FUNCT_2:2;
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 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; :: thesis: verum

end;
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 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; :: thesis: verum

for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2

proof

then A14:
f2 is one-to-one
by FUNCT_1:def 4;
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: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, Th25; :: thesis: verum

end;
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: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, Th25; :: thesis: verum

RN_Base n c= rng f

proof

then
rng f = RN_Base n
by A3, XBOOLE_0:def 10;
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:1;

then f . i = Base_FinSeq (n,i) by A2;

hence y in rng f by A2, A15, A18, FUNCT_1:def 3; :: thesis: verum

end;
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:1;

then f . i = Base_FinSeq (n,i) by A2;

hence y in rng f by A2, A15, A18, FUNCT_1:def 3; :: thesis: verum

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:57; :: thesis: verum

begin

theorem Th42: :: EUCLID_7:42

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

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 Th43: :: EUCLID_7:43

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

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 Th44: :: EUCLID_7:44

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

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 Th45: :: EUCLID_7:45

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)

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

B is Basis of RealVectSpace (Seg n)

proof end;

theorem Th47: :: EUCLID_7:47

for n being Nat

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

card B = n

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

card B = n

proof end;