:: Linear Independence in Left Module over Domain
:: by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990-2013 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 FUNCSDOM, VECTSP_2, VECTSP_1, SUBSET_1, XBOOLE_0, ALGSTR_0,
RLVECT_3, RLVECT_2, CARD_3, SUPINF_2, TARSKI, MESFUNC1, FUNCT_1,
STRUCT_0, FUNCT_2, FINSET_1, RELAT_1, FINSEQ_1, VALUED_1, NAT_1,
FINSEQ_4, NUMBERS, PARTFUN1, RLSUB_1, ARYTM_3;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, NAT_1,
FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_4,
DOMAIN_1, STRUCT_0, ALGSTR_0, RLVECT_1, VECTSP_1, VECTSP_2, VECTSP_4,
VECTSP_5, VECTSP_6;
constructors PARTFUN1, DOMAIN_1, FINSEQ_4, VECTSP_2, VECTSP_5,
VECTSP_6, RELSET_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, STRUCT_0,
VECTSP_1, VECTSP_4, ORDINAL1;
requirements SUBSET, BOOLE;
definitions XBOOLE_0, TARSKI, VECTSP_4, VECTSP_6;
equalities VECTSP_4, VECTSP_6;
expansions XBOOLE_0, TARSKI;
theorems TARSKI, ZFMISC_1, RLVECT_1, VECTSP_1, VECTSP_6, FUNCT_2, VECTSP_4,
VECTSP_5, XBOOLE_0, XBOOLE_1, VECTSP_2, FINSEQ_1, FINSEQ_3, FUNCT_1,
FINSEQ_4, RELAT_1, RLVECT_2, FINSEQ_2, STRUCT_0, PARTFUN1;
schemes FUNCT_2, FINSEQ_1;
begin
reserve x for set,
R for Ring,
V for LeftMod of R,
v,v1,v2 for Vector of V,
A, B for Subset of V;
definition
let R be non empty doubleLoopStr;
let V be non empty VectSpStr over R;
let IT be Subset of V;
attr IT is linearly-independent means
for l be Linear_Combination of IT st Sum(l) = 0.V holds Carrier(l) = {};
end;
notation
let R be non empty doubleLoopStr;
let V be non empty VectSpStr over R;
let IT be Subset of V;
antonym IT is linearly-dependent for IT is linearly-independent;
end;
theorem
A c= B & B is linearly-independent implies A is linearly-independent
proof
assume that
A1: A c= B and
A2: B is linearly-independent;
let l be Linear_Combination of A;
reconsider L = l as Linear_Combination of B by A1,VECTSP_6:4;
assume Sum(l) = 0.V;
then Carrier(L) = {} by A2;
hence thesis;
end;
theorem Th2:
0.R <> 1.R & A is linearly-independent implies not 0.V in A
proof
assume that
A1: 0.R <> 1.R and
A2: A is linearly-independent and
A3: 0.V in A;
deffunc U(set) = 0.R;
consider f be Function of the carrier of V, the carrier of R such that
A4: f.(0.V) = 1.R and
A5: for v be Element of V st v <> 0.V holds f.v = U(v) from FUNCT_2:sch
6;
reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
ex T be finite Subset of V st for v st not v in T holds f.v = 0.R
proof
take T = {0.V};
let v;
assume not v in T;
then v <> 0.V by TARSKI:def 1;
hence thesis by A5;
end;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
A6: Carrier(f) = {0.V}
proof
thus Carrier(f) c= {0.V}
proof
let x be object;
assume x in Carrier(f);
then consider v such that
A7: v = x and
A8: f.v <> 0.R;
v = 0.V by A5,A8;
hence thesis by A7,TARSKI:def 1;
end;
let x be object;
assume x in {0.V};
then x = 0.V by TARSKI:def 1;
hence thesis by A1,A4;
end;
then Carrier(f) c= A by A3,ZFMISC_1:31;
then reconsider f as Linear_Combination of A by VECTSP_6:def 4;
Sum(f) = f.(0.V) * 0.V by A6,VECTSP_6:20
.= 0.V by VECTSP_1:14;
hence contradiction by A2,A6;
end;
theorem
{}(the carrier of V) is linearly-independent
proof
let l be Linear_Combination of {}(the carrier of V);
Carrier(l) c= {} by VECTSP_6:def 4;
hence thesis;
end;
theorem Th4:
0.R <> 1.R & {v1,v2} is linearly-independent implies v1 <> 0.V & v2 <> 0.V
proof
A1: v1 in {v1,v2} & v2 in {v1,v2} by TARSKI:def 2;
assume 0.R <> 1.R & {v1,v2} is linearly-independent;
hence thesis by A1,Th2;
end;
theorem
0.R <> 1.R implies {v,0.V} is linearly-dependent & {0.V,v} is
linearly-dependent by Th4;
theorem Th6:
for R being domRing, V being LeftMod of R, L being
Linear_Combination of V, a being Scalar of R holds a <> 0.R implies Carrier(a *
L) = Carrier(L)
proof
let R be domRing, V be LeftMod of R, L be Linear_Combination of V, a be
Scalar of R;
set T = {u where u is Vector of V : (a * L).u <> 0.R};
set S = {v where v is Vector of V : L.v <> 0.R};
assume
A1: a <> 0.R;
T = S
proof
thus T c= S
proof
let x be object;
assume x in T;
then consider u be Vector of V such that
A2: x = u and
A3: (a * L).u <> 0.R;
(a * L).u = a * L.u by VECTSP_6:def 9;
then L.u <> 0.R by A3;
hence thesis by A2;
end;
let x be object;
assume x in S;
then consider v be Vector of V such that
A4: x = v and
A5: L.v <> 0.R;
(a * L).v = a * L.v by VECTSP_6:def 9;
then (a * L).v <> 0.R by A1,A5,VECTSP_2:def 1;
hence thesis by A4;
end;
hence thesis;
end;
theorem Th7:
for R being domRing, V being LeftMod of R, L being
Linear_Combination of V, a being Scalar of R holds Sum(a * L) = a * Sum(L)
proof
let R be domRing, V be LeftMod of R, L be Linear_Combination of V, a be
Scalar of R;
per cases;
suppose
A1: a <> 0.R;
set l = a * L;
A2: Carrier(l) = Carrier(L) by A1,Th6;
consider G be FinSequence of the carrier of V such that
A3: G is one-to-one and
A4: rng G = Carrier(L) and
A5: Sum(L) = Sum(L (#) G) by VECTSP_6:def 6;
set g = L (#) G;
consider F be FinSequence of the carrier of V such that
A6: F is one-to-one and
A7: rng F = Carrier(a * L) and
A8: Sum(a * L) = Sum((a * L) (#) F) by VECTSP_6:def 6;
A9: len G = len F by A1,A6,A7,A3,A4,Th6,FINSEQ_1:48;
set f = (a * L) (#) F;
deffunc U(Nat) = F <- (G.$1);
consider P be FinSequence such that
A10: len P = len F and
A11: for k be Nat st k in dom P holds P.k = U(k) from FINSEQ_1:sch 2;
A12: Seg len F = dom F & dom P = dom F by A10,FINSEQ_1:def 3,FINSEQ_3:29;
A13: now
let x be object;
assume
A14: x in dom G;
then reconsider n = x as Element of NAT;
G.n in rng F by A7,A4,A2,A14,FUNCT_1:def 3;
then
A15: F just_once_values G.n by A6,FINSEQ_4:8;
n in Seg len F by A9,A14,FINSEQ_1:def 3;
then F.(P.n) = F.(F <- (G.n)) by A11,A12
.= G.n by A15,FINSEQ_4:def 3;
hence G.x = F.(P.x);
end;
A16: rng P c= dom F
proof
let x be object;
assume x in rng P;
then consider y be object such that
A17: y in dom P and
A18: P.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A17;
y in dom G by A10,A9,A17,FINSEQ_3:29;
then G.y in rng F by A7,A4,A2,FUNCT_1:def 3;
then
A19: F just_once_values G.y by A6,FINSEQ_4:8;
P.y = F <- (G.y) by A11,A17;
hence thesis by A18,A19,FINSEQ_4:def 3;
end;
now
let x be object;
thus x in dom G implies x in dom P & P.x in dom F
proof
assume x in dom G;
hence x in dom P by A10,A9,FINSEQ_3:29;
then P.x in rng P by FUNCT_1:def 3;
hence thesis by A16;
end;
assume that
A20: x in dom P and
P.x in dom F;
thus x in dom G by A10,A9,A20,FINSEQ_3:29;
end;
then
A21: G = F * P by A13,FUNCT_1:10;
dom F c= rng P
proof
set f = F" * G;
let x be object;
assume
A22: x in dom F;
dom(F") = rng G by A6,A7,A4,A2,FUNCT_1:33;
then
A23: rng f = rng(F") by RELAT_1:28
.= dom F by A6,FUNCT_1:33;
f = F " * F * P by A21,RELAT_1:36
.= id(dom F) * P by A6,FUNCT_1:39
.= P by A16,RELAT_1:53;
hence thesis by A22,A23;
end;
then
A24: dom F = rng P by A16;
A25: dom P = dom F by A10,FINSEQ_3:29;
then
A26: P is one-to-one by A24,FINSEQ_4:60;
reconsider P as Function of dom F, dom F by A16,A25,FUNCT_2:2;
A27: len f = len F by VECTSP_6:def 5;
then
A28: dom f = dom F by FINSEQ_3:29;
then reconsider P as Function of dom f, dom f;
reconsider Fp = f * P as FinSequence of the carrier of V by FINSEQ_2:47;
reconsider P as Permutation of dom f by A24,A26,A28,FUNCT_2:57;
A29: Fp = f * P;
then
A30: len Fp = len f by FINSEQ_2:44;
then
A31: len Fp = len g by A9,A27,VECTSP_6:def 5;
A32: now
let k be Nat;
let v be Vector of V;
assume that
A33: k in dom Fp and
A34: v = g.k;
A35: k in Seg(len g) by A31,A33,FINSEQ_1:def 3;
then
A36: k in dom P by A10,A27,A30,A31,FINSEQ_1:def 3;
A37: k in dom G by A9,A27,A30,A31,A35,FINSEQ_1:def 3;
then G.k in rng G by FUNCT_1:def 3;
then F just_once_values G.k by A6,A7,A4,A2,FINSEQ_4:8;
then
A38: (F <- (G.k)) in dom F by FINSEQ_4:def 3;
then reconsider i = F <- (G.k) as Element of NAT;
A39: G/.k = G.k by A37,PARTFUN1:def 6
.= F.(P.k) by A21,A36,FUNCT_1:13
.= F.i by A11,A12,A27,A30,A31,A35
.= F/.i by A38,PARTFUN1:def 6;
A40: k in dom g by A35,FINSEQ_1:def 3;
i in Seg(len f) by A27,A38,FINSEQ_1:def 3;
then
A41: i in dom f by FINSEQ_1:def 3;
thus Fp.k = f.(P.k) by A36,FUNCT_1:13
.= f.(F <- (G.k)) by A11,A12,A27,A30,A31,A35
.= l.(F/.i) * (F/.i) by A41,VECTSP_6:def 5
.= a * L.(F/.i) * (F/.i) by VECTSP_6:def 9
.= a * (L.(F/.i) * (F/.i)) by VECTSP_1:def 16
.= a * v by A34,A40,A39,VECTSP_6:def 5;
end;
Sum(Fp) = Sum(f) by A29,RLVECT_2:7;
hence thesis by A8,A5,A31,A32,RLVECT_2:66;
end;
suppose
A42: a = 0.R;
hence Sum(a * L) = Sum(ZeroLC(V)) by VECTSP_6:30
.= 0.V by VECTSP_6:15
.= a * Sum(L) by A42,VECTSP_1:14;
end;
end;
reserve R for domRing,
V for LeftMod of R,
A,B for Subset of V,
l for Linear_Combination of A,
f,g for Function of the carrier of V, the carrier of R;
definition
let R;
let V;
let A;
func Lin(A) -> strict Subspace of V means
:Def2:
the carrier of it = the set of all Sum(l) ;
existence
proof
set A1 = the set of all Sum(l) ;
A1 c= the carrier of V
proof
let x be object;
assume x in A1;
then ex l st x = Sum(l);
hence thesis;
end;
then reconsider A1 as Subset of V;
reconsider l = ZeroLC(V) as Linear_Combination of A by VECTSP_6:5;
A1: A1 is linearly-closed
proof
thus for v,u be Vector of V st v in A1 & u in A1 holds v + u in A1
proof
let v,u be Vector of V;
assume that
A2: v in A1 and
A3: u in A1;
consider l1 being Linear_Combination of A such that
A4: v = Sum(l1) by A2;
consider l2 being Linear_Combination of A such that
A5: u = Sum(l2) by A3;
reconsider f = l1 + l2 as Linear_Combination of A by VECTSP_6:24;
v + u = Sum(f) by A4,A5,VECTSP_6:44;
hence thesis;
end;
let a be Scalar of R;
let v be Vector of V;
assume v in A1;
then consider l such that
A6: v = Sum(l);
reconsider f = a * l as Linear_Combination of A by VECTSP_6:31;
a * v = Sum(f) by A6,Th7;
hence thesis;
end;
Sum(l) = 0.V by VECTSP_6:15;
then 0.V in A1;
hence thesis by A1,VECTSP_4:34;
end;
uniqueness by VECTSP_4:29;
end;
theorem Th8:
x in Lin(A) iff ex l st x = Sum(l)
proof
thus x in Lin(A) implies ex l st x = Sum(l)
proof
assume x in Lin(A);
then x in the carrier of Lin(A) by STRUCT_0:def 5;
then x in the set of all Sum(l) by Def2;
hence thesis;
end;
given k being Linear_Combination of A such that
A1: x = Sum(k);
x in the set of all Sum(l) by A1;
then x in the carrier of Lin(A) by Def2;
hence thesis by STRUCT_0:def 5;
end;
theorem Th9:
x in A implies x in Lin(A)
proof
deffunc U(set) = 0.R;
assume
A1: x in A;
then reconsider v = x as Vector of V;
consider f being Function of the carrier of V, the carrier of R such that
A2: f.v = 1.R and
A3: for u be Vector of V st u <> v holds f.u = U(u) from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
ex T be finite Subset of V st for u be Vector of V st not u in T holds f
.u = 0.R
proof
take T = {v};
let u be Vector of V;
assume not u in T;
then u <> v by TARSKI:def 1;
hence thesis by A3;
end;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
A4: Carrier(f) c= {v}
proof
let x be object;
assume x in Carrier(f);
then consider u be Vector of V such that
A5: x = u and
A6: f.u <> 0.R;
u = v by A3,A6;
hence thesis by A5,TARSKI:def 1;
end;
then reconsider f as Linear_Combination of {v} by VECTSP_6:def 4;
A7: Sum(f) = 1.R * v by A2,VECTSP_6:17
.= v by VECTSP_1:def 17;
{v} c= A by A1,ZFMISC_1:31;
then Carrier(f) c= A by A4;
then reconsider f as Linear_Combination of A by VECTSP_6:def 4;
Sum(f) = v by A7;
hence thesis by Th8;
end;
theorem
Lin({}(the carrier of V)) = (0).V
proof
set A = Lin({}(the carrier of V));
now
let v be Vector of V;
thus v in A implies v in (0).V
proof
assume v in A;
then
A1: v in the carrier of A by STRUCT_0:def 5;
the carrier of A = the set of all
Sum(l0) where l0 is Linear_Combination of {}(the
carrier of V) by Def2;
then
ex l0 be Linear_Combination of {}(the carrier of V) st v = Sum (l0)
by A1;
then v = 0.V by VECTSP_6:16;
hence thesis by VECTSP_4:35;
end;
assume v in (0).V;
then v = 0.V by VECTSP_4:35;
hence v in A by VECTSP_4:17;
end;
hence thesis by VECTSP_4:30;
end;
theorem
Lin(A) = (0).V implies A = {} or A = {0.V}
proof
assume that
A1: Lin(A) = (0).V and
A2: A <> {};
thus A c= {0.V}
proof
let x be object;
assume x in A;
then x in Lin(A) by Th9;
then x = 0.V by A1,VECTSP_4:35;
hence thesis by TARSKI:def 1;
end;
set y = the Element of A;
let x be object;
assume x in {0.V};
then
A3: x = 0.V by TARSKI:def 1;
y in A & y in Lin(A) by A2,Th9;
hence thesis by A1,A3,VECTSP_4:35;
end;
theorem Th12:
for W being strict Subspace of V st 0.R <> 1.R & A = the carrier
of W holds Lin(A) = W
proof
let W be strict Subspace of V;
assume that
A1: 0.R <> 1.R and
A2: A = the carrier of W;
now
let v be Vector of V;
thus v in Lin(A) implies v in W
proof
assume v in Lin(A);
then
A3: ex l st v = Sum(l) by Th8;
A is linearly-closed by A2,VECTSP_4:33;
then v in the carrier of W by A1,A2,A3,VECTSP_6:14;
hence thesis by STRUCT_0:def 5;
end;
v in W iff v in the carrier of W by STRUCT_0:def 5;
hence v in W implies v in Lin(A) by A2,Th9;
end;
hence thesis by VECTSP_4:30;
end;
theorem
for V being strict LeftMod of R, A being Subset of V st 0.R <> 1.R & A
= the carrier of V holds Lin(A) = V
proof
let V be strict LeftMod of R, A be Subset of V such that
A1: 0.R <> 1.R;
assume
A2: A = the carrier of V;
(Omega).V = V;
hence thesis by A1,A2,Th12;
end;
theorem Th14:
A c= B implies Lin(A) is Subspace of Lin(B)
proof
assume
A1: A c= B;
now
let v be Vector of V;
assume v in Lin(A);
then consider l such that
A2: v = Sum(l) by Th8;
reconsider l as Linear_Combination of B by A1,VECTSP_6:4;
Sum(l) = v by A2;
hence v in Lin(B) by Th8;
end;
hence thesis by VECTSP_4:28;
end;
theorem
for V being strict LeftMod of R, A,B being Subset of V st Lin(A) = V &
A c= B holds Lin(B) = V
proof
let V be strict LeftMod of R, A,B be Subset of V;
assume Lin(A) = V & A c= B;
then V is Subspace of Lin(B) by Th14;
hence thesis by VECTSP_4:25;
end;
theorem
Lin(A \/ B) = Lin(A) + Lin(B)
proof
now
deffunc V(object) = 0.R;
let v be Vector of V;
assume v in Lin(A \/ B);
then consider l being Linear_Combination of A \/ B such that
A1: v = Sum(l) by Th8;
deffunc U(object) = l.$1;
set D = Carrier(l) \ A;
set C = Carrier(l) /\ A;
defpred X[object] means $1 in C;
A2: now
let x be object;
assume x in the carrier of V;
then reconsider v = x as Vector of V;
f.v in the carrier of R;
hence X[x] implies U(x) in the carrier of R;
assume not X[x];
thus V(x) in the carrier of R;
end;
A3: D c= B
proof
let x be object;
assume x in D;
then
A4: x in Carrier(l) & not x in A by XBOOLE_0:def 5;
Carrier(l) c= A \/ B by VECTSP_6:def 4;
hence thesis by A4,XBOOLE_0:def 3;
end;
consider f being Function of the carrier of V, the carrier of R such that
A5: for x being object st x in the carrier of V
holds (X[x] implies f.x = U(x)) &
(not X[x] implies f.x = V(x)) from FUNCT_2:sch 5(A2);
reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
for u be Vector of V holds not u in C implies f.u = 0.R by A5;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
A6: Carrier(f) c= C
proof
let x be object;
assume x in Carrier(f);
then
A7: ex u be Vector of V st x = u & f.u <> 0.R;
assume not x in C;
hence thesis by A5,A7;
end;
C c= A by XBOOLE_1:17;
then Carrier(f) c= A by A6;
then reconsider f as Linear_Combination of A by VECTSP_6:def 4;
defpred X[object] means $1 in D;
A8: now
let x be object;
assume x in the carrier of V;
then reconsider v = x as Vector of V;
g.v in the carrier of R;
hence X[x] implies U(x) in the carrier of R;
assume not X[x];
thus V(x) in the carrier of R;
end;
consider g being Function of the carrier of V, the carrier of R such that
A9: for x being object st x in the carrier of V
holds (X[x] implies g.x = U(x)) &
(not X[x] implies g.x = V(x)) from FUNCT_2:sch 5(A8);
reconsider g as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
for u be Vector of V holds not u in D implies g.u = 0.R by A9;
then reconsider g as Linear_Combination of V by VECTSP_6:def 1;
Carrier(g) c= D
proof
let x be object;
assume x in Carrier(g);
then
A10: ex u be Vector of V st x = u & g.u <> 0.R;
assume not x in D;
hence thesis by A9,A10;
end;
then Carrier(g) c= B by A3;
then reconsider g as Linear_Combination of B by VECTSP_6:def 4;
l = f + g
proof
let v be Vector of V;
now
per cases;
suppose
A11: v in C;
A12: now
assume v in D;
then not v in A by XBOOLE_0:def 5;
hence contradiction by A11,XBOOLE_0:def 4;
end;
thus (f + g).v = f.v + g.v by VECTSP_6:22
.= l.v + g.v by A5,A11
.= l.v + 0.R by A9,A12
.= l.v by RLVECT_1:4;
end;
suppose
A13: not v in C;
now
per cases;
suppose
A14: v in Carrier(l);
A15: now
assume not v in D;
then not v in Carrier(l) or v in A by XBOOLE_0:def 5;
hence contradiction by A13,A14,XBOOLE_0:def 4;
end;
thus (f + g). v = f.v + g.v by VECTSP_6:22
.= 0.R + g.v by A5,A13
.= g.v by RLVECT_1:4
.= l.v by A9,A15;
end;
suppose
A16: not v in Carrier(l);
then
A17: not v in D by XBOOLE_0:def 5;
A18: not v in C by A16,XBOOLE_0:def 4;
thus (f + g).v = f.v + g.v by VECTSP_6:22
.= 0.R + g.v by A5,A18
.= 0.R + 0.R by A9,A17
.= 0.R by RLVECT_1:4
.= l.v by A16;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then
A19: v = Sum(f) + Sum(g) by A1,VECTSP_6:44;
Sum(f) in Lin(A) & Sum(g) in Lin(B) by Th8;
hence v in Lin(A) + Lin(B) by A19,VECTSP_5:1;
end;
then
A20: Lin(A \/ B) is Subspace of Lin(A) + Lin(B) by VECTSP_4:28;
Lin(A) is Subspace of Lin(A \/ B) & Lin(B) is Subspace of Lin(A \/ B) by Th14
,XBOOLE_1:7;
then Lin(A) + Lin(B) is Subspace of Lin(A \/ B) by VECTSP_5:34;
hence thesis by A20,VECTSP_4:25;
end;
theorem
Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B)
proof
Lin(A /\ B) is Subspace of Lin(A) & Lin(A /\ B) is Subspace of Lin(B) by Th14
,XBOOLE_1:17;
hence thesis by VECTSP_5:19;
end;