:: 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 Association of Mizar Users
theorem :: EUCLID_7:1
theorem Th2: :: EUCLID_7:2
theorem Th4: :: EUCLID_7:3
theorem :: EUCLID_7:4
theorem Th6: :: EUCLID_7:5
theorem Th7: :: EUCLID_7:6
Lm1:
for n, m being Nat st n < m holds
ex k being Nat st m = (n + 1) + k
:: deftheorem Def2 defines increasing EUCLID_7:def 1 :
theorem Th9: :: EUCLID_7:7
theorem Th10: :: EUCLID_7:8
theorem Th11: :: EUCLID_7:9
theorem Th12: :: EUCLID_7:10
:: deftheorem defines (*) EUCLID_7:def 2 :
theorem Th13: :: EUCLID_7:11
theorem Th14: :: EUCLID_7:12
theorem :: EUCLID_7:13
theorem Th16: :: EUCLID_7:14
theorem Th17: :: EUCLID_7:15
:: deftheorem Def4 defines R-orthogonal EUCLID_7:def 3 :
theorem :: EUCLID_7:16
:: deftheorem Def5 defines R-normal EUCLID_7:def 4 :
theorem Th19: :: EUCLID_7:17
theorem Th20: :: EUCLID_7:18
:: deftheorem Def6 defines R-orthonormal EUCLID_7:def 5 :
:: deftheorem Def7 defines complete EUCLID_7:def 6 :
:: deftheorem Def8 defines orthogonal_basis EUCLID_7:def 7 :
theorem Th21: :: EUCLID_7:19
theorem :: EUCLID_7:20
:: deftheorem Def9 defines linear_manifold EUCLID_7:def 8 :
theorem Th23: :: EUCLID_7:21
:: deftheorem defines L_Span EUCLID_7:def 9 :
:: deftheorem Def11 defines Sum EUCLID_7:def 10 :
:: deftheorem Def12 defines accum EUCLID_7:def 11 :
theorem Th24: :: EUCLID_7:22
theorem Th25: :: EUCLID_7:23
theorem Th26: :: EUCLID_7:24
theorem Th27: :: EUCLID_7:25
theorem Th28: :: EUCLID_7:26
theorem Th29: :: EUCLID_7:27
theorem Th30: :: EUCLID_7:28
theorem Th31: :: EUCLID_7:29
theorem Th32: :: EUCLID_7:30
theorem Th33: :: EUCLID_7:31
theorem Th34: :: EUCLID_7:32
definition
let n be
Nat;
let x0 be
Element of
REAL n;
func ProjFinSeq x0 -> FinSequence of
REAL n means :
Def13:
:: 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 b1 being FinSequence of REAL n st
( len b1 = n & ( for i being Nat st 1 <= i & i <= n holds
b1 . i = |(x0,(Base_FinSeq n,i))| * (Base_FinSeq n,i) ) )
uniqueness
for b1, b2 being FinSequence of REAL n st len b1 = n & ( for i being Nat st 1 <= i & i <= n holds
b1 . i = |(x0,(Base_FinSeq n,i))| * (Base_FinSeq n,i) ) & len b2 = n & ( for i being Nat st 1 <= i & i <= n holds
b2 . i = |(x0,(Base_FinSeq n,i))| * (Base_FinSeq n,i) ) holds
b1 = b2
end;
:: deftheorem Def13 defines ProjFinSeq EUCLID_7:def 12 :
theorem Th35: :: EUCLID_7:33
:: deftheorem defines RN_Base EUCLID_7:def 13 :
theorem Th36: :: EUCLID_7:34
theorem Th37: :: EUCLID_7:35
theorem Th38: :: EUCLID_7:36
theorem Th39: :: EUCLID_7:37
:: deftheorem defines REAL-L EUCLID_7:def 14 :
theorem Th42: :: EUCLID_7:38
theorem Th43: :: EUCLID_7:39
theorem :: EUCLID_7:40
Lm2:
for n being Nat
for X being Subspace of REAL-L 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
theorem Th45: :: EUCLID_7:41
theorem Th46: :: EUCLID_7:42
theorem Th49: :: EUCLID_7:43
Lm3:
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
not
n is
empty
;
:: thesis: ( RN_Base n is finite & card (RN_Base n) = n )
then reconsider n =
n as non
empty Nat ;
defpred S1[
set ,
set ]
means for
i being
Element of
NAT st
i = $1 holds
$2
= Base_FinSeq n,
i;
A3:
for
x being
set st
x in Seg n holds
ex
y being
set st
S1[
x,
y]
consider f being
Function such that A4:
(
dom f = Seg n & ( for
x2 being
set st
x2 in Seg n holds
S1[
x2,
f . x2] ) )
from CLASSES1:sch 1(A3);
A7:
rng f c= RN_Base n
then reconsider f2 =
f as
Function of
Seg n,
RN_Base n by A4, 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 A10:
(
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 )
;
:: thesis: x1 = x2
then reconsider nx1 =
x1,
nx2 =
x2 as
Element of
NAT by A4;
A11:
( 1
<= nx1 &
nx1 <= n )
by A10, A4, FINSEQ_1:3;
A12:
( 1
<= nx2 &
nx2 <= n )
by A10, A4, FINSEQ_1:3;
A13:
f . x1 = Base_FinSeq n,
nx1
by A4, A10;
f . x2 = Base_FinSeq n,
nx2
by A4, A10;
hence
x1 = x2
by Th29, A13, A10, A11, A12;
:: thesis: verum
end;
then A14:
f2 is
one-to-one
by FUNCT_1:def 8;
RN_Base n c= rng f
then
rng f = RN_Base n
by A7, XBOOLE_0:def 10;
then
f2 is
onto
by FUNCT_2:def 3;
then
card (Seg n) = card (RN_Base n)
by A14, Th4;
hence
(
RN_Base n is
finite &
card (RN_Base n) = n )
by FINSEQ_1:78;
:: thesis: verum
end;
end;
end;
end;
theorem :: EUCLID_7:44
theorem Th51: :: EUCLID_7:45
theorem Th52: :: EUCLID_7:46
theorem Th53: :: EUCLID_7:47
theorem Th54: :: EUCLID_7:48
theorem :: EUCLID_7:49
theorem Th56: :: EUCLID_7:50
theorem Th57: :: EUCLID_7:51
theorem Th58: :: EUCLID_7:52
theorem Th59: :: EUCLID_7:53
theorem :: EUCLID_7:54
theorem :: EUCLID_7:55