:: Rank of Submodule, Linear Transformations and Linearly Independent Subsets
:: of $\mathbb Z$-module
:: by Kazuhisa Nakasho , Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received July 10, 2014
:: Copyright (c) 2014-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 TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
FUNCOP_1, REALSET1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, CARD_3, ARYTM_3,
ARYTM_1, NUMBERS, XXREAL_0, REAL_1, NAT_1, INT_1, VALUED_0, ORDINAL4,
GRCAT_1, MESFUNC1, MOD_3, CLASSES1, RFINSEQ, FINSEQ_1, VALUED_1,
SUPINF_2, MSSUBFAM, STRUCT_0, RLVECT_1, RLSUB_1, RLSUB_2, RLVECT_2,
RLVECT_3, RMOD_2, PRELAMB, UNIALG_1, MSAFREE2, RANKNULL, UPROOTS,
VECTSP10, ZMODUL01, ZMODUL03, ZMODUL05, SETWISEO, BINOP_2, VECTSP_1,
INT_3, FUNCSDOM, VECTSP_2;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
CLASSES1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, FUNCOP_1, FUNCT_4,
FINSET_1, SETWOP_2, RFINSEQ, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, INT_1, VALUED_0, FINSEQ_1, FINSEQOP, RVSUM_1, FUNCT_7, STRUCT_0,
ALGSTR_0, GROUP_1, RLVECT_1, GR_CY_1, VECTSP_1, MOD_2, GRCAT_1, RLVECT_2,
VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, INT_3, LOPBAN_1, VECTSP_7,
ZMODUL01, ZMODUL02, ZMODUL03, RANKNULL;
constructors RELSET_1, REALSET1, CLASSES1, FINSEQOP, FINSOP_1, FUNCT_7,
ALGSTR_1, GR_CY_1, LOPBAN_1, ZMODUL02, ZMODUL03, SETWISEO, BINOP_2,
VECTSP_2, VECTSP_4, VECTSP_6, VECTSP_7, INT_3, ALGSTR_0, RLVECT_2,
REAL_1, VFUNCT_1, RFINSEQ, GRCAT_1, MOD_2, VECTSP_5, MOD_4, ZMODUL01,
RANKNULL;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
FUNCT_2, FUNCOP_1, FINSET_1, CARD_1, NUMBERS, XREAL_0, NAT_1, INT_1,
VALUED_0, FINSEQ_1, STRUCT_0, RLVECT_1, ZMODUL02, ZMODUL03, ZMODUL04,
BINOP_2, INT_3, MEMBERED;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, FUNCT_1, FUNCT_2;
equalities FINSEQ_1, STRUCT_0, ALGSTR_0, SUBSET_1, VECTSP_4, VECTSP_6,
RELAT_1;
expansions TARSKI, XBOOLE_0, FINSEQ_1, STRUCT_0, VECTSP_1, ZMODUL03, MOD_2,
VECTSP_6, VECTSP_7, CLASSES1;
theorems TARSKI, XBOOLE_0, XBOOLE_1, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1,
FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1,
CLASSES1, NAT_1, INT_1, CARD_2, FINSEQ_1, FINSEQ_2, FINSEQOP, FINSEQ_3,
FINSEQ_4, RVSUM_1, RFINSEQ, FUNCT_7, RLVECT_1, VECTSP_1, GR_CY_1,
RANKNULL, ZMODUL01, ZMODUL02, ZMODUL03, ZMODUL04, FINSOP_1, VECTSP_5,
VECTSP_7, VECTSP_4, VECTSP_6, MOD_2, INT_3, MOD_3;
schemes FUNCT_2, CLASSES1, NAT_1, FINSEQ_2;
begin :: 1. Rank of submodule of $\mathbb Z$-module
reserve V,W for Z_Module;
registration
let V be LeftMod of INT.Ring;
let A be finite Subset of V;
cluster Lin(A) -> finitely-generated;
correctness
proof
for x being object st x in A holds x in the carrier of Lin(A)
proof
let x be object such that
A1: x in A;
x in Lin(A) by A1,MOD_3:5;
hence thesis;
end;
then A c= the carrier of Lin(A);
then reconsider AA = A as finite Subset of Lin(A);
Lin(AA) = Lin(A) by ZMODUL03:20;
hence thesis;
end;
end;
theorem RL5Th33:
for V be finite-rank free Z_Module holds
rank V = 0 iff (Omega).V = (0).V
proof
let V be finite-rank free Z_Module;
consider I being finite Subset of V such that
A1: I is Basis of V by ZMODUL03:def 3;
hereby
consider I being finite Subset of V such that
A2: I is Basis of V by ZMODUL03:def 3;
assume rank V = 0;
then card I = 0 by A2,ZMODUL03:def 5; then
A3: I = {}(the carrier of V);
(Omega).V = Lin(I) by A2,VECTSP_7:def 3
.= (0).V by A3,ZMODUL02:67;
hence (Omega).V = (0).V;
end;
assume (Omega).V = (0).V;
then Lin(I) = (0).V by A1,VECTSP_7:def 3;
then I = {} or I = {0.V} by ZMODUL02:68;
hence thesis by A1,VECTSP_7:def 3,ZMODUL03:def 5,CARD_1:27;
end;
registration
let V be finite-rank free Z_Module;
cluster finite for Basis of V;
existence
proof
consider A being finite Subset of V such that
A1: A is Basis of V by ZMODUL03:def 3;
reconsider A as Basis of V by A1;
take A;
thus thesis;
end;
end;
registration
let V be finite-rank free Z_Module;
cluster -> finite for Basis of V;
correctness;
end;
theorem RL5Th29:
for V being finite-rank free Z_Module, W being Submodule of V holds
rank W <= rank V
proof
let V be finite-rank free Z_Module, W be Submodule of V;
consider I be finite Subset of V such that
A1: I is Basis of V by ZMODUL03:def 3;
W is finite-rank;
then consider A be finite Subset of W such that
A2: A is Basis of W;
reconsider AA = A as linearly-independent Subset of V
by A2,ZMODUL03:15,VECTSP_7:def 3;
card AA c= card I by A1,ZMODUL04:20;
then card A c< card I or card A = card I;
then card (card A) < card (card I) or card A = card I by CARD_2:48;
then card A <= rank V by A1,ZMODUL03:def 5;
hence thesis by A2,ZMODUL03:def 5;
end;
theorem RL5Th30:
for V being Z_Module, A being finite linearly-independent Subset of V holds
card A = rank Lin(A)
proof
let V be Z_Module, A be finite linearly-independent Subset of V;
set W = Lin(A);
now
let x be object;
assume x in A;
then x in W by ZMODUL02:65;
hence x in the carrier of W;
end;
then reconsider B = A as finite linearly-independent Subset of W
by ZMODUL03:16,TARSKI:def 3;
W = Lin B by ZMODUL03:20;
then reconsider B as Basis of W by VECTSP_7:def 3;
card B = rank W by ZMODUL03:def 5;
hence thesis;
end;
theorem
for V being finite-rank free Z_Module holds
rank V = rank (Omega).V
proof
let V be finite-rank free Z_Module;
consider I being finite Subset of V such that
A1: I is Basis of V by ZMODUL03:def 3;
A2: (Omega).V = Lin(I) by A1,VECTSP_7:def 3;
card I = rank V & I is linearly-independent
by A1,ZMODUL03:def 5,VECTSP_7:def 3;
hence thesis by A2,RL5Th30;
end;
theorem
for V being finite-rank free Z_Module holds
rank V = 1 iff ex v being VECTOR of V st v <> 0.V & (Omega).V = Lin{v}
proof
let V be finite-rank free Z_Module;
hereby
consider I being finite Subset of V such that
A1: I is Basis of V by ZMODUL03:def 3;
assume rank V = 1;
then card I = 1 by A1,ZMODUL03:def 5;
then consider v being object such that
A2: I = {v} by CARD_2:42;
v in I by A2,TARSKI:def 1;
then reconsider v as VECTOR of V;
A3: v <> 0.V by A1,A2,VECTSP_7:def 3;
Lin{v} = the ModuleStr of V by A1,A2,VECTSP_7:def 3;
hence ex v being VECTOR of V st v <> 0.V & (Omega).V = Lin{v} by A3;
end;
given v being VECTOR of V such that
A4: v <> 0.V & (Omega).V = Lin{v};
{v} is linearly-independent & Lin{v} = the ModuleStr of V
by A4,ZMODUL02:59; then
A5: {v} is Basis of V by VECTSP_7:def 3;
card {v} = 1 by CARD_1:30;
hence thesis by A5,ZMODUL03:def 5;
end;
theorem
for V being finite-rank free Z_Module holds
rank V = 2 iff ex u, v being VECTOR of V st u <> v &
{u, v} is linearly-independent & (Omega).V = Lin{u, v}
proof
let V be finite-rank free Z_Module;
hereby
consider I being finite Subset of V such that
A1: I is Basis of V by ZMODUL03:def 3;
assume rank V = 2; then
A2: card I = 2 by A1,ZMODUL03:def 5;
then consider u being object such that
A3: u in I by CARD_1:27,XBOOLE_0:def 1;
reconsider u as VECTOR of V by A3;
now
assume I c= {u};
then card I <= card {u} by NAT_1:43;
then 2 <= 1 by A2,CARD_1:30;
hence contradiction;
end;
then consider v being object such that
A4: v in I and
A5: not v in {u};
reconsider v as VECTOR of V by A4;
A6: v <> u by A5,TARSKI:def 1;
A7:
now
assume not I c= {u, v};
then consider w being object such that
A8: w in I and
A9: not w in {u, v};
{u, v, w} c= I by A3,A4,A8,ENUMSET1:def 1; then
A10: card {u, v, w} <= card I by NAT_1:43;
w <> u & w <> v by A9,TARSKI:def 2;
then 3 <= 2 by A2,A6,A10,CARD_2:58;
hence contradiction;
end;
{u, v} c= I by A3,A4,TARSKI:def 2; then
A11: I = {u, v} by A7; then
A12: {u, v} is linearly-independent by A1,VECTSP_7:def 3;
Lin{u, v} = (Omega).V by A1,A11,VECTSP_7:def 3;
hence
ex u, v being VECTOR of V st u <> v & {u, v} is linearly-independent &
(Omega).V = Lin{u, v} by A6,A12;
end;
given u, v being VECTOR of V such that
A13: u <> v and
A14: {u, v} is linearly-independent and
A15: (Omega).V = Lin{u, v};
A16: {u, v} is Basis of V by A14,A15,VECTSP_7:def 3;
card {u, v} = 2 by A13,CARD_2:57;
hence thesis by A16,ZMODUL03:def 5;
end;
:: Fixed-Dimensional Subspace Family and Pencil of Subspaces
RL5Lm2: for V being finite-rank free Z_Module, W being Submodule of V,
n being Nat holds
n <= rank V implies ex W being strict free Submodule of V st rank W = n
proof
let V be finite-rank free Z_Module, W be Submodule of V, n be Nat;
consider I being finite Subset of V such that
A1: I is Basis of V by ZMODUL03:def 3;
assume n <= rank V;
then n <= card I by A1,ZMODUL03:def 5;
then consider A being finite Subset of I such that
A2: card A = n by FINSEQ_4:72;
reconsider A as finite Subset of V by XBOOLE_1:1;
reconsider W = Lin(A) as strict finite-rank free Submodule of V;
A is linearly-independent by ZMODUL02:56,A1,VECTSP_7:def 3;
then rank W = n by A2,RL5Th30;
hence thesis;
end;
theorem
for V being finite-rank free Z_Module, W being Submodule of V,
n being Nat holds
n <= rank V iff ex W being strict free Submodule of V st rank W = n
by RL5Lm2,RL5Th29;
definition
let V be finite-rank free Z_Module, n be Nat;
func n Submodules_of V -> set means :RL5Def4:
for x being object holds
x in it iff ex W being strict free Submodule of V st W = x & rank W = n;
existence
proof
set S = {Lin(A) where A is finite Subset of V: A is linearly-independent &
card A = n};
take S;
for x being object holds
x in S iff ex W being strict free Submodule of V st W = x & rank W = n
proof
let x be object;
hereby
assume x in S; then
A1: ex A being finite Subset of V st x = Lin(A) &
A is linearly-independent & card A = n;
then reconsider W = x as strict free Submodule of V;
rank W = n by A1,RL5Th30;
hence ex W being strict free Submodule of V st W = x & rank W = n;
end;
given W being strict free Submodule of V such that
A2: W = x and
A3: rank W = n;
consider A being finite Subset of W such that
A4: A is Basis of W by ZMODUL03:def 3;
reconsider A as Subset of W;
reconsider B = A as linearly-independent Subset of V
by A4,ZMODUL03:15,VECTSP_7:def 3;
A5: x = Lin(A) by A2,A4,VECTSP_7:def 3
.= Lin(B) by ZMODUL03:20;
then card B = n by A2,A3,RL5Th30;
hence thesis by A5;
end;
hence thesis;
end;
uniqueness
proof
let S1, S2 be set;
assume that
A6: for x being object holds
x in S1 iff ex W being strict free Submodule of V st W = x &
rank W = n and
A7: for x being object holds
x in S2 iff ex W being strict free Submodule of V st W = x & rank W = n;
for x being object holds x in S1 iff x in S2
proof
let x be object;
hereby
assume x in S1;
then ex W being strict free Submodule of V st W = x & rank W = n by A6;
hence x in S2 by A7;
end;
assume x in S2;
then ex W being strict free Submodule of V st W = x & rank W = n by A7;
hence thesis by A6;
end;
hence thesis by TARSKI:2;
end;
end;
theorem
for V being finite-rank free Z_Module, n being Nat holds
n <= rank V implies n Submodules_of V is non empty
proof
let V be finite-rank free Z_Module, n be Nat;
assume n <= rank V;
then ex W being strict free Submodule of V st rank W = n by RL5Lm2;
hence thesis by RL5Def4;
end;
theorem
for V being finite-rank free Z_Module, n being Nat holds
rank V < n implies n Submodules_of V = {}
proof
let V be finite-rank free Z_Module, n be Nat;
assume that
A1: rank V < n and
A2: n Submodules_of V <> {};
consider x being object such that
A3: x in n Submodules_of V by A2,XBOOLE_0:def 1;
ex W being strict free Submodule of V st W = x & rank W = n by A3,RL5Def4;
hence contradiction by A1,RL5Th29;
end;
theorem
for V being finite-rank free Z_Module, W being Submodule of V,
n being Nat holds
n Submodules_of W c= n Submodules_of V
proof
let V be finite-rank free Z_Module, W be Submodule of V, n be Nat;
let x be object;
assume x in n Submodules_of W;
then consider W1 being strict free Submodule of W such that
A1: W1 = x and
A2: rank W1 = n by RL5Def4;
reconsider W1 as strict free Submodule of V by ZMODUL01:42;
W1 in n Submodules_of V by A2,RL5Def4;
hence thesis by A1;
end;
theorem
for F,G being FinSequence of INT, v be Integer holds
len F = len G + 1 & G = F | (dom G) & v = F.(len F) implies
Sum(F) = Sum(G) + v
proof
let F,G be FinSequence of INT, v be Integer;
assume that
A1: len F = len G + 1 and
A2: G = F | (dom G) and
A3: v = F.(len F);
reconsider Fr = F, Gr = G as real-valued FinSequence;
reconsider vr = v as Real;
set k = len G;
dom G = Seg k by FINSEQ_1:def 3;
then Fr = Gr^<*vr*> by A1,A2,A3,FINSEQ_3:55;
hence thesis by RVSUM_1:74;
end;
theorem RLVECT142: ::: should be proven for real-valued
for F,G being FinSequence of INT
st rng F = rng G & F is one-to-one
& G is one-to-one holds Sum(F) = Sum(G)
proof
let F,G be FinSequence of INT;
assume A1:rng F = rng G & F is one-to-one & G is one-to-one;
thus Sum F = addint $$ F by GR_CY_1:2
.= addint $$ G by A1,FINSOP_1:8
.= Sum G by GR_CY_1:2;
end;
definition
let T be finite Subset of the carrier of INT.Ring;
::: what for? defined for reals, then redefine
func Sum T -> Element of INT.Ring means
ex F being FinSequence of INT st
rng F = T & F is one-to-one & it = Sum F;
existence
proof
consider p being FinSequence such that
A1: rng p = T and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of the carrier of INT.Ring
by A1,FINSEQ_1:def 4;
INT = the carrier of INT.Ring by INT_3:def 3; then
reconsider F = p as FinSequence of INT;
reconsider Sp = Sum F as Element of INT.Ring by INT_3:def 3;
take Sp,F;
thus rng F = T & F is one-to-one & Sum F = Sp by A1,A2;
end;
uniqueness by RLVECT142;
end;
theorem RF9:
for K being Ring
for R1,R2 be FinSequence of K st R1,R2 are_fiberwise_equipotent
holds Sum R1 = Sum R2
proof
let K be Ring;
let R1,R2 be FinSequence of K;
defpred P[Nat] means for f,g be FinSequence of K st f,g
are_fiberwise_equipotent & len f = $1 holds Sum f = Sum g;
assume
A1: R1,R2 are_fiberwise_equipotent;
A2: len R1 = len R1;
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A4: P[n];
let f,g be FinSequence of K;
assume that
A5: f,g are_fiberwise_equipotent and
A6: len f = n+1;
set a = f/.(n+1);
A7: rng f = rng g by A5,CLASSES1:75;
0 qua Nat+1<=n+1 by NAT_1:13;
then
Z: n+1 in dom f by A6,FINSEQ_3:25; then
X: a = f.(n+1) by PARTFUN1:def 6;
then a in rng g by A7,FUNCT_1:def 3,Z;
then consider m being Nat such that
A8: m in dom g and
A9: g.m = a by FINSEQ_2:10;
set gg = g/^m, gm = g|m;
m<=len g by A8,FINSEQ_3:25; then
A10: len gm = m by FINSEQ_1:59;
A11: 1<=m by A8,FINSEQ_3:25;
then max(0,m-1) = m-1 by FINSEQ_2:4;
then reconsider m1 = m-1 as Element of NAT by FINSEQ_2:5;
A12: m = m1+1; then
A13: Seg m1 c= Seg m by FINSEQ_1:5,NAT_1:11;
m in Seg m by A11;
then gm.m = a by A8,A9,RFINSEQ:6;
then
A14: gm = (gm|m1)^<*a*> by A10,A12,RFINSEQ:7;
set fn = f|n;
A15: g = (g|m)^(g/^m) by RFINSEQ:8;
A16: gm|m1 = gm|(Seg m1)
.= (g|(Seg m))|(Seg m1)
.= g|((Seg m)/\(Seg m1)) by RELAT_1:71
.= g|(Seg m1) by A13,XBOOLE_1:28
.= g|m1;
A17: f = fn ^ <*a*> by A6,RFINSEQ:7,X;
now
let x be object;
card Coim(f,x) = card Coim(g,x) by A5; then
card(fn"{x}) + card(<*a*>"{x}) =
card(((g|m1)^<*a*>^(g/^m))"{x}) by A15,A14,A16,A17,FINSEQ_3:57
.= card(((g|m1)^<*a*>)"{x}) + card((g/^m)"{x}) by FINSEQ_3:57
.= card((g|m1)"{x})+ card(<*a*>"{x}) + card((g/^m)"{x}) by FINSEQ_3:57
.= card((g|m1)"{x}) + card((g/^m)"{x})+ card(<*a*>"{x})
.= card(((g|m1)^(g/^m))"{x})+ card(<*a*>"{x}) by FINSEQ_3:57;
hence card Coim(fn,x) = card Coim((g|m1)^(g/^m),x);
end; then
A18: fn, (g|m1)^(g/^m) are_fiberwise_equipotent;
len fn = n by A6,FINSEQ_1:59,NAT_1:11;
then Sum fn = Sum((g|m1)^gg) by A4,A18;
hence Sum f = Sum((g|m1)^gg) + Sum <*a*> by A17,RLVECT_1:41
.= Sum(g|m1) + Sum gg + Sum <*a*> by RLVECT_1:41
.= Sum(g|m1) + (Sum gg + Sum <*a*>) by RLVECT_1:def 3
.= Sum(g|m1) + (Sum <*a*> + Sum gg)
.= Sum(g|m1) + Sum <*a*> + Sum gg by RLVECT_1:def 3
.= Sum gm + Sum gg by A14,A16,RLVECT_1:41
.= Sum g by A15,RLVECT_1:41;
end;
A19: P[0]
proof
let f,g be FinSequence of K;
assume f,g are_fiberwise_equipotent & len f = 0; then
A20: len g = 0 & f = <*>the carrier of INT.Ring by RFINSEQ:3;
then g = <*>the carrier of INT.Ring;
hence thesis by A20;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A19,A3);
hence thesis by A1,A2;
end;
::$CT 2
::theorem
::: for X be finite Subset of INT st X = {}
::: holds Sum X = 0 by Def2,GR_CY_1:3,RELAT_1:38;
::theorem
:: for v be Element of INT holds Sum {v} = v
:: proof
:: let v be Element of INT;
:: A1: Sum <*v*> = v by RVSUM_1:73;
:: rng <*v*> = {v} & <*v*> is one-to-one by FINSEQ_1:39;
:: hence Sum {v} = v by A1,Def2;
:: end;
::theorem
:: for S, T being finite Subset of INT
:: st T misses S holds
:: Sum (T \/ S) = (Sum T) + (Sum S)
:: proof
:: let S, T be finite Subset of INT;
:: consider F being FinSequence of INT such that
:: A1: rng F = T \/ S and
:: A2: F is one-to-one & Sum (T \/ S) = Sum F by Def2;
:: consider G being FinSequence of INT such that
:: A3: rng G = T and
:: A4: G is one-to-one and
:: A5: Sum T = Sum G by Def2;
:: consider H being FinSequence of INT such that
:: A6: rng H = S and
:: A7: H is one-to-one and
:: A8: Sum S = Sum H by Def2;
:: set I = G ^ H;
:: reconsider G0 = G, H0 = H as real-valued FinSequence;
::: A9: Sum (G0 ^ H0) = Sum (G) + Sum (H) by RVSUM_1:75;
:: assume T misses S; then
:: A10: G ^ H is one-to-one by A3,A4,A6,A7,FINSEQ_3:91;
:: rng (G ^ H) = rng F by A1,A3,A6,FINSEQ_1:31;
:: hence Sum (T \/ S) = (Sum T) + (Sum S) by A2,A5,A8,A9,A10,RLVECT142;
:: end;
definition
::$CD 3
end;
theorem MATRLIN16:
for R being Ring
for V1, V2 being LeftMod of R
for f being Function of V1, V2
for p being FinSequence of V1 st f is additive homogeneous holds
f . (Sum p) = Sum (f * p)
proof
let R be Ring;
let V1, V2 be LeftMod of R, f be Function of V1,V2;
let p be FinSequence of V1;
defpred P[FinSequence of V1] means f.Sum($1) = Sum(f*$1);
assume
A1: f is additive homogeneous;
A2: for p being FinSequence of V1 for w being Element of V1 st P[p] holds
P[p^<*w*>]
proof
let p be FinSequence of V1;
let w be Element of V1 such that
A3: f.Sum p = Sum (f*p);
thus f.Sum(p^<*w*>) = f.(Sum(p) + Sum<*w*>) by RLVECT_1:41
.= Sum(f*p) + f.Sum<*w*> by A1,A3
.= Sum(f*p) + f.w by RLVECT_1:44
.= Sum(f*p) + Sum<*f.w*> by RLVECT_1:44
.= Sum(f*p^<*f.w*>) by RLVECT_1:41
.= Sum(f*(p^<*w*>)) by FINSEQOP:8;
end;
f.Sum(<*>(the carrier of V1)) = f.(0.V1) by RLVECT_1:43
.= f.(0.R * 0.V1) by VECTSP_1:14
.= 0.R * f.(0.V1) by A1
.= 0.V2 by VECTSP_1:14
.= Sum(<*>(the carrier of V2)) by RLVECT_1:43
.= Sum(f*<*>(the carrier of V1)); then
A4: P[<*>(the carrier of V1)];
for p being FinSequence of V1 holds P[p] from FINSEQ_2:sch 2(A4,A2);
hence thesis;
end;
theorem
for V be free Z_Module st [#]V is finite holds
(Omega).V = (0).V
proof
let V be free Z_Module;
assume
A1: [#]V is finite;
assume
A2: (Omega).V <> (0).V;
consider A being Subset of V such that
a3: A is base by VECTSP_7:def 4;
per cases;
suppose A = {};
then Lin(A) = Lin({}(the carrier of V))
.= (0).V by VECTSP_7:9;
hence contradiction by A2,a3;
end;
suppose A <> {};
then consider v be object such that
A4: v in A by XBOOLE_0:def 1;
reconsider v as VECTOR of V by A4;
{v} is linearly-independent by a3,A4,ZFMISC_1:31,ZMODUL02:56; then
A5: v <> 0.V;
deffunc F(Element of INT.Ring) = $1*v;
consider f being Function of the carrier of INT.Ring,
the carrier of V such that
A6: for x being Element of INT.Ring holds f.x = F(x) from FUNCT_2:sch 4;
A7: dom f = the carrier of INT.Ring &
rng f c= the carrier of V by FUNCT_2:def 1;
for x1, x2 being object st x1 in the carrier of INT.Ring &
x2 in the carrier of INT.Ring & f.x1 = f.x2 holds
x1 = x2
proof
let x1, x2 be object;
assume
A8: x1 in the carrier of INT.Ring & x2 in the carrier of
INT.Ring & f.x1 = f.x2;
then reconsider a1=x1,a2=x2 as Element of INT.Ring;
a1*v = f.a2 by A6,A8
.= a2*v by A6;
then a1*v - a2*v = 0.V by RLVECT_1:5;
then (a1-a2)* v = 0.V by ZMODUL01:9;
then a1-a2 = 0.INT.Ring by A5,ZMODUL01:def 7;
hence x1 = x2 by INT_3:def 3;
end;
then f is one-to-one by FUNCT_2:19;
then card(the carrier of INT.Ring) c=
card(the carrier of V) by A7,CARD_1:10;
hence contradiction by A1;
end;
end;
begin :: Basic facts of linear transformations
reserve T for linear-transformation of V,W;
theorem
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) by RANKNULL:8;
theorem
T.(0.V) = 0.W by RANKNULL:9;
theorem
for x being Element of V holds x in ker T iff T.x = 0.W by RANKNULL:10;
theorem
0.V in ker T by RANKNULL:11;
theorem
for X being Subset of V holds T .: X is Subset of im T by RANKNULL:12;
theorem
for y being Element of W holds y in im T iff
ex x being Element of V st y = T.x by RANKNULL:13;
theorem
for x being Element of ker T holds T.x = 0.W by RANKNULL:14;
theorem
T is one-to-one implies ker T = (0).V by RANKNULL:15;
theorem
for V being finite-rank free Z_Module holds rank ((0).V) = 0
proof
let V be finite-rank free Z_Module;
(Omega).((0).V) = (0).((0).V) by ZMODUL01:51;
hence thesis by RL5Th33;
end;
theorem Th17:
for x,y being Element of V st T.x = T.y holds x - y in ker T
by RANKNULL:17;
theorem Th18:
for A being Subset of V, x,y being Element of V st x - y in Lin A holds
x in Lin (A \/ {y}) by RANKNULL:18;
begin :: Some basic facts about linearly independent subsets and linear
:: combinations
theorem
for X being Subset of V st V is Submodule of W holds X is Subset of W
proof
let X be Subset of V;
assume V is Submodule of W; then
A1: [#]V c= [#]W by VECTSP_4:def 2;
X c= [#]W by A1;
hence thesis;
end;
theorem ThLin4:
for R being Ring
for V being LeftMod of R,
A being Subset of V holds A is Subset of Lin(A)
proof
let R be Ring;
let V be LeftMod of R;
let A be Subset of V;
for x being object st x in A holds x in the carrier of Lin(A)
proof
let x be object such that
A1: x in A;
x in Lin(A) by A1,MOD_3:5;
hence thesis;
end;
then A c= the carrier of Lin(A);
hence thesis;
end;
theorem ThLin7:
for V being LeftMod of INT.Ring,
A being linearly-independent Subset of V
holds A is Basis of Lin(A)
proof
let V be LeftMod of INT.Ring,
A be linearly-independent Subset of V;
reconsider AA = A as Subset of Lin(A) by ThLin4;
(Omega).Lin(A) = Lin(AA) by ZMODUL03:20;
hence thesis by ZMODUL03:16,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 V be finite-rank free Z_Module,
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 V be finite-rank free Z_Module,
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;
reconsider X = {x} as Subset of Lin A by A1,SUBSET_1:41;
reconsider A9 = A as Basis of Lin A by A3,ThLin7;
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 ZMODUL03:18;
hence thesis by ZMODUL03:16;
end;
suppose
A is linearly-dependent;
hence thesis by ZMODUL02:56,XBOOLE_1:7;
end;
end;
registration
let V be finite-rank free Z_Module, W be Z_Module;
let T be linear-transformation of V,W;
cluster ker T -> finite-rank free;
correctness;
end;
reserve T for linear-transformation of V,W;
theorem Th22:
for V be finite-rank free Z_Module,A being Subset of V,
B being Basis of V,
T being linear-transformation of V,W
st A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
proof
let V be finite-rank free Z_Module,
A be Subset of V, B be Basis of V,
T be linear-transformation of V,W 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: not x1 in (A9 \/ {x2})
proof
assume
A8: x1 in A9 \/ {x2};
per cases by A8,XBOOLE_0:def 3;
suppose
x1 in A9;
hence contradiction by A3,XBOOLE_0:def 5;
end;
suppose
x1 in {x2};
hence contradiction by A6,TARSKI:def 1;
end;
end;
A9: f.x2 = T.x2 by A4,FUNCT_1:49;
reconsider A as Subset of (ker T) by A1;
reconsider A as Basis of (ker T) by A1;
A10: ker T = Lin A by VECTSP_7:def 3;
f.x1 = T.x1 by A3,FUNCT_1:49;
then x1 - x2 in ker T by A5,A9,Th17;
then x1 - x2 in Lin A9 by A10,ZMODUL03:20; then
A11: x1 in Lin (A9 \/ {x2}) by Th18;
{x2} \/ {x1} = {x1,x2} by ENUMSET1:1; then
A12: (A9 \/ {x2}) \/ {x1} = A9 \/ {x1,x2} by XBOOLE_1:4;
{x1,x2} c= B
proof
let z be object such that
A13: z in {x1,x2};
per cases by A13,TARSKI:def 2;
suppose
z = x1;
hence thesis by A3,XBOOLE_0:def 5;
end;
suppose
z = x2;
hence thesis by A4,XBOOLE_0:def 5;
end;
end; then
A14: A9 \/ {x1,x2} c= B by A2,XBOOLE_1:8;
B is linearly-independent by VECTSP_7:def 3;
hence thesis by A7,A11,A12,A14,Th21,ZMODUL02:56;
end;
theorem
for R being Ring, V being LeftMod of R
for A being Subset of V, l being Linear_Combination of A,
x being Element of V, a being Element of R holds
l +* (x,a) is Linear_Combination of A \/ {x}
proof
let R be Ring, V be LeftMod of R;
let A be Subset of V, l be Linear_Combination of A,
x be Element of V, a be Element of R;
set m = l +* (x,a);
A1: dom m = dom l by FUNCT_7:30
.= [#]V by FUNCT_2:def 1;
rng m c= the carrier of R;
then reconsider m as Element of Funcs ([#]V,the carrier of R)
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.R
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.R;
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;
T c= A \/ {x} by XBOOLE_1:9,VECTSP_6:def 4;
then Carrier m c= A \/ {x} by A9;
hence thesis by VECTSP_6:def 4;
end;
reserve l for Linear_Combination of V;
registration
let R be non degenerated Ring, V be LeftMod of R;
cluster linearly-dependent for Subset of V;
existence
proof
reconsider S = {0.V} as Subset of V;
take S;
thus thesis;
end;
end;
:: Restricting a linear combination to a given set
definition
let R be Ring;
let V be LeftMod of R, l be Linear_Combination of V, A be Subset of V;
func l!A -> Linear_Combination of A equals
(l|A) +* ((A`) --> 0.R);
coherence
proof
set f = (l|A) +* ((A`) --> 0.R);
A1: dom f = dom (l|A) \/ dom ((A`) --> 0.R) by FUNCT_4:def 1;
dom l = [#]V by FUNCT_2:92; then
dom (l|A) = A by RELAT_1:62; then
A4: dom f = [#]V by A1,XBOOLE_1:45;
rng f c= rng (l|A) \/ rng ((A`) --> 0.R) & rng (l|A) \/
rng ((A`) --> 0.R) c= [#]R by FUNCT_4:17; then
rng f c= the carrier of R;
then reconsider f as Element of Funcs([#]V,the carrier of R)
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.R
proof
set D = { v where v is Element of V : f.v <> 0.R};
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.R;
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
A10: x = v and
A11: f.v <> 0.R;
A13:
now
assume
A14: v in A`;
then f.v = ((A`) --> 0.R).v by A1,A4,FUNCT_4:def 1
.= 0.R by A14,FUNCOP_1:7;
hence contradiction by A11;
end;
then v in A by XBOOLE_0:def 5; then
A15: (l|A).v = l.v by FUNCT_1:49;
not v in dom ((A`) --> 0.R) by A13;
then f.v = (l|A).v by FUNCT_4:11;
hence thesis by A10,A11,A15;
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
A16: x in Carrier f;
reconsider x as Element of V by A16;
now
assume not x in A; then
A17: x in A` by XBOOLE_0:def 5;
then x in dom (l|A) \/ (dom ((A`) --> 0.R))
by XBOOLE_0:def 3;
then f.x = ((A`) --> 0.R).x by A17,FUNCT_4:def 1;
hence contradiction by A16,A17,FUNCOP_1:7,VECTSP_6:2;
end;
hence thesis;
end;
hence thesis by VECTSP_6:def 4;
end;
end;
theorem Th24:
for R be Ring
for V be LeftMod of R, l be Linear_Combination of V holds
l = l!Carrier l
proof
let R be Ring;
let V be LeftMod of R, l be Linear_Combination of V;
set f = l | (Carrier l);
set g = (Carrier l)` --> 0.R;
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;
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 (Carrier l)` by XBOOLE_0:def 5;
then m.x = g.x & g.x = 0.R by A3,FUNCOP_1:7,FUNCT_4:def 1;
hence thesis by A6;
end;
end;
hence thesis by A2;
end;
Lm1: for R being Ring for V being LeftMod of R
for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite
proof
let R be Ring;
let V be LeftMod of R;
let l be Linear_Combination of V;
let X be Subset of V;
A1: l = l!(Carrier l) by Th24;
(rng (l|Carrier l)) \/ rng ((Carrier l)` --> 0.R) 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 R being Ring for V being LeftMod of R
for l being Linear_Combination of V
for A being Subset of V, v being Element of V st v in A holds
(l !A).v = l.v
proof
let R be Ring;
let V be LeftMod of R;
let l be Linear_Combination of V;
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 ((A`) --> 0.R)) = [#]V by FUNCT_4:def 1;
not v in dom ((A`) --> 0.R) 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 R being Ring, V being LeftMod of R
for l being Linear_Combination of V
for A being Subset of V, v being Element of V st not v in A holds
(l!A).v = 0.R
proof
let R be Ring, V be LeftMod of R;
let l be Linear_Combination of V;
let A be Subset of V, v be Element of V;
assume not v in A; then
A1: v in A` by XBOOLE_0:def 5;
A2: dom (l!A) = [#]V by FUNCT_2:92;
dom ((A`) --> 0.R) = A` &
dom (l!A) = (dom (l|A)) \/ (dom ((A`) --> 0.R))
by FUNCT_4:def 1;
then (l!A).v = ((A`) --> 0.R).v by A1,A2,FUNCT_4:def 1
.= 0.R by A1,FUNCOP_1:7;
hence thesis;
end;
theorem Th27:
for R being Ring, V being LeftMod of R
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 R be Ring, V be LeftMod of R;
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.R by Th26;
(l!A).v = l.v by A4,Th25;
then r.v = l.v + 0.R by A5,VECTSP_6:22
.= l.v;
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.R by Th26;
(l!(B\A)).v = l.v by A6,Th25;
then r.v = 0.R + l.v by A7,VECTSP_6:22
.= l.v;
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.R by Th26;
(l!A).v = 0.R by A1,A8,Th26;
then r.v = 0.R + 0.R by A10,VECTSP_6:22
.= 0.R;
hence l.v = r.v by A9;
end;
end;
registration
let R be Ring, V be LeftMod of R,
l be Linear_Combination of V, X be Subset of V;
cluster l .: X -> finite;
coherence by Lm1;
end;
theorem Th28:
for R being Ring, V being LeftMod of R,
l be Linear_Combination of V
for X being Subset of V st X misses Carrier l holds l .: X c= {0.R}
proof
let R be Ring, V be LeftMod of R, l be Linear_Combination of V;
let X be Subset of V such that
A1: X misses Carrier l;
set M = l .: X;
for y be object st y in l .: X holds y in {0.R}
proof
let y be object;
assume y in M;
then consider x being object such that
x in dom l and
A2: x in X and
A3: y = l.x by FUNCT_1:def 6;
reconsider x as Element of V by A2;
now
assume l.x <> 0.R;
then x in Carrier l;
hence contradiction by A1,A2,XBOOLE_0:def 4;
end;
hence thesis by A3,TARSKI:def 1;
end;
hence l .: X c= {0.R};
end;
definition
let K be Ring;
let V,W be VectSp of K,
l be Linear_Combination of V,
T be linear-transformation of V,W;
let w be Element of W;
func lCFST(l,T,w) -> (the carrier of K) -valued FinSequence equals
l * canFS((T"{w}) /\ (Carrier l));
correctness
proof
set p = l * canFS((T"{w})/\(Carrier l));
set f = canFS((T"{w})/\(Carrier l));
dom l = the carrier of V by FUNCT_2:def 1;
then rng f c= dom l by XBOOLE_1:1;
hence thesis by FINSEQ_1:16;
end;
end;
reserve V,W for Z_Module;
reserve l for Linear_Combination of V;
reserve T for linear-transformation of V,W;
theorem ThTF3C0:
for V,W be non empty set,
f be FinSequence,
l be Function of V,W
st rng f c= V
holds l*f is W-valued FinSequence-like
proof
let V,W be non empty set,
f be FinSequence,
l be Function of V,W;
assume rng f c= V; then
rng f c= dom l by FUNCT_2:def 1;
hence thesis by FINSEQ_1:16;
end;
registration
let V,W be non empty set,
f be V-valued FinSequence,
l be Function of V,W;
cluster l*f -> W -valued FinSequence-like;
coherence
proof
rng f c= V;
hence l*f is W-valued FinSequence-like by ThTF3C0;
end;
end;
ThTF3C1:
for V,W be non empty set,
A be finite Subset of V,
l be Function of V,W
holds l*canFS(A) is W-valued FinSequence-like
proof
let V,W be non empty set,
A be finite Subset of V,
l be Function of V,W;
set p = l*canFS(A);
set f = canFS(A);
dom l = V by FUNCT_2:def 1;
then rng f c= dom l by XBOOLE_1:1;
hence thesis by FINSEQ_1:16;
end;
registration
let V,W be non empty set,
A be finite Subset of V,
l be Function of V,W;
cluster l*canFS(A) -> W -valued FinSequence-like;
coherence by ThTF3C1;
end;
registration
let R be Ring;
let V be LeftMod of R,
A be finite Subset of V,
l be Linear_Combination of V;
cluster l*canFS(A) -> (the carrier of R) -valued FinSequence-like;
coherence;
end;
theorem ThTF3C3:
for V,W be non empty set,
f,g be V-valued FinSequence,
l be Function of V,W
holds l*(f^g) = (l*f)^(l*g)
proof
let V,W be non empty set,
f,g be V-valued FinSequence,
l be Function of V,W;
A1: dom l = V by FUNCT_2:def 1;
A2: rng f c= V;
A3: rng g c= V;
A4: rng(f^g) = rng f \/ rng g by FINSEQ_1:31;
A5: dom(l*f) = dom f by A1,A2,RELAT_1:27
.= Seg(len f) by FINSEQ_1:def 3; then
A6: len(l*f) = len f by FINSEQ_1:def 3;
dom(l*g) = dom g by A1,A3,RELAT_1:27
.= Seg(len g) by FINSEQ_1:def 3; then
A7: len(l*g) = len g by FINSEQ_1:def 3;
A8: dom(f^g) = Seg(len(f^g)) by FINSEQ_1:def 3
.= Seg(len f + len g) by FINSEQ_1:22;
A9: len((l*f)^(l*g)) = len(l*f) + len(l*g) by FINSEQ_1:22
.= len f + len g by A5,A7,FINSEQ_1:def 3;
A10: dom((l*f)^(l*g)) = Seg(len f + len g) by A9,FINSEQ_1:def 3;
now let k be object;
assume
A11: k in dom(l*(f^g));
then reconsider i = k as Nat;
A12: i in dom(f^g) by A1,A4,A11,RELAT_1:27;
per cases by A12,FINSEQ_1:25;
suppose
A13: i in dom f; then
A14: i in dom(l*f) by A1,A2,RELAT_1:27;
thus (l*(f^g)).k = l.((f^g).i) by A11,FUNCT_1:12
.= l.(f.i) by A13,FINSEQ_1:def 7
.= (l*f).i by A13,FUNCT_1:13
.= ((l*f)^(l*g)).k by A14,FINSEQ_1:def 7;
end;
suppose ex n be Nat st n in dom g & i = len f + n;
then consider n be Nat such that
A15: n in dom g & i = len f + n;
A16: n in dom(l*g) by A1,A3,A15,RELAT_1:27;
thus (l*(f^g)).k = l.((f^g).i) by A11,FUNCT_1:12
.= l.(g.n) by A15,FINSEQ_1:def 7
.= (l*g).n by A15,FUNCT_1:13
.= ((l*f)^(l*g)).k by A6,A15,A16,FINSEQ_1:def 7;
end;
end;
hence thesis by A1,A4,A8,A10,FUNCT_1:2,RELAT_1:27;
end;
theorem ThTF3C2:
for R being Ring
for V be LeftMod of R,
A,B be finite Subset of V,
l be Linear_Combination of V,
l0,l1,l2 being FinSequence of R
st A /\ B = {} & l0 = l*canFS(A \/ B) & l1 = l*canFS(A) & l2 = l*canFS(B)
holds Sum l0 = Sum l1 + Sum l2
proof
let R be Ring;
let V be LeftMod of R,
A,B be finite Subset of V,
l be Linear_Combination of V,
l0,l1,l2 being FinSequence of R;
assume A1: A /\ B = {};
assume TT: l0 = l*canFS(A \/ B) & l1 = l*canFS(A) & l2 = l*canFS(B);
per cases;
suppose
A2: A \/ B = {}; then
A3: A = {};
a3: B = {} by A2;
rng (l*canFS(B)) c= the carrier of R; then
reconsider lC = l*canFS(B) as FinSequence of R by FINSEQ_1:def 4;
lC = <*>the carrier of R by a3; then
Sum (lC) = 0.R by RLVECT_1:43
.= 0.R;
hence Sum l0 = Sum l1 + Sum l2 by A2,A3,TT;
end;
suppose
A5: A \/ B <> {};
rng canFS(A) = A by FUNCT_2:def 3;
then reconsider ca = canFS(A) as (the carrier of V)-valued FinSequence
by RELAT_1:def 19;
rng canFS(B) = B by FUNCT_2:def 3;
then reconsider cb = canFS(B) as (the carrier of V)-valued FinSequence
by RELAT_1:def 19;
set la = len(canFS(A));
set lb = len(canFS(B));
set lab = len(canFS(A)^canFS(B));
set lavb = len(canFS(A \/ B));
set F = l*canFS(A \/ B);
set G = l1^l2;
set H = (canFS(A \/ B))" * (canFS(A)^canFS(B));
A6: la = card(A) by FINSEQ_1:93;
A7: lavb = card(A \/ B) by FINSEQ_1:93
.= card(A) + card(B) by A1,CARD_2:40,XBOOLE_0:def 7
.= la + lb by A6,FINSEQ_1:93;
A8: lab = la + lb by FINSEQ_1:22; then
A9: dom(canFS(A)^canFS(B)) = Seg(la + lb) by FINSEQ_1:def 3;
A10: rng(canFS(A)^canFS(B))
= rng(canFS(A)) \/ rng(canFS(B)) by FINSEQ_1:31
.= A \/ rng(canFS(B)) by FUNCT_2:def 3
.= A \/ B by FUNCT_2:def 3;
reconsider AB = (canFS(A))^(canFS(B)) as Function of Seg(la+lb),A \/ B
by A9,A10,FUNCT_2:1;
A11: rng(canFS(A \/ B)) = A \/ B by FUNCT_2:def 3;
reconsider INVAB = (canFS(A \/ B))"
as Function of (A \/ B), Seg card(A \/B) by FINSEQ_1:95;
A12: INVAB * canFS(A \/ B) = id dom(canFS(A \/ B))
& canFS(A \/ B) * INVAB = id rng(canFS(A \/ B)) by FUNCT_1:39;
A13: dom(canFS(A \/ B)) = Seg len(canFS(A \/ B)) by FINSEQ_1:def 3
.= Seg card(A \/ B) by FINSEQ_1:93; then
A14: (canFS(A \/ B)) is Function of Seg card(A \/ B),(A \/ B)
by A11,FUNCT_2:1;
A15: dom INVAB = (A \/ B) by A5,FUNCT_2:def 1;
A16: rng INVAB = Seg card(A \/ B) by A12,A13,A14,FUNCT_2:18
.= Seg(card(A) + card(B)) by A1,CARD_2:40,XBOOLE_0:def 7
.= Seg(la + lb) by A6,FINSEQ_1:93;
A17: dom H = dom(canFS(A)^canFS(B)) by A10,A15,RELAT_1:27
.= Seg(la + lb) by A8,FINSEQ_1:def 3;
A18: rng H = Seg(la + lb) by A10,A15,A16,RELAT_1:28;
A19: the carrier of V = dom l by FUNCT_2:def 1;
A20: dom F = dom canFS(A \/ B) by A11,A19,RELAT_1:27
.= Seg(la + lb) by A7,FINSEQ_1:def 3;
rng canFS(A) = A by FUNCT_2:def 3;
then dom(l*canFS(A)) = dom canFS(A) by A19,RELAT_1:27
.= Seg la by FINSEQ_1:def 3; then
A21: len(l*canFS(A)) = la by FINSEQ_1:def 3;
A22: rng canFS(B) = B by FUNCT_2:def 3;
then dom(l*canFS(B)) = dom canFS(B) by A19,RELAT_1:27
.= Seg lb by FINSEQ_1:def 3; then
A23: len(l*canFS(B)) = lb by FINSEQ_1:def 3;
set G = (l*canFS(A))^(l*canFS(B));
A24: len G = la + lb by A21,A23,FINSEQ_1:22;
rng(canFS(A)) misses rng(canFS(B)) by A1,A22,FUNCT_2:def 3; then
A25: (canFS(A)^canFS(B)) is one-to-one by FINSEQ_3:91;
A26: dom H = dom G by A17,A24,FINSEQ_1:def 3;
A27: F * H = l * canFS(A \/ B) * (canFS(A \/ B))" * (canFS(A)^canFS(B))
by RELAT_1:36
.= l * (canFS(A \/ B)*(canFS(A \/ B))") * (canFS(A)^canFS(B))
by RELAT_1:36
.= l * (id rng(canFS(A \/ B))) * (canFS(A)^canFS(B)) by FUNCT_1:39
.= l * (id (A \/ B)) * (canFS(A)^canFS(B)) by FUNCT_2:def 3
.= l * (id (A \/ B) * AB) by RELAT_1:36
.= l * (canFS(A)^canFS(B)) by FUNCT_2:17
.= (l*ca)^(l*cb) by ThTF3C3
.= G;
Z2: rng G = rng (l*canFS(A)) \/ rng (l*canFS(B)) by FINSEQ_1:31;
rng F c= the carrier of R;
then reconsider FR = F as FinSequence of R by FINSEQ_1:def 4;
reconsider GR = G as FinSequence of R by Z2,FINSEQ_1:def 4;
thus Sum l0 = Sum(FR) by TT
.= Sum (GR) by A18,A20,A25,A26,A27,CLASSES1:77,RF9
.= Sum (l1 ^ l2) by TT
.= Sum (l*canFS(A)) + Sum(l*canFS(B)) by TT,RLVECT_1:41
.= Sum l1 + Sum l2 by TT;
end;
end;
theorem ThTF3C3:
for R being Ring
for V be LeftMod of R,
A be finite Subset of V,
l,l0 be Linear_Combination of V
st l | (Carrier l0) = l0 | (Carrier l0)
& Carrier l0 c= Carrier l & A c= Carrier l0
holds Sum(l*canFS(A)) = Sum(l0*canFS(A))
proof
let R be Ring;
let V be LeftMod of R,
A be finite Subset of V,
l,l0 be Linear_Combination of V;
assume
A1: l | (Carrier l0) = l0 | (Carrier l0)
& Carrier l0 c= Carrier l & A c= Carrier l0;
dom l0 = the carrier of V by FUNCT_2:def 1;
then dom(l0 | (Carrier l0)) = (Carrier l0) by RELAT_1:62; then
A2: rng (canFS(A)) c= dom (l0 | (Carrier l0)) by A1;
then l * canFS(A) = (l0 | (Carrier l0)) * canFS(A) by A1,RELAT_1:165;
hence thesis by A2,RELAT_1:165;
end;
definition
let R be Ring;
let V,W be LeftMod of R,
l be Linear_Combination of V, T be linear-transformation of V,W;
func T @* l -> Linear_Combination of W means
:LDef5:
Carrier it c= T.:(Carrier l)
& for w being Element of W holds it.w = Sum(lCFST(l,T,w));
existence
proof
defpred P[object,object] means
ex w being Element of W st $1 = w & $2 = Sum (lCFST(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 (lCFST(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= the carrier of R
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;
consider w being Element of W such that
A7: x = w & f.x = Sum lCFST(l,T,w) by A2,A3,A5;
thus thesis by A6,A7;
end;
A8: for w being Element of W holds f.w = Sum (lCFST(l,T,w))
proof
let w be Element of W;
ex w9 being Element of W st w = w9 & f.w = Sum (lCFST(l,T,w9)) by A3;
hence thesis;
end;
reconsider f as Element of Funcs([#]W,the carrier of R)
by A2,A4,FUNCT_2:def 2;
set X = { w where w is Element of W : f.w <> 0.R };
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.R;
hence thesis;
end;
then reconsider X as Subset of W;
set C = Carrier l;
reconsider TC = T .: C as Subset of W;
A9: X c= TC
proof
let x be object;
assume x in X;
then consider w being Element of W such that
A10: x = w and
A11: f.w <> 0.R;
T"{w} meets Carrier l
proof
assume T"{w} misses Carrier l; then
lCFST(l,T,w) = <*>the carrier of R; then
Sum(lCFST(l,T,w)) = 0.R by RLVECT_1:43;
hence contradiction by A8,A11;
end;
then consider y being object such that
A13: y in T"{w} and
A14: y in Carrier l by XBOOLE_0:3;
A15: dom T = [#]V by RANKNULL:7;
reconsider y as Element of V by A14;
T.y in {w} by A13,FUNCT_1:def 7;
then T.y = w by TARSKI:def 1;
hence thesis by A10,A14,A15,FUNCT_1:def 6;
end;
then reconsider X as finite Subset of W;
ex T being finite Subset of W
st for w being Element of W st not w in T holds f.w = 0.R
proof
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(lCFST(l,T,w))
proof
let w be Element of W;
ex w9 being Element of W st w = w9 & f.w = Sum(lCFST(l,T,w9)) by A3;
hence thesis;
end;
hence thesis by A9;
end;
uniqueness
proof
let f,g be Linear_Combination of W such that
A16: Carrier f c= T.:(Carrier l)
& for w being Element of W holds f.w = Sum(lCFST(l,T,w)) and
A17: Carrier g c= T.:(Carrier l)
& for w being Element of W holds g.w = Sum(lCFST(l,T,w));
A18: 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 (lCFST(l,T,x)) by A16;
hence thesis by A17;
end;
dom f = [#]W & dom g = [#]W by FUNCT_2:92;
hence thesis by A18;
end;
end;
theorem LTh29:
for R being Ring
for V,W be LeftMod of R,
l be Linear_Combination of V, T be linear-transformation of V,W holds
(T@*l) is Linear_Combination of T .: (Carrier l)
proof
let R be Ring;
let V,W be LeftMod of R;
let l be Linear_Combination of V, T be linear-transformation of V,W;
Carrier (T@*l) c= T.:(Carrier l) by LDef5;
hence thesis by VECTSP_6:def 4;
end;
theorem ThTF3B2:
for K being Ring
for V,W being LeftMod of K,
T being linear-transformation of V,W,
s being Vector of W holds
(for A being Subset of V, l being Linear_Combination of A
st (for v being Vector of V st v in Carrier l holds T.v = s)
holds T.Sum(l) = Sum(lCFST(l,T,s)) * s)
proof
let K be Ring;
let V, W be LeftMod of K,
T be linear-transformation of V,W,
s be Vector of W;
A1: T is additive;
defpred P[Nat] means
for A being Subset of V, l being Linear_Combination of A
st card (Carrier l) = $1
& (for v being Vector of V st v in Carrier l holds T.v = s)
holds T.Sum(l) = Sum(lCFST(l,T,s)) * s;
reconsider SZ0 = {0.K} as finite Subset of K;
A2: P[0]
proof
let A be Subset of V, l be Linear_Combination of A;
assume card Carrier l = 0
& for v being Vector of V st v in Carrier l holds T.v = s; then
A3: Carrier l = {}; then
A4: T.Sum(l) = T.(0.V) by VECTSP_6:19
.= T.(0.K * 0.V) by VECTSP_1:14
.= 0.K * T.(0.V) by MOD_2:def 2
.= 0.W by VECTSP_1:14;
set g = canFS((T"{s}) /\ Carrier l);
lCFST(l,T,s) = <*>the carrier of K by A3; then
Sum(lCFST(l,T,s)) = 0.K by RLVECT_1:43;
hence T.Sum(l) = Sum(lCFST(l,T,s)) * s by A4,VECTSP_1:14;
end;
A5: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A6: P[n];
let A be Subset of V,
l be Linear_Combination of A;
assume
A7: card(Carrier l) = n + 1
& (for v being Vector of V st v in Carrier l holds T.v = s);
then (Carrier l) <> {};
then consider w be object such that
A8: w in Carrier l by XBOOLE_0:def 1;
reconsider w as Element of the carrier of V by A8;
A9: card((Carrier l) \ {w})
= card(Carrier l) - card({w}) by A8,CARD_2:44,ZFMISC_1:31
.= n + 1 - 1 by A7,CARD_2:42
.= n;
reconsider A0 = (Carrier l) \ {w} as finite Subset of V;
reconsider B0 = {w} as finite Subset of V;
defpred PA0[object, object] means $1 is Vector of V implies
($1 in A0 & $2 = l.$1) or (not $1 in A0 & $2 = 0.K);
A10: for x being object st x in the carrier of V
ex y being object st y in the carrier of K & PA0[x, y]
proof
let x be object;
assume x in the carrier of V;
then reconsider x9 = x as Vector of V;
per cases;
suppose
A11: x in A0;
l.x9 in the carrier of K;
hence thesis by A11;
end;
suppose
not x in A0;
hence thesis;
end;
end;
consider l0 be Function of the carrier of V, the carrier of K
such that
A13: for x being object st x in the carrier of V holds PA0[x, l0.x]
from FUNCT_2:sch 1(A10);
A14: for v being Vector of V st not v in A0 holds l0.v = 0.K by A13;
reconsider l0 as Element of Funcs(the carrier of V, the carrier
of K) by FUNCT_2:8;
reconsider l0 as Linear_Combination of V by A14,VECTSP_6:def 1;
A15: for x be object holds x in A0 iff x in Carrier l0
proof
let x be object;
hereby
assume
A16: x in A0;
then reconsider v=x as Vector of V;
A17: l0.v = l.v by A13,A16;
v in Carrier l by A16,XBOOLE_0:def 5;
then l0.v <> 0.K by A17,VECTSP_6:2;
hence x in Carrier l0;
end;
assume
A18: x in Carrier(l0);
then reconsider v = x as Vector of V;
ex v9 being Vector of V st v9 = v & l0.v9 <> 0.K by A18;
hence x in A0 by A13;
end; then
A19: Carrier(l0) = A0 by TARSKI:2;
then reconsider l0 as Linear_Combination of A0 by VECTSP_6:def 4;
A20: l0 | Carrier(l0) = l | Carrier(l0)
proof
reconsider L0 = l0 as Function of V,K;
reconsider L1 = l as Function of V,K;
reconsider L00 = L0 | Carrier(l0) as Function of Carrier(l0),
the carrier of K by FUNCT_2:32;
reconsider L11= L1 | Carrier(l0) as Function of Carrier(l0),
the carrier of K by FUNCT_2:32;
now
let x be object;
assume
A21: x in Carrier(l0);
then reconsider v = x as Vector of V;
thus L00.x = l0.v by A21,FUNCT_1:49
.= l.v by A13,A19,A21
.= L11.x by A21,FUNCT_1:49;
end;
hence thesis by FUNCT_2:12;
end;
defpred PB0[object, object] means $1 is Vector of V implies
($1 in B0 & $2 = l.$1) or (not $1 in B0 & $2 = 0.K);
A22: for x being object st x in the carrier of V
ex y being object st y in the carrier of K & PB0[x, y]
proof
let x be object;
assume x in the carrier of V;
then reconsider x9 = x as Vector of V;
per cases;
suppose
A23: x in B0;
l.x9 in the carrier of K;
hence thesis by A23;
end;
suppose
not x in B0;
hence thesis;
end;
end;
consider l1 be Function of V, K such that
A25: for x being object
st x in the carrier of V holds PB0[x, l1.x] from FUNCT_2:sch 1(A22);
A26: for v being Vector of V st not v in B0 holds l1.v = 0.K by A25;
reconsider l1 as Element of Funcs(the carrier of V,
the carrier of K) by FUNCT_2:8;
reconsider l1 as Linear_Combination of V by A26,VECTSP_6:def 1;
for x being object holds x in B0 iff x in Carrier l1
proof
let x be object;
hereby
assume
A27: x in B0; then
A28: x = w by TARSKI:def 1; then
A29: l1.w = l.w by A25,A27;
l.w <> 0.K by A8,VECTSP_6:2;
hence x in Carrier l1 by A28,A29;
end;
assume
A30:x in Carrier(l1);
then reconsider v = x as Vector of V;
ex v9 being Vector of V st v9 = v & l1.v9 <> 0.K by A30;
hence x in B0 by A25;
end;
then Carrier(l1) = B0 by TARSKI:2;
then reconsider l1 as Linear_Combination of B0 by VECTSP_6:def 4;
for v being Element of V holds l.v = (l0+l1).v
proof
let v be Element of V;
per cases;
suppose
A31: not v in Carrier l; then
A32: l.v = 0.K;
not v in A0 by A31,XBOOLE_0:def 5; then
l0.v = 0.K by A13; then
l.v = l0.v + l1.v by A25,A32;
hence thesis by VECTSP_6:22;
end;
suppose
A34: v in Carrier l;
per cases;
suppose
A35: v in {w};
then not v in A0 by XBOOLE_0:def 5; then
l0.v = 0.K by A13; then
l.v = l0.v + l1.v by A25,A35;
hence thesis by VECTSP_6:22;
end;
suppose
A37: not v in {w}; then
A38: v in A0 by A34,XBOOLE_0:def 5;
l1.v = 0.K by A25,A37; then
l.v = l0.v + l1.v by A13,A38;
hence thesis by VECTSP_6:22;
end;
end;
end;
then l = l0 + l1; then
A39: Sum (l) = Sum(l0) + Sum(l1) by VECTSP_6:44;
for v being Vector of V st v in (Carrier l0) holds T.v = s
proof
let v be Vector of V;
assume v in Carrier l0;
then v in Carrier l by A19,XBOOLE_0:def 5;
hence thesis by A7;
end; then
A40: T.Sum(l0) = Sum(lCFST(l0,T,s)) * s by A6,A9,A19;
A41: A0 \/ B0 = (Carrier l) \/ B0 by XBOOLE_1:39
.= (Carrier l) by A8,XBOOLE_1:12,ZFMISC_1:31;
A42: w in B0 by TARSKI:def 1;
A43: T.(Sum(l1)) = T.((l1.w)*w) by VECTSP_6:17
.= (l1.w)*T.w by MOD_2:def 2
.= (l1.w)*s by A7,A8
.= (l.w)*s by A25,A42
.= Sum(<*l.w*>)*s by RLVECT_1:44;
set WW = (lCFST(l0,T,s))^<*l/.w*>;
rng WW = rng lCFST(l0,T,s) \/ rng <*l/.w*> by FINSEQ_1:31;
then reconsider WW as FinSequence of K by FINSEQ_1:def 4;
reconsider L = Sum WW as Element of K;
A44: (T"{s}) /\ (Carrier l)
= (T"{s}) /\ A0 \/ (T"{s}) /\ B0 by A41,XBOOLE_1:23
.= (T"{s}) /\ (Carrier l0) \/ ((T"{s}) /\ B0) by A15,TARSKI:2;
reconsider S1 = (T"{s}) /\ (Carrier l0) as finite Subset of V;
now
let z be object;
assume
A45: z in B0;
T.w = s by A7,A8; then
A46: T.w in {s} by TARSKI:def 1;
w in T"{s} by A46,FUNCT_2:38;
hence z in T"{s} by A45,TARSKI:def 1;
end;
then B0 c= T"{s}; then
A47: (T"{s}) /\ B0 = {w} by XBOOLE_1:28;
reconsider S2 = (T"{s}) /\ B0 as finite Subset of the carrier of V;
A48: ((Carrier l) \ {w}) /\ B0
= (B0 /\ (Carrier l)) \ B0 by XBOOLE_1:49
.= {} by XBOOLE_1:17,37;
A49: S1 /\ S2 = ((T"{s}) /\ (Carrier l0) /\ B0) /\ (T"{s}) by XBOOLE_1:16
.= ((T"{s}) /\ ((Carrier l) \ {w}) /\ B0) /\ (T"{s}) by A15,TARSKI:2
.= ((T"{s}) /\ {}) /\ (T"{s}) by A48,XBOOLE_1:16
.= {};
A50: Carrier l0 c= Carrier l by A19,XBOOLE_1:36;
reconsider ll = l as Function of the carrier of V,
the carrier of K;
A51: l*canFS(S2) = ll*(<*w*>) by A47,FINSEQ_1:94
.= <* ll.w *> by FINSEQ_2:35;
rng (l*canFS(S1)) c= the carrier of K;
then reconsider l1 = l*canFS(S1) as FinSequence of K by FINSEQ_1:def 4;
reconsider l2 = l*canFS(S2) as FinSequence of K by A51;
rng lCFST(l,T,s) c= the carrier of K;
then reconsider ll0 = lCFST(l,T,s) as FinSequence of K by FINSEQ_1:def 4;
A52: Sum ll0 = Sum l1 + Sum l2 by A44,A49,ThTF3C2
.= Sum(lCFST(l0,T,s)) + Sum(<*l.w*>) by A20,A50,A51,ThTF3C3,XBOOLE_1:17;
thus T.Sum(l)
= Sum(lCFST(l0,T,s)) * s + Sum(<*l.w*>) * s by A1,A39,A40,A43
.= Sum(lCFST(l,T,s)) * s by A52,VECTSP_1:def 15;
end;
A53: for n being Nat holds P[n] from NAT_1:sch 2(A2,A5);
let A be Subset of V,
l be Linear_Combination of A;
assume
A54: for v being Vector of V st v in Carrier l holds T.v = s;
card (Carrier l) is Nat;
hence thesis by A53,A54;
end;
theorem
for K being Ring
for V, W being LeftMod of K,
T being linear-transformation of V,W,
A being Subset of V,
l being Linear_Combination of A,
Tl being Linear_Combination of T.:(Carrier l)
st Tl = T@*l
holds T.Sum(l) = Sum (Tl)
proof
let K be Ring;
let V, W be LeftMod of K,
T be linear-transformation of V,W;
A1: T is additive;
A2: dom T = the carrier of V by FUNCT_2:def 1;
defpred P[Nat] means
for A being Subset of V,
l being Linear_Combination of A,
Tl being Linear_Combination of T.:(Carrier l)
st Tl = T@*l & card(T.:(Carrier l)) = $1 holds T.Sum(l) = Sum (Tl);
A3: P[0]
proof
let A be Subset of V,
l be Linear_Combination of A,
Tl be Linear_Combination of T.:(Carrier l);
assume P1: Tl = T@*l & card (T.:(Carrier l)) = 0;
A4: T.:(Carrier l) = {} by P1;
Carrier l = {} or not Carrier l c= dom T by P1; then
A5: T.Sum(l) = T.(0.V) by A2,VECTSP_6:19
.= T.(0.K * 0.V) by VECTSP_1:14
.= 0.K * T.(0.V) by MOD_2:def 2
.= 0.W by VECTSP_1:14;
Carrier(T@*l) c= {} by A4,LDef5;
then Carrier(T@*l) = {};
hence T.Sum(l) = Sum(Tl) by A5,P1,VECTSP_6:19;
end;
A6: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A21: P[n];
let A be Subset of V,
l be Linear_Combination of A,
Tl be Linear_Combination of T.:(Carrier l);
assume
A7: Tl = T@*l & card(T.:(Carrier l)) = n + 1;
then T.:(Carrier l) <> {};
then consider w be object such that
A8: w in T.:(Carrier l) by XBOOLE_0:def 1;
reconsider w as Element of the carrier of W by A8;
A9: card((T.:(Carrier l)) \ {w} )
= card((T.:(Carrier l))) - card({w}) by A8,CARD_2:44,ZFMISC_1:31
.= n + 1 - 1 by A7,CARD_2:42
.= n;
reconsider A0 = (Carrier l) \ T"{w} as finite Subset of V;
reconsider B0 = T"{w} /\ (Carrier l) as Subset of V;
reconsider B0 as finite Subset of V;
defpred PA0[object, object] means $1 is Vector of V implies
($1 in A0 & $2 = l.$1) or (not $1 in A0 & $2 = 0.K);
A10: for x being object st x in the carrier of V
ex y being object st y in the carrier of K & PA0[x, y]
proof
let x be object;
assume x in the carrier of V;
then reconsider x9 = x as Vector of V;
per cases;
suppose
A11: x in A0;
l.x9 in the carrier of K;
hence thesis by A11;
end;
suppose
not x in A0;
hence thesis;
end;
end;
consider l0 be Function of the carrier of V,
the carrier of K such that
A13: for x being object st x in the carrier of V holds PA0[x, l0.x]
from FUNCT_2:sch 1(A10);
A14: for v being Vector of V st not v in A0 holds l0.v = 0.K by A13;
reconsider l0 as Element of Funcs(the carrier of V, the carrier of
K) by FUNCT_2:8;
reconsider l0 as Linear_Combination of V by A14,VECTSP_6:def 1;
A15: for x being object holds x in A0 iff x in Carrier l0
proof
let x be object;
hereby
assume
A16: x in A0;
then reconsider v=x as Vector of V;
A17: l0.v = l.v by A13,A16;
v in (Carrier l) by A16,XBOOLE_0:def 5;
then l0.v <> 0.K by A17,VECTSP_6:2;
hence x in Carrier l0;
end;
assume
A18: x in Carrier(l0);
then reconsider v = x as Vector of V;
ex v9 being Vector of V st v9= v & l0.v9 <> 0.K by A18;
hence x in A0 by A13;
end;
then
A19: Carrier(l0) = A0 by TARSKI:2;
then reconsider l0 as Linear_Combination of A0 by VECTSP_6:def 4;
A20: l0 | Carrier(l0) = l | Carrier(l0)
proof
set L0 = l0;
set L1 = l;
reconsider L00 = L0 | Carrier(l0) as Function of Carrier(l0),
the carrier of K by FUNCT_2:32;
reconsider L11 = L1 | Carrier(l0) as Function of Carrier(l0),
the carrier of K by FUNCT_2:32;
now
let x be object;
assume
A21: x in Carrier(l0);
then reconsider v = x as Vector of V;
thus L00.x = L0.x by A21,FUNCT_1:49
.= l.v by A13,A19,A21
.= L11.x by A21,FUNCT_1:49;
end;
hence thesis by FUNCT_2:12;
end;
defpred PB0[object, object] means $1 is Vector of V implies
($1 in B0 & $2 = l.$1) or (not $1 in B0 & $2 = 0.K);
A22: for x being object st x in the carrier of V
ex y being object st y in the carrier of K & PB0[x, y]
proof
let x be object;
assume x in the carrier of V;
then reconsider x9 = x as Vector of V;
per cases;
suppose
A23: x in B0;
l.x9 in the carrier of K;
hence thesis by A23;
end;
suppose
not x in B0;
hence thesis;
end;
end;
consider l1 be Function of the carrier of V,
the carrier of K such that
A25: for x being object st x in the carrier of V holds PB0[x, l1.x]
from FUNCT_2:sch 1(A22);
A26: for v being Vector of V st not v in B0 holds l1.v = 0.K by A25;
reconsider l1 as Element of Funcs(the carrier of V, the carrier of
K) by FUNCT_2:8;
reconsider l1 as Linear_Combination of V by A26,VECTSP_6:def 1;
A27: for x being object holds x in B0 iff x in (Carrier l1)
proof
let x be object;
hereby
assume
A28: x in B0;
then reconsider v = x as Vector of V;
A29: l1.v = l.v by A25,A28;
v in (Carrier l) by A28,XBOOLE_0:def 4;
then l1.v <> 0.K by A29,VECTSP_6:2;
hence x in Carrier l1;
end;
assume X1: x in Carrier(l1);
then reconsider v = x as Vector of V;
ex v9 being Vector of V st v9 = v & l1.v9 <> 0.K by X1;
hence x in B0 by A25;
end;
then
A30: Carrier(l1) = B0 by TARSKI:2;
then reconsider l1 as Linear_Combination of B0 by VECTSP_6:def 4;
A31: l1 | Carrier(l1) = l | Carrier(l1)
proof
reconsider L0 = l1 as Function of V, K;
reconsider L1 = l as Function of V, K;
reconsider L00 = L0 | Carrier(l1) as Function of Carrier(l1),
the carrier of K by FUNCT_2:32;
reconsider L11 = L1 | Carrier(l1) as Function of Carrier(l1),
the carrier of K by FUNCT_2:32;
now
let x be object;
assume
A32: x in Carrier(l1);
then reconsider v = x as Vector of V;
thus L00.x = L0.x by A32,FUNCT_1:49
.= l.v by A25,A30,A32
.= L11.x by A32,FUNCT_1:49;
end;
hence thesis by FUNCT_2:12;
end;
A33: for v being Element of V holds l.v = (l0 + l1).v
proof
let v be Element of V;
per cases;
suppose
A34: not v in Carrier l; then
A35: l.v = 0.K;
not v in A0 by A34,XBOOLE_0:def 5; then
A36: l0.v = 0.K by A13;
l.v = l1.v + l0.v by A25,A35,A36;
hence l.v = (l0 + l1).v by VECTSP_6:22;
end;
suppose
A37: v in Carrier l;
per cases;
suppose
A38: v in T"{w};
then not v in A0 by XBOOLE_0:def 5;
then
A39: l0.v = 0.K by A13;
v in B0 by A37,A38,XBOOLE_0:def 4;
then l.v = l1.v + l0.v by A25,A39;
hence l.v = (l0 + l1).v by VECTSP_6:22;
end;
suppose
A40: not v in T"{w}; then
A41: v in A0 by A37,XBOOLE_0:def 5;
not v in B0 by A40,XBOOLE_0:def 4;
then l1.v = 0.K by A25;
then l.v = l1.v + l0.v by A13,A41;
hence l.v = (l0 + l1).v by VECTSP_6:22;
end;
end;
end;
then
A42: l = l0 + l1;
reconsider Tl0 = T@*l0 as Linear_Combination of T.:(Carrier l0)
by LTh29;
reconsider Tl1 = T@*l1 as Linear_Combination of T.:(Carrier l1)
by LTh29;
A43: (T.:(Carrier l0)) /\ (T.:(Carrier l1)) = {}
proof
assume (T.:(Carrier l0)) /\ (T.:(Carrier l1)) <> {};
then consider y be object such that
A44: y in (T.:(Carrier l0)) /\ (T.:(Carrier l1)) by XBOOLE_0:def 1;
A45: y in (T.:(Carrier l0)) & y in (T.:(Carrier l1))
by A44,XBOOLE_0:def 4;
then consider x be object such that
A46: x in the carrier of V & x in (Carrier l0) & y = T.x by FUNCT_2:64;
consider z be object such that
A47: z in the carrier of V & z in (Carrier l1) & y = T.z
by A45,FUNCT_2:64;
x in (Carrier l) \ T"{w} by A15,A46;
then not x in T"{w} by XBOOLE_0:def 5;
then
A48: not y in {w} by A46,FUNCT_2:38;
z in T"{w} /\ (Carrier l) by A27,A47;
then z in T"{w} by XBOOLE_0:def 4;
hence contradiction by A47,A48,FUNCT_2:38;
end;
A49: T.:(Carrier(l)) c= T.:(Carrier(l1) \/ Carrier(l0))
by A42,RELAT_1:123,VECTSP_6:23;
A50: for w being Vector of W st w in (T.:(Carrier l0)) holds Tl.w = Tl0.w
proof
let v be Vector of W;
assume v in (T.:(Carrier l0));
then consider x be object such that
A51: x in the carrier of V & x in (Carrier l0) & v = T.x
by FUNCT_2:64;
reconsider x as Vector of V by A51;
A52: Tl0.v = Sum(lCFST(l0,T,v)) by LDef5;
A53: Tl.v = Sum(lCFST(l,T,v)) by A7,LDef5;
A54: Carrier(l0) c= Carrier(l) by A19,XBOOLE_1:36;
now
let s be object;
assume s in (T"{v}) /\ (Carrier l);
then
A55: s in (T"{v}) & s in (Carrier l) by XBOOLE_0:def 4;
then s in the carrier of V & T.s in {v} by FUNCT_2:38;
then
A56: T.s = T.x by A51,TARSKI:def 1;
not s in T"{w}
proof
assume s in T"{w};
then T.x in {w} by A56,FUNCT_2:38;
then x in T"{w} by FUNCT_2:38;
hence contradiction by A19,A51,XBOOLE_0:def 5;
end;
then s in (Carrier l0) by A19,A55,XBOOLE_0:def 5;
hence s in (T"{v}) /\ (Carrier l0) by A55,XBOOLE_0:def 4;
end;
then (T"{v}) /\ (Carrier l) c= (T"{v}) /\ (Carrier l0);
then
A57: (T"{v}) /\ (Carrier l0)
= (T"{v}) /\ (Carrier l) by A19,XBOOLE_1:26,XBOOLE_1:36;
reconsider XX = (T"{v}) /\ (Carrier l0) as finite Subset of V;
thus thesis by A20,A52,A53,A54,A57,ThTF3C3,XBOOLE_1:17;
end;
A58: for w being Vector of W st w in (T.:(Carrier l1)) holds Tl.w = Tl1.w
proof
let v be Vector of W;
assume v in (T.:(Carrier l1));
then consider x be object such that
A59: x in the carrier of V & x in (Carrier l1) & v = T.x
by FUNCT_2:64;
reconsider x as Vector of V by A59;
A60: Tl1.v = Sum(lCFST(l1,T,v)) by LDef5;
A61: Tl.v = Sum(lCFST(l,T,v)) by A7,LDef5;
A62: Carrier(l1) c= Carrier(l) by A30,XBOOLE_1:17;
now
let s be object;
assume
A63: s in (T"{v}) /\ (Carrier l); then
A64: s in (T"{v}) & s in (Carrier l) by XBOOLE_0:def 4;
then s in the carrier of V & T.s in {v} by FUNCT_2:38; then
A65: T.s = T.x by A59,TARSKI:def 1;
x in T"{w} by A30,A59,XBOOLE_0:def 4;
then T.s in {w} by A65,FUNCT_2:38;
then s in T"{w} by A63,FUNCT_2:38;
then s in (Carrier l1) by A30,A64,XBOOLE_0:def 4;
hence s in (T"{v}) /\ (Carrier l1) by A64,XBOOLE_0:def 4;
end;
then (T"{v}) /\ (Carrier l) c= (T"{v}) /\ (Carrier l1);
then
A66: (T"{v}) /\ (Carrier l1)
= (T"{v}) /\ (Carrier l) by A30,XBOOLE_1:17,XBOOLE_1:26;
reconsider XX = (T"{v}) /\ (Carrier l1) as finite Subset of V;
thus thesis by A31,A60,A61,A62,A66,ThTF3C3,XBOOLE_1:17;
end;
A67: for x being object st x in Carrier Tl0 holds x in Carrier Tl
proof
let x be object;
assume
A68: x in Carrier Tl0;
then reconsider v = x as Vector of W;
A69: v in T .: (Carrier l0) by A68,LDef5,TARSKI:def 3;
Tl0.v <> 0.K by A68,VECTSP_6:2;
then Tl.v <> 0.K by A50,A69;
hence x in Carrier Tl;
end;
A70: for x being object st x in Carrier Tl1 holds x in Carrier Tl
proof
let x be object;
assume
A71: x in Carrier Tl1;
then reconsider v = x as Vector of W;
A72: v in T .: (Carrier l1) by A71,LDef5,TARSKI:def 3;
Tl1.v <> 0.K by A71,VECTSP_6:2;
then Tl.v <> 0.K by A58,A72;
hence x in Carrier Tl;
end;
A73: T.:(Carrier(l0)) = T.:((Carrier l) \ T"{w}) by A15,TARSKI:2;
then
A74: T.:(Carrier l) \ T.: (T"{w}) c= T.:(Carrier(l0)) by RELAT_1:122;
A75: T.:Carrier l c= T.:(dom T) by RELAT_1:114;
A76: T.:Carrier l c= rng T by A75,RELAT_1:113;
for x being object st x in T.:(Carrier(l0))
holds x in (T.: Carrier l) \ {w}
proof
let x be object;
assume x in T.:(Carrier l0);
then consider z be object such that
A77: z in the carrier of V & z in (Carrier l) \ T"{w} & x = T.z
by A73,FUNCT_2:64;
z in Carrier l by A77,XBOOLE_0:def 5; then
A78: x in T.: (Carrier l) by A77,FUNCT_2:35;
not x in {w}
proof
assume
A79: x in {w};
z in dom T by A77,FUNCT_2:def 1;
then z in T"{w} by A77,A79,FUNCT_1:def 7;
hence contradiction by A77,XBOOLE_0:def 5;
end;
hence x in (T.: (Carrier l)) \ {w} by A78,XBOOLE_0:def 5;
end;
then T.:(Carrier(l0)) c= T.: (Carrier l) \ {w};
then
A80: T.:(Carrier l0) = (T.:(Carrier l)) \ {w}
by A8,A74,A76,FUNCT_1:77,ZFMISC_1:31;
for y being object st y in Carrier(Tl1) holds y in {w}
proof
let y be object;
assume
A81: y in Carrier(Tl1);
then reconsider v = y as Vector of W;
A83: Tl1.v = Sum(lCFST(l1,T,v)) by LDef5;
y = w
proof
assume
A84: y <> w;
A85: (T"{v}) /\ (T"{w}) = {}
proof
assume (T"{v}) /\ (T"{w}) <> {};
then consider x be object such that
A86: x in (T"{v}) /\ (T"{w}) by XBOOLE_0:def 1;
x in (T"{v}) & x in (T"{w}) by A86,XBOOLE_0:def 4;
then T.x in {v} & T.x in {w} by FUNCT_1:def 7;
then T.x = v & T.x = w by TARSKI:def 1;
hence contradiction by A84;
end;
set g = canFS((T"{v}) /\ (Carrier l1));
T"{v} /\ Carrier(l1) = T"{v} /\ (T"{w} /\ (Carrier l))
by A27,TARSKI:2
.= {} /\ (Carrier l) by A85,XBOOLE_1:16
.= {};
then lCFST(l1,T,v) = <*>the carrier of K;
hence contradiction by A81,A83,RLVECT_1:43,VECTSP_6:2;
end;
hence y in {w} by TARSKI:def 1;
end;
then
A87: Carrier(Tl1) c= {w};
A88: T.Sum(l1) = Sum (Tl1)
proof
A89: Tl1.w = Sum(lCFST(l1,T,w)) by LDef5;
reconsider w as Vector of W;
A90: for v being Vector of V st v in Carrier(l1) holds T.v = w
proof
let v be Vector of V;
assume v in Carrier(l1);
then v in T"{w} /\ (Carrier l) by A27;
then v in T"{w} by XBOOLE_0:def 4;
then T.v in {w} by FUNCT_1:def 7;
hence T.v = w by TARSKI:def 1;
end;
per cases;
suppose
A91: Sum(lCFST(l1,T,w)) = 0.K;
then
A92: not w in Carrier(Tl1) by A89,VECTSP_6:2;
A93: Carrier(Tl1) = {}
proof
assume Carrier(Tl1) <> {};
then consider x be object such that
A94: x in Carrier(Tl1) by XBOOLE_0:def 1;
thus contradiction by A87,A92,A94,TARSKI:def 1;
end;
T.Sum(l1) = 0.K * w by A90,A91,ThTF3B2
.= 0.W by VECTSP_1:14;
hence T.Sum(l1) = Sum (Tl1) by A93,VECTSP_6:19;
end;
suppose
Sum(lCFST(l1,T,w)) <> 0.K;
then w in Carrier(Tl1) by A89; then
A95: {w} = Carrier(Tl1) by A87,ZFMISC_1:31;
Sum(Tl1) = Sum(lCFST(l1,T,w)) * w by A89,A95,VECTSP_6:20
.= T.Sum l1 by A90,ThTF3B2;
hence T.Sum(l1)=Sum (Tl1);
end;
end;
for w being Element of W holds Tl.w = (Tl0 + Tl1).w
proof
let w be Element of W;
per cases;
suppose
A96: not w in Carrier Tl; then
A97: Tl.w = 0.K;
not w in (Carrier Tl0) by A67,A96; then
A98: Tl0.w = 0.K;
not w in (Carrier Tl1) by A70,A96;
then Tl.w = Tl1.w + Tl0.w by A97,A98;
hence Tl.w = (Tl0 + Tl1).w by VECTSP_6:22;
end;
suppose
w in Carrier Tl;
then w in T.:(Carrier l) by TARSKI:def 3,VECTSP_6:def 4;
then w in T.:((Carrier l0) \/ (Carrier l1)) by A49;
then
A99: w in (T.:(Carrier l0)) \/ (T.:(Carrier l1)) by RELAT_1:120;
thus Tl.w = (Tl0 + Tl1).w
proof
per cases by A99,XBOOLE_0:def 3;
suppose
A100: w in T.:(Carrier l1);
not w in T.:Carrier l0 by A43,A100,XBOOLE_0:def 4;
then not w in Carrier Tl0 by LDef5,TARSKI:def 3;
then Tl0.w = 0.K;
then Tl.w = Tl1.w + Tl0.w by A58,A100;
hence Tl.w = (Tl0 + Tl1).w by VECTSP_6:22;
end;
suppose
A101: w in (T.:(Carrier l0));
not w in T.:(Carrier l1) by A43,A101,XBOOLE_0:def 4;
then not w in Carrier Tl1 by LDef5,TARSKI:def 3;
then Tl1.w = 0.K;
then Tl.w = Tl1.w + Tl0.w by A50,A101;
hence Tl.w = (Tl0 + Tl1).w by VECTSP_6:22;
end;
end;
end;
end;
then
A102: Tl = Tl0 + Tl1;
l = l0 + l1 by A33;
hence T.Sum(l) = T.(Sum(l0) + Sum(l1)) by VECTSP_6:44
.= T.(Sum(l0)) + T.(Sum(l1)) by A1
.= Sum(Tl0) + Sum(Tl1) by A9,A21,A80,A88
.= Sum(Tl) by A102,VECTSP_6:44;
end;
A103: for n being Nat holds P[n] from NAT_1:sch 2(A3,A6);
let A be Subset of V,
l be Linear_Combination of A,
Tl be Linear_Combination of T.:(Carrier l);
assume
A104: Tl = T@*l;
card (T.:(Carrier l)) is Nat;
hence thesis by A103,A104;
end;
::: same as ZMODUL04:25
theorem Th31:
for R being Ring
for V being LeftMod of R
for l,m being Linear_Combination of V
st (Carrier l) misses (Carrier m) holds
Carrier(l + m) = (Carrier l) \/ (Carrier m)
proof
let R be Ring;
let V be LeftMod of R;
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
A4: (l+m).v = (l.v) + (m.v) & m.v = 0.R by VECTSP_6:22;
l.v <> 0.R 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
A6: (l+m).v = (l.v) + (m.v) & l.v = 0.R by VECTSP_6:22;
m.v <> 0.R by A5,VECTSP_6:2;
hence thesis by A6;
end;
end;
end;
theorem Th32:
for R being Ring
for V being LeftMod of R
for l, m being Linear_Combination of V
st (Carrier l) misses (Carrier m) holds
Carrier (l - m) = (Carrier l) \/ (Carrier m)
proof
let R be Ring;
let V be LeftMod of R;
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
for R being Ring
for V being LeftMod of R, A being Subset of V,
l1, l2 being Linear_Combination of A
st Carrier(l1) misses Carrier(l2) holds
Carrier(l1 - l2) = Carrier(l1) \/ Carrier(l2)
proof
let R be Ring;
let V be LeftMod of R;
let A be Subset of V,
l1, l2 be Linear_Combination of A such that
A1: Carrier(l1) misses Carrier(l2);
A2: Carrier(l1) misses Carrier(-l2) by A1,VECTSP_6:38;
thus Carrier(l1 - l2) = Carrier(l1 +- l2)
.= Carrier(l1) \/ Carrier(-l2) by A2,Th31
.= Carrier(l1) \/ Carrier(l2) by VECTSP_6:38;
end;
theorem
for V be free Z_Module,
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 V be free Z_Module, 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 Submodule of U by ZMODUL01:54;
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 ZMODUL01:94;
then consider l being Linear_Combination of A such that
A6: v = Sum l by ZMODUL02:64;
v in Lin (B \ A) by A5,ZMODUL01:94;
then consider m being Linear_Combination of B \ A such that
A7: v = Sum m by ZMODUL02:64;
A8: 0.V = (Sum l) - (Sum m) by A6,A7,VECTSP_1:19
.= Sum (l - m) by ZMODUL02:55;
A9: Carrier (l - m) c= (Carrier l) \/ (Carrier m) & A \/ (B \ A) = B
by A1,XBOOLE_1:45,ZMODUL02:40;
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 A4,A8;
then l = ZeroLC(V) by VECTSP_6:def 3;
then Sum l = 0.V by ZMODUL02:19;
hence thesis by A6,ZMODUL02:66;
end;
hence thesis by ZMODUL01:149;
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,ZMODUL03:14;
then consider l being Linear_Combination of B such that
A12: v = Sum l by ZMODUL02:64;
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,ZMODUL02:52,ZMODUL02:64;
end;
then v in (Lin A) + (Lin (B \ A)) by ZMODUL01:92;
hence thesis;
end;
[#]U = [#]V by A11,VECTSP_4:def 2;
hence thesis by ZMODUL01:45;
end;
hence thesis by A3,VECTSP_5:def 4;
end;
theorem
for R being Ring
for V,W being LeftMod of R
for A being Subset of V, l being Linear_Combination of A,
T being linear-transformation of V,W,
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 R be Ring;
let V,W be LeftMod of R;
let A be Subset of V,
l be Linear_Combination of A,
T be linear-transformation of V,W,
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 RANKNULL:7; 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 contradiction by A1,A2,A4,A6,A7,FUNCT_1:def 4;
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 TARSKI:def 1,RANKNULL:7;
hence thesis by A9,FUNCT_1:def 7;
end;
hence thesis by A3,XBOOLE_1:45;
end;
theorem
for R being Ring
for V being LeftMod of R, A being Subset of V,
l being Linear_Combination of A
for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {0.R}
proof
let R be Ring;
let V be LeftMod of R, A be Subset of V;
let l be Linear_Combination of A;
let X be Subset of V such that
A1: X misses Carrier l and
A2: X <> {};
dom l = [#]V by FUNCT_2:92;
hence thesis by A1,A2,Th28,ZFMISC_1:33;
end;
theorem Th36:
for R being Ring
for V,W being LeftMod of R
for l being Linear_Combination of V,
T being linear-transformation of V,W
for w being Element of W st w in Carrier (T@*l) holds T"{w} meets Carrier l
proof
let R be Ring;
let V,W be LeftMod of R;
let l be Linear_Combination of V,
T be linear-transformation of V,W;
let w be Element of W;
assume w in Carrier (T@*l); then
A1: (T@*l).w <> 0.R by ZMODUL02:8;
assume T"{w} misses Carrier l; then
lCFST(l,T,w) = <*>the carrier of R; then
Sum(lCFST(l,T,w)) = 0.R by RLVECT_1:43;
hence thesis by A1,LDef5;
end;
theorem Th37:
for R being Ring
for V,W being LeftMod of R
for l being Linear_Combination of V,
T being linear-transformation of V,W
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 R be Ring;
let V,W be LeftMod of R;
let l be Linear_Combination of V,
T be linear-transformation of V,W;
let v be Element of V such that
A1: T | (Carrier l) is one-to-one and
A2: v in Carrier l;
v in the carrier of V; then
A3: v in dom l by FUNCT_2:def 1;
A4: dom T = the carrier of V by FUNCT_2:def 1;
for x be object holds
x in T"{T.v} /\ Carrier(l) iff x in {v}
proof
let x be object;
hereby assume x in T"{T.v} /\ Carrier(l); then
A5: x in T"{T.v} & x in Carrier(l) by XBOOLE_0:def 4; then
A6: x in the carrier of V & T.x in {T.v} by FUNCT_2:38;
A7: T | (Carrier l).x = T.x by A5,FUNCT_1:49
.= T.v by A6,TARSKI:def 1
.= T | (Carrier l).v by A2,FUNCT_1:49;
A8: x in dom(T | (Carrier l)) by A4,A5,RELAT_1:57;
v in dom(T | (Carrier l)) by A2,A4,RELAT_1:57;
then x = v by A1,A7,A8,FUNCT_1:def 4;
hence x in {v} by TARSKI:def 1;
end;
assume x in {v}; then
A9: x = v by TARSKI:def 1;
x in the carrier of V & T.x in {T.v} by A9,TARSKI:def 1;
then x in T"{T.v} by FUNCT_2:38;
hence thesis by A2,A9,XBOOLE_0:def 4;
end;
then T"{T.v} /\ Carrier(l) = {v} by TARSKI:2;
then canFS((T"{T.v}) /\ (Carrier l)) = <*v*> by FINSEQ_1:94;
then lCFST(l,T,T.v) = <*l.v*> by A3,FINSEQ_2:34;
then Sum(lCFST(l,T,T.v)) = l.v by RLVECT_1:44;
hence thesis by LDef5;
end;
theorem Th38:
for R being Ring
for V,W being LeftMod of R
for l being Linear_Combination of V,
T being linear-transformation of V,W
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 R be Ring;
let V,W be LeftMod of R;
let l be Linear_Combination of V,
T be linear-transformation of V,W;
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 RANKNULL:7;
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 A5,A7,A8,A11,A12,VECTSP_6:def 5;
end;
hence thesis by A3,A4;
end;
theorem Th39:
for R being Ring
for V,W being LeftMod of R
for l being Linear_Combination of V,
T being linear-transformation of V,W holds
T | (Carrier l) is one-to-one implies T .: (Carrier l) = Carrier(T@*l)
proof
let R be Ring;
let V,W be LeftMod of R;
let l be Linear_Combination of V,
T be linear-transformation of V,W;
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.R by A1,A4,Th37,ZMODUL02:8;
hence thesis by A5;
end;
thus thesis by LDef5,A2;
end;
theorem
for V being finite-rank free Z_Module,
A being Subset of V,
B being Basis of V,
T being linear-transformation of V,W,
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 V be finite-rank free Z_Module,
A be Subset of V, B be Basis of V,
T be linear-transformation of V,W,
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;
A2: (T | (B \ A)) | (Carrier l) = T | (Carrier l)
by RELAT_1:74,VECTSP_6:def 4; 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 RANKNULL:7;
then H is one-to-one by A1,A2,A4,A5,FUNCT_1:52,RANKNULL:1; then
A8: Sum (T@*l) = Sum ((T@*l) (#) H) by A7,VECTSP_6:def 6;
T*(l (#) G) = (T@*l) (#) H by A3,A5,Th38;
hence thesis by A6,A8,MATRLIN16;
end;
theorem
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;
:: "Pulling back" a linear combination from the image space of a
:: linear transformation to the base space.
definition
let R be Ring;
let V,W be LeftMod of R, 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) +* ((X`) --> 0.R);
coherence
proof
reconsider SZ0 = {0.R} as finite Subset of R;
dom l = [#]W by FUNCT_2:92;
then rng T c= dom l; then
A3: dom (l*T) = dom T by RELAT_1:27;
set f = (l*T) +* ((X`) --> 0.R);
A4: dom ((X`) --> 0.R) = X`;
rng f c= rng (l*T) \/ rng ((X`) --> 0.R) &
rng (l*T) \/ rng ((X`) --> 0.R) c= the carrier of R
by FUNCT_4:17; then
A5: rng f c= the carrier of R;
dom T = [#]V & [#]V \/ ([#]V \ X) = [#]V by RANKNULL:7,XBOOLE_1:12;
then dom f = [#]V by A3,A4,FUNCT_4:def 1;
then reconsider f as Element of Funcs ([#]V,the carrier of
R) 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.R
proof
set C = { v where v is Element of V : f.v <> 0.R };
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.R;
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.R by A7;
reconsider x as Element of V by A7;
A9:
now
assume not x in X; then
A10: x in X` by XBOOLE_0:def 5;
then x in dom ((X`) --> 0.R);
then f.x = ((X`) --> 0.R).x by FUNCT_4:13;
hence contradiction by A8,A10,FUNCOP_1:7;
end;
then not x in X` by XBOOLE_0:def 5;
then
A11: f.x = (l*T).x by A4,FUNCT_4:11;
A12: dom T = [#]V by RANKNULL:7;
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 RANKNULL:7;
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.R by A21,ZMODUL02:8;
not x in dom ((X`) --> 0.R) 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 A22,A23;
end;
hence thesis by A1,A6,A13,A14,RANKNULL:2,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 X` by XBOOLE_0:def 5;
then f.x = ((X`) --> 0.R).x by A4,FUNCT_4:13
.= 0.R by A25,FUNCOP_1:7;
hence contradiction by A24,ZMODUL02:8;
end;
hence thesis;
end;
hence thesis by VECTSP_6:def 4;
end;
end;
theorem Th42:
for R being Ring
for V,W be LeftMod of R, X be Subset of V,
T be linear-transformation of V,W
for X being Subset of V,
l be 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 R be Ring;
let V,W be LeftMod of R, X be Subset of V,
T be linear-transformation of V,W;
let X be Subset of V,
l be Linear_Combination of T.:X;
let v be Element of V;
assume v in X & T|X is one-to-one;
then not v in dom ((X`) --> (0.R)) &
T#l = (l*T) +* ((X`) --> (0.R)) by Def6,XBOOLE_0:def 5; then
A1: (T#l).v = (l*T).v by FUNCT_4:11;
dom T = [#]V by RANKNULL:7;
hence thesis by A1,FUNCT_1:13;
end;
:: # is a right inverse of @*
theorem
for R being Ring
for V,W be LeftMod of R, X be Subset of V,
T be linear-transformation of V,W,
X being Subset of V,
l be Linear_Combination of T .: X st
T|X is one-to-one holds T@*(T#l) = l
proof
let R be Ring;
let V,W be LeftMod of R, X be Subset of V,
T be linear-transformation of V,W;
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);
reconsider SZ0 = {0.R} as finite Subset of R;
per cases;
suppose
A2: w in Carrier l;
Carrier l c= T .: X by VECTSP_6:def 4;
then consider v being object such that
A3: v in dom T and
A4: v in X and
A5: w = T.v by A2,FUNCT_1:def 6;
reconsider v as Element of V by A3;
w in the carrier of W; then
A6: w in dom l by FUNCT_2:def 1;
A7: v in the carrier of V;
for x be object holds
x in T"{w} /\ Carrier((T#l)) iff x in {v} /\ Carrier((T#l))
proof
let x be object;
hereby
assume
A8: x in T"{w} /\ Carrier((T#l)); then
A9: x in T"{w} & x in Carrier((T#l)) by XBOOLE_0:def 4; then
A10: x in X by TARSKI:def 3,VECTSP_6:def 4;
x in the carrier of V by A8; then
A11: x in dom T by FUNCT_2:def 1;
A12: x in the carrier of V & T.x in {w} by A9,FUNCT_2:38;
A13:(T|X).x = T.x by A10,FUNCT_1:49
.= T.v by A5,A12,TARSKI:def 1
.= (T|X).v by A4,FUNCT_1:49;
A14: x in dom (T|X) by A10,A11,RELAT_1:57;
v in dom (T|X) by A3,A4,RELAT_1:57;
then x = v by A1,A13,A14,FUNCT_1:def 4;
then x in {v} by TARSKI:def 1;
hence x in {v} /\ Carrier((T#l)) by A9,XBOOLE_0:def 4;
end;
assume x in {v} /\ Carrier((T#l)); then
A15: x in {v} & x in Carrier((T#l)) by XBOOLE_0:def 4; then
A16: x = v by TARSKI:def 1;
x in the carrier of V & T.x in {w} by A5,A16,TARSKI:def 1;
then x in T"{w} by FUNCT_2:38;
hence x in T"{w} /\ Carrier((T#l)) by A15,XBOOLE_0:def 4;
end; then
A17: T"{w} /\ Carrier((T#l)) = {v} /\ Carrier((T#l)) by TARSKI:2;
per cases;
suppose
A18: not v in Carrier((T#l));
{v} /\ Carrier((T#l)) = {}
proof
assume {v} /\ Carrier((T#l)) <> {};
then consider x be object such that
A19: x in {v} /\ Carrier((T#l)) by XBOOLE_0:def 1;
A20: x in {v} by A19,XBOOLE_0:def 4;
x in Carrier((T#l)) by A19,XBOOLE_0:def 4;
hence contradiction by A18,A20,TARSKI:def 1;
end; then
b1: lCFST(T#l,T,w) = <*>the carrier of R by A17;
(T@*(T#l)).w = Sum(lCFST(T#l,T,w)) by LDef5; then
A21: (T@*(T#l)).w = 0.R by RLVECT_1:43,b1;
A22:(T#l).v = 0.R by A18;
A23: not v in dom((X`) --> 0.R) by A4,XBOOLE_0:def 5;
(T#l) = (l*T) +* ((X`) --> 0.R) by A1,Def6;
then (T#l).v = (l*T).v by A23,FUNCT_4:11;
hence (T@*(T#l)).w = l.w by A3,A5,A21,A22,FUNCT_1:13;
end;
suppose
v in Carrier((T#l));
then T"{w} /\ Carrier(T#l) = {v} by A17,XBOOLE_1:28,ZFMISC_1:31;
then
A24: canFS((T"{w}) /\ (Carrier (T#l))) = <*v*> by FINSEQ_1:94;
A25: not v in dom((X`) --> 0.R) by A4,XBOOLE_0:def 5;
A26: (T#l) = (l*T) +* ((X`) --> 0.R) by A1,Def6;
A27: v in dom(T#l) by A7,FUNCT_2:def 1;
A28: v in dom(l*T) by A7,FUNCT_2:def 1;
(T#l) * (<*v*>) = <* (T#l).v *> by A27,FINSEQ_2:34
.= <* (l*T).v *> by A25,A26,FUNCT_4:11
.= (l*T) * (<*v*>) by A28,FINSEQ_2:34
.= l * (T * (<*v*>)) by RELAT_1:36
.= l * (<*T.v*>) by A3,FINSEQ_2:34
.= <* l.w *> by A5,A6,FINSEQ_2:34;
then Sum(lCFST((T#l),T,w)) = l.w by A24,RLVECT_1:44;
hence m.w = l.w by LDef5;
end;
end;
suppose
A29: not w in Carrier l; then
A30: l.w = 0.R;
now
assume
A31: m.w <> 0.R;
then w in Carrier m;
then consider v being Element of V such that
A32: v in T"{w} and
A33: v in Carrier (T#l) by RANKNULL:3,Th36;
T.v in {w} by A32,FUNCT_1:def 7; then
A34: T.v = w by TARSKI:def 1;
A35: Carrier (T#l) c= X by VECTSP_6:def 4;
T | (Carrier (T#l)) is one-to-one by A1,RANKNULL:2,VECTSP_6:def 4;
then m.w = (T#l).v by A33,A34,Th37
.= 0.R by A1,A30,A33,A34,A35,Th42;
hence contradiction by A31;
end;
hence thesis by A29;
end;
end;