:: Basis of Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received July 10, 1990
:: Copyright (c) 1990-2021 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 REAL_1, SUBSET_1, NUMBERS, RLVECT_1, RLSUB_1, FINSET_1, RLVECT_2,
FINSEQ_1, STRUCT_0, FUNCT_1, XBOOLE_0, ORDERS_1, VALUED_1, ORDINAL4,
ARYTM_3, RELAT_1, PARTFUN1, NAT_1, CARD_3, CARD_1, SUPINF_2, FINSEQ_4,
TARSKI, FUNCT_2, ARYTM_1, ZFMISC_1, ORDINAL1, RLVECT_3, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, FINSEQ_1,
RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, ORDERS_1, DOMAIN_1, XCMPLX_0,
XREAL_0, STRUCT_0, RLVECT_1, FINSEQ_4, FINSET_1, REAL_1, RLSUB_1,
RLSUB_2, RLVECT_2, NAT_1;
constructors PARTFUN1, REAL_1, NAT_1, ORDERS_1, FINSEQ_4, REALSET1, RLSUB_2,
RLVECT_2, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, NUMBERS,
STRUCT_0, RLVECT_1, RLSUB_1, ORDINAL1, XREAL_0, RLVECT_2;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin
reserve x,y for object, X,Y,Z for set;
reserve a,b for Real;
reserve k for Element of NAT;
reserve V for RealLinearSpace;
reserve W1,W2,W3 for Subspace of V;
reserve v,v1,v2,u for VECTOR of V;
reserve A,B,C for Subset of V;
reserve T for finite Subset of V;
reserve L,L1,L2 for Linear_Combination of V;
reserve l for Linear_Combination of A;
reserve F,G,H for FinSequence of the carrier of V;
reserve f,g for Function of the carrier of V, REAL;
reserve p,q,r for FinSequence;
reserve M for non empty set;
reserve CF for Choice_Function of M;
theorem :: RLVECT_3:1
Sum(L1 + L2) = Sum(L1) + Sum(L2);
theorem :: RLVECT_3:2
Sum(a * L) = a * Sum(L);
theorem :: RLVECT_3:3
Sum(- L) = - Sum(L);
theorem :: RLVECT_3:4
Sum(L1 - L2) = Sum(L1) - Sum(L2);
definition
let V;
let A;
attr A is linearly-independent means
:: RLVECT_3:def 1
for l st Sum(l) = 0.V holds Carrier(l) = {};
end;
notation
let V;
let A;
antonym A is linearly-dependent for A is linearly-independent;
end;
theorem :: RLVECT_3:5
A c= B & B is linearly-independent implies A is linearly-independent;
theorem :: RLVECT_3:6
A is linearly-independent implies not 0.V in A;
theorem :: RLVECT_3:7
{}(the carrier of V) is linearly-independent;
registration
let V;
cluster linearly-independent for Subset of V;
end;
theorem :: RLVECT_3:8
{v} is linearly-independent iff v <> 0.V;
theorem :: RLVECT_3:9
{0.V} is linearly-dependent;
theorem :: RLVECT_3:10
{v1,v2} is linearly-independent implies v1 <> 0.V & v2 <> 0.V;
theorem :: RLVECT_3:11
{v,0.V} is linearly-dependent & {0.V,v} is linearly-dependent;
theorem :: RLVECT_3:12
v1 <> v2 & {v1,v2} is linearly-independent iff v2 <> 0.V & for a
holds v1 <> a * v2;
theorem :: RLVECT_3:13
v1 <> v2 & {v1,v2} is linearly-independent iff for a,b st a * v1 + b *
v2 = 0.V holds a = 0 & b = 0;
definition
let V;
let A;
func Lin(A) -> strict Subspace of V means
:: RLVECT_3:def 2
the carrier of it = the set of all Sum(l) ;
end;
theorem :: RLVECT_3:14
x in Lin(A) iff ex l st x = Sum(l);
theorem :: RLVECT_3:15
x in A implies x in Lin(A);
reserve l0 for Linear_Combination of {}(the carrier of V);
theorem :: RLVECT_3:16
Lin({}(the carrier of V)) = (0).V;
theorem :: RLVECT_3:17
Lin(A) = (0).V implies A = {} or A = {0.V};
theorem :: RLVECT_3:18
for W being strict Subspace of V holds A = the carrier of W
implies Lin(A) = W;
theorem :: RLVECT_3:19
for V being strict RealLinearSpace,A being Subset of V holds A = the
carrier of V implies Lin(A) = V;
theorem :: RLVECT_3:20
A c= B implies Lin(A) is Subspace of Lin(B);
theorem :: RLVECT_3:21
for V being strict RealLinearSpace,A,B being Subset of V holds Lin(A)
= V & A c= B implies Lin(B) = V;
theorem :: RLVECT_3:22
Lin(A \/ B) = Lin(A) + Lin(B);
theorem :: RLVECT_3:23
Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B);
theorem :: RLVECT_3:24
A is linearly-independent implies ex B st A c= B & B is
linearly-independent & Lin(B) = the RLSStruct of V;
theorem :: RLVECT_3:25
Lin(A) = V implies ex B st B c= A & B is linearly-independent & Lin(B) = V;
definition
let V be RealLinearSpace;
mode Basis of V -> Subset of V means
:: RLVECT_3:def 3
it is linearly-independent & Lin (it) = the RLSStruct of V;
end;
reserve I for Basis of V;
theorem :: RLVECT_3:26
for V being strict RealLinearSpace,A being Subset of V holds A is
linearly-independent implies ex I being Basis of V st A c= I;
theorem :: RLVECT_3:27
Lin(A) = V implies ex I st I c= A;
::
:: Auxiliary theorems.
::
theorem :: RLVECT_3:28
not {} in M implies dom CF = M;
theorem :: RLVECT_3:29
x in (0).V iff x = 0.V;
theorem :: RLVECT_3:30
W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3;
theorem :: RLVECT_3:31
W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of
W2 /\ W3;
theorem :: RLVECT_3:32
W1 is Subspace of W3 & W2 is Subspace of W3 implies W1 + W2 is
Subspace of W3;
theorem :: RLVECT_3:33
W1 is Subspace of W2 implies W1 is Subspace of W2 + W3;
theorem :: RLVECT_3:34
f (#) (F ^ G) = (f (#) F) ^ (f (#) G);