:: Real Vector Space and Related Notions
:: by Kazuhisa Nakasho , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received June 30, 2021
:: Copyright (c) 2021-2026 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 ALGSTR_0, ARYTM_1, ARYTM_3, CARD_1, CARD_3, CLASSES1, EUCLID,
FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FUNCT_1, FUNCT_2, MATRIX_1,
MATRIX13, MATRLIN, MATRLIN2, MESFUNC1, NAT_1, NUMBERS, PARTFUN1,
PRE_TOPC, PRVECT_1, RANKNULL, RELAT_1, RLAFFIN1, RLSUB_1, RLVECT_1,
RLVECT_2, RLVECT_3, RLVECT_5, SEMI_AF1, STRUCT_0, SUBSET_1, SUPINF_2,
TARSKI, VALUED_0, VALUED_1, VECTSP_1, XBOOLE_0, XXREAL_0, REAL_NS1,
FUNCSDOM, FUNCOP_1, ZFMISC_1, REAL_1, NORMSP_2, PCOMPS_1, METRIC_1,
RUSUB_4, MATRIX_6, SETFAM_1, BINOP_2, MSSUBFAM, UNIALG_1, COMPLEX1,
NORMSP_1, REALSET1, MATRIXR1, MATRIXR2, LOPBAN_1, DUALSP01;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, REALSET1, FINSET_1, CARD_1,
ORDINAL1,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, VALUED_0, BINOP_2, FINSEQ_1,
FINSEQ_2, FINSEQOP, RVSUM_1, MATRIX_0, STRUCT_0, ALGSTR_0, PRE_TOPC,
RLVECT_1, RLSUB_1, VECTSP_1, FUNCSDOM, RLVECT_2, METRIC_1, RLVECT_3,
VECTSP_4, NORMSP_0, NORMSP_1, VECTSP_6, VECTSP_7, MATRIX_1, FVSUM_1,
MATRLIN, PCOMPS_1, RLVECT_5, RUSUB_4, EUCLID, LOPBAN_1, VECTSP_9,
RANKNULL, PRVECT_1, MATRIXR1, RLAFFIN1, MATRIX_6, MATRIXR2, MATRIX13,
MATRLIN2, REAL_NS1, NORMSP_2, MATRTOP1, DUALSP01;
constructors FVSUM_1, MATRIX_6, MATRIX13, MATRLIN2, MATRTOP1, MONOID_0,
RANKNULL, REALSET1, RELSET_1, RLAFFIN1, RLVECT_3, RUSUB_5, VECTSP10,
PCOMPS_1, BINOP_2, REAL_NS1, RLVECT_5, REAL_1, VECTSP_9, NORMSP_2,
MATRIXR2, LOPBAN_1, DUALSP01, FINSOP_1, FINSEQOP, MATRIX_3;
registrations CARD_1, EUCLID, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_1, FUNCT_2,
MATRIX13, MATRLIN, MEMBERED, MONOID_0, NAT_1, NUMBERS, PRVECT_1, RELAT_1,
RELSET_1, RLAFFIN1, RLVECT_3, RVSUM_1, STRUCT_0, VALUED_0, VECTSP_1,
XREAL_0, ORDINAL1, REAL_NS1, RLVECT_5, RUSUB_4, XBOOLE_0, RLAFFIN3,
MATRIX_3;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0, VECTSP_1;
equalities EUCLID, STRUCT_0, RUSUB_4, BINOP_1, VECTSP_1, RLVECT_1, FUNCSDOM,
MATRIXR1, MATRIXR2, REALSET1, NORMSP_2, ALGSTR_0, FVSUM_1, DUALSP01;
expansions STRUCT_0, LOPBAN_1, MATRLIN, VECTSP_1;
theorems CARD_1, EUCLID, FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCT_1, FUNCT_2,
NORMSP_2, PRVECT_1, RUSUB_4, SETFAM_1, BINOP_2, MOD_2, MATRIX_6,
MATRIX13, MATRIXR2, MATRLIN, MATRLIN2, FINSEQOP, NAT_1, PARTFUN1,
RLAFFIN1, RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_5, TARSKI,
VECTSP_1, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, XREAL_0, ZFMISC_1,
MATRTOP2, FUNCOP_1, FUNCSDOM, REAL_NS1, BINOP_1, VECTSP12, ZMODUL06,
LOPBAN_1;
schemes FUNCT_2, NAT_1;
begin :: Common properties between norm and topology
:: in finite dimensional linear spaces
reserve X for set,
n,m,k for Nat,
K for Field,
f for n-element real-valued FinSequence,
M for Matrix of n,m,F_Real;
theorem Th1:
the RLSStruct of TOP-REAL n = the RLSStruct of REAL-NS n
proof
set V = the RLSStruct of TOP-REAL n;
set W = the RLSStruct of REAL-NS n;
A1: the carrier of W
= REAL n by REAL_NS1:def 4
.= the carrier of V by EUCLID:22;
A2: RLSStruct(# the carrier of (TOP-REAL n),
the ZeroF of (TOP-REAL n),
the addF of (TOP-REAL n),
the Mult of (TOP-REAL n) #)
= RealVectSpace Seg n by EUCLID:def 8;
A3: the ZeroF of W
= 0.(REAL-NS n)
.= 0* n by REAL_NS1:def 4
.= 0.(RealVectSpace Seg n) by FINSEQ_2:def 2
.= the ZeroF of V by EUCLID:def 8;
A4: Funcs(Seg n,REAL) = REAL n by FINSEQ_2:93;
for x,y be Element of REAL n
holds (Euclid_add n).(x,y) = (RealFuncAdd Seg n).(x,y)
proof
let x,y be Element of REAL n;
reconsider x1 = x, y1 = y as Point of TOP-REAL n by A1,REAL_NS1:def 4;
thus (Euclid_add n).(x,y) = x1 + y1 by REAL_NS1:def 1
.= (RealFuncAdd Seg n).(x,y) by A2;
end; then
Euclid_add n = RealFuncAdd Seg n by A4,BINOP_1:2; then
A5: the addF of W
= the addF of RealVectSpace Seg n by REAL_NS1:def 4
.= the addF of V by EUCLID:def 8;
for x be Element of REAL, y be Element of REAL n holds
(Euclid_mult n).(x,y) = (RealFuncExtMult Seg n).(x,y)
proof
let x be Element of REAL,
y be Element of REAL n;
reconsider y1 = y as Point of TOP-REAL n by A1,REAL_NS1:def 4;
reconsider x1 = x as Real;
reconsider y2 = y as VECTOR of REAL-NS n by REAL_NS1:def 4;
thus (Euclid_mult n). (x,y)
= x1 * y2 by REAL_NS1:def 4
.= x1 * y1 by REAL_NS1:3
.= (RealFuncExtMult Seg n).(x,y) by A2;
end; then
Euclid_mult n = RealFuncExtMult Seg n by A4,BINOP_1:2; then
the Mult of W
= the Mult of RealVectSpace Seg n by REAL_NS1:def 4
.= the Mult of V by EUCLID:def 8;
hence thesis by A1,A3,A5;
end;
Lm1:
for n be Nat holds
the carrier of (n -VectSp_over F_Real) = the carrier of TOP-REAL n
proof
let n be Nat;
thus the carrier of (n -VectSp_over F_Real)
= REAL n by MATRIX13:102
.= the carrier of TOP-REAL n by EUCLID:22;
end;
theorem Th2:
Euclid n = MetricSpaceNorm REAL-NS n
proof
set X = REAL-NS n;
A1: the carrier of Euclid n
= the carrier of X by REAL_NS1:def 4;
for x,y be Element of REAL n holds
(the distance of Euclid n).(x,y)
= (distance_by_norm_of X).(x,y)
proof
let x,y be Element of REAL n;
reconsider x1=x, y1=y as Point of REAL-NS n by REAL_NS1:def 4;
thus (the distance of Euclid n).(x,y)
= |. x-y .| by EUCLID:def 6
.= ||. x1-y1 .|| by REAL_NS1:1,5
.= (distance_by_norm_of X).(x,y) by NORMSP_2:def 1;
end;
hence thesis by BINOP_1:2,A1;
end;
theorem
the TopStruct of TOP-REAL n = TopSpaceNorm REAL-NS n
proof
thus the TopStruct of TOP-REAL n
= TopSpaceMetr(Euclid n) by EUCLID:def 8
.= TopSpaceNorm(REAL-NS n) by Th2;
end;
theorem Th4:
the carrier of TOP-REAL n = the carrier of REAL-NS n
proof
thus the carrier of TOP-REAL n
= the carrier of the RLSStruct of (TOP-REAL n)
.= the carrier of the RLSStruct of REAL-NS n by Th1
.= the carrier of REAL-NS n;
end;
Lm2:
the carrier of (n -VectSp_over F_Real) = the carrier of TOP-REAL n
proof
thus the carrier of (n -VectSp_over F_Real)
= REAL n by MATRIX13:102
.= the carrier of (TOP-REAL n) by EUCLID:22;
end;
theorem Th5:
the carrier of (n -VectSp_over F_Real) = the carrier of REAL-NS n
proof
thus the carrier of (n -VectSp_over F_Real)
= the carrier of TOP-REAL n by Lm2
.= the carrier of REAL-NS n by Th4;
end;
theorem Th6:
0.(TOP-REAL n) = 0.(REAL-NS n)
proof
thus 0.(TOP-REAL n)
= 0.(the RLSStruct of TOP-REAL n)
.= 0.(the RLSStruct of REAL-NS n) by Th1
.= 0.(REAL-NS n);
end;
theorem Th7:
for p,q be Element of TOP-REAL n,
f,g be Element of REAL-NS n
st p=f & q=g
holds p+q = f+g
proof
let p,q be Element of TOP-REAL n,
f,g be Element of REAL-NS n;
assume
A1: p=f & q=g;
thus p+q
= (the addF of (the RLSStruct of TOP-REAL n)).(p,q)
.= (the addF of (the RLSStruct of REAL-NS n)).(p,q) by Th1
.= f+g by A1;
end;
theorem Th8:
for r be Real,
q be Element of TOP-REAL n,
g be Element of REAL-NS n
st q = g
holds r*q = r*g
proof
let r be Real,
q be Element of TOP-REAL n,
g be Element of REAL-NS n;
assume
A1: q = g;
thus r*q
= (the Mult of (the RLSStruct of TOP-REAL n)).(r,q)
.= (the Mult of (the RLSStruct of REAL-NS n)).(r,q) by Th1
.= r*g by A1;
end;
theorem Th9:
for q be Element of TOP-REAL n,
g be Element of REAL-NS n
st q = g
holds -q = -g
proof
let q be Element of TOP-REAL n,
g be Element of REAL-NS n;
assume
A1: q = g;
thus -q = (-1)*q by RLVECT_1:16
.= (-1)*g by A1,Th8
.= -g by RLVECT_1:16;
end;
theorem
for p,q be Element of TOP-REAL n,
f,g be Element of REAL-NS n
st p = f & q = g
holds p-q = f-g
proof
let p,q be Element of TOP-REAL n,
f,g be Element of REAL-NS n;
assume
A1: p=f & q=g; then
-q = -g by Th9;
hence p-q = f-g by A1,Th7;
end;
theorem Th11:
for X be set
for n be Nat
holds
X is Linear_Combination of REAL-NS n
iff
X is Linear_Combination of TOP-REAL n
proof
let X be set;
let n be Nat;
A1: the carrier of TOP-REAL n
= the carrier of REAL-NS n by Th4;
hereby
assume X is Linear_Combination of REAL-NS n; then
reconsider Lr = X as Linear_Combination of REAL-NS n;
consider T be finite Subset of REAL-NS n such that
A2: for v be Element of REAL-NS n st not v in T holds
Lr.v = 0 by RLVECT_2:def 3;
thus X is Linear_Combination of TOP-REAL n by A1,A2,RLVECT_2:def 3;
end;
assume X is Linear_Combination of TOP-REAL n; then
reconsider Lr = X as Linear_Combination of TOP-REAL n;
consider T be finite Subset of TOP-REAL n such that
A3: for v be Element of TOP-REAL n st not v in T holds
Lr.v = 0 by RLVECT_2:def 3;
thus X is Linear_Combination of REAL-NS n by A1,A3,RLVECT_2:def 3;
end;
theorem
for X be set
for n be Nat holds
X is Linear_Combination of REAL-NS n
iff
X is Linear_Combination of n-VectSp_over F_Real
proof
let X be set;
let n be Nat;
X is Linear_Combination of REAL-NS n
iff X is Linear_Combination of TOP-REAL n by Th11;
hence thesis by MATRTOP2:1;
end;
theorem
for Lv be Linear_Combination of TOP-REAL n,
Lr be Linear_Combination of REAL-NS n
st Lr = Lv
holds Carrier Lr = Carrier Lv;
theorem
for Lv be Linear_Combination of n-VectSp_over F_Real,
Lr be Linear_Combination of REAL-NS n
st Lr = Lv
holds Carrier Lr = Carrier Lv
proof
let Lv be Linear_Combination of n-VectSp_over F_Real,
Lr be Linear_Combination of REAL-NS n;
assume
A1: Lr = Lv;
reconsider Lr1 = Lr as Linear_Combination of TOP-REAL n by Th11;
Carrier Lr1 = Carrier Lv by A1, MATRTOP2:2;
hence thesis;
end;
theorem
for F be set
holds
F is Subset of TOP-REAL n
iff
F is Subset of REAL-NS n by Th4;
theorem
for F be set
holds
F is Subset of REAL-NS n
iff
F is Subset of n-VectSp_over F_Real by Th5;
theorem
for F be set
holds
F is FinSequence of TOP-REAL n
iff
F is FinSequence of REAL-NS n by Th4;
theorem Th18:
for F be set
holds
F is Function of TOP-REAL n, REAL
iff
F is Function of REAL-NS n, REAL
proof
let F be set;
the carrier of TOP-REAL n = the carrier of REAL-NS n by Th4;
hence thesis;
end;
theorem Th19:
for Fr be FinSequence of TOP-REAL n,
fr be Function of TOP-REAL n,REAL,
Fv be FinSequence of REAL-NS n,
fv be Function of REAL-NS n,REAL
st fr = fv & Fr = Fv
holds fr(#)Fr = fv(#)Fv
proof
let Fr be FinSequence of TOP-REAL n,
fr be Function of TOP-REAL n,REAL,
Fv be FinSequence of REAL-NS n,
fv be Function of REAL-NS n,REAL;
assume
A1: fr = fv & Fr = Fv; then
A2: len(fv(#)Fv) = len Fr by RLVECT_2:def 7;
A3: fv(#)Fv is FinSequence of TOP-REAL n by Th4;
for i be Nat st i in dom (fv(#)Fv) holds
(fv(#)Fv).i = (fr.(Fr /. i)) * (Fr /. i)
proof
let i be Nat;
assume
A4: i in dom (fv(#)Fv);
A5: Fv /. i = Fr /. i by A1,Th4;
thus (fv(#)Fv).i = (fv . (Fv /. i)) * (Fv /. i) by A4,RLVECT_2:def 7
.= (fr . (Fr /. i)) * (Fr /. i) by A1,A5,Th8;
end;
hence thesis by A2,A3,RLVECT_2:def 7;
end;
theorem
for F be FinSequence of REAL-NS n,
fr be Function of REAL-NS n,REAL,
Fv be FinSequence of n-VectSp_over F_Real,
fv be Function of n-VectSp_over F_Real,F_Real
st fr = fv & F = Fv
holds fr(#)F = fv(#)Fv
proof
let F be FinSequence of REAL-NS n,
fr be Function of REAL-NS n,REAL,
Fv be FinSequence of n-VectSp_over F_Real,
fv be Function of n-VectSp_over F_Real,F_Real;
assume
A1: fr = fv & F = Fv;
reconsider fr1 = fr as Function of TOP-REAL n,REAL by Th18;
reconsider F1 = F as FinSequence of TOP-REAL n by Th4;
fr1(#)F1 = fr(#)F by Th19;
hence thesis by A1,MATRTOP2:3;
end;
theorem Th21:
for Ft be FinSequence of TOP-REAL n,
Fr be FinSequence of REAL-NS n
st Ft = Fr
holds Sum Ft = Sum Fr
proof
let F be FinSequence of TOP-REAL n,
Fv be FinSequence of REAL-NS n;
assume
A1: F = Fv;
set T = TOP-REAL n;
set V = REAL-NS n;
consider f be sequence of the carrier of T such that
A2: Sum F = f.(len F) and
A3: f.0 = 0.T and
A4: for j be Nat
for v be Element of T
st j < len F & v = F.(j + 1)
holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
consider fv be sequence of the carrier of V such that
A5: Sum Fv = fv.(len Fv) and
A6: fv.0 = 0.V and
A7: for j be Nat
for v be Element of V
st j < len Fv & v = Fv.(j + 1)
holds fv.(j + 1) = fv.j + v by RLVECT_1:def 12;
defpred S1[ Nat] means
($1 <= len F implies f.$1 = fv.$1);
A8: for i be Nat st S1[i] holds S1[i + 1]
proof
let i be Nat;
assume
A9: S1[i];
assume
A10: i + 1 <= len F; then
A11: i + 1 in dom F by NAT_1:11,FINSEQ_3:25;
then F.(i + 1) = F /. (i + 1) by PARTFUN1:def 6;
then
A12: f.(i + 1) = f.i + F /. (i + 1) by A4, A10,NAT_1:13;
A13: Fv /. (i + 1) = Fv.(i + 1) by A1,A11,PARTFUN1:def 6;
then Fv /. (i + 1) = F /. (i + 1) by A1,A11,PARTFUN1:def 6;
hence f.(i + 1)
= fv.i + Fv /. (i + 1) by A9,A10,A12,Th7,NAT_1:13
.= fv.(i + 1) by A1,A7,A10,A13,NAT_1:13;
end;
A14: S1[ 0 ] by A3,A6,Th6;
for n be Nat holds S1[n] from NAT_1:sch 2(A14, A8);
hence Sum F = Sum Fv by A1,A2,A5;
end;
theorem
for F be FinSequence of REAL-NS n,
Fv be FinSequence of n-VectSp_over F_Real
st Fv = F
holds Sum F = Sum Fv
proof
let F be FinSequence of REAL-NS n,
Fv be FinSequence of n-VectSp_over F_Real;
assume
A1: Fv = F;
reconsider Ft = F as FinSequence of TOP-REAL n by Th4;
Sum F = Sum Ft by Th21;
hence thesis by A1,MATRTOP2:4;
end;
theorem Th23:
for Lr be Linear_Combination of REAL-NS n,
Lt be Linear_Combination of TOP-REAL n st Lr = Lt
holds Sum Lr = Sum Lt
proof
let Lr be Linear_Combination of REAL-NS n,
Lt be Linear_Combination of TOP-REAL n;
assume
A1: Lr = Lt;
set R = REAL-NS n;
set T = TOP-REAL n;
consider Ft be FinSequence of the carrier of (TOP-REAL n) such that
A2: (Ft is one-to-one & rng Ft = Carrier Lt) and
A3: Sum Lt = Sum (Lt (#) Ft) by RLVECT_2:def 8;
reconsider Fr = Ft as FinSequence of the carrier of (REAL-NS n) by Th4;
thus Sum Lt
= Sum (Lr (#) Fr) by A1,A3,Th19,Th21
.= Sum Lr by A1,A2,RLVECT_2:def 8;
end;
theorem
for Lv be Linear_Combination of n-VectSp_over F_Real,
Lr be Linear_Combination of REAL-NS n st Lr = Lv
holds Sum Lr = Sum Lv
proof
let Lv be Linear_Combination of n-VectSp_over F_Real,
Lr be Linear_Combination of REAL-NS n;
assume
A1: Lr = Lv;
reconsider Lt = Lr as Linear_Combination of TOP-REAL n by Th11;
Sum Lt = Sum Lr by Th23;
hence thesis by A1,MATRTOP2:5;
end;
theorem Th25:
for Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n
st Ar = At
holds
for X be object holds
X is Linear_Combination of Ar
iff
X is Linear_Combination of At
proof
let Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n;
assume
A1: Ar = At;
let X be object;
hereby
assume X is Linear_Combination of Ar; then
reconsider L=X as Linear_Combination of Ar;
reconsider L1 = L as Linear_Combination of TOP-REAL n by Th11;
Carrier L1 = Carrier L & Carrier L c= Ar by RLVECT_2:def 6;
hence X is Linear_Combination of At by A1, RLVECT_2:def 6;
end;
assume X is Linear_Combination of At; then
reconsider L = X as Linear_Combination of At;
reconsider L1 = L as Linear_Combination of REAL-NS n by Th11;
Carrier L1 = Carrier L & Carrier L c= At by RLVECT_2:def 6;
hence X is Linear_Combination of Ar by A1,RLVECT_2:def 6;
end;
theorem Th26:
for Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n st Ar = At
holds [#]Lin Ar = [#]Lin At
proof
let Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n;
assume
A1: Ar = At;
hereby
let x be object;
assume x in [#] (Lin Ar);
then x in Lin Ar;
then consider L be Linear_Combination of Ar such that
A2: x = Sum L by RLVECT_3:14;
reconsider L1 = L as Linear_Combination of TOP-REAL n by Th11;
Carrier L1 = Carrier L & Carrier L c= Ar by RLVECT_2:def 6;
then A3: L1 is Linear_Combination of At by A1,RLVECT_2:def 6;
Sum L1 = Sum L by Th23;
then x in Lin At by A2,A3,RLVECT_3:14;
hence x in [#] (Lin At);
end;
let x be object;
assume x in [#] (Lin At);
then x in Lin At;
then consider L be Linear_Combination of At such that
A4: x = Sum L by RLVECT_3:14;
reconsider L1 = L as Linear_Combination of REAL-NS n by Th11;
Carrier L1 = Carrier L & Carrier L c= At by RLVECT_2:def 6; then
A5: L1 is Linear_Combination of Ar by A1,RLVECT_2:def 6;
Sum L1 = Sum L by Th23;
then x in Lin Ar by A4,A5,RLVECT_3:14;
hence x in [#] (Lin Ar);
end;
theorem
for Af be Subset of n-VectSp_over F_Real,
Ar be Subset of REAL-NS n st Af = Ar
holds [#]Lin Ar = [#]Lin Af
proof
let Af be Subset of n-VectSp_over F_Real,
Ar be Subset of REAL-NS n;
assume
A1: Af = Ar;
reconsider At = Ar as Subset of TOP-REAL n by Th4;
[#]Lin At = [#]Lin Ar by Th26;
hence thesis by MATRTOP2:6,A1;
end;
theorem Th28:
for Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n
st Ar = At
holds
Ar is linearly-independent
iff
At is linearly-independent
proof
let Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n;
assume
A1: Ar = At;
hereby
assume
A2: Ar is linearly-independent;
now
let L be Linear_Combination of At;
reconsider L1 = L as Linear_Combination of REAL-NS n by Th11;
A3: Carrier L1 = Carrier L;
assume Sum L = 0. (TOP-REAL n); then
A4: 0. (REAL-NS n) = Sum L by Th6
.= Sum L1 by Th23;
L1 is Linear_Combination of Ar by A1,A3,RLVECT_2:def 6;
hence Carrier L = {} by A2,A4,RLVECT_3:def 1;
end;
hence At is linearly-independent by RLVECT_3:def 1;
end;
assume
A5: At is linearly-independent;
now
let L be Linear_Combination of Ar;
reconsider L1 = L as Linear_Combination of TOP-REAL n by Th11;
A6: Carrier L1 = Carrier L;
reconsider L1 = L as Linear_Combination of At by A1,A6,RLVECT_2:def 6;
assume Sum L = 0.(REAL-NS n);
then 0. (TOP-REAL n)
= Sum L by Th6
.= Sum L1 by Th23;
hence Carrier L = {} by A5,RLVECT_3:def 1;
end;
hence Ar is linearly-independent by RLVECT_3:def 1;
end;
theorem
for Af be Subset of n-VectSp_over F_Real,
Ar be Subset of REAL-NS n
st Af = Ar
holds
Af is linearly-independent
iff
Ar is linearly-independent
proof
let Af be Subset of n-VectSp_over F_Real,
Ar be Subset of REAL-NS n;
assume
A1: Af = Ar;
reconsider At = Ar as Subset of TOP-REAL n by Th4;
Ar is linearly-independent
iff
At is linearly-independent by Th28;
hence thesis by A1,MATRTOP2:7;
end;
theorem Th30:
for X be object holds
X is Subspace of REAL-NS n
iff
X is Subspace of TOP-REAL n
proof
let X be object;
A1: the addF of REAL-NS n
= the addF of (the RLSStruct of REAL-NS n)
.= the addF of (the RLSStruct of TOP-REAL n) by Th1
.= the addF of TOP-REAL n;
A2: the Mult of REAL-NS n
= the Mult of (the RLSStruct of REAL-NS n)
.= the Mult of (the RLSStruct of TOP-REAL n) by Th1
.= the Mult of TOP-REAL n;
hereby
assume X is Subspace of REAL-NS n; then
reconsider V = X as Subspace of REAL-NS n;
A3: the carrier of V c= the carrier of REAL-NS n
& 0. V = 0. (REAL-NS n)
& the addF of V = (the addF of (REAL-NS n)) || the carrier of V
& the Mult of V = (the Mult of (REAL-NS n))
| [:REAL, the carrier of V:] by RLSUB_1:def 2; then
A4: the carrier of V c= the carrier of TOP-REAL n by Th4;
0.V = 0. (TOP-REAL n) by A3,Th6;
hence X is Subspace of TOP-REAL n by A1,A2,A3,A4,RLSUB_1:def 2;
end;
assume X is Subspace of TOP-REAL n;
then reconsider V = X as Subspace of TOP-REAL n;
A5: the carrier of V c= the carrier of TOP-REAL n
& 0. V = 0. (TOP-REAL n)
& the addF of V = (the addF of (TOP-REAL n)) || the carrier of V
& the Mult of V = (the Mult of (TOP-REAL n))
| [:REAL, the carrier of V:] by RLSUB_1:def 2;
A6: the carrier of V c= the carrier of REAL-NS n by A5,Th4;
0.V = 0. (REAL-NS n) by A5,Th6;
hence X is Subspace of REAL-NS n by A1,A2,A5,A6,RLSUB_1:def 2;
end;
theorem
for X be set,
U be Subspace of REAL-NS n,
W be Subspace of n -VectSp_over F_Real
st [#] U = [#] W
holds
X is Linear_Combination of U
iff
X is Linear_Combination of W
proof
let X be set;
let U be Subspace of REAL-NS n;
let W be Subspace of n -VectSp_over F_Real;
assume
A1: [#] U = [#] W;
reconsider S=U as Subspace of TOP-REAL n by Th30;
X is Linear_Combination of S
iff
X is Linear_Combination of W by A1,MATRTOP2:11;
hence thesis;
end;
theorem Th32:
for F be one-to-one FinSequence of REAL-NS n
st rng F is linearly-independent
holds
ex M be Matrix of n,F_Real
st M is invertible & M | len F = F
proof
let F be one-to-one FinSequence of REAL-NS n;
assume
A1: rng F is linearly-independent;
reconsider F0 = F as FinSequence of TOP-REAL n by Th4;
rng F0 is linearly-independent by A1,Th28; then
consider M be Matrix of n,F_Real such that
A2: M is invertible & M | len F0 = F0 by MATRTOP2:19;
take M;
thus thesis by A2;
end;
theorem Th33:
for M be Matrix of n,F_Real
for N be Matrix of n,REAL
st N = MXF2MXR M
holds
M is invertible iff N is invertible
proof
let M be Matrix of n,F_Real;
let N be Matrix of n,REAL;
assume
A1: N = MXF2MXR M;
hereby
assume M is invertible; then
consider M2 be Matrix of n,F_Real such that
A2: M is_reverse_of M2 by MATRIX_6:def 3;
set B = MXF2MXR M2;
A3: B*N = 1_Rmatrix n by A1,A2,MATRIX_6:def 2;
N*B = 1_Rmatrix n by A1,A2,MATRIX_6:def 2;
hence N is invertible by MATRIXR2:def 5,A3;
end;
assume N is invertible; then
ex B be Matrix of n,REAL st
(B * N = 1_Rmatrix n & N * B = 1_Rmatrix n) by MATRIXR2:def 5;
hence M is invertible by A1,MATRIX_6:def 2,def 3;
end;
theorem
for M be Matrix of n,REAL
holds
M is invertible iff MXR2MXF M is invertible
proof
let M be Matrix of n,REAL;
hereby
assume M is invertible;
then consider B be Matrix of n,REAL such that
A1: (B * M = 1_Rmatrix n & M * B = 1_Rmatrix n) by MATRIXR2:def 5;
thus MXR2MXF M is invertible by A1,MATRIX_6:def 2,def 3;
end;
assume MXR2MXF M is invertible;
then consider M2 be Matrix of n,F_Real such that
A2: MXR2MXF M is_reverse_of M2 by MATRIX_6:def 3;
set B = MXF2MXR M2;
A3: M*B = 1_Rmatrix n by A2,MATRIX_6:def 2;
B*M = 1_Rmatrix n by A2,MATRIX_6:def 2;
hence M is invertible by A3,MATRIXR2:def 5;
end;
theorem
for F be one-to-one FinSequence of REAL-NS n
st rng F is linearly-independent
holds
ex M be Matrix of n,REAL
st M is invertible & M | len F = F
proof
let F be one-to-one FinSequence of REAL-NS n;
assume rng F is linearly-independent;
then consider M be Matrix of n,F_Real such that
A1: M is invertible & M | len F = F by Th32;
reconsider N = MXF2MXR M as Matrix of n,REAL;
take N;
thus N is invertible by A1,Th33;
thus N | len F = F by A1;
end;
theorem
for F be one-to-one FinSequence of REAL-NS n
st rng F is linearly-independent
holds
for B be OrdBasis of n -VectSp_over F_Real
st B = MX2FinS(1. (F_Real,n))
holds
for M be Matrix of n,F_Real
st M is invertible & M | len F = F
holds
(Mx2Tran M) .: ([#] (Lin (rng (B | len F))))
= [#] (Lin rng F)
proof
let F be one-to-one FinSequence of REAL-NS n;
assume
A1: rng F is linearly-independent;
let B be OrdBasis of n -VectSp_over F_Real;
assume
A2: B = MX2FinS(1. (F_Real,n));
let M be Matrix of n,F_Real;
assume
A3: M is invertible & M | len F = F;
reconsider F0 = F as FinSequence of TOP-REAL n by Th4;
rng F0 is linearly-independent by A1,Th28; then
(Mx2Tran M) .: ([#] (Lin (rng (B | len F0))))
= [#] (Lin rng F0) by A2,A3,MATRTOP2:21;
hence thesis by Th26;
end;
theorem
for A,B be linearly-independent Subset of REAL-NS n
st card A = card B
holds
ex M be Matrix of n,F_Real
st M is invertible
& (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B)
proof
let A,B be linearly-independent Subset of REAL-NS n;
assume
A1: card A = card B;
reconsider A0 = A, B0 = B as Subset of TOP-REAL n by Th4;
A0 is linearly-independent Subset of TOP-REAL n &
B0 is linearly-independent Subset of TOP-REAL n by Th28; then
consider M be Matrix of n,F_Real such that
A2: M is invertible
& (Mx2Tran M) .: ([#] (Lin A0)) = [#] (Lin B0) by A1,MATRTOP2:22;
take M;
thus M is invertible by A2;
[#] (Lin A0) = [#] (Lin A) &
[#] (Lin B0) = [#] (Lin B) by Th26;
hence thesis by A2;
end;
theorem
for n, m be Nat
for M be Matrix of n,m,F_Real
for A be linearly-independent Subset of REAL-NS n
st the_rank_of M = n
holds
(Mx2Tran M) .: A is linearly-independent
proof
let n, m be Nat;
let M be Matrix of n,m,F_Real;
let A be linearly-independent Subset of REAL-NS n;
assume
A1: the_rank_of M = n;
reconsider A0 = A as linearly-independent Subset of TOP-REAL n
by Th4,Th28;
(Mx2Tran M) .: A0 is linearly-independent by A1,MATRTOP2:23;
hence thesis;
end;
theorem Th39:
for p be Element of TOP-REAL n,
f be Element of REAL-NS n,
H be Subset of TOP-REAL n,
I be Subset of REAL-NS n
st p = f & H = I
holds p + H = f + I
proof
let p be Element of TOP-REAL n,
f be Element of REAL-NS n,
H be Subset of TOP-REAL n,
I be Subset of REAL-NS n;
assume
A1: p = f & H = I;
for x be object holds
x in p+H iff x in f+I
proof
let x be object;
hereby
assume x in p+H;
then
consider v be Element of TOP-REAL n such that
A2: x = p+v & v in H;
reconsider w = v as Element of REAL-NS n by Th4;
x = f+w by A1,A2,Th7;
hence x in f+I by A2,A1;
end;
assume x in f+I;
then consider v be Element of REAL-NS n such that
A3: x = f+v & v in I;
reconsider w = v as Element of TOP-REAL n by Th4;
x = p+w by A1,A3,Th7;
hence x in p+H by A1,A3;
end;
hence thesis by TARSKI:2;
end;
theorem Th40:
for Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n
st Ar = At
holds
Ar is Affine
iff
At is Affine
proof
let Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n;
assume
A1: Ar = At;
hereby
assume
A2: Ar is Affine;
for x, y be VECTOR of TOP-REAL n
for a be Real st x in At & y in At holds
((1 - a) * x) + (a * y) in At
proof
let x, y be VECTOR of TOP-REAL n;
let a be Real;
assume
A3: x in At & y in At;
reconsider x0 = x, y0 = y as VECTOR of REAL-NS n by Th4;
(1 - a) * x = (1 - a) * x0 &
a * y = a * y0 by Th8; then
((1 - a) * x) + (a * y) = ((1 - a) * x0) + (a * y0) by Th7;
hence ((1 - a) * x) + (a * y) in At by A1,A2,A3,RUSUB_4:def 4;
end;
hence At is Affine by RUSUB_4:def 4;
end;
assume
A4: At is Affine;
for x, y be VECTOR of REAL-NS n
for a be Real
st x in Ar & y in Ar
holds
((1 - a) * x) + (a * y) in Ar
proof
let x, y be VECTOR of REAL-NS n;
let a be Real;
assume
A5: x in Ar & y in Ar;
reconsider x0 = x, y0 = y as VECTOR of TOP-REAL n by Th4;
(1 - a) * x = (1 - a) * x0 &
a * y = a * y0 by Th8;
then ((1 - a) * x) + (a * y)
= ((1 - a) * x0) + (a * y0) by Th7;
hence ((1 - a) * x) + (a * y) in Ar by A1,A4,A5,RUSUB_4:def 4;
end;
hence Ar is Affine by RUSUB_4:def 4;
end;
theorem Th41:
for X be set
holds
X is affinely-independent Subset of REAL-NS n
iff
X is affinely-independent Subset of TOP-REAL n
proof
let X be set;
hereby
assume X is affinely-independent Subset of REAL-NS n;
then
reconsider Ar = X as affinely-independent Subset of REAL-NS n;
reconsider At = Ar as Subset of TOP-REAL n by Th4;
per cases by RLAFFIN1:def 4;
suppose
Ar is empty; then
At is empty;
hence X is affinely-independent Subset of TOP-REAL n;
end;
suppose
ex v be VECTOR of REAL-NS n
st v in Ar & ((- v) + Ar) \ {(0. (REAL-NS n))}
is linearly-independent; then
consider v be VECTOR of REAL-NS n such that
A1: v in Ar & ((- v) + Ar) \ {(0. (REAL-NS n))}
is linearly-independent;
reconsider w=v as VECTOR of TOP-REAL n by Th4;
A2 : 0. (REAL-NS n) = 0. (TOP-REAL n) by Th6;
((- v) + Ar) \ {(0. (REAL-NS n))}
= ((- w) + At) \ {(0. (TOP-REAL n))} by A2,Th9,Th39; then
((- w) + At) \ {(0. (TOP-REAL n))}
is linearly-independent by A1,Th28;
hence X is affinely-independent Subset of TOP-REAL n
by A1,RLAFFIN1:def 4;
end;
end;
assume X is affinely-independent Subset of TOP-REAL n;
then
reconsider At = X as affinely-independent Subset of TOP-REAL n;
reconsider Ar=At as Subset of REAL-NS n by Th4;
per cases by RLAFFIN1:def 4;
suppose
At is empty; then
Ar is empty;
hence X is affinely-independent Subset of REAL-NS n;
end;
suppose
ex v be VECTOR of TOP-REAL n
st v in At & ((- v) + At) \ {(0. (TOP-REAL n))}
is linearly-independent; then
consider v be VECTOR of TOP-REAL n such that
A3: v in At & ((- v) + At) \ {(0. (TOP-REAL n))}
is linearly-independent;
reconsider w=v as VECTOR of REAL-NS n by Th4;
A4: 0. (REAL-NS n) = 0. (TOP-REAL n) by Th6;
((- w) + Ar) \ {(0. (REAL-NS n))}
= ((- v) + At) \ {(0. (TOP-REAL n))} by A4,Th9,Th39;
then
((- w) + Ar) \ {(0. (REAL-NS n))}
is linearly-independent by A3,Th28;
hence
X is affinely-independent Subset of REAL-NS n by A3,RLAFFIN1:def 4;
end;
end;
theorem
for n, m be Nat
for M be Matrix of n,m,F_Real
for A be affinely-independent Subset of REAL-NS n
st the_rank_of M = n
holds
(Mx2Tran M) .: A is affinely-independent
proof
let n, m be Nat;
let M be Matrix of n,m,F_Real;
let A be affinely-independent Subset of REAL-NS n;
assume
A1: the_rank_of M = n;
reconsider B = A as affinely-independent Subset of TOP-REAL n by Th41;
(Mx2Tran M) .: B is affinely-independent by A1, MATRTOP2:24;
hence thesis;
end;
theorem Th43:
for Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n
st Ar = At
holds
Affin Ar = Affin At
proof
let Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n;
assume
A1: Ar = At;
set AM = { B where B is Affine Subset of REAL-NS n : Ar c= B };
set BM = { B where B is Affine Subset of TOP-REAL n : At c= B };
A2: Affin Ar = meet AM by RLAFFIN1:def 6;
A3: Affin At = meet BM by RLAFFIN1:def 6;
At c= Affin At by RLAFFIN1:49; then
A4: Affin At in BM;
Ar c= Affin Ar by RLAFFIN1:49; then
A5: Affin Ar in AM;
for x be object holds
x in Affin Ar
iff
x in Affin At
proof
let x be object;
hereby
assume
A6: x in Affin Ar;
now
let Y be set;
assume Y in BM;
then
consider B be Affine Subset of TOP-REAL n such that
A7: Y = B & At c= B;
reconsider A = B as Subset of REAL-NS n by Th4;
reconsider A as Affine Subset of REAL-NS n by Th40;
Y = A & Ar c= A by A1,A7; then
Y in AM;
hence x in Y by A2,A6,SETFAM_1:def 1;
end;
hence x in Affin At by A4;
end;
assume
A8: x in Affin At;
now
let Y be set;
assume Y in AM; then
consider B be Affine Subset of REAL-NS n such that
A9: Y = B & Ar c= B;
reconsider A = B as Subset of TOP-REAL n by Th4;
reconsider A as Affine Subset of TOP-REAL n by Th40;
Y = B & At c= A by A1,A9;
then Y in BM;
hence x in Y by A3,A8,SETFAM_1:def 1;
end;
hence x in Affin Ar by A5;
end;
hence thesis by TARSKI:2;
end;
theorem Th44:
for L be Linear_Combination of REAL-NS n,
S be Linear_Combination of TOP-REAL n
st L = S
holds
sum L = sum S
proof
let L be Linear_Combination of REAL-NS n,
S be Linear_Combination of TOP-REAL n;
assume
A1: L = S;
consider F be FinSequence of REAL-NS n such that
A2: F is one-to-one & rng F = Carrier L
& sum L = Sum (L * F) by RLAFFIN1:def 3;
reconsider E = F as FinSequence of TOP-REAL n by Th4;
Sum (L * F) = Sum (S * E) by A1;
hence thesis by A2,A1,RLAFFIN1:def 3;
end;
theorem Th45:
for Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n,
v be Element of REAL-NS n,
w be Element of TOP-REAL n
st Ar = At & v = w & v in Affin Ar & Ar is affinely-independent
holds
v |-- Ar = w |-- At
proof
let Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n,
v be Element of REAL-NS n,
w be Element of TOP-REAL n;
assume
A1: Ar = At & v=w & v in Affin Ar
& Ar is affinely-independent;
then
A2: At is affinely-independent by Th41;
reconsider h = v |-- Ar as Linear_Combination of At by A1,Th25;
A3: Sum h
= Sum (v |-- Ar) by Th23
.= w by A1,RLAFFIN1:def 7;
A4: sum h
= sum (v |-- Ar) by Th44
.= 1 by RLAFFIN1:def 7,A1;
w in Affin At by A1,Th43;
hence thesis by A2,A3,A4,RLAFFIN1:def 7;
end;
theorem
for n, m be Nat
for M be Matrix of n,m,F_Real
for A be affinely-independent Subset of REAL-NS n
st the_rank_of M = n
holds
for v be Element of REAL-NS n
st v in Affin A
holds
(Mx2Tran M).v in Affin((Mx2Tran M) .: A)
& (for f be n -element real-valued FinSequence
holds (v |-- A).f = (((Mx2Tran M).v)
|-- ((Mx2Tran M) .: A)) . ((Mx2Tran M).f))
proof
let n, m be Nat;
let M be Matrix of n,m,F_Real;
let B be affinely-independent Subset of REAL-NS n;
assume
A1: the_rank_of M = n;
let w be Element of REAL-NS n;
assume
A2: w in Affin B;
reconsider A = B as affinely-independent Subset of TOP-REAL n by Th41;
reconsider v = w as Element of TOP-REAL n by Th4;
A3: v in Affin A by A2,Th43;
v |-- A = w |-- B by A2,Th45;
hence thesis by A1,A3,MATRTOP2:25;
end;
theorem
for n, m be Nat
for M be Matrix of n,m,F_Real
for A be linearly-independent Subset of REAL-NS m
st the_rank_of M = n
holds
(Mx2Tran M) " A is linearly-independent
proof
let n, m be Nat;
let M be Matrix of n,m,F_Real;
let A be linearly-independent Subset of REAL-NS m;
assume
A1: the_rank_of M = n;
reconsider B = A as linearly-independent Subset of TOP-REAL m
by Th4,Th28;
(Mx2Tran M) " B is linearly-independent by A1,MATRTOP2:26;
hence
(Mx2Tran M) " A is linearly-independent;
end;
theorem
for n, m be Nat
for M be Matrix of n,m,F_Real
for A be affinely-independent Subset of REAL-NS m
st the_rank_of M = n
holds
(Mx2Tran M) " A is affinely-independent
proof
let n, m be Nat;
let M be Matrix of n,m,F_Real;
let A be affinely-independent Subset of REAL-NS m;
assume
A1: the_rank_of M = n;
reconsider B = A as affinely-independent Subset of TOP-REAL m by Th41;
(Mx2Tran M) " B is affinely-independent by A1,MATRTOP2:27;
hence (Mx2Tran M) " A is affinely-independent;
end;
theorem Th49:
for V be RealLinearSpace,
W be strict Subspace of V
holds
W is strict Subspace of (Omega). V
proof
let V be RealLinearSpace,
W be strict Subspace of V;
set V0 = (Omega). V;
A1: V0
= RLSStruct(# the carrier of V,
the ZeroF of V,
the addF of V,
the Mult of V #) by RLSUB_1:def 4;
A2: the carrier of W c= the carrier of V
& 0. W = 0. V
& the addF of W = (the addF of V) || (the carrier of W)
& the Mult of W = (the Mult of V) | [:REAL, the carrier of W:]
by RLSUB_1:def 2;
the carrier of V = the carrier of V0
& 0. V = 0. V0
& the addF of V = the addF of V0
& the Mult of V = the Mult of V0 by A1;
hence thesis by A2,RLSUB_1:def 2;
end;
theorem Th50:
for X be set holds
X is Basis of n -VectSp_over F_Real
iff
X is Basis of TOP-REAL n
proof
let X be set;
set V = n -VectSp_over F_Real;
set W = TOP-REAL n;
hereby
assume X is Basis of V;
then
reconsider A = X as Basis of V;
reconsider B = A as Subset of W by Lm1;
A is linearly-independent
& Lin A = ModuleStr(# the carrier of V,
the addF of V,
the ZeroF of V,
the lmult of V #) by VECTSP_7:def 3;
then
A1: B is linearly-independent by MATRTOP2:7;
set W0 = Lin B;
A2: the carrier of W0 c= the carrier of W
& 0. W0 = 0. W
& the addF of W0 = (the addF of W) || (the carrier of W0)
& the Mult of W0 = (the Mult of W) | [:REAL, the carrier of W0:]
by RLSUB_1:def 2;
the carrier of W0
= [#]W0
.= [#] Lin A by MATRTOP2:6
.= the carrier of V by VECTSP_7:def 3
.= the carrier of W by Lm1;
hence X is Basis of W by A2,A1,RLVECT_3:def 3;
end;
assume X is Basis of W;
then
reconsider A = X as Basis of W;
reconsider B = A as Subset of V by Lm1;
A3: A is linearly-independent
& Lin A = RLSStruct(# the carrier of W,
the ZeroF of W,
the addF of W,
the Mult of W #) by RLVECT_3:def 3;
then
A4: B is linearly-independent by MATRTOP2:7;
set V0 = Lin B;
A5: the carrier of V0 c= the carrier of V
& 0. V0 = 0. V
& the addF of V0 = (the addF of V) || the carrier of V0
& the lmult of V0 = (the lmult of V) |
[: the carrier of F_Real, the carrier of V0:] by VECTSP_4:def 2;
the carrier of V0
= [#]V0
.= [#] Lin A by MATRTOP2:6
.= the carrier of V by A3,Lm1;
hence X is Basis of V by A4,A5,VECTSP_7:def 3;
end;
theorem Th51:
for n be non empty Nat holds
RealFuncAdd Seg n = product(the addF of F_Real,n)
proof
let n be non empty Nat;
set OP1 = RealFuncAdd Seg n;
set OP2 = product(the addF of F_Real,n);
A1: Funcs(Seg n,REAL) = REAL n by FINSEQ_2:93;
for x, y be Element of REAL n
holds OP1 . (x,y) = OP2 . (x,y)
proof
let x, y be Element of REAL n;
reconsider x0 = x, y0 = y as Element of Funcs(Seg n,REAL)
by FINSEQ_2:93;
[x,y] in [:REAL n,REAL n:] by ZFMISC_1:87;
then
OP2.(x,y) in REAL n by FUNCT_2:5;
then
reconsider h = OP2.(x0,y0) as Element of Funcs(Seg n,REAL)
by FINSEQ_2:93;
for i be Element of Seg n
holds h . i = (x0 . i) + (y0 . i)
proof
let i be Element of Seg n;
A2: OP2 . (x0,y0) = addreal .: (x0,y0) by PRVECT_1:def 1;
dom h = Seg n by FUNCT_2:def 1;
hence
h.i = addreal . (x0.i, y0.i) by FUNCOP_1:22,A2
.= (x0. i) + (y0 . i) by BINOP_2:def 9;
end;
hence thesis by FUNCSDOM:1;
end;
hence thesis by BINOP_1:2,A1;
end;
theorem Th52:
for n be non empty Nat holds
RealFuncExtMult(Seg n) = n -Mult_over F_Real
proof
let n be non empty Nat;
set OP1 = RealFuncExtMult Seg n;
set OP2 = n -Mult_over F_Real;
A1: Funcs(Seg n,REAL) = REAL n by FINSEQ_2:93;
for x be Element of REAL,
y be Element of REAL n
holds OP1.(x,y) = OP2.(x,y)
proof
let x be Element of REAL,
y be Element of REAL n;
reconsider y0 = y as Element of Funcs(Seg n,REAL) by FINSEQ_2:93;
[x,y] in [:REAL,REAL n:] by ZFMISC_1:87; then
OP2.(x,y) in REAL n by FUNCT_2:5; then
reconsider h = OP2.(x,y0) as Element of Funcs(Seg n,REAL)
by FINSEQ_2:93;
for i be Element of Seg n
holds h.i = x * (y0.i)
proof
let i be Element of Seg n;
A2: OP2.[x,y0]
= OP2.(x,y0)
.= (multreal) [;] (x,y0) by PRVECT_1:def 4;
dom h = Seg n by FUNCT_2:def 1;
hence h.i = (multreal).(x,y0.i) by FUNCOP_1:32,A2
.= x*(y0.i) by BINOP_2:def 11;
end;
hence thesis by FUNCSDOM:4;
end;
hence thesis by BINOP_1:2,A1;
end;
theorem Th53: ::: see also RLAFFIN3:4, not really used here
TOP-REAL n is finite-dimensional
&
dim TOP-REAL n = n
proof
set V = n -VectSp_over F_Real;
set W = TOP-REAL n;
A1: dim V = n by MATRIX13:112;
consider A be finite Subset of V such that
A2: A is Basis of V by MATRLIN:def 1;
A3: card A = n by A1,A2,VECTSP_9:def 1;
reconsider B = A as finite Subset of W by Lm1;
thus W is finite-dimensional;
B is Basis of W by A2,Th50;
hence dim W = n by A3,RLVECT_5:def 2;
end;
theorem Th54:
for n be non empty Nat holds
the carrier of (TOP-REAL n) = the carrier of (n -VectSp_over F_Real)
& 0. (TOP-REAL n) = 0. (n -VectSp_over F_Real)
& the addF of (TOP-REAL n) = the addF of (n -VectSp_over F_Real)
& the Mult of (TOP-REAL n) = the lmult of (n -VectSp_over F_Real)
proof
let n be non empty Nat;
set V = n -VectSp_over F_Real;
set W = TOP-REAL n;
thus the carrier of (TOP-REAL n)
= the carrier of (n -VectSp_over F_Real) by Lm1;
A1: n -Group_over F_Real
= addLoopStr(# n -tuples_on the carrier of F_Real,
product(the addF of F_Real,n),
n |-> (0. F_Real) #) by PRVECT_1:def 3;
A2: addLoopStr(# the carrier of V,
the addF of V,
the ZeroF of V #)
= n -Group_over F_Real
& the lmult of V = n -Mult_over F_Real
by PRVECT_1:def 5;
A3: RLSStruct(# the carrier of W,
the ZeroF of W,
the addF of W,
the Mult of W #)
= RealVectSpace Seg n by EUCLID:def 8;
thus 0. (TOP-REAL n)
= 0* n by EUCLID:70
.= 0.(n -VectSp_over F_Real) by A1,A2;
thus the addF of TOP-REAL n
= the addF of (n -VectSp_over F_Real) by A1,A2,A3,Th51;
thus the Mult of TOP-REAL n
= n -Mult_over F_Real by A3,Th52
.= the lmult of (n -VectSp_over F_Real) by PRVECT_1:def 5;
end;
theorem
for n be non empty Nat,
xv, yv be Element of n -VectSp_over F_Real,
xt, yt be Element of TOP-REAL n
st xv = xt & yv = yt
holds xv + yv = xt + yt by Th54;
theorem
for n be non empty Nat,
af be Element of F_Real,
r be Real,
xv be Element of n -VectSp_over F_Real,
xt be Element of TOP-REAL n
st af = r & xv = xt
holds af * xv = r * xt by Th54;
theorem Th57:
for n be non empty Nat,
xv be Element of n -VectSp_over F_Real,
xt be Element of TOP-REAL n
st xv = xt
holds -xv = -xt
proof
let n be non empty Nat,
xv be Element of n -VectSp_over F_Real,
xt be Element of TOP-REAL n;
assume
A1: xv=xt;
thus -xv = (-1.F_Real)*xv by VECTSP_1:14
.= (-1)*xt by A1,Th54
.= -xt by RLVECT_1:16;
end;
theorem
for n be non empty Nat,
xv, yv be Element of n -VectSp_over F_Real,
xt, yt be Element of TOP-REAL n
st xv = xt & yv = yt
holds xv - yv = xt - yt
proof
let n be non empty Nat,
xv, yv be Element of n -VectSp_over F_Real,
xt, yt be Element of TOP-REAL n;
assume
A1: xv=xt & yv=yt; then
-yv = -yt by Th57;
hence xv - yv = xt - yt by A1,Th54;
end;
theorem
for n be non empty Nat
for At be Subset of TOP-REAL n,
Ar be Subset of n -VectSp_over F_Real
st At = Ar
holds
the carrier of Lin At = the carrier of (Lin Ar)
& 0.(Lin At) = 0.(Lin Ar)
& the addF of Lin At = the addF of (Lin Ar)
& the Mult of Lin At = the lmult of (Lin Ar)
proof
let n be non empty Nat;
let At be Subset of TOP-REAL n,
Ar be Subset of n -VectSp_over F_Real;
assume
A1: At = Ar;
set V = TOP-REAL n;
set W = n -VectSp_over F_Real;
set Lt = Lin At;
set Lr = Lin Ar;
A2: the carrier of Lr c= the carrier of W
& 0. Lr = 0. W
& the addF of Lr = (the addF of W) || the carrier of Lr
& the lmult of Lr = (the lmult of W) |
[: the carrier of F_Real, the carrier of Lr:] by VECTSP_4:def 2;
A3: the carrier of Lt c= the carrier of V
& 0. Lt = 0. V
& the addF of Lt = (the addF of V) || the carrier of Lt
& the Mult of Lt = (the Mult of V) | [:REAL, the carrier of Lt:]
by RLSUB_1:def 2;
thus
A4: the carrier of Lt
= [#]Lin At
.= [#]Lin Ar by A1,MATRTOP2:6
.= the carrier of Lr;
A5: the addF of Lt
= (the addF of W) || the carrier of Lr by A3,A4,Th54
.= the addF of Lr by VECTSP_4:def 2;
the Mult of Lt
= (the lmult of W) | [:REAL, the carrier of Lr:] by A3,A4,Th54
.= the lmult of Lr by VECTSP_4:def 2;
hence thesis by A2,A3,A5,Th54;
end;
theorem
for At be Subset of TOP-REAL n,
Ar be Subset of REAL-NS n
st At = Ar
holds Lin At = Lin Ar
proof
let At be Subset of TOP-REAL n,
Ar be Subset of REAL-NS n;
assume
A1: At = Ar;
set V = TOP-REAL n;
set W = REAL-NS n;
set Lt = Lin At;
set Lr = Lin Ar;
A2: the carrier of Lt c= the carrier of V
& 0. Lt = 0. V
& the addF of Lt = (the addF of V) || the carrier of Lt
& the Mult of Lt = (the Mult of V) | [:REAL, the carrier of Lt:]
by RLSUB_1:def 2;
A3: the carrier of Lt
= [#]Lin At
.= [#]Lin Ar by A1,Th26
.= the carrier of Lr;
A4: the RLSStruct of TOP-REAL n =the RLSStruct of REAL-NS n by Th1;
then
the carrier of V = the carrier of W
& 0.V = 0.W
& the addF of V = the addF of W
& the Mult of V = the Mult of W;
then
A5: 0.Lt = 0.Lr by A2,RLSUB_1:def 2;
A6: the addF of Lt
= (the addF of W) || the carrier of Lr by A3,A4,RLSUB_1:def 2
.= the addF of Lr by RLSUB_1:def 2;
the Mult of Lt
= (the Mult of W) | [:REAL, the carrier of Lr:] by A3,A4,RLSUB_1:def 2
.= the Mult of Lr by RLSUB_1:def 2;
hence thesis by A3,A5,A6;
end;
theorem Th61:
for X be set holds
X is Basis of TOP-REAL n
iff
X is Basis of REAL-NS n
proof
let X be set;
set V = TOP-REAL n;
set W = REAL-NS n;
hereby
assume X is Basis of V;
then
reconsider A = X as Basis of V;
reconsider B = A as Subset of W by Th4;
A1: A is linearly-independent
& Lin A = RLSStruct(# the carrier of V,
the ZeroF of V,
the addF of V,
the Mult of V #) by RLVECT_3:def 3;
then
A2: B is linearly-independent by Th28;
set W0 = (Omega). W;
A3: W0 = RLSStruct(# the carrier of W,
the ZeroF of W,
the addF of W,
the Mult of W #) by RLSUB_1:def 4;
A4: Lin B is strict Subspace of W0 by Th49;
A5: [#]Lin A = the carrier of W by A1,Th4;
the carrier of (Lin B)
= [#](Lin B)
.= the carrier of W0 by A3,A5,Th26;
then
Lin B
= W0 by A4,RLSUB_1:32
.= RLSStruct(# the carrier of W,
the ZeroF of W,
the addF of W,
the Mult of W #) by RLSUB_1:def 4;
hence X is Basis of W by A2,RLVECT_3:def 3;
end;
assume X is Basis of W; then
reconsider A = X as Basis of W;
reconsider B = A as Subset of V by Th4;
A6: A is linearly-independent
& Lin A = RLSStruct(# the carrier of W,
the ZeroF of W,
the addF of W,
the Mult of W #) by RLVECT_3:def 3;
then
A7: B is linearly-independent by Th28;
set V0 = (Omega). V;
A8: V0 = RLSStruct(# the carrier of V,
the ZeroF of V,
the addF of V,
the Mult of V #) by RLSUB_1:def 4;
A9: Lin B is strict Subspace of V0 by Th49;
A10: [#]Lin A = the carrier of V by A6,Th4;
the carrier of (Lin B)
= [#](Lin B)
.= the carrier of V0 by A8,A10,Th26; then
Lin B = V0 by A9,RLSUB_1:32
.= RLSStruct(# the carrier of V,
the ZeroF of V,
the addF of V,
the Mult of V #) by RLSUB_1:def 4;
hence
X is Basis of V by A7,RLVECT_3:def 3;
end;
theorem Th62:
REAL-NS n is finite-dimensional
&
dim (REAL-NS n) = n
proof
set V = TOP-REAL n;
set W = REAL-NS n;
A1: dim V = n by Th53;
consider A be finite Subset of V such that
A3: A is Basis of V by RLVECT_5:def 1;
A4: card A = n by A1,A3,RLVECT_5:def 2;
reconsider B = A as finite Subset of W by Th4;
A5: B is Basis of W by A3,Th61;
hence W is finite-dimensional by RLVECT_5:def 1;
hence dim W = n by A4,A5,RLVECT_5:def 2;
end;
begin :: Finite dimensional vector spaces over real field
registration
cluster finite-dimensional for RealNormSpace;
existence
proof
set n = the non empty Nat;
set X = REAL-NS n;
take X;
thus X is finite-dimensional by Th62;
end;
end;
theorem Th63:
for K be Field,
V be finite-dimensional VectSp of K,
b be OrdBasis of V
holds
ex T be linear-transformation of V, (dim V) -VectSp_over K
st T is bijective
&
for x be Element of V holds T.x = x |-- b
proof
let K be Field;
let V be finite-dimensional VectSp of K;
let b be OrdBasis of V;
set W = (dim V) -VectSp_over K;
set W0 = (dim V) -Group_over K;
A1: W0 = addLoopStr(# (dim V) -tuples_on the carrier of K,
product(the addF of K, dim V),
(dim V) |-> 0.K #) by PRVECT_1:def 3;
A2: addLoopStr(# the carrier of W,
the addF of W,
the ZeroF of W #)
= W0 by PRVECT_1:def 5;
defpred P1[object,object] means
ex x be Element of V
st $1 = x & $2 = x |-- b;
A3: the carrier of ((dim V) -VectSp_over K)
= (dim V) -tuples_on the carrier of K by MATRIX13:102;
A4: for x be Element of the carrier of V
ex y be Element of the carrier of W st P1[x,y]
proof
let x be Element of the carrier of V;
set y = x |-- b;
len y
= len b by MATRLIN:def 7
.= dim V by MATRLIN2:21;
then
y is Element of (dim V) -tuples_on the carrier of K by FINSEQ_2:92;
hence thesis by A3;
end;
consider f be Function of the carrier of V, the carrier of W
such that
A5: for x be Element of the carrier of V holds P1[x, f.x]
from FUNCT_2:sch 3(A4);
A6: for x be Element of V holds f.x = x |-- b
proof
let x be Element of V;
ex x0 be Element of V
st x = x0 & f.x = x0 |-- b by A5;
hence f.x = x |-- b;
end;
for x, y be Element of V
holds f.(x + y) = f.x + f.y
proof
let x, y be Element of V;
thus f.(x + y)
= (x + y) |-- b by A6
.= (x |-- b) + (y |-- b) by MATRLIN2:17
.= (the addF of K) .: (f.x, y |-- b) by A6
.= (the addF of K) .: (f.x, f.y) by A6
.= f.x + f.y by A1,A2,PRVECT_1:def 1;
end;
then
A12: f is additive;
for a be Scalar of K
for x be Vector of V
holds f . (a * x) = a * (f . x)
proof
let a be Scalar of K;
let x be Element of V;
A13: f.x = x |-- b by A6;
len(x |-- b)
= len b by MATRLIN:def 7
.= dim V by MATRLIN2:21;
then
A14: f.x is Element of (dim V) -tuples_on (the carrier of K)
by A13,FINSEQ_2:92;
thus f . (a*x)
= (a*x) |-- b by A6
.= a * (x |-- b) by MATRLIN2:18
.= ((the multF of K) [;] (a,(id the carrier of K))) * (f.x) by A6
.=(the multF of K) [;] (a,f.x) by A14,FINSEQOP:22
.= ((dim V) -Mult_over K).(a,f.x) by A14,PRVECT_1:def 4
.= a * f.x by PRVECT_1:def 5;
end;
then
A15: f is linear-transformation of V, W by A12,MOD_2:def 2;
for x,y be object
st x in dom f & y in dom f & f.x = f.y
holds x = y
proof
let x,y be object;
assume
A16: x in dom f & y in dom f & f.x = f.y;
reconsider x0 = x, y0 = y as Element of V by A16;
x0 |-- b
= f.x0 by A6
.= y0 |-- b by A6,A16;
hence
x = y by MATRLIN:34;
end;
then
A17: f is one-to-one by FUNCT_1:def 4;
for y be object st y in the carrier of W
holds
ex x be object st
x in the carrier of V & y = f . x
proof
let y0 be object;
assume y0 in the carrier of W;
then
reconsider y = y0 as Element of (dim V) -tuples_on the carrier of K
by MATRIX13:102;
A18: len y
= dim V by CARD_1:def 7
.= len b by MATRLIN2:21;
reconsider x = Sum(lmlt(y,b)) as Element of the carrier of V;
take x;
thus x in the carrier of V;
thus y0 = x |-- b by A18, MATRLIN:36
.= f.x by A6;
end;
then
rng f = the carrier of W by FUNCT_2:10;
then
f is onto by FUNCT_2:def 3;
hence thesis by A15,A6,A17;
end;
theorem Th64:
for K be Field,
V be finite-dimensional VectSp of K
ex T be linear-transformation of V, (dim V) -VectSp_over K
st T is bijective
proof
let K be Field;
let V be finite-dimensional VectSp of K;
set b = the OrdBasis of V;
set W = (dim V) -VectSp_over K;
set W0 = (dim V) -Group_over K;
ex T be linear-transformation of V, (dim V) -VectSp_over K
st T is bijective
& for x be Element of V holds T.x= (x |-- b) by Th63;
hence thesis;
end;
theorem
for K be Field,
V,W be finite-dimensional VectSp of K
holds
dim V = dim W
iff
ex T be linear-transformation of V, W st T is bijective
proof
let K be Field,
V,W be finite-dimensional VectSp of K;
hereby
assume
A1: dim V = dim W;
consider T1 be linear-transformation of V, (dim V) -VectSp_over K
such that
A2: T1 is bijective by Th64;
consider T2 be linear-transformation of W, (dim V) -VectSp_over K
such that
A3: T2 is bijective by A1,Th64;
consider S be linear-transformation of (dim V) -VectSp_over K,W
such that
A4: (S = T2 " & S is bijective) by A3,ZMODUL06:42;
set T = S * T1;
reconsider T as linear-transformation of V, W;
T is bijective by A2,A4,FINSEQ_4:85;
hence
ex T be linear-transformation of V, W st T is bijective;
end;
assume ex T be linear-transformation of V, W st T is bijective;
hence dim V = dim W by VECTSP12:4;
end;
theorem
for X be RealLinearSpace
holds
the carrier of X = the carrier of (RLSp2RVSp X)
& the ZeroF of X = the ZeroF of (RLSp2RVSp X)
& the addF of X = the addF of (RLSp2RVSp X)
& the Mult of X = the lmult of (RLSp2RVSp X);
theorem
for X be strict RealLinearSpace
holds RVSp2RLSp RLSp2RVSp X = X;
theorem
for X be strict VectSp of F_Real
holds RLSp2RVSp RVSp2RLSp X = X;
theorem
for V be RealLinearSpace,
F be set
holds
F is Subset of V
iff
F is Subset of RLSp2RVSp(V);
theorem
for V be RealLinearSpace,
F be set
holds
F is FinSequence of V
iff
F is FinSequence of RLSp2RVSp(V);
theorem
for V be RealLinearSpace,
F be set
holds
F is Function of V,REAL
iff
F is Function of RLSp2RVSp(V),REAL;
theorem Th72:
for T be RealLinearSpace,
X be set
holds
X is Linear_Combination of RLSp2RVSp(T)
iff
X is Linear_Combination of T
proof
let T be RealLinearSpace,
X be set;
set V = RLSp2RVSp(T);
hereby
assume X is Linear_Combination of RLSp2RVSp(T);
then reconsider L = X as Linear_Combination of RLSp2RVSp(T);
consider S be finite Subset of RLSp2RVSp(T) such that
A1: for v be Element of RLSp2RVSp(T) st not v in S
holds L.v = 0. F_Real by VECTSP_6:def 1;
thus X is Linear_Combination of T by A1,RLVECT_2:def 3;
end;
assume X is Linear_Combination of T;
then reconsider L = X as Linear_Combination of T;
consider S be finite Subset of T such that
A2: for v be Element of T st not v in S
holds L.v = 0 by RLVECT_2:def 3;
for v be Element of RLSp2RVSp(T) st not v in S
holds 0. F_Real = L.v by A2;
hence X is Linear_Combination of RLSp2RVSp(T) by VECTSP_6:def 1;
end;
theorem Th73:
for T be RealLinearSpace,
Lv be Linear_Combination of RLSp2RVSp(T),
Lr be Linear_Combination of T
st Lr = Lv
holds Carrier Lr = Carrier Lv
proof
let T be RealLinearSpace,
Lv be Linear_Combination of RLSp2RVSp(T),
Lr be Linear_Combination of T;
assume
A1: Lr = Lv;
thus Carrier Lr c= Carrier Lv
proof
let x be object;
assume
A2: x in Carrier Lr;
then reconsider v = x as Element of T;
reconsider u = v as Element of RLSp2RVSp(T);
Lv.u <> 0. F_Real by A1,A2,RLVECT_2:19;
hence x in Carrier Lv by VECTSP_6:1;
end;
let x be object;
assume x in Carrier Lv;
then consider u be Element of RLSp2RVSp(T) such that
A3: x = u and
A4: Lv.u <> 0. F_Real by VECTSP_6:1;
thus x in Carrier Lr by A1,A4,RLVECT_2:19,A3;
end;
theorem Th74:
for V be RealLinearSpace,
Fr be FinSequence of V,
fr be Function of V,REAL,
Fv be FinSequence of RLSp2RVSp(V),
fv be Function of RLSp2RVSp(V),F_Real
st fr = fv & Fr = Fv
holds fr(#)Fr = fv(#)Fv
proof
let V be RealLinearSpace,
Fr be FinSequence of V,
fr be Function of V,REAL,
Fv be FinSequence of RLSp2RVSp(V),
fv be Function of RLSp2RVSp(V),F_Real;
assume
A1: fr = fv & Fr = Fv; then
A2: len (fv(#)Fv) = len Fr by VECTSP_6:def 5;
for i be Nat st i in dom (fv(#)Fv) holds
(fv(#)Fv) . i = (fr . (Fr /. i)) * (Fr /. i)
proof
let i be Nat;
assume i in dom (fv(#)Fv);
hence (fv(#)Fv) . i
= (fv . (Fv /. i)) * (Fv /. i) by VECTSP_6:def 5
.= (fr . (Fr /. i)) * (Fr /. i) by A1;
end;
hence thesis by A2,RLVECT_2:def 7;
end;
theorem
for T be RealLinearSpace,
Ft be FinSequence of T,
Fr be FinSequence of RLSp2RVSp(T)
st Ft = Fr
holds Sum Ft = Sum Fr;
theorem Th76:
for T be RealLinearSpace,
Lv be Linear_Combination of RLSp2RVSp(T),
Lr be Linear_Combination of T
st Lr = Lv
holds Sum Lr = Sum Lv
proof
let T be RealLinearSpace;
let Lv be Linear_Combination of RLSp2RVSp(T);
let Lr be Linear_Combination of T;
assume
A1: Lr = Lv;
consider F be FinSequence of the carrier of T such that
A2: F is one-to-one & rng F = Carrier Lr and
A3: Sum Lr = Sum(Lr (#) F) by RLVECT_2:def 8;
reconsider F1 = F as FinSequence of the carrier of RLSp2RVSp(T);
Carrier Lr = Carrier Lv by A1,Th73;
hence Sum Lv = Sum (Lv (#) F1) by A2,VECTSP_6:def 6
.= Sum Lr by A1,A3,Th74;
end;
theorem Th77:
for T be RealLinearSpace,
Af be Subset of RLSp2RVSp(T),
Ar be Subset of T
st Af = Ar
holds [#] (Lin Ar) = [#] (Lin Af)
proof
let T be RealLinearSpace;
let Af be Subset of RLSp2RVSp(T);
let Ar be Subset of T;
assume
A1: Af = Ar;
hereby
let x be object;
assume x in [#] (Lin Ar);
then x in Lin Ar;
then consider L be Linear_Combination of Ar such that
A2: x = Sum L by RLVECT_3:14;
reconsider L1 = L as Linear_Combination of RLSp2RVSp(T) by Th72;
Carrier L1 = Carrier L & Carrier L c= Ar
by Th73,RLVECT_2:def 6; then
A3: L1 is Linear_Combination of Af by A1,VECTSP_6:def 4;
Sum L1 = Sum L by Th76;
then x in Lin Af by A2,A3,VECTSP_7:7;
hence x in [#] (Lin Af);
end;
let x be object;
assume x in [#] (Lin Af);
then x in Lin Af;
then consider L be Linear_Combination of Af such that
A4: x = Sum L by VECTSP_7:7;
reconsider L1 = L as Linear_Combination of T by Th72;
Carrier L1 = Carrier L & Carrier L c= Af by Th73,VECTSP_6:def 4; then
A5: L1 is Linear_Combination of Ar by A1,RLVECT_2:def 6;
Sum L1 = Sum L by Th76;
then x in Lin Ar by A4,A5,RLVECT_3:14;
hence x in [#] (Lin Ar);
end;
theorem Th78:
for T be RealLinearSpace,
Af be Subset of RLSp2RVSp(T),
Ar be Subset of T
st Af = Ar
holds
Af is linearly-independent
iff
Ar is linearly-independent
proof
let T be RealLinearSpace;
let AV be Subset of RLSp2RVSp(T);
let AR be Subset of T;
assume
A1: AV = AR;
hereby
assume
A2: AV is linearly-independent;
now
let L be Linear_Combination of AR;
reconsider L1 = L as Linear_Combination of RLSp2RVSp(T) by Th72;
A3: Carrier L1 = Carrier L by Th73;
assume Sum L = 0.T; then
A4: 0. (RLSp2RVSp(T)) = Sum L1 by Th76;
L1 is Linear_Combination of AV
by A1,A3,RLVECT_2:def 6,VECTSP_6:def 4;
hence Carrier L = {} by A2,A3,A4,VECTSP_7:def 1;
end;
hence AR is linearly-independent by RLVECT_3:def 1;
end;
assume
A5: AR is linearly-independent;
now
let L be Linear_Combination of AV;
reconsider L1 = L as Linear_Combination of T by Th72;
A6: Carrier L1 = Carrier L by Th73;
reconsider L1 as Linear_Combination of AR
by VECTSP_6:def 4,A1, A6, RLVECT_2:def 6;
assume Sum L = 0. (RLSp2RVSp(T));
then 0. T = Sum L1 by Th76;
hence Carrier L = {} by A5, A6, RLVECT_3:def 1;
end;
hence AV is linearly-independent by VECTSP_7:def 1;
end;
theorem
for T be RealLinearSpace
for X be set
for U be Subspace of RLSp2RVSp(T)
for W be Subspace of T
st [#] U = [#] W
holds
X is Linear_Combination of U
iff
X is Linear_Combination of W
proof
let T be RealLinearSpace;
let X be set;
let U be Subspace of RLSp2RVSp(T);
let W be Subspace of T;
assume
A1: [#] U = [#] W;
hereby
assume X is Linear_Combination of U;
then reconsider L = X as Linear_Combination of U;
ex S be finite Subset of U
st for v be Element of U st not v in S
holds L.v = 0. F_Real by VECTSP_6:def 1;
hence X is Linear_Combination of W by A1,RLVECT_2:def 3;
end;
assume X is Linear_Combination of W;
then reconsider L = X as Linear_Combination of W;
consider S be finite Subset of W such that
A2: for v be Element of W st not v in S
holds L.v = 0 by RLVECT_2:def 3;
for v be Element of U st not v in S
holds 0. F_Real = L.v by A1, A2;
hence X is Linear_Combination of U by A1, VECTSP_6:def 1;
end;
theorem Th80:
for W be RealLinearSpace,
X be set
holds
X is Basis of RLSp2RVSp(W)
iff
X is Basis of W
proof
let W be RealLinearSpace,
X be set;
set V = RLSp2RVSp(W);
hereby
assume X is Basis of V;
then reconsider A = X as Basis of V;
reconsider B = A as Subset of W;
A is linearly-independent
&
Lin A = ModuleStr(# the carrier of V,
the addF of V,
the ZeroF of V,
the lmult of V #) by VECTSP_7:def 3;
then
A1: B is linearly-independent by Th78;
set W0 = Lin B;
A2: the carrier of W0 c= the carrier of W
& 0. W0 = 0. W
& the addF of W0 = (the addF of W) || (the carrier of W0)
& the Mult of W0 = (the Mult of W) | [:REAL, the carrier of W0:]
by RLSUB_1:def 2;
A3: the carrier of W0
= [#] W0
.= [#] Lin A by Th77
.= the carrier of W by VECTSP_7:def 3;
thus X is Basis of W by A2,A3,A1,RLVECT_3:def 3;
end;
assume X is Basis of W; then
reconsider A = X as Basis of W;
reconsider B = A as Subset of V;
A4: A is linearly-independent
& Lin A = RLSStruct(# the carrier of W,
the ZeroF of W,
the addF of W,
the Mult of W #) by RLVECT_3:def 3;
then
A5: B is linearly-independent by Th78;
set V0 = Lin B;
A6: the carrier of V0 c= the carrier of V
& 0. V0 = 0. V
& the addF of V0 = (the addF of V) || the carrier of V0
& the lmult of V0 = (the lmult of V) |
[: the carrier of F_Real, the carrier of V0:] by VECTSP_4:def 2;
the carrier of V0
= [#] V0
.= [#] Lin A by Th77
.= the carrier of V by A4;
hence X is Basis of V by A5,A6,VECTSP_7:def 3;
end;
theorem Th81:
for W be RealLinearSpace
st W is finite-dimensional
holds
RLSp2RVSp(W) is finite-dimensional
&
dim RLSp2RVSp(W) = dim W
proof
let W be RealLinearSpace;
assume
A1: W is finite-dimensional;
then consider A be finite Subset of W such that
A2: A is Basis of W by RLVECT_5:def 1;
reconsider B = A as finite Subset of RLSp2RVSp(W);
A3: B is Basis of RLSp2RVSp(W) by A2,Th80;
thus RLSp2RVSp (W) is finite-dimensional by A2,Th80;
hence dim RLSp2RVSp (W)
= card B by A3,VECTSP_9:def 1
.= dim W by A1,A2,RLVECT_5:def 2;
end;
theorem
for W be RealLinearSpace holds
W is finite-dimensional
iff
RLSp2RVSp(W) is finite-dimensional
proof
let W be RealLinearSpace;
hereby
assume W is finite-dimensional;
then ex A be finite Subset of W st
A is Basis of W by RLVECT_5:def 1;
hence RLSp2RVSp(W) is finite-dimensional by Th80;
end;
thus thesis by Th80,RLVECT_5:def 1;
end;
theorem Th83:
for n be non empty Nat
holds
RLSp2RVSp(RealVectSpace(Seg n)) = n -VectSp_over F_Real
proof
let n be non empty Nat;
set X = RealVectSpace(Seg n);
set V = n -VectSp_over F_Real;
set W = TOP-REAL n;
A1: n -Group_over F_Real
= addLoopStr(# n -tuples_on the carrier of F_Real,
product(the addF of F_Real, n),
n |-> (0. F_Real) #) by PRVECT_1:def 3;
A2: addLoopStr(# the carrier of V,
the addF of V,
the ZeroF of V #)
= n -Group_over F_Real
& the lmult of V = n -Mult_over F_Real by PRVECT_1:def 5;
A3: RLSStruct(# the carrier of W,
the ZeroF of W,
the addF of W,
the Mult of W #)
= X by EUCLID:def 8;
A5: 0.(RLSp2RVSp X)
= 0. (TOP-REAL n) by A3
.= 0*n by EUCLID:70
.= 0.(n -VectSp_over F_Real) by A1,A2;
A6: the addF of (RLSp2RVSp X)
= the addF of (n -VectSp_over F_Real) by A1,A2,Th51;
the lmult of (RLSp2RVSp X)
= n -Mult_over F_Real by Th52
.= the lmult of (n -VectSp_over F_Real) by PRVECT_1:def 5;
hence thesis by A3,A5,A6,Lm1;
end;
theorem Th84:
for V,W be RealLinearSpace,
X be set
holds
X is LinearOperator of V,W
iff
X is linear-transformation of RLSp2RVSp(V),RLSp2RVSp(W)
proof
let V,W be RealLinearSpace,
X be set;
hereby
assume X is LinearOperator of V,W; then
reconsider T = X as LinearOperator of V,W;
reconsider f = T as Function of RLSp2RVSp(V),RLSp2RVSp(W);
for x, y be Element of RLSp2RVSp(V)
holds f . (x + y) = (f . x) + (f . y)
proof
let x, y be Element of RLSp2RVSp (V);
A1: T is additive;
reconsider x0 = x, y0 = y as Element of V;
thus f . (x + y) = T.(x0 + y0)
.= (T.x0) + (T.y0) by A1
.= f.x + f.y;
end;
then
A2: f is additive;
for a be Scalar of F_Real
for x be Vector of RLSp2RVSp(V)
holds f . (a * x) = a * (f . x)
proof
let a be Scalar of F_Real;
let x be Element of RLSp2RVSp (V);
reconsider x0 = x as Element of V;
reconsider a0 = a as Element of REAL;
thus f.(a * x)
= T.(a0 * x0)
.= a0 * T.x0 by LOPBAN_1:def 5
.= a * f.x;
end;
hence X is linear-transformation of RLSp2RVSp(V),RLSp2RVSp(W)
by MOD_2:def 2,A2;
end;
assume X is linear-transformation of RLSp2RVSp(V),RLSp2RVSp(W); then
reconsider T = X as linear-transformation of RLSp2RVSp(V),RLSp2RVSp(W);
reconsider f = T as Function of V,W;
for x, y be Element of V
holds f . (x + y) = (f . x) + (f . y)
proof
let x, y be Element of V;
A3: T is additive;
reconsider x0 = x, y0 = y as Element of RLSp2RVSp(V);
thus f . (x + y)
= T.(x0 + y0)
.= (T.x0) + (T.y0) by A3
.= f.x + f.y;
end;
then
A4: f is additive;
for a be Real,
x be VECTOR of V
holds f . (a * x) = a * (f . x)
proof
let a be Real;
let x be VECTOR of V;
reconsider x0 = x as Element of RLSp2RVSp (V);
reconsider a0 = a as Element of F_Real by XREAL_0:def 1;
thus f.(a * x)
= T.(a0 * x0)
.= a0 * T.x0 by MOD_2:def 2
.= a * f.x;
end;
then f is homogeneous;
hence X is LinearOperator of V,W by A4;
end;
theorem Th85:
for X, Y be RealLinearSpace,
L be LinearOperator of X,Y
st L is bijective
holds
ex K be LinearOperator of Y,X
st K = L" & K is one-to-one onto
proof
let X, Y be RealLinearSpace;
let L be LinearOperator of X,Y;
assume
A1: L is bijective;
then
A2: rng L = the carrier of Y by FUNCT_2:def 3;
then reconsider K = L" as Function of the carrier of Y,the carrier of X
by A1,FUNCT_2:25;
A3: dom L = the carrier of X by FUNCT_2:def 1;
A4: K is additive
proof
let x, y be Element of Y;
consider a be Element of X such that
A5: x = L . a by A2,FUNCT_2:113;
consider b be Element of X such that
A6: y = L . b by A2,FUNCT_2:113;
A7: K . x = a by A1,A3,A5,FUNCT_1:34;
A8: K . y = b by A1,A3,A6,FUNCT_1:34;
x + y = L . (a + b) by A5,A6,VECTSP_1:def 20;
hence K . (x + y) = (K . x) + (K . y) by A1,A3,A7,A8,FUNCT_1:34;
end;
for x be VECTOR of Y
for r be Real
holds K . (r * x) = r * (K . x)
proof
let x be VECTOR of Y;
let r be Real;
consider a be VECTOR of X such that
A9: x = L . a by A2,FUNCT_2:113;
A10: K . x = a by A1,A3,A9,FUNCT_1:34;
r * x = L . (r * a) by A9,LOPBAN_1:def 5;
hence K . (r * x) = r * (K . x) by A1,A3,A10,FUNCT_1:34;
end;
then reconsider K as LinearOperator of Y,X by A4,LOPBAN_1:def 5;
take K;
rng K = the carrier of X by A1,A3,FUNCT_1:33;
hence K = L " & K is one-to-one onto by A1,FUNCT_2:def 3;
end;
theorem Th86:
for X,Y,Z be RealLinearSpace,
L be LinearOperator of X,Y,
K be LinearOperator of Y,Z
holds K*L is LinearOperator of X,Z
proof
let X,Y,Z be RealLinearSpace,
L be LinearOperator of X,Y,
K be LinearOperator of Y,Z;
reconsider T = K*L as Function of X,Z;
for x, y be Element of X
holds T . (x + y) = (T . x) + (T . y)
proof
let x, y be Element of X;
A1: L is additive;
A2: K is additive;
thus T.(x + y)
= K.(L.(x + y)) by FUNCT_2:15
.= K.(L.x + L.y) by A1
.= K.(L.x) + K.(L.y) by A2
.= T.x + K.(L.y) by FUNCT_2:15
.= T.x + T.y by FUNCT_2:15;
end;
then
A3: T is additive;
for a be Real,
x be VECTOR of X
holds T . (a * x) = a * (T . x)
proof
let a be Real;
let x be VECTOR of X;
thus T . (a * x)
= K.(L.(a * x)) by FUNCT_2:15
.= K.(a * L.x) by LOPBAN_1:def 5
.= a * K.(L.x) by LOPBAN_1:def 5
.= a * T.x by FUNCT_2:15;
end;
then
T is homogeneous;
hence K * L is LinearOperator of X,Z by A3;
end;
theorem Th87:
for V,W be RealLinearSpace,
A be Subset of V,
T be LinearOperator of V,W
st T is bijective
holds
A is Basis of V
iff
T.:A is Basis of W
proof
let V,W be RealLinearSpace;
let A be Subset of V;
let T be LinearOperator of V,W;
assume
A1: T is bijective;
reconsider S = T as linear-transformation of RLSp2RVSp(V),RLSp2RVSp(W)
by Th84;
reconsider B = A as Subset of RLSp2RVSp(V);
B is Basis of RLSp2RVSp(V)
iff
S .: B is Basis of RLSp2RVSp(W) by VECTSP12:2,A1;
hence thesis by Th80;
end;
theorem Th88:
for V be finite-dimensional RealLinearSpace,
W be RealLinearSpace
st (ex T be LinearOperator of V,W
st T is bijective)
holds
W is finite-dimensional
&
dim W = dim V
proof
let V be finite-dimensional RealLinearSpace,
W be RealLinearSpace;
given T be LinearOperator of V,W such that
A1: T is bijective;
consider A be finite Subset of V such that
A2: A is Basis of V by RLVECT_5:def 1;
A3: dom T = the carrier of V by FUNCT_2:def 1;
A4: T.:A is Basis of W by A1,A2,Th87;
hence W is finite-dimensional by RLVECT_5:def 1;
hence dim W
= card (T.:A) by A4,RLVECT_5:def 2
.= card A by A1,A3,CARD_1:5,CARD_1:33
.= dim V by A2,RLVECT_5:def 2;
end;
theorem Th89:
for V be finite-dimensional RealLinearSpace
st dim V <> 0
ex T be LinearOperator of V, RealVectSpace(Seg(dim V))
st T is bijective
proof
let V be finite-dimensional RealLinearSpace;
assume
A1: dim V <> 0;
RLSp2RVSp(V) is finite-dimensional
&
dim RLSp2RVSp(V) = dim V by Th81; then
consider T be linear-transformation
of RLSp2RVSp(V), (dim V) -VectSp_over F_Real
such that
A2: T is bijective by Th64;
(dim V) -VectSp_over F_Real
= RLSp2RVSp(RealVectSpace(Seg(dim V))) by Th83,A1;
then
reconsider S = T as LinearOperator of V,RealVectSpace(Seg(dim V)) by Th84;
take S;
the carrier of RealVectSpace(Seg(dim V))
= the carrier of (RLSp2RVSp(RealVectSpace(Seg(dim V))))
.= the carrier of ((dim V) -VectSp_over F_Real) by Th83,A1;
hence S is bijective by A2;
end;
theorem
for V,W be finite-dimensional RealLinearSpace
st dim V <> 0
holds
dim V = dim W
iff
ex T be LinearOperator of V, W st T is bijective
proof
let V,W be finite-dimensional RealLinearSpace;
assume A1: dim V <> 0;
hereby
assume
A2: dim V = dim W;
consider T1 be LinearOperator of V,
RealVectSpace Seg dim V such that
A3: T1 is bijective by A1,Th89;
consider T2 be LinearOperator of W,
RealVectSpace Seg dim V such that
A4: T2 is bijective by A1,A2,Th89;
consider S be LinearOperator of RealVectSpace(Seg(dim V)),W such that
A5: S = T2 " & S is one-to-one onto by A4,Th85;
set T = S * T1;
reconsider T as LinearOperator of V,W by Th86;
T is bijective by A3,A5,FINSEQ_4:85;
hence ex T be LinearOperator of V,W
st T is bijective;
end;
assume ex T be LinearOperator of V, W st T is bijective;
hence dim V = dim W by Th88;
end;