:: The Rank+Nullity Theorem
:: by Jesse Alama
::
:: Received July 31, 2007
:: Copyright (c) 2007-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 FUNCT_1, RELAT_1, TARSKI, STRUCT_0, SUBSET_1, XBOOLE_0, VECTSP_1,
RLVECT_5, FINSET_1, RLVECT_3, LOPBAN_1, ARYTM_3, SUPINF_2, CARD_1,
RLSUB_1, FUNCT_2, ARYTM_1, MESFUNC1, VECTSP10, RLVECT_2, FUNCT_4,
REALSET1, FUNCOP_1, QC_LANG1, CARD_3, RLSUB_2, FINSEQ_1, VALUED_1, NAT_1,
XXREAL_0, PARTFUN1, PBOOLE, RANKNULL, MSSUBFAM, UNIALG_1, RLVECT_1,
ALGSTR_0, FUNCSDOM;
notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, RELAT_1, RELSET_1, FUNCT_1,
ORDINAL1, NAT_1, NUMBERS, FUNCOP_1, PARTFUN1, FUNCT_2, FUNCT_4, XCMPLX_0,
XXREAL_0, CARD_1, FINSET_1, FINSEQ_1, FINSEQOP, STRUCT_0, RLVECT_1,
RLVECT_2, VECTSP_1, FUNCT_7, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7,
MOD_2, MATRLIN, VECTSP_9, LOPBAN_1;
constructors NAT_1, FINSEQOP, HAHNBAN, VECTSP_6, VECTSP_7, MOD_2, VECTSP_9,
REALSET1, RLVECT_2, WELLORD2, LOPBAN_1, VECTSP_5, FUNCT_7, FUNCT_4,
XXREAL_0, MATRLIN, RELSET_1;
registrations RELAT_1, FUNCT_1, STRUCT_0, CARD_1, FINSET_1, VECTSP_9,
XBOOLE_0, MATRLIN, FUNCOP_1, ORDINAL1, XREAL_0, RELSET_1, VECTSP_4;
requirements BOOLE, SUBSET, NUMERALS, ARITHM;
definitions TARSKI, FUNCT_1, XBOOLE_0, MATRLIN, FUNCT_2;
equalities RELAT_1, FINSEQ_1, VECTSP_4, VECTSP_6, RLVECT_1, STRUCT_0,
LOPBAN_1;
expansions TARSKI, FUNCT_1, FINSEQ_1, VECTSP_4, XBOOLE_0, STRUCT_0;
theorems TARSKI, ZFMISC_1, RELAT_1, FINSET_1, FINSEQ_1, FUNCT_1, VECTSP_7,
VECTSP_9, CARD_2, XBOOLE_1, FUNCT_2, SUBSET_1, XBOOLE_0, VECTSP_1,
RLVECT_1, VECTSP_4, VECTSP_6, RLVECT_2, MOD_2, MATRLIN, CARD_1, FUNCOP_1,
VECTSP_5, FUNCT_7, FINSEQ_2, FUNCT_4, ENUMSET1, PARTFUN1;
schemes CLASSES1;
begin
theorem Th1:
for f,g being Function st g is one-to-one &
f|(rng g) is one-to-one & rng g c= dom f holds f*g is one-to-one
proof
let f,g be Function such that
A1: g is one-to-one and
A2: f|(rng g) is one-to-one and
A3: rng g c= dom f;
set h = f*g;
A4: dom h c= dom g
by FUNCT_1:11;
dom g c= dom h
proof
let x be object such that
A5: x in dom g;
g.x in rng g by A5,FUNCT_1:3;
hence thesis by A3,A5,FUNCT_1:11;
end;
then
A6: dom h = dom g by A4;
for x1,x2 being object st x1 in dom h & x2 in dom h & h.x1 = h.x2
holds x1 = x2
proof
let x1,x2 be object such that
A7: x1 in dom h and
A8: x2 in dom h and
A9: h.x1 = h.x2;
A10: h.x1 = f.(g.x1) & h.x2 = f.(g.x2) by A7,A8,FUNCT_1:12;
dom (f|(rng g)) = rng g by A3,RELAT_1:62;
then
A11: g.x1 in dom (f|(rng g)) by A4,A7,FUNCT_1:3;
g.x2 in rng g by A4,A8,FUNCT_1:3;
then
A12: g.x2 in dom (f|(rng g)) by A3,RELAT_1:62;
f.(g.x1) = (f|(rng g)).(g.x1) & f.(g.x2) = (f|(rng g)).(g.x2) by A6,A7,A8,
FUNCT_1:3,49;
then g.x1 = g.x2 by A2,A9,A10,A11,A12;
hence thesis by A1,A4,A7,A8;
end;
hence thesis;
end;
:: If a function is one-to-one on a set X, then it is one-to-one on
:: any subset of X.
theorem Th2:
for f being Function, X,Y being set st X c= Y & f|Y is one-to-one
holds f|X is one-to-one
proof
let f be Function, X,Y be set such that
A1: X c= Y and
A2: f|Y is one-to-one;
f|X = (f|Y)|X by A1,RELAT_1:74;
hence thesis by A2,FUNCT_1:52;
end;
theorem Th3:
for V being 1-sorted, X,Y being Subset of V holds X meets Y iff
ex v being Element of V st v in X & v in Y
proof
let V be 1-sorted, X,Y be Subset of V;
X meets Y implies ex v being Element of V st v in X & v in Y
proof
assume X meets Y;
then consider z being object such that
A1: z in X and
A2: z in Y by XBOOLE_0:3;
reconsider v = z as Element of V by A1;
take v;
thus thesis by A1,A2;
end;
hence thesis by XBOOLE_0:3;
end;
reserve K for Ring,
V1,W1 for VectSp of K;
reserve F for Field,
V,W for VectSp of F;
registration
let F be Field, V be finite-dimensional VectSp of F;
cluster finite for Basis of V;
existence
proof
consider A being finite Subset of V such that
A1: A is Basis of V by MATRLIN:def 1;
reconsider A as Basis of V by A1;
take A;
thus thesis;
end;
end;
registration
let F be Ring;
let V,W be VectSp of F;
cluster additive homogeneous for Function of V,W;
existence
proof
set f = FuncZero ([#]V,W);
reconsider f as Function of V,W;
A1: for x,y being Vector of V holds f.(x+y) = (f.x)+(f.y) by RLVECT_1:def 4;
take f;
for a being Element of F, x being Element of V holds f.(a*x) = a*(f.x)
by VECTSP_1:14;
hence f is additive homogeneous by A1,MOD_2:def 2,VECTSP_1:def 20;
end;
end;
theorem Th4:
[#]V is finite implies V is finite-dimensional
proof
set B = the Basis of V;
assume [#]V is finite;
then reconsider B as finite Subset of V;
take B;
thus thesis;
end;
theorem
for V being finite-dimensional VectSp of F st card ([#]V) = 1 holds dim V = 0
proof
let V be finite-dimensional VectSp of F such that
A1: card ([#]V) = 1;
[#]V = {0.V}
proof
ex y being object st [#]V = {y} by A1,CARD_2:42;
hence thesis by TARSKI:def 1;
end;
then (Omega).V = (0).V by VECTSP_4:def 3;
hence thesis by VECTSP_9:29;
end;
theorem
card ([#]V) = 2 implies dim V = 1
proof
assume
A1: card ([#]V) = 2;
then
A2: [#]V is finite;
reconsider C = [#]V as finite set by A1;
reconsider V as finite-dimensional VectSp of F by A2,Th4;
ex v being Vector of V st v <> 0.V & (Omega).V = Lin ({v})
proof
consider x,y being object such that
A3: x <> y and
A4: [#]V = {x,y} by A1,CARD_2:60;
per cases by A4,TARSKI:def 2;
suppose
A5: x = 0.V;
then reconsider x as Element of V;
reconsider y as Element of V by A4,TARSKI:def 2;
set L = Lin ({y});
take y;
for v being Element of V holds v in (Omega).V iff v in L
proof
let v be Element of V;
v in (Omega).V implies v in L
proof
assume v in (Omega).V;
A6: y in {y} by TARSKI:def 1;
A7: 0.L in L;
per cases by A4,TARSKI:def 2;
suppose
v = x;
hence thesis by A5,A7,VECTSP_4:def 2;
end;
suppose
v = y;
hence thesis by A6,VECTSP_7:8;
end;
end;
hence thesis;
end;
hence thesis by A3,A5,VECTSP_4:30;
end;
suppose
A8: y = 0.V;
reconsider x as Element of V by A4,TARSKI:def 2;
reconsider y as Element of V by A8;
set L = Lin ({x});
take x;
for v being Element of V holds v in (Omega).V iff v in L
proof
let v be Element of V;
v in (Omega).V implies v in L
proof
assume v in (Omega).V;
A9: x in {x} by TARSKI:def 1;
A10: 0.L in L;
per cases by A4,TARSKI:def 2;
suppose
v = y;
hence thesis by A8,A10,VECTSP_4:def 2;
end;
suppose
v = x;
hence thesis by A9,VECTSP_7:8;
end;
end;
hence thesis;
end;
hence thesis by A3,A8,VECTSP_4:30;
end;
end;
hence thesis by VECTSP_9:30;
end;
begin :: Basic facts of linear transformations
definition
let F be Ring, V,W be VectSp of F;
mode linear-transformation of V,W is additive homogeneous Function of V,W;
end;
reserve T for linear-transformation of V,W;
theorem Th7:
for V, W being non empty 1-sorted, T being Function of V,W holds
dom T = [#]V & rng T c= [#]W
proof
let V, W be non empty 1-sorted, T be Function of V,W;
T is Element of Funcs([#]V,[#]W) by FUNCT_2:8;
hence thesis by FUNCT_2:92;
end;
theorem Th8:
for F being Ring,
V, W being VectSp of F,
T being linear-transformation of V,W
for x,y being Element of V holds T.x - T.y = T.(x - y)
proof
let F be Ring,
V, W be VectSp of F,
T be linear-transformation of V,W;
let x,y be Element of V;
A1: T.((-1.F)*y) = (-1.F)*(T.y) by MOD_2:def 2;
T.(x - y) = T.x + T.(-y) & -y = (-1.F)*y by VECTSP_1:14,def 20;
hence thesis by A1,VECTSP_1:14;
end;
theorem Th9:
for F being Ring,
V, W being VectSp of F,
T being linear-transformation of V,W holds
T.(0.V) = 0.W
proof
let F be Ring,
V, W be VectSp of F,
T be linear-transformation of V,W;
0.V = (0.F)*(0.V) by VECTSP_1:14;
then T.(0.V) = (0.F)*T.(0.V) by MOD_2:def 2
.= 0.W by VECTSP_1:14;
hence thesis;
end;
definition
let F be Ring, V,W be VectSp of F, T be linear-transformation of V,W;
func ker T -> strict Subspace of V means
:Def1:
[#]it = { u where u is Element of V : T.u = 0.W };
existence
proof
set K = { u where u is Element of V : T.u = 0.W };
K c= [#]V
proof
let x be object;
assume x in K;
then ex u being Element of V st u = x & T.u = 0.W;
hence thesis;
end;
then reconsider K as Subset of V;
A1: for v being Element of V st v in K holds T.v = 0.W
proof
let v be Element of V;
assume v in K;
then ex u being Element of V st u = v & T.u = 0.W;
hence thesis;
end;
now
let u be Element of V, a be Element of F;
assume u in K;
then T.u = 0.W by A1;
then T.(a*u) = a*(0.W) by MOD_2:def 2
.= 0.W by VECTSP_1:14;
hence a*u in K;
end;
then
A2: for a being Element of F, u being Element of V st u in K holds a*u in K;
T.(0.V) = 0.W by Th9;
then
A3: 0.V in K;
now
let u,v be Element of V;
assume u in K & v in K;
then T.u = 0.W & T.v = 0.W by A1;
then T.(u+v) = 0.W + 0.W by VECTSP_1:def 20
.= 0.W by RLVECT_1:def 4;
hence u+v in K;
end;
then K is linearly-closed by A2;
then consider W being strict Subspace of V such that
A4: K = the carrier of W by A3,VECTSP_4:34;
take W;
thus thesis by A4;
end;
uniqueness by VECTSP_4:29;
end;
theorem Th10:
for F being Ring,
V, W being VectSp of F,
T being linear-transformation of V,W
for x being Element of V holds x in ker T iff T.x = 0.W
proof
let F be Ring,
V, W be VectSp of F,
T be linear-transformation of V,W;
let x be Element of V;
thus x in ker T implies T.x = 0.W
proof
assume x in ker T;
then
A1: x in [#]ker T;
[#]ker T = { u where u is Element of V : T.u = 0.W } by Def1;
then ex u being Element of V st u = x & T.u = 0.W by A1;
hence thesis;
end;
assume T.x = 0.W;
then x in { u where u is Element of V : T.u = 0.W };
then x in [#]ker T by Def1;
hence thesis;
end;
definition
let V,W be non empty 1-sorted, T be Function of V,W, X be Subset of V;
redefine func T .: X -> Subset of W; :: redefines .: (FUNCT_1, redefinition) → .: (RELAT_1, definition)
coherence
proof
rng T c= [#]W & T .: X c= rng T by Th7,RELAT_1:111;
hence thesis by XBOOLE_1:1;
end;
end;
definition
let F be Ring, V,W be VectSp of F, T be linear-transformation of V,W;
func im T -> strict Subspace of W means
:Def2:
[#]it = T .: [#]V;
existence
proof
reconsider U = T .: [#]V as Subset of W;
A1: for u being Element of W holds u in U iff ex v being Element of V st T
.v = u
proof
let u be Element of W;
thus u in U implies ex v being Element of V st T.v = u
proof
assume u in U;
then consider x being object such that
x in dom T and
A2: x in [#]V and
A3: u = T.x by FUNCT_1:def 6;
reconsider x as Element of V by A2;
take x;
thus thesis by A3;
end;
thus (ex v being Element of V st T.v = u) implies u in U
proof
given v being Element of V such that
A4: T.v = u;
v in [#]V;
then v in dom T by Th7;
hence thesis by A4,FUNCT_1:def 6;
end;
end;
A5: now
let u,v be Element of W such that
A6: u in U and
A7: v in U;
consider x being Element of V such that
A8: T.x = u by A1,A6;
consider y being Element of V such that
A9: T.y = v by A1,A7;
u+v = T.(x+y) by A8,A9,VECTSP_1:def 20;
hence u+v in U by A1;
end;
now
let a be Element of F, w be Element of W;
assume w in U;
then consider v being Element of V such that
A10: T.v = w by A1;
T.(a*v) = a*w by A10,MOD_2:def 2;
hence a*w in U by A1;
end;
then
A11: U is linearly-closed by A5;
T.(0.V) = 0.W by Th9;
then U <> {} by A1;
then consider A being strict Subspace of W such that
A12: U = the carrier of A by A11,VECTSP_4:34;
take A;
thus thesis by A12;
end;
uniqueness by VECTSP_4:29;
end;
theorem
for F being Ring,
V, W being VectSp of F,
T being linear-transformation of V,W holds
0.V in ker T
proof
let F be Ring,
V, W be VectSp of F,
T be linear-transformation of V,W;
0.V = (0.F)*(0.V) by VECTSP_1:14;
then T.(0.V) = (0.F)*T.(0.V) by MOD_2:def 2
.= 0.W by VECTSP_1:14;
hence thesis by Th10;
end;
theorem Th12:
for F being Ring, V, W being VectSp of F,
T being linear-transformation of V,W holds
for X being Subset of V holds T .: X is Subset of im T
proof
let F be Ring, V, W be VectSp of F,
T be linear-transformation of V,W;
let X be Subset of V;
[#](im T) = T .: [#]V by Def2;
hence thesis by RELAT_1:123;
end;
theorem Th13:
for F being Ring, V, W being VectSp of F,
T being linear-transformation of V,W holds
for y being Element of W holds y in im T iff
ex x being Element of V st y = T.x
proof
let F be Ring, V, W be VectSp of F,
T be linear-transformation of V,W;
let y be Element of W;
A1: y in im T implies ex x being Element of V st y = T.x
proof
assume y in im T;
then reconsider y as Element of im T;
[#](im T) = T .: [#]V by Def2;
then consider x being object such that
x in dom T and
A2: x in [#]V and
A3: y = T.x by FUNCT_1:def 6;
reconsider x as Element of V by A2;
take x;
thus thesis by A3;
end;
(ex x being Element of V st y = T.x) implies y in im T
proof
assume
A4: ex x being Element of V st y = T.x;
dom T = [#]V by Th7;
then y in T .: [#]V by A4,FUNCT_1:def 6;
then y in [#](im T) by Def2;
hence thesis;
end;
hence thesis by A1;
end;
theorem
for F being Ring, V, W being VectSp of F,
T being linear-transformation of V,W
for x being Element of ker T holds T.x = 0.W
proof
let F be Ring, V, W be VectSp of F,
T be linear-transformation of V,W;
let x be Element of ker T;
reconsider y = x as Element of V by VECTSP_4:10;
y in ker T;
hence thesis by Th10;
end;
theorem Th15:
for F being Ring, V, W being VectSp of F,
T being linear-transformation of V,W st
T is one-to-one holds ker T = (0).V
proof
let F be Ring, V, W be VectSp of F,
T be linear-transformation of V,W;
reconsider Z = (0).V as Subspace of ker T by VECTSP_4:39;
assume
A1: T is one-to-one;
for v being Element of ker T holds v in Z
proof
let v be Element of ker T;
A2: v in ker T;
assume not v in Z; then
A3: not v = 0.V by VECTSP_4:35;
A4: T.(0.V) = 0.W & dom T = [#]V by Th7,Th9;
reconsider v as Element of V by VECTSP_4:10;
T.v = 0.W by A2,Th10;
hence thesis by A1,A3,A4;
end;
hence thesis by VECTSP_4:32;
end;
theorem Th16:
for V being finite-dimensional VectSp of F holds dim ((0).V) = 0
proof
let V be finite-dimensional VectSp of F;
(Omega).((0).V) = (0).((0).V) by VECTSP_4:36;
hence thesis by VECTSP_9:29;
end;
theorem Th17:
for F being Ring, V, W being VectSp of F,
T being linear-transformation of V,W
for x,y being Element of V st T.x = T.y holds x - y in ker T
proof
let F be Ring, V, W be VectSp of F,
T be linear-transformation of V,W;
let x,y be Element of V such that
A1: T.x = T.y;
T.(x - y) = T.x - T.y by Th8
.= 0.W by A1,VECTSP_1:19;
hence thesis by Th10;
end;
theorem Th18:
for F being Ring, V, W being VectSp of F
for A being Subset of V, x,y being Element of V st x - y in Lin
A holds x in Lin (A \/ {y})
proof
let F be Ring, V, W be VectSp of F;
let A be Subset of V, x,y be Element of V such that
A1: x - y in Lin A;
A2: Lin (A \/ {y}) = (Lin A) + (Lin {y}) by VECTSP_7:15;
y in {y} by TARSKI:def 1;
then
A3: y in Lin ({y}) by VECTSP_7:8;
(x - y) + y = x - (y - y) by RLVECT_1:29
.= x - 0.V by VECTSP_1:19
.= x by RLVECT_1:13;
hence thesis by A1,A3,A2,VECTSP_5:1;
end;
begin :: Some basic facts about linearly independent subsets and linear
:: combinations
theorem Th19:
for F being Ring, V, W being VectSp of F
for X being Subset of V st V is Subspace of W holds X is Subset of W
proof
let F be Ring, V, W be VectSp of F;
let X be Subset of V;
assume V is Subspace of W; then
A1: [#]V c= [#]W by VECTSP_4:def 2;
X c= [#]W by A1;
hence thesis;
end;
:: A linearly independent set is a basis of its linear span.
theorem Th20:
for A being Subset of V st A is linearly-independent holds A is
Basis of Lin A
proof
let A be Subset of V such that
A1: A is linearly-independent;
A c= [#](Lin A)
proof
let x be object such that
A2: x in A;
reconsider x as Element of V by A2;
x in Lin A by A2,VECTSP_7:8;
hence thesis;
end;
then reconsider B = A as Subset of Lin A;
A3: Lin B = Lin A by VECTSP_9:17;
B is linearly-independent by A1,VECTSP_9:12;
hence thesis by A3,VECTSP_7:def 3;
end;
:: Adjoining an element x to A that is already in its linear span
:: results in a linearly dependent set.
theorem Th21:
for A being Subset of V, x being Element of V st x in Lin A &
not x in A holds A \/ {x} is linearly-dependent
proof
let A be Subset of V, x be Element of V such that
A1: x in Lin A and
A2: not x in A;
per cases;
suppose
A3: A is linearly-independent;
x in [#](Lin A) by A1;
then reconsider X = {x} as Subset of Lin A by SUBSET_1:41;
reconsider A9 = A as Basis of Lin A by A3,Th20;
reconsider B = A9 \/ X as Subset of Lin A;
X misses A9
proof
assume X meets A9;
then ex y being object st y in X & y in A9 by XBOOLE_0:3;
hence contradiction by A2,TARSKI:def 1;
end;
then B is linearly-dependent by VECTSP_9:15;
hence thesis by VECTSP_9:12;
end;
suppose
A is linearly-dependent;
hence thesis by VECTSP_7:1,XBOOLE_1:7;
end;
end;
theorem Th22:
for A being Subset of V, B being Basis of V st A is Basis of ker
T & A c= B holds T|(B \ A) is one-to-one
proof
let A be Subset of V, B be Basis of V such that
A1: A is Basis of ker T and
A2: A c= B;
reconsider A9 = A as Subset of V;
set f = T|(B \ A);
let x1,x2 be object such that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f.x1 = f.x2 and
A6: x1 <> x2;
x2 in dom T by A4,RELAT_1:57;
then reconsider x2 as Element of V;
x1 in dom T by A3,RELAT_1:57;
then reconsider x1 as Element of V;
A7: x1 in B \ A by A3;
A8: not x1 in (A9 \/ {x2})
proof
assume
A9: x1 in A9 \/ {x2};
per cases by A9,XBOOLE_0:def 3;
suppose
x1 in A9;
hence contradiction by A7,XBOOLE_0:def 5;
end;
suppose
x1 in {x2};
hence contradiction by A6,TARSKI:def 1;
end;
end;
A10: x2 in B \ A by A4;
then
A11: f.x2 = T.x2 by FUNCT_1:49;
reconsider A as Basis of ker T by A1;
A12: ker T = Lin A by VECTSP_7:def 3;
f.x1 = T.x1 by A7,FUNCT_1:49;
then x1 - x2 in ker T by A5,A11,Th17;
then x1 - x2 in Lin A9 by A12,VECTSP_9:17;
then
A13: x1 in Lin (A9 \/ {x2}) by Th18;
{x2} \/ {x1} = {x1,x2} by ENUMSET1:1;
then
A14: (A9 \/ {x2}) \/ {x1} = A9 \/ {x1,x2} by XBOOLE_1:4;
{x1,x2} c= B
proof
let z be object such that
A15: z in {x1,x2};
per cases by A15,TARSKI:def 2;
suppose
z = x1;
hence thesis by A7,XBOOLE_0:def 5;
end;
suppose
z = x2;
hence thesis by A10,XBOOLE_0:def 5;
end;
end;
then
A16: A9 \/ {x1,x2} c= B by A2,XBOOLE_1:8;
B is linearly-independent by VECTSP_7:def 3;
hence thesis by A13,A14,A8,A16,Th21,VECTSP_7:1;
end;
theorem
for A being Subset of V, l being Linear_Combination of A,
x being Element of V, a being Element of F holds
l +* (x,a) is Linear_Combination of A \/ {x}
proof
let A be Subset of V, l be Linear_Combination of A,
x be Element of V, a be Element of F;
set m = l +* (x,a);
A1: dom m = [#]V by FUNCT_2:def 1;
rng m c= [#]F
proof
let y be object;
assume y in rng m;
then consider x9 being object such that
A2: x9 in dom m and
A3: m.x9 = y by FUNCT_1:def 3;
A4: x9 in dom l by A1,A2,FUNCT_2:92;
per cases;
suppose
x9 = x;
then m.x9 = a by A4,FUNCT_7:31;
hence thesis by A3;
end;
suppose
A5: x9 <> x;
A6: l.x9 in rng l & rng l c= [#]F by A4,FUNCT_1:3,FUNCT_2:92;
m.x9 = l.x9 by A5,FUNCT_7:32;
hence thesis by A3,A6;
end;
end;
then reconsider m as Element of Funcs ([#]V,[#]F) by A1,FUNCT_2:def 2;
set T = Carrier l \/ {x};
for v being Element of V st not v in T holds m.v = 0.F
proof
let v be Element of V such that
A7: not v in T;
not v in {x} by A7,XBOOLE_0:def 3;
then v <> x by TARSKI:def 1;
then
A8: m.v = l.v by FUNCT_7:32;
not v in Carrier l by A7,XBOOLE_0:def 3;
hence thesis by A8;
end;
then reconsider m as Linear_Combination of V by VECTSP_6:def 1;
A9: Carrier m c= T
proof
let y be object;
assume y in Carrier m;
then consider z being Element of V such that
A10: y = z and
A11: m.z <> 0.F;
per cases;
suppose
A12: z = x;
x in {x} & {x} c= T by TARSKI:def 1,XBOOLE_1:7;
hence thesis by A10,A12;
end;
suppose
z <> x;
then m.z = l.z by FUNCT_7:32;
then
A13: z in Carrier l by A11;
Carrier l c= T by XBOOLE_1:7;
hence thesis by A10,A13;
end;
end;
Carrier l c= A by VECTSP_6:def 4;
then T c= A \/ {x} by XBOOLE_1:9;
then Carrier m c= A \/ {x} by A9;
hence thesis by VECTSP_6:def 4;
end;
definition
let V be 1-sorted, X be Subset of V;
func V \ X -> Subset of V equals
[#]V \ X;
coherence;
end;
definition
let F be Field, V be VectSp of F,
l be Linear_Combination of V, X be Subset of V;
redefine func l .: X -> Subset of F; :: redefines .: (FUNCT_1, redefinition) → .: (RELAT_1, definition)
coherence
proof
l .: X c= [#]F;
hence thesis;
end;
end;
reserve l for Linear_Combination of V;
registration
let F be Field, V be VectSp of F;
cluster linearly-dependent for Subset of V;
existence
proof
reconsider S = {0.V} as Subset of V;
take S;
0.V in S by TARSKI:def 1;
hence thesis by VECTSP_7:2;
end;
end;
:: Restricting a linear combination to a given set
definition
let F be Field, V be VectSp of F, l be Linear_Combination of V, A be Subset
of V;
func l!A -> Linear_Combination of A equals
(l|A) +* ((V \ A) --> 0.F);
coherence
proof
set f = (l|A) +* ((V \ A) --> 0.F);
A1: dom f = dom (l|A) \/ dom ((V \ A) --> 0.F) by FUNCT_4:def 1;
dom l = [#]V by FUNCT_2:92;
then
A3: dom (l|A) = A by RELAT_1:62;
then
A4: dom f = [#]V by A1,XBOOLE_1:45;
A5: A \/ ([#]V \ A) = [#]V by XBOOLE_1:45;
rng f c= [#]F
proof
let y be object;
assume y in rng f;
then consider x being object such that
A6: x in dom f and
A7: y = f.x by FUNCT_1:def 3;
reconsider x as Element of V by A1,A3,A6,XBOOLE_1:45;
per cases by A5,XBOOLE_0:def 3;
suppose
A8: x in A;
then not x in dom ((V \ A) --> 0.F) by XBOOLE_0:def 5;
then
A9: f.x = (l|A).x by FUNCT_4:11;
(l|A).x = l.x by A8,FUNCT_1:49;
hence thesis by A7,A9;
end;
suppose
A10: x in V \ A;
then x in dom ((V \ A) --> 0.F);
then f.x = ((V \ A) --> 0.F).x by FUNCT_4:13
.= 0.F by A10,FUNCOP_1:7;
hence thesis by A7;
end;
end;
then reconsider f as Element of Funcs([#]V,[#]F) by A4,FUNCT_2:def 2;
ex T being finite Subset of V st for v being Element of V st not v in
T holds f.v = 0.F
proof
set D = { v where v is Element of V : f.v <> 0.F };
D c= [#]V
proof
let x be object;
assume x in D;
then ex v being Element of V st x = v & f.v <> 0.F;
hence thesis;
end;
then reconsider D as Subset of V;
set C = Carrier l;
D c= C
proof
let x be object;
assume x in D;
then consider v being Element of V such that
A11: x = v and
A12: f.v <> 0.F;
A14: now
assume
A15: v in V \ A;
then f.v = ((V \ A) --> 0.F).v by A1,A4,FUNCT_4:def 1
.= 0.F by A15,FUNCOP_1:7;
hence contradiction by A12;
end;
then v in A by XBOOLE_0:def 5;
then
A16: (l|A).v = l.v by FUNCT_1:49;
not v in dom ((V \ A) --> 0.F) by A14;
then f.v = (l|A).v by FUNCT_4:11;
hence thesis by A11,A12,A16;
end;
then reconsider D as finite Subset of V;
take D;
thus thesis;
end;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
Carrier f c= A
proof
let x be object such that
A17: x in Carrier f;
reconsider x as Element of V by A17;
A18: f.x <> 0.F by A17,VECTSP_6:2;
now
assume not x in A;
then
A19: x in V \ A by XBOOLE_0:def 5;
then x in dom (l|A) \/ (dom ((V \ A) --> 0.F)) by XBOOLE_0:def 3;
then f.x = ((V \ A) --> 0.F).x by A19,FUNCT_4:def 1;
hence contradiction by A18,A19,FUNCOP_1:7;
end;
hence thesis;
end;
hence thesis by VECTSP_6:def 4;
end;
end;
theorem Th24:
l = l!Carrier l
proof
set f = l|(Carrier l);
set g = (V \ Carrier l) --> 0.F;
set m = f +* g;
A2: dom l = [#]V by FUNCT_2:92;
then dom f = Carrier l by RELAT_1:62;
then
A3: (dom f) \/ (dom g) = [#]V by XBOOLE_1:45;
A4: for x being object st x in dom l holds l.x = m.x
proof
let x be object;
assume x in dom l;
then reconsider x as Element of V;
per cases;
suppose
A5: x in Carrier l;
then not x in dom g by XBOOLE_0:def 5;
then m.x = f.x by A3,FUNCT_4:def 1;
hence thesis by A5,FUNCT_1:49;
end;
suppose
A6: not x in Carrier l;
then x in V \ (Carrier l) by XBOOLE_0:def 5;
then m.x = g.x & g.x = 0.F by A3,FUNCOP_1:7,FUNCT_4:def 1;
hence thesis by A6;
end;
end;
dom l = dom m by A2,A3,FUNCT_4:def 1;
hence thesis by A4;
end;
Lm1: for X being Subset of V holds l .: X is finite
proof
let X be Subset of V;
A1: l = l!(Carrier l) by Th24;
(rng (l|Carrier l)) \/ rng ((V \ (Carrier l)) --> 0.F) is finite;
then rng l is finite by A1,FINSET_1:1,FUNCT_4:17;
hence thesis by FINSET_1:1,RELAT_1:111;
end;
theorem Th25:
for A being Subset of V, v being Element of V st v in A holds (l !A).v = l.v
proof
let A be Subset of V, v be Element of V such that
A1: v in A;
dom (l!A) = [#]V by FUNCT_2:92;
then
A2: (dom (l|A)) \/ (dom ((V \ A) --> 0.F)) = [#]V by FUNCT_4:def 1;
not v in dom ((V \ A) --> 0.F) by A1,XBOOLE_0:def 5;
then (l!A).v = (l|A).v by A2,FUNCT_4:def 1
.= l.v by A1,FUNCT_1:49;
hence thesis;
end;
theorem Th26:
for A being Subset of V, v being Element of V st not v in A
holds (l!A).v = 0.F
proof
let A be Subset of V, v be Element of V;
assume not v in A;
then
A1: v in V \ A by XBOOLE_0:def 5;
A2: dom (l!A) = [#]V by FUNCT_2:92;
dom ((V \ A) --> 0.F) = V \ A & dom (l!A) = (dom (l|A)) \/ (dom ((V \ A)
--> 0.F)) by FUNCT_4:def 1;
then (l!A).v = ((V \ A) --> 0.F).v by A2,A1,FUNCT_4:def 1
.= 0.F by A1,FUNCOP_1:7;
hence thesis;
end;
theorem Th27:
for A,B being Subset of V, l being Linear_Combination of B st A
c= B holds l = (l!A) + (l!(B\A))
proof
let A,B be Subset of V, l be Linear_Combination of B such that
A1: A c= B;
set r = (l!A) + (l!(B\A));
let v be Element of V;
A2: v in B implies (v in A or v in B \ A)
proof
assume
A3: v in B;
B = A \/ (B \ A) by A1,XBOOLE_1:45;
hence thesis by A3,XBOOLE_0:def 3;
end;
per cases by A2;
suppose
A4: v in A;
then not v in B \ A by XBOOLE_0:def 5;
then
A5: (l!(B\A)).v = 0.F by Th26;
(l!A).v = l.v by A4,Th25;
then r.v = l.v + 0.F by A5,VECTSP_6:22
.= l.v by RLVECT_1:4;
hence l.v = r.v;
end;
suppose
A6: v in B\A;
then not v in A by XBOOLE_0:def 5;
then
A7: (l!A).v = 0.F by Th26;
(l!(B\A)).v = l.v by A6,Th25;
then r.v = 0.F + l.v by A7,VECTSP_6:22
.= l.v by RLVECT_1:4;
hence l.v = r.v;
end;
suppose
A8: not v in B;
Carrier l c= B by VECTSP_6:def 4;
then
A9: not v in Carrier l by A8;
not v in B\A by A8,XBOOLE_0:def 5;
then
A10: (l!(B\A)).v = 0.F by Th26;
not v in A by A1,A8;
then (l!A).v = 0.F by Th26;
then r.v = 0.F + 0.F by A10,VECTSP_6:22
.= 0.F by RLVECT_1:4;
hence l.v = r.v by A9;
end;
end;
registration
let F be Field, V be VectSp of F, l be Linear_Combination of V, X be Subset
of V;
cluster l .: X -> finite;
coherence by Lm1;
end;
definition
let V,W be non empty 1-sorted, T be Function of V,W, X be Subset of W;
redefine func T"X -> Subset of V; :: redefines " (FUNCT_1, redefinition) → " (RELAT_1, definition)
coherence
proof
dom T = [#]V by Th7;
hence thesis by RELAT_1:132;
end;
end;
theorem Th28:
for X being Subset of V st X misses Carrier l holds l .: X c= { 0.F}
proof
let X be Subset of V such that
A1: X misses Carrier l;
set M = l .: X;
let y be object;
assume y in M;
then consider x being object such that
A2: x in dom l and
A3: x in X and
A4: y = l.x by FUNCT_1:def 6;
reconsider x as Element of V by A2;
now
assume l.x <> 0.F;
then x in Carrier l;
then x in (Carrier l) /\ X by A3,XBOOLE_0:def 4;
hence contradiction by A1;
end;
hence thesis by A4,TARSKI:def 1;
end;
:: The image of a linear combination under a linear transformation:
::
:: T(a1*v1 + a2*v2 + ... + an*vn)
:: = a1*T(v1) + a2*T(v2) + ... + an*T(vn).
::
:: Linear combinations are represented as functions from the space to
:: the underlying field having finite support, so to define a new
:: linear combination it is enough to say what its values are for the
:: elements of W and to prove that its support is finite.
::
:: The only difficulty is that some values T(vi) and T(vj) may be
:: equal. In this case, the new linear combination should be the sum
:: of the coefficients ai and aj, i.e., l(vi) and l(vj).
definition
let F be Field, V,W be VectSp of F, l be Linear_Combination of V, T be
linear-transformation of V,W;
func T@l -> Linear_Combination of W means
:Def5:
for w being Element of W holds it.w = Sum (l .: (T"{w}));
existence
proof
defpred P[object,object] means
ex w being Element of W st $1 = w & $2 = Sum (l.: (T"{w}));
A1: for x being object st x in [#]W holds ex y being object st P[x,y]
proof
let x be object;
assume x in [#]W;
then reconsider x as Element of W;
take Sum (l .: (T"{x}));
thus thesis;
end;
consider f being Function such that
A2: dom f = [#]W and
A3: for x being object st x in [#]W holds P[x,f.x] from CLASSES1:sch 1(A1
);
A4: rng f c= [#]F
proof
let y be object;
assume y in rng f;
then consider x being object such that
A5: x in dom f and
A6: f.x = y by FUNCT_1:def 3;
ex w being Element of W st x = w & f.x = Sum (l .: (T"{w} )) by A2,A3,A5;
hence thesis by A6;
end;
A7: for w being Element of W holds f.w = Sum (l .: (T"{w}))
proof
let w be Element of W;
ex w9 being Element of W st w = w9 & f.w = Sum (l .: (T"{ w9})) by A3;
hence thesis;
end;
reconsider f as Element of Funcs([#]W,[#]F) by A2,A4,FUNCT_2:def 2;
ex T being finite Subset of W st for w being Element of W st not w in
T holds f.w = 0.F
proof
set X = { w where w is Element of W : f.w <> 0.F };
X c= [#]W
proof
let x be object;
assume x in X;
then ex w being Element of W st x = w & f.w <> 0.F;
hence thesis;
end;
then reconsider X as Subset of W;
set C = Carrier l;
reconsider TC = T .: C as Subset of W;
X c= TC
proof
let x be object;
assume x in X;
then consider w being Element of W such that
A8: x = w and
A9: f.w <> 0.F;
T"{w} meets Carrier l
proof
assume
A10: T"{w} misses Carrier l;
then
A11: l .: T"{w} c= {0.F} by Th28;
Sum (l .: T"{w}) = 0.F
proof
per cases;
suppose
l .: T"{w} = {}F;
hence thesis by RLVECT_2:8;
end;
suppose
A12: l .: T"{w} <> {}F;
A13: {0.F} c= l .: T"{w}
proof
let y be object;
assume y in {0.F};
then
A14: y = 0.F by TARSKI:def 1;
ex z being object st z in l .: T"{w} by A12,XBOOLE_0:def 1;
hence thesis by A11,A14,TARSKI:def 1;
end;
l .: T"{w} c= {0.F} by A10,Th28;
then l .: T"{w} = {0.F} by A13;
hence thesis by RLVECT_2:9;
end;
end;
hence contradiction by A7,A9;
end;
then consider y being object such that
A15: y in T"{w} and
A16: y in Carrier l by XBOOLE_0:3;
A17: dom T = [#]V by Th7;
reconsider y as Element of V by A16;
T.y in {w} by A15,FUNCT_1:def 7;
then T.y = w by TARSKI:def 1;
hence thesis by A8,A16,A17,FUNCT_1:def 6;
end;
then reconsider X as finite Subset of W;
take X;
thus thesis;
end;
then reconsider f as Linear_Combination of W by VECTSP_6:def 1;
take f;
for w being Element of W holds f.w = Sum (l .: (T"{w}))
proof
let w be Element of W;
ex w9 being Element of W st w = w9 & f.w = Sum (l .: (T"{ w9})) by A3;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let f,g be Linear_Combination of W such that
A18: for w being Element of W holds f.w = Sum (l .: (T"{w})) and
A19: for w being Element of W holds g.w = Sum (l .: (T"{w}));
A20: for x being object st x in dom f holds f.x = g.x
proof
let x be object;
assume x in dom f;
then reconsider x as Element of W;
f.x = Sum (l .: (T"{x})) by A18;
hence thesis by A19;
end;
dom f = [#]W & dom g = [#]W by FUNCT_2:92;
hence thesis by A20;
end;
end;
theorem Th29:
T@l is Linear_Combination of T .: (Carrier l)
proof
Carrier (T@l) c= T .: (Carrier l)
proof
let w be object such that
A1: w in Carrier (T@l);
reconsider w as Element of W by A1;
A2: (T@l).w <> 0.F by A1,VECTSP_6:2;
now
assume
A3: T"{w} misses Carrier l;
then
A4: l .: T"{w} c= {0.F} by Th28;
Sum (l .: T"{w}) = 0.F
proof
per cases;
suppose
l .: T"{w} = {}F;
hence thesis by RLVECT_2:8;
end;
suppose
A5: l .: T"{w} <> {}F;
A6: {0.F} c= l .: T"{w}
proof
let y be object;
assume y in {0.F};
then
A7: y = 0.F by TARSKI:def 1;
ex z being object st z in l .: T"{w} by A5,XBOOLE_0:def 1;
hence thesis by A4,A7,TARSKI:def 1;
end;
l .: T"{w} c= {0.F} by A3,Th28;
then l .: T"{w} = {0.F} by A6;
hence thesis by RLVECT_2:9;
end;
end;
hence contradiction by A2,Def5;
end;
then consider x being object such that
A8: x in T"{w} and
A9: x in Carrier l by XBOOLE_0:3;
A10: x in dom T by A8,FUNCT_1:def 7;
A11: T.x in {w} by A8,FUNCT_1:def 7;
reconsider x as Element of V by A8;
T.x = w by A11,TARSKI:def 1;
hence thesis by A9,A10,FUNCT_1:def 6;
end;
hence thesis by VECTSP_6:def 4;
end;
theorem Th30:
Carrier (T@l) c= T .: (Carrier l)
proof
T@l is Linear_Combination of T .: (Carrier l) by Th29;
hence thesis by VECTSP_6:def 4;
end;
theorem Th31:
for l,m being Linear_Combination of V st (Carrier l) misses (
Carrier m) holds Carrier (l + m) = (Carrier l) \/ (Carrier m)
proof
let l,m be Linear_Combination of V such that
A1: (Carrier l) misses (Carrier m);
thus Carrier (l+m) c= (Carrier l) \/ (Carrier m) by VECTSP_6:23;
thus (Carrier l) \/ (Carrier m) c= Carrier (l+m)
proof
let v be object such that
A2: v in (Carrier l) \/ (Carrier m);
per cases by A2,XBOOLE_0:def 3;
suppose
A3: v in Carrier l;
then reconsider v as Element of V;
not v in Carrier m by A1,A2,A3,XBOOLE_0:5;
then (l+m).v = (l.v) + (m.v) & m.v = 0.F by VECTSP_6:22;
then
A4: (l+m).v = l.v by RLVECT_1:4;
l.v <> 0.F by A3,VECTSP_6:2;
hence thesis by A4;
end;
suppose
A5: v in Carrier m;
then reconsider v as Element of V;
not v in Carrier l by A1,A2,A5,XBOOLE_0:5;
then (l+m).v = (l.v) + (m.v) & l.v = 0.F by VECTSP_6:22;
then
A6: (l+m).v = m.v by RLVECT_1:4;
m.v <> 0.F by A5,VECTSP_6:2;
hence thesis by A6;
end;
end;
end;
theorem Th32:
for l,m being Linear_Combination of V st (Carrier l) misses (
Carrier m) holds Carrier (l - m) = (Carrier l) \/ (Carrier m)
proof
let l,m be Linear_Combination of V such that
A1: (Carrier l) misses (Carrier m);
Carrier (-m) = Carrier m by VECTSP_6:38;
hence thesis by A1,Th31;
end;
theorem Th33:
for A,B being Subset of V st A c= B & B is Basis of V holds V
is_the_direct_sum_of Lin A, Lin (B \ A)
proof
let A,B be Subset of V such that
A1: A c= B and
A2: B is Basis of V;
A3: (Lin A) /\ (Lin (B \ A)) = (0).V
proof
set U = (Lin A) /\ (Lin (B \ A));
reconsider W = (0).V as strict Subspace of U by VECTSP_4:39;
for v being Element of U holds v in W
proof
let v be Element of U;
A4: B is linearly-independent by A2,VECTSP_7:def 3;
A5: v in U;
then v in Lin A by VECTSP_5:3;
then consider l being Linear_Combination of A such that
A6: v = Sum l by VECTSP_7:7;
v in Lin (B \ A) by A5,VECTSP_5:3;
then consider m being Linear_Combination of B \ A such that
A7: v = Sum m by VECTSP_7:7;
A8: 0.V = (Sum l) - (Sum m) by A6,A7,VECTSP_1:19
.= Sum (l - m) by VECTSP_6:47;
A9: Carrier (l - m) c= (Carrier l) \/ (Carrier m) & A \/ (B \ A) = B by A1,
VECTSP_6:41,XBOOLE_1:45;
A10: Carrier l c= A & Carrier m c= B \ A by VECTSP_6:def 4;
then (Carrier l) \/ (Carrier m) c= A \/ (B \ A) by XBOOLE_1:13;
then Carrier (l - m) c= B by A9;
then reconsider n = l - m as Linear_Combination of B by VECTSP_6:def 4;
A misses (B \ A) by XBOOLE_1:79;
then Carrier n = (Carrier l) \/ (Carrier m) by A10,Th32,XBOOLE_1:64;
then Carrier l = {} by A8,A4,VECTSP_7:def 1;
then l = ZeroLC(V) by VECTSP_6:def 3;
then Sum l = 0.V by VECTSP_6:15;
hence thesis by A6,VECTSP_4:35;
end;
hence thesis by VECTSP_4:32;
end;
(Omega).V = (Lin A) + (Lin (B \ A))
proof
set U = (Lin A) + (Lin (B \ A));
A11: [#]V c= [#]U
proof
let v be object;
assume v in [#]V;
then reconsider v as Element of V;
v in Lin B by A2,VECTSP_9:10;
then consider l being Linear_Combination of B such that
A12: v = Sum l by VECTSP_7:7;
set n = l!(B\A);
set m = l!A;
A13: l = m + n by A1,Th27;
ex v1,v2 being Element of V st v1 in Lin A & v2 in Lin (B \ A) & v
= v1 + v2
proof
take Sum m, Sum n;
thus thesis by A12,A13,VECTSP_6:44,VECTSP_7:7;
end;
then v in (Lin A) + (Lin (B \ A)) by VECTSP_5:1;
hence thesis;
end;
[#]U c= [#]V by VECTSP_4:def 2;
then [#]U = [#]V by A11;
hence thesis by VECTSP_4:29;
end;
hence thesis by A3,VECTSP_5:def 4;
end;
theorem Th34:
for A being Subset of V, l being Linear_Combination of A, v
being Element of V st T|A is one-to-one & v in A holds ex X being Subset of V
st X misses A & T"{T.v} = {v} \/ X
proof
let A be Subset of V, l be Linear_Combination of A, v be Element of V such
that
A1: T|A is one-to-one and
A2: v in A;
set X = T"{T.v} \ {v};
A3: X misses A
proof
dom T = [#]V by Th7;
then
A4: dom (T|A) = A by RELAT_1:62;
assume X meets A;
then consider x being object such that
A5: x in X and
A6: x in A by XBOOLE_0:3;
not x in {v} by A5,XBOOLE_0:def 5;
then
A7: x <> v by TARSKI:def 1;
x in T"{T.v} by A5,XBOOLE_0:def 5;
then T.x in {T.v} by FUNCT_1:def 7;
then
A8: T.x = T.v by TARSKI:def 1;
T.x = (T|A).x by A6,FUNCT_1:49;
then (T|A).v = (T|A).x by A2,A8,FUNCT_1:49;
hence thesis by A1,A2,A6,A7,A4;
end;
take X;
{v} c= T"{T.v}
proof
let x be object;
assume x in {v};
then
A9: x = v by TARSKI:def 1;
dom T = [#]V & T.v in {T.v} by Th7,TARSKI:def 1;
hence thesis by A9,FUNCT_1:def 7;
end;
hence thesis by A3,XBOOLE_1:45;
end;
theorem Th35:
for X being Subset of V st X misses Carrier l & X <> {} holds l .: X = {0.F}
proof
let X be Subset of V such that
A1: X misses Carrier l and
A2: X <> {};
dom l = [#]V by FUNCT_2:92;
then
A3: l .: X <> {} by A2,RELAT_1:119;
l .: X c= {0.F} by A1,Th28;
hence thesis by A3,ZFMISC_1:33;
end;
theorem Th36:
for w being Element of W st w in Carrier (T@l) holds T"{w} meets Carrier l
proof
let w be Element of W;
assume w in Carrier (T@l);
then
A1: (T@l).w <> 0.F by VECTSP_6:2;
assume
A2: T"{w} misses Carrier l;
per cases;
suppose
T"{w} = {};
then Sum (l .: T"{w}) = Sum ({}F)
.= 0.F by RLVECT_2:8;
hence thesis by A1,Def5;
end;
suppose
T"{w} <> {};
then l .: T"{w} = {0.F} by A2,Th35;
then Sum (l .: T"{w}) = 0.F by RLVECT_2:9;
hence thesis by A1,Def5;
end;
end;
theorem Th37:
for v being Element of V st T|(Carrier l) is one-to-one & v in
Carrier l holds (T@l).(T.v) = l.v
proof
let v be Element of V such that
A1: T|(Carrier l) is one-to-one and
A2: v in Carrier l;
consider X being Subset of V such that
A3: X misses Carrier l and
A4: T"{T.v} = {v} \/ X by A1,A2,Th34;
per cases;
suppose
A5: X = {};
A6: dom l = [#]V by FUNCT_2:92;
l .: {v} = Im (l,v) .= {l.v} by A6,FUNCT_1:59;
then Sum (l .: T"{T.v}) = l.v by A4,A5,RLVECT_2:9;
hence thesis by Def5;
end;
suppose
A7: X <> {};
A8: l .: X c= {0.F}
proof
let y be object;
assume y in l .: X;
then consider x being object such that
A9: x in dom l and
A10: x in X and
A11: y = l.x by FUNCT_1:def 6;
A12: not x in Carrier l by A3,A10,XBOOLE_0:def 4;
reconsider x as Element of V by A9;
l.x = 0.F by A12;
hence thesis by A11,TARSKI:def 1;
end;
A13: l .: X misses l .: {v}
proof
assume l .: X meets l .: {v};
then consider x being object such that
A14: x in l .: X and
A15: x in l .: {v} by XBOOLE_0:3;
A16: dom l = [#]V by FUNCT_2:92;
l .: {v} = Im (l,v) .= {l.v} by A16,FUNCT_1:59;
then
A17: x = l.v by A15,TARSKI:def 1;
x = 0.F by A8,A14,TARSKI:def 1;
hence thesis by A2,A17,VECTSP_6:2;
end;
A18: dom l = [#]V by FUNCT_2:92;
{0.F} c= l .: X
proof
consider y being object such that
A19: y in X by A7,XBOOLE_0:def 1;
A20: not y in Carrier l by A3,A19,XBOOLE_0:def 4;
reconsider y as Element of V by A19;
let x be object;
assume x in {0.F};
then x = 0.F by TARSKI:def 1;
then l.y = x by A20;
hence thesis by A18,A19,FUNCT_1:def 6;
end;
then
A21: l .: X = {0.F} by A8;
A22: l .: {v} = Im (l,v) .= {l.v} by A18,FUNCT_1:59;
l .: T"{T.v} = (l .: {v}) \/ (l .: X) by A4,RELAT_1:120;
then Sum (l .: T"{T.v}) = (Sum (l .: {v})) + (Sum (l .: X)) by A13,
RLVECT_2:12
.= l.v + (Sum ({0.F})) by A22,A21,RLVECT_2:9
.= l.v + 0.F by RLVECT_2:9
.= l.v by RLVECT_1:4;
hence thesis by Def5;
end;
end;
theorem Th38:
for G being FinSequence of V st rng G = Carrier l & T|(Carrier l
) is one-to-one holds T*(l (#) G) = (T@l) (#) (T*G)
proof
let G be FinSequence of V such that
A1: rng G = Carrier l and
A2: T|(Carrier l) is one-to-one;
reconsider R = (T@l) (#) (T*G) as FinSequence of W;
reconsider L = T*(l (#) G) as FinSequence of W;
A3: len R = len (T*G) by VECTSP_6:def 5
.= len G by FINSEQ_2:33;
A4: len L = len (l (#) G) by FINSEQ_2:33
.= len G by VECTSP_6:def 5;
for k being Nat st 1 <= k & k <= len L holds L.k = R.k
proof
A5: dom R = Seg len G by A3,FINSEQ_1:def 3;
let k be Nat such that
A6: 1 <= k & k <= len L;
reconsider gk = G/.k as Element of V;
len (l (#) G) = len G by VECTSP_6:def 5;
then
A7: dom (l (#) G) = Seg len G by FINSEQ_1:def 3;
A8: k in dom (l (#) G) by A4,A6,A7;
then
A9: k in dom G by A7,FINSEQ_1:def 3;
then
A10: G.k = G/.k by PARTFUN1:def 6;
then reconsider Gk = G.k as Element of V;
(T*G).k = T.Gk by A9,FUNCT_1:13;
then reconsider TGk = (T*G).k as Element of W;
(l (#) G).k = (l.gk)*gk by A8,VECTSP_6:def 5;
then
A11: L.k = T.((l.gk)*gk) by A8,FUNCT_1:13
.= (l.gk)*(T.gk) by MOD_2:def 2
.= (l.Gk)*TGk by A9,A10,FUNCT_1:13;
G.k in rng G & (T*G).k = T.(G.k) by A9,FUNCT_1:3,13;
then
A12: (T@l).((T*G).k) = l.(G.k) by A1,A2,Th37;
dom T = [#]V by Th7;
then dom (T*G) = dom G by A1,RELAT_1:27;
then (T*G)/.k = (T*G).k by A9,PARTFUN1:def 6;
hence thesis by A7,A8,A11,A5,A12,VECTSP_6:def 5;
end;
hence thesis by A4,A3;
end;
theorem Th39:
T|(Carrier l) is one-to-one implies T .: (Carrier l) = Carrier ( T@l)
proof
assume
A1: T|(Carrier l) is one-to-one;
A2: T .: (Carrier l) c= Carrier (T@l)
proof
let w be object;
assume w in T .: (Carrier l);
then consider v being object such that
A3: v in dom T and
A4: v in Carrier l and
A5: T.v = w by FUNCT_1:def 6;
reconsider v as Element of V by A3;
(T@l).(T.v) = l.v & l.v <> 0.F by A1,A4,Th37,VECTSP_6:2;
hence thesis by A5;
end;
Carrier (T@l) c= T .: (Carrier l) by Th30;
hence thesis by A2;
end;
theorem Th40:
for A being Subset of V, B being Basis of V, l being
Linear_Combination of B \ A st A is Basis of ker T & A c= B holds T.(Sum l) =
Sum (T@l)
proof
let A be Subset of V, B be Basis of V, l be Linear_Combination of B \ A;
assume A is Basis of ker T & A c= B;
then
A1: T|(B \ A) is one-to-one by Th22;
Carrier l c= B \ A by VECTSP_6:def 4;
then
A2: (T|(B \ A))|(Carrier l) = T|(Carrier l) by RELAT_1:74;
then
A3: T|(Carrier l) is one-to-one by A1,FUNCT_1:52;
consider G being FinSequence of V such that
A4: G is one-to-one and
A5: rng G = Carrier l and
A6: Sum l = Sum (l (#) G) by VECTSP_6:def 6;
set H = T*G;
reconsider H as FinSequence of W;
A7: rng H = T .: (Carrier l) by A5,RELAT_1:127
.= Carrier (T@l) by A3,Th39;
dom T = [#]V by Th7;
then H is one-to-one by A4,A5,A1,A2,Th1,FUNCT_1:52;
then
A8: Sum (T@l) = Sum ((T@l) (#) H) by A7,VECTSP_6:def 6;
T*(l (#) G) = (T@l) (#) H by A5,A3,Th38;
hence thesis by A6,A8,MATRLIN:16;
end;
theorem Th41:
for X being Subset of V st X is linearly-dependent holds ex l
being Linear_Combination of X st Carrier l <> {} & Sum l = 0.V
proof
let X be Subset of V;
assume X is linearly-dependent;
then
not (for l being Linear_Combination of X st Sum l = 0.V holds Carrier l
= {}) by VECTSP_7:def 1;
hence thesis;
end;
:: "Pulling back" a linear combination from the image space of a
:: linear transformation to the base space.
definition
let F be Field, V,W be VectSp of F, X be Subset of V, T be
linear-transformation of V,W, l be Linear_Combination of T .: X;
assume
A1: T|X is one-to-one;
func T#l -> Linear_Combination of X equals
:Def6:
(l*T) +* ((V \ X) --> 0.F);
coherence
proof
rng (l*T) c= rng l & rng l c= [#]F by FUNCT_2:92,RELAT_1:26;
then
A2: rng (l*T) c= [#]F;
dom l = [#]W by FUNCT_2:92;
then rng T c= dom l by Th7;
then
A3: dom (l*T) = dom T by RELAT_1:27;
set f = (l*T) +* ((V \ X) --> 0.F);
A4: dom ((V \ X) --> 0.F) = [#]V \ X;
rng ((V \ X) --> 0.F) c= {0.F} by FUNCOP_1:13;
then rng ((V \ X) --> 0.F) c= [#]F by XBOOLE_1:1;
then rng f c= rng (l*T) \/ rng ((V \ X) --> 0.F) & rng (l*T) \/ rng ((V \
X) --> 0.F) c= [#]F by A2,FUNCT_4:17,XBOOLE_1:8;
then
A5: rng f c= [#]F;
dom T = [#]V & [#]V \/ ([#]V \ X) = [#]V by Th7,XBOOLE_1:12;
then dom f = [#]V by A3,A4,FUNCT_4:def 1;
then reconsider f as Element of Funcs ([#]V,[#]F) by A5,FUNCT_2:def 2;
ex T being finite Subset of V st for v being Element of V st not v in
T holds f.v = 0.F
proof
set C = { v where v is Element of V : f.v <> 0.F };
C c= [#]V
proof
let x be object;
assume x in C;
then ex v being Element of V st v = x & f.v <> 0.F;
hence thesis;
end;
then reconsider C as Subset of V;
ex g being Function st g is one-to-one & dom g = C & rng g c= Carrier l
proof
set S = (T"(Carrier l)) /\ X;
set g = T|S;
take g;
A6: C c= S
proof
let x be object such that
A7: x in C;
A8: ex v being Element of V st v = x & f.v <> 0.F by A7;
reconsider x as Element of V by A7;
A9: now
assume not x in X;
then
A10: x in V \ X by XBOOLE_0:def 5;
then x in dom ((V \ X) --> 0.F);
then f.x = ((V \ X) --> 0.F).x by FUNCT_4:13;
hence contradiction by A8,A10,FUNCOP_1:7;
end;
then not x in V \ X by XBOOLE_0:def 5;
then
A11: f.x = (l*T).x by A4,FUNCT_4:11;
A12: dom T = [#]V by Th7;
then (l*T).x = l.(T.x) by FUNCT_1:13;
then T.x in Carrier l by A8,A11;
then x in T"(Carrier l) by A12,FUNCT_1:def 7;
hence thesis by A9,XBOOLE_0:def 4;
end;
A13: dom T = [#]V by Th7;
A14: rng g c= Carrier l
proof
let y be object;
assume y in rng g;
then consider x being object such that
A15: x in dom g and
A16: y = g.x by FUNCT_1:def 3;
x in T"(Carrier l) by A15,XBOOLE_0:def 4;
then T.x in Carrier l by FUNCT_1:def 7;
hence thesis by A15,A16,FUNCT_1:49;
end;
S c= C
proof
let x be object such that
A17: x in S;
A18: x in X by A17,XBOOLE_0:def 4;
A19: x in T"(Carrier l) by A17,XBOOLE_0:def 4;
then
A20: x in dom T by FUNCT_1:def 7;
A21: T.x in Carrier l by A19,FUNCT_1:def 7;
reconsider x as Element of V by A17;
A22: l.(T.x) <> 0.F by A21,VECTSP_6:2;
not x in dom ((V \ X) --> 0.F) by A18,XBOOLE_0:def 5;
then
A23: f.x = (l*T).x by FUNCT_4:11;
(l*T).x = l.(T.x) by A20,FUNCT_1:13;
hence thesis by A23,A22;
end;
then S = C by A6;
hence thesis by A1,A13,A14,Th2,RELAT_1:62,XBOOLE_1:17;
end;
then card C c= card Carrier l by CARD_1:10;
then reconsider C as finite Subset of V;
take C;
thus thesis;
end;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
Carrier f c= X
proof
let x be object such that
A24: x in Carrier f;
reconsider x as Element of V by A24;
now
assume not x in X;
then
A25: x in V \ X by XBOOLE_0:def 5;
then f.x = ((V \ X) --> 0.F).x by A4,FUNCT_4:13
.= 0.F by A25,FUNCOP_1:7;
hence contradiction by A24,VECTSP_6:2;
end;
hence thesis;
end;
hence thesis by VECTSP_6:def 4;
end;
end;
theorem Th42:
for X being Subset of V, l being Linear_Combination of T .: X, v
being Element of V st v in X & T|X is one-to-one holds (T#l).v = l.(T.v)
proof
let X be Subset of V, l be Linear_Combination of T .: X, v be Element of V;
assume v in X & T|X is one-to-one;
then ( not v in dom ((V \ X) --> 0.F))& T#l = (l*T) +* ((V \ X) --> 0.F) by
Def6,XBOOLE_0:def 5;
then
A1: (T#l).v = (l*T).v by FUNCT_4:11;
dom T = [#]V by Th7;
hence thesis by A1,FUNCT_1:13;
end;
:: # is a right inverse of @
theorem Th43:
for X being Subset of V, l being Linear_Combination of T .: X st
T|X is one-to-one holds T@(T#l) = l
proof
let X be Subset of V, l be Linear_Combination of T .: X such that
A1: T|X is one-to-one;
let w be Element of W;
set m = T@(T#l);
per cases;
suppose
A2: w in Carrier l;
then
A3: l.w <> 0.F by VECTSP_6:2;
A4: dom (T#l) = [#]V by FUNCT_2:92;
Carrier l c= T .: X by VECTSP_6:def 4;
then consider v being object such that
A5: v in dom T and
A6: v in X and
A7: w = T.v by A2,FUNCT_1:def 6;
reconsider v as Element of V by A5;
consider B being Subset of V such that
A8: B misses X and
A9: T"{T.v} = {v} \/ B by A1,A6,Th34;
A10: (T#l).v = l.(T.v) by A1,A6,Th42;
A11: (T#l) .: {v} = Im (T#l,v) .= {(T#l).v} by A4,FUNCT_1:59;
A12: m.w = Sum ((T#l) .: T"{T.v}) by A7,Def5
.= Sum ({l.(T.v)} \/ ((T#l) .: B)) by A9,A10,A11,RELAT_1:120;
per cases;
suppose
B = {};
then m.w = Sum ({l.(T.v)} \/ {}F) by A12
.= l.w by A7,RLVECT_2:9;
hence thesis;
end;
suppose
A13: B <> {};
Carrier (T#l) c= X by VECTSP_6:def 4;
then B misses Carrier (T#l) by A8,XBOOLE_1:63;
then m.w = Sum ({l.(T.v)} \/ {0.F}) by A12,A13,Th35
.= Sum ({l.(T.v)}) + Sum ({0.F}) by A3,A7,RLVECT_2:12,ZFMISC_1:11
.= l.(T.v) + Sum ({0.F}) by RLVECT_2:9
.= l.(T.v) + 0.F by RLVECT_2:9
.= l.w by A7,RLVECT_1:4;
hence thesis;
end;
end;
suppose
A14: not w in Carrier l;
then
A15: l.w = 0.F;
now
assume
A16: m.w <> 0.F;
then w in Carrier m;
then T"{w} meets Carrier (T#l) by Th36;
then consider v being Element of V such that
A17: v in T"{w} and
A18: v in Carrier (T#l) by Th3;
T.v in {w} by A17,FUNCT_1:def 7;
then
A19: T.v = w by TARSKI:def 1;
A20: Carrier (T#l) c= X by VECTSP_6:def 4;
then T|(Carrier (T#l)) is one-to-one by A1,Th2;
then m.w = (T#l).v by A18,A19,Th37
.= 0.F by A1,A15,A18,A19,A20,Th42;
hence contradiction by A16;
end;
hence thesis by A14;
end;
end;
begin :: The rank+nullity theorem
definition
let F be Field, V,W be finite-dimensional VectSp of F, T be
linear-transformation of V,W;
func rank(T) -> Nat equals
dim (im T);
coherence;
func nullity(T) -> Nat equals
dim (ker T);
coherence;
end;
::$N Rank-nullity theorem
theorem Th44:
for V,W being finite-dimensional VectSp of F, T being
linear-transformation of V,W holds dim V = rank(T) + nullity(T)
proof
let V,W be finite-dimensional VectSp of F, T be linear-transformation of V,W;
set A = the finite Basis of ker T;
reconsider A9 = A as Subset of V by Th19;
consider B being Basis of V such that
A1: A c= B by VECTSP_9:13;
reconsider B as finite Subset of V;
reconsider X = B \ A9 as finite Subset of B by XBOOLE_1:36;
reconsider X as finite Subset of V;
A2: B = A \/ X by A1,XBOOLE_1:45;
reconsider B as finite Basis of V;
reconsider A as finite Basis of ker T;
reconsider C = T .: X as finite Subset of W;
A3: T|X is one-to-one by A1,Th22;
A4: C is linearly-independent
proof
assume C is linearly-dependent;
then consider l being Linear_Combination of C such that
A5: Carrier l <> {} and
A6: Sum l = 0.W by Th41;
ex m being Linear_Combination of X st l = T@m
proof
reconsider l9 = l as Linear_Combination of T .: X;
set m = T#(l9);
take m;
thus thesis by A3,Th43;
end;
then consider m being Linear_Combination of B \ A9 such that
A7: l = T@m;
T.(Sum m) = 0.W by A1,A6,A7,Th40;
then Sum m in ker T by Th10;
then Sum m in Lin A by VECTSP_7:def 3;
then Sum m in Lin A9 by VECTSP_9:17;
then consider n being Linear_Combination of A9 such that
A8: Sum m = Sum n by VECTSP_7:7;
A9: Carrier (m - n) c= (Carrier m) \/ (Carrier n) & (B \ A9) \/ A9 = B by A1,
VECTSP_6:41,XBOOLE_1:45;
A10: Carrier m c= B \ A9 & Carrier n c= A by VECTSP_6:def 4;
then (Carrier m) \/ (Carrier n) c= (B \ A9) \/ A by XBOOLE_1:13;
then Carrier (m - n) c= B by A9;
then reconsider o = m - n as Linear_Combination of B by VECTSP_6:def 4;
A11: B is linearly-independent by VECTSP_7:def 3;
(Sum m) - (Sum n) = 0.V by A8,VECTSP_1:19;
then Sum (m - n) = 0.V by VECTSP_6:47;
then
A12: Carrier o = {} by A11,VECTSP_7:def 1;
A9 misses B \ A9 by XBOOLE_1:79;
then Carrier (m - n) = (Carrier m) \/ (Carrier n) by A10,Th32,XBOOLE_1:64;
then Carrier m = {} by A12;
then T .: (Carrier m) = {};
hence thesis by A5,A7,Th30,XBOOLE_1:3;
end;
dom T = [#]V by Th7;
then X c= dom (T|X) by RELAT_1:62;
then X,(T|X) .: X are_equipotent by A3,CARD_1:33;
then X,C are_equipotent by RELAT_1:129;
then
A13: card C = card X by CARD_1:5;
reconsider C as finite Subset of im T by Th12;
reconsider L = Lin C as strict Subspace of im T;
for v being Element of im T holds v in L
proof
reconsider A9 = A as Subset of V by Th19;
let v be Element of im T;
reconsider v9 = v as Element of W by VECTSP_4:10;
reconsider C9 = C as Subset of W;
v in im T;
then consider u being Element of V such that
A14: T.u = v9 by Th13;
V is_the_direct_sum_of Lin A9, Lin (B \ A9) by A1,Th33;
then
A15: (Omega).V = (Lin A9) + (Lin (B \ A9)) by VECTSP_5:def 4;
u in (Omega).V;
then consider u1, u2 being Element of V such that
A16: u1 in Lin A9 and
A17: u2 in Lin (B \ A9) and
A18: u = u1 + u2 by A15,VECTSP_5:1;
consider l being Linear_Combination of B \ A9 such that
A19: u2 = Sum l by A17,VECTSP_7:7;
Lin A = ker T by VECTSP_7:def 3;
then u1 in ker T by A16,VECTSP_9:17;
then
A20: T.u1 = 0.W by Th10;
T@l is Linear_Combination of T .: (Carrier l) & Carrier l c= B \ A9
by Th29,VECTSP_6:def 4;
then reconsider m = T@l as Linear_Combination of C9 by RELAT_1:123
,VECTSP_6:4;
T.u = T.u1 + T.u2 by A18,VECTSP_1:def 20;
then
A21: T.u = T.u2 by A20,RLVECT_1:4;
ex m being Linear_Combination of C9 st v = Sum m
proof
take m;
thus thesis by A1,A14,A21,A19,Th40;
end;
then v in Lin C9 by VECTSP_7:7;
hence thesis by VECTSP_9:17;
end;
then
A22: Lin C = im T by VECTSP_4:32;
reconsider C as linearly-independent Subset of im T by A4,VECTSP_9:12;
reconsider C as finite Basis of im T by A22,VECTSP_7:def 3;
A23: nullity T = card A & rank T = card C by VECTSP_9:def 1;
dim V = card B by VECTSP_9:def 1
.= rank T + nullity T by A2,A13,A23,CARD_2:40,XBOOLE_1:79;
hence thesis;
end;
theorem
for V,W being finite-dimensional VectSp of F, T being
linear-transformation of V,W st T is one-to-one holds dim V = rank T
proof
let V,W be finite-dimensional VectSp of F, T be linear-transformation of V,W;
assume T is one-to-one;
then ker T = (0).V by Th15;
then
A1: nullity(T) = 0 by Th16;
dim V = rank(T) + nullity(T) by Th44
.= rank(T) by A1;
hence thesis;
end;