:: RANKNULL semantic presentation
begin
theorem Th1: :: RANKNULL:1
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; ::_thesis: ( g is one-to-one & f | (rng g) is one-to-one & rng g c= dom f implies f * g is one-to-one )
assume that
A1: g is one-to-one and
A2: f | (rng g) is one-to-one and
A3: rng g c= dom f ; ::_thesis: f * g is one-to-one
set h = f * g;
A4: dom (f * g) c= dom g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (f * g) or x in dom g )
assume x in dom (f * g) ; ::_thesis: x in dom g
hence x in dom g by FUNCT_1:11; ::_thesis: verum
end;
dom g c= dom (f * g)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom g or x in dom (f * g) )
assume A5: x in dom g ; ::_thesis: x in dom (f * g)
g . x in rng g by A5, FUNCT_1:3;
hence x in dom (f * g) by A3, A5, FUNCT_1:11; ::_thesis: verum
end;
then A6: dom (f * g) = dom g by A4, XBOOLE_0:def_10;
for x1, x2 being set st x1 in dom (f * g) & x2 in dom (f * g) & (f * g) . x1 = (f * g) . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom (f * g) & x2 in dom (f * g) & (f * g) . x1 = (f * g) . x2 implies x1 = x2 )
assume that
A7: x1 in dom (f * g) and
A8: x2 in dom (f * g) and
A9: (f * g) . x1 = (f * g) . x2 ; ::_thesis: x1 = x2
A10: ( (f * g) . x1 = f . (g . x1) & (f * g) . 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, FUNCT_1:49;
then g . x1 = g . x2 by A2, A9, A10, A11, A12, FUNCT_1:def_4;
hence x1 = x2 by A1, A4, A7, A8, FUNCT_1:def_4; ::_thesis: verum
end;
hence f * g is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;
theorem Th2: :: RANKNULL:2
for f being Function
for 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; ::_thesis: for X, Y being set st X c= Y & f | Y is one-to-one holds
f | X is one-to-one
let X, Y be set ; ::_thesis: ( X c= Y & f | Y is one-to-one implies f | X is one-to-one )
assume that
A1: X c= Y and
A2: f | Y is one-to-one ; ::_thesis: f | X is one-to-one
f | X = (f | Y) | X by A1, RELAT_1:74;
hence f | X is one-to-one by A2, FUNCT_1:52; ::_thesis: verum
end;
theorem Th3: :: RANKNULL:3
for V being 1-sorted
for 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 ; ::_thesis: for X, Y being Subset of V holds
( X meets Y iff ex v being Element of V st
( v in X & v in Y ) )
let X, Y be Subset of V; ::_thesis: ( X meets Y iff ex v being Element of V st
( v in X & v in Y ) )
( X meets Y implies ex v being Element of V st
( v in X & v in Y ) )
proof
assume X meets Y ; ::_thesis: ex v being Element of V st
( v in X & v in Y )
then consider z being set 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 ; ::_thesis: ( v in X & v in Y )
thus ( v in X & v in Y ) by A1, A2; ::_thesis: verum
end;
hence ( X meets Y iff ex v being Element of V st
( v in X & v in Y ) ) by XBOOLE_0:3; ::_thesis: verum
end;
registration
let F be Field;
let V be finite-dimensional VectSp of F;
cluster finite for Basis of V;
existence
ex b1 being Basis of V st b1 is finite
proof
consider A being finite Subset of V such that
A1: A is Basis of V by MATRLIN:def_1;
reconsider A = A as Basis of V by A1;
take A ; ::_thesis: A is finite
thus A is finite ; ::_thesis: verum
end;
end;
registration
let F be Field;
let V, W be VectSp of F;
cluster Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous for Element of K6(K7( the carrier of V, the carrier of W));
existence
ex b1 being Function of V,W st
( b1 is additive & b1 is homogeneous )
proof
set f = FuncZero (([#] V),W);
reconsider f = FuncZero (([#] V),W) as Function of V,W ;
A1: for x, y being Vector of V holds f . (x + y) = (f . x) + (f . y)
proof
let x, y be Vector of V; ::_thesis: f . (x + y) = (f . x) + (f . y)
A2: f . y = 0. W by FUNCOP_1:7;
( f . (x + y) = 0. W & f . x = 0. W ) by FUNCOP_1:7;
hence f . (x + y) = (f . x) + (f . y) by A2, RLVECT_1:def_4; ::_thesis: verum
end;
take f ; ::_thesis: ( f is additive & f is homogeneous )
for a being Element of F
for x being Element of V holds f . (a * x) = a * (f . x)
proof
let a be Element of F; ::_thesis: for x being Element of V holds f . (a * x) = a * (f . x)
let x be Element of V; ::_thesis: f . (a * x) = a * (f . x)
( f . (a * x) = 0. W & f . x = 0. W ) by FUNCOP_1:7;
hence f . (a * x) = a * (f . x) by VECTSP_1:14; ::_thesis: verum
end;
hence ( f is additive & f is homogeneous ) by A1, VECTSP_1:def_20, MOD_2:def_2; ::_thesis: verum
end;
end;
theorem Th4: :: RANKNULL:4
for F being Field
for V being VectSp of F st [#] V is finite holds
V is finite-dimensional
proof
let F be Field; ::_thesis: for V being VectSp of F st [#] V is finite holds
V is finite-dimensional
let V be VectSp of F; ::_thesis: ( [#] V is finite implies V is finite-dimensional )
set B = the Basis of V;
assume [#] V is finite ; ::_thesis: V is finite-dimensional
then reconsider B = the Basis of V as finite Subset of V ;
take B ; :: according to MATRLIN:def_1 ::_thesis: B is Basis of V
thus B is Basis of V ; ::_thesis: verum
end;
theorem :: RANKNULL:5
for F being Field
for V being finite-dimensional VectSp of F st card ([#] V) = 1 holds
dim V = 0
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F st card ([#] V) = 1 holds
dim V = 0
let V be finite-dimensional VectSp of F; ::_thesis: ( card ([#] V) = 1 implies dim V = 0 )
assume A1: card ([#] V) = 1 ; ::_thesis: dim V = 0
[#] V = {(0. V)}
proof
ex y being set st [#] V = {y} by A1, CARD_2:42;
hence [#] V = {(0. V)} by TARSKI:def_1; ::_thesis: verum
end;
then (Omega). V = (0). V by VECTSP_4:def_3;
hence dim V = 0 by VECTSP_9:29; ::_thesis: verum
end;
theorem :: RANKNULL:6
for F being Field
for V being VectSp of F st card ([#] V) = 2 holds
dim V = 1
proof
let F be Field; ::_thesis: for V being VectSp of F st card ([#] V) = 2 holds
dim V = 1
let V be VectSp of F; ::_thesis: ( card ([#] V) = 2 implies dim V = 1 )
assume A1: card ([#] V) = 2 ; ::_thesis: dim V = 1
then A2: [#] V is finite ;
reconsider C = [#] V as finite set by A1;
reconsider V = 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 set such that
A3: x <> y and
A4: [#] V = {x,y} by A1, CARD_2:60;
percases ( x = 0. V or y = 0. V ) by A4, TARSKI:def_2;
supposeA5: x = 0. V ; ::_thesis: ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} )
then reconsider x = x as Element of V ;
reconsider y = y as Element of V by A4, TARSKI:def_2;
set L = Lin {y};
take y ; ::_thesis: ( y <> 0. V & (Omega). V = Lin {y} )
for v being Element of V holds
( v in (Omega). V iff v in Lin {y} )
proof
let v be Element of V; ::_thesis: ( v in (Omega). V iff v in Lin {y} )
( v in (Omega). V implies v in Lin {y} )
proof
assume v in (Omega). V ; ::_thesis: v in Lin {y}
A6: y in {y} by TARSKI:def_1;
A7: 0. (Lin {y}) in Lin {y} by STRUCT_0:def_5;
percases ( v = x or v = y ) by A4, TARSKI:def_2;
suppose v = x ; ::_thesis: v in Lin {y}
hence v in Lin {y} by A5, A7, VECTSP_4:def_2; ::_thesis: verum
end;
suppose v = y ; ::_thesis: v in Lin {y}
hence v in Lin {y} by A6, VECTSP_7:8; ::_thesis: verum
end;
end;
end;
hence ( v in (Omega). V iff v in Lin {y} ) by STRUCT_0:def_5; ::_thesis: verum
end;
hence ( y <> 0. V & (Omega). V = Lin {y} ) by A3, A5, VECTSP_4:30; ::_thesis: verum
end;
supposeA8: y = 0. V ; ::_thesis: ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} )
reconsider x = x as Element of V by A4, TARSKI:def_2;
reconsider y = y as Element of V by A8;
set L = Lin {x};
take x ; ::_thesis: ( x <> 0. V & (Omega). V = Lin {x} )
for v being Element of V holds
( v in (Omega). V iff v in Lin {x} )
proof
let v be Element of V; ::_thesis: ( v in (Omega). V iff v in Lin {x} )
( v in (Omega). V implies v in Lin {x} )
proof
assume v in (Omega). V ; ::_thesis: v in Lin {x}
A9: x in {x} by TARSKI:def_1;
A10: 0. (Lin {x}) in Lin {x} by STRUCT_0:def_5;
percases ( v = y or v = x ) by A4, TARSKI:def_2;
suppose v = y ; ::_thesis: v in Lin {x}
hence v in Lin {x} by A8, A10, VECTSP_4:def_2; ::_thesis: verum
end;
suppose v = x ; ::_thesis: v in Lin {x}
hence v in Lin {x} by A9, VECTSP_7:8; ::_thesis: verum
end;
end;
end;
hence ( v in (Omega). V iff v in Lin {x} ) by STRUCT_0:def_5; ::_thesis: verum
end;
hence ( x <> 0. V & (Omega). V = Lin {x} ) by A3, A8, VECTSP_4:30; ::_thesis: verum
end;
end;
end;
hence dim V = 1 by VECTSP_9:30; ::_thesis: verum
end;
begin
definition
let F be Field;
let V, W be VectSp of F;
mode linear-transformation of V,W is additive homogeneous Function of V,W;
end;
theorem Th7: :: RANKNULL:7
for V, W being non empty 1-sorted
for T being Function of V,W holds
( dom T = [#] V & rng T c= [#] W )
proof
let V, W be non empty 1-sorted ; ::_thesis: for T being Function of V,W holds
( dom T = [#] V & rng T c= [#] W )
let T be Function of V,W; ::_thesis: ( dom T = [#] V & rng T c= [#] W )
T is Element of Funcs (([#] V),([#] W)) by FUNCT_2:8;
hence ( dom T = [#] V & rng T c= [#] W ) by FUNCT_2:92; ::_thesis: verum
end;
theorem Th8: :: RANKNULL:8
for F being Field
for W, V being VectSp of F
for 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 Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for x, y being Element of V holds (T . x) - (T . y) = T . (x - y)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for x, y being Element of V holds (T . x) - (T . y) = T . (x - y)
let T be linear-transformation of V,W; ::_thesis: for x, y being Element of V holds (T . x) - (T . y) = T . (x - y)
let x, y be Element of V; ::_thesis: (T . x) - (T . y) = T . (x - y)
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:def_20, VECTSP_1:14;
hence (T . x) - (T . y) = T . (x - y) by A1, VECTSP_1:14; ::_thesis: verum
end;
theorem Th9: :: RANKNULL:9
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W holds T . (0. V) = 0. W
proof
let F be Field; ::_thesis: for V, W being VectSp of F
for T being linear-transformation of V,W holds T . (0. V) = 0. W
let V, W be VectSp of F; ::_thesis: for T being linear-transformation of V,W holds T . (0. V) = 0. W
let T be linear-transformation of V,W; ::_thesis: T . (0. V) = 0. 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 T . (0. V) = 0. W ; ::_thesis: verum
end;
definition
let F be Field;
let V, W be VectSp of F;
let T be linear-transformation of V,W;
func ker T -> strict Subspace of V means :Def1: :: RANKNULL:def 1
[#] it = { u where u is Element of V : T . u = 0. W } ;
existence
ex b1 being strict Subspace of V st [#] b1 = { u where u is Element of V : T . u = 0. W }
proof
set K = { u where u is Element of V : T . u = 0. W } ;
{ u where u is Element of V : T . u = 0. W } c= [#] V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is Element of V : T . u = 0. W } or x in [#] V )
assume x in { u where u is Element of V : T . u = 0. W } ; ::_thesis: x in [#] V
then ex u being Element of V st
( u = x & T . u = 0. W ) ;
hence x in [#] V ; ::_thesis: verum
end;
then reconsider K = { u where u is Element of V : T . u = 0. W } 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; ::_thesis: ( v in K implies T . v = 0. W )
assume v in K ; ::_thesis: T . v = 0. W
then ex u being Element of V st
( u = v & T . u = 0. W ) ;
hence T . v = 0. W ; ::_thesis: verum
end;
now__::_thesis:_for_u_being_Element_of_V
for_a_being_Element_of_F_st_u_in_K_holds_
a_*_u_in_K
let u be Element of V; ::_thesis: for a being Element of F st u in K holds
a * u in K
let a be Element of F; ::_thesis: ( u in K implies a * u in K )
assume u in K ; ::_thesis: a * 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 ; ::_thesis: verum
end;
then A2: for a being Element of F
for 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__::_thesis:_for_u,_v_being_Element_of_V_st_u_in_K_&_v_in_K_holds_
u_+_v_in_K
let u, v be Element of V; ::_thesis: ( u in K & v in K implies u + v in K )
assume ( u in K & v in K ) ; ::_thesis: u + 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 ; ::_thesis: verum
end;
then K is linearly-closed by A2, VECTSP_4:def_1;
then consider W being strict Subspace of V such that
A4: K = the carrier of W by A3, VECTSP_4:34;
take W ; ::_thesis: [#] W = { u where u is Element of V : T . u = 0. W }
thus [#] W = { u where u is Element of V : T . u = 0. W } by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subspace of V st [#] b1 = { u where u is Element of V : T . u = 0. W } & [#] b2 = { u where u is Element of V : T . u = 0. W } holds
b1 = b2 by VECTSP_4:29;
end;
:: deftheorem Def1 defines ker RANKNULL:def_1_:_
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for b5 being strict Subspace of V holds
( b5 = ker T iff [#] b5 = { u where u is Element of V : T . u = 0. W } );
theorem Th10: :: RANKNULL:10
for F being Field
for V, W being VectSp of F
for 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 Field; ::_thesis: for V, W being VectSp of F
for T being linear-transformation of V,W
for x being Element of V holds
( x in ker T iff T . x = 0. W )
let V, W be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for x being Element of V holds
( x in ker T iff T . x = 0. W )
let T be linear-transformation of V,W; ::_thesis: for x being Element of V holds
( x in ker T iff T . x = 0. W )
let x be Element of V; ::_thesis: ( x in ker T iff T . x = 0. W )
thus ( x in ker T implies T . x = 0. W ) ::_thesis: ( T . x = 0. W implies x in ker T )
proof
assume x in ker T ; ::_thesis: T . x = 0. W
then A1: x in [#] (ker T) by STRUCT_0:def_5;
[#] (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 T . x = 0. W ; ::_thesis: verum
end;
assume T . x = 0. W ; ::_thesis: x in ker T
then x in { u where u is Element of V : T . u = 0. W } ;
then x in [#] (ker T) by Def1;
hence x in ker T by STRUCT_0:def_5; ::_thesis: verum
end;
definition
let V, W be non empty 1-sorted ;
let T be Function of V,W;
let X be Subset of V;
:: original: .:
redefine funcT .: X -> Subset of W;
coherence
T .: X is Subset of W
proof
( rng T c= [#] W & T .: X c= rng T ) by Th7, RELAT_1:111;
hence T .: X is Subset of W by XBOOLE_1:1; ::_thesis: verum
end;
end;
definition
let F be Field;
let V, W be VectSp of F;
let T be linear-transformation of V,W;
func im T -> strict Subspace of W means :Def2: :: RANKNULL:def 2
[#] it = T .: ([#] V);
existence
ex b1 being strict Subspace of W st [#] b1 = T .: ([#] V)
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; ::_thesis: ( u in U iff ex v being Element of V st T . v = u )
thus ( u in U implies ex v being Element of V st T . v = u ) ::_thesis: ( ex v being Element of V st T . v = u implies u in U )
proof
assume u in U ; ::_thesis: ex v being Element of V st T . v = u
then consider x being set such that
x in dom T and
A2: x in [#] V and
A3: u = T . x by FUNCT_1:def_6;
reconsider x = x as Element of V by A2;
take x ; ::_thesis: T . x = u
thus T . x = u by A3; ::_thesis: verum
end;
thus ( ex v being Element of V st T . v = u implies u in U ) ::_thesis: verum
proof
given v being Element of V such that A4: T . v = u ; ::_thesis: u in U
v in [#] V ;
then v in dom T by Th7;
hence u in U by A4, FUNCT_1:def_6; ::_thesis: verum
end;
end;
A5: now__::_thesis:_for_u,_v_being_Element_of_W_st_u_in_U_&_v_in_U_holds_
u_+_v_in_U
let u, v be Element of W; ::_thesis: ( u in U & v in U implies u + v in U )
assume that
A6: u in U and
A7: v in U ; ::_thesis: u + 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; ::_thesis: verum
end;
now__::_thesis:_for_a_being_Element_of_F
for_w_being_Element_of_W_st_w_in_U_holds_
a_*_w_in_U
let a be Element of F; ::_thesis: for w being Element of W st w in U holds
a * w in U
let w be Element of W; ::_thesis: ( w in U implies a * w in U )
assume w in U ; ::_thesis: a * 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; ::_thesis: verum
end;
then A11: U is linearly-closed by A5, VECTSP_4:def_1;
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 ; ::_thesis: [#] A = T .: ([#] V)
thus [#] A = T .: ([#] V) by A12; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subspace of W st [#] b1 = T .: ([#] V) & [#] b2 = T .: ([#] V) holds
b1 = b2 by VECTSP_4:29;
end;
:: deftheorem Def2 defines im RANKNULL:def_2_:_
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for b5 being strict Subspace of W holds
( b5 = im T iff [#] b5 = T .: ([#] V) );
theorem :: RANKNULL:11
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W holds 0. V in ker T
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W holds 0. V in ker T
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W holds 0. V in ker T
let T be linear-transformation of V,W; ::_thesis: 0. V in ker T
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 0. V in ker T by Th10; ::_thesis: verum
end;
theorem Th12: :: RANKNULL:12
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V holds T .: X is Subset of (im T)
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V holds T .: X is Subset of (im T)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for X being Subset of V holds T .: X is Subset of (im T)
let T be linear-transformation of V,W; ::_thesis: for X being Subset of V holds T .: X is Subset of (im T)
let X be Subset of V; ::_thesis: T .: X is Subset of (im T)
[#] (im T) = T .: ([#] V) by Def2;
hence T .: X is Subset of (im T) by RELAT_1:123; ::_thesis: verum
end;
theorem Th13: :: RANKNULL:13
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
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 Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for y being Element of W holds
( y in im T iff ex x being Element of V st y = T . x )
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for y being Element of W holds
( y in im T iff ex x being Element of V st y = T . x )
let T be linear-transformation of V,W; ::_thesis: for y being Element of W holds
( y in im T iff ex x being Element of V st y = T . x )
let y be Element of W; ::_thesis: ( y in im T iff ex x being Element of V st y = T . x )
A1: ( y in im T implies ex x being Element of V st y = T . x )
proof
assume y in im T ; ::_thesis: ex x being Element of V st y = T . x
then reconsider y = y as Element of (im T) by STRUCT_0:def_5;
[#] (im T) = T .: ([#] V) by Def2;
then consider x being set such that
x in dom T and
A2: x in [#] V and
A3: y = T . x by FUNCT_1:def_6;
reconsider x = x as Element of V by A2;
take x ; ::_thesis: y = T . x
thus y = T . x by A3; ::_thesis: verum
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 ; ::_thesis: y in im T
dom T = [#] V by Th7;
then y in T .: ([#] V) by A4, FUNCT_1:def_6;
then y in [#] (im T) by Def2;
hence y in im T by STRUCT_0:def_5; ::_thesis: verum
end;
hence ( y in im T iff ex x being Element of V st y = T . x ) by A1; ::_thesis: verum
end;
theorem :: RANKNULL:14
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for x being Element of (ker T) holds T . x = 0. W
proof
let F be Field; ::_thesis: for V, W being VectSp of F
for T being linear-transformation of V,W
for x being Element of (ker T) holds T . x = 0. W
let V, W be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for x being Element of (ker T) holds T . x = 0. W
let T be linear-transformation of V,W; ::_thesis: for x being Element of (ker T) holds T . x = 0. W
let x be Element of (ker T); ::_thesis: T . x = 0. W
reconsider y = x as Element of V by VECTSP_4:10;
y in ker T by STRUCT_0:def_5;
hence T . x = 0. W by Th10; ::_thesis: verum
end;
theorem Th15: :: RANKNULL:15
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W st T is one-to-one holds
ker T = (0). V
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W st T is one-to-one holds
ker T = (0). V
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W st T is one-to-one holds
ker T = (0). V
let T be linear-transformation of V,W; ::_thesis: ( T is one-to-one implies ker T = (0). V )
reconsider Z = (0). V as Subspace of ker T by VECTSP_4:39;
assume A1: T is one-to-one ; ::_thesis: ker T = (0). V
for v being Element of (ker T) holds v in Z
proof
let v be Element of (ker T); ::_thesis: v in Z
A2: v in ker T by STRUCT_0:def_5;
assume not v in Z ; ::_thesis: contradiction
then A3: not v = 0. V by VECTSP_4:35;
A4: ( T . (0. V) = 0. W & dom T = [#] V ) by Th7, Th9;
reconsider v = v as Element of V by VECTSP_4:10;
T . v = 0. W by A2, Th10;
hence contradiction by A1, A3, A4, FUNCT_1:def_4; ::_thesis: verum
end;
hence ker T = (0). V by VECTSP_4:32; ::_thesis: verum
end;
theorem Th16: :: RANKNULL:16
for F being Field
for V being finite-dimensional VectSp of F holds dim ((0). V) = 0
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F holds dim ((0). V) = 0
let V be finite-dimensional VectSp of F; ::_thesis: dim ((0). V) = 0
(Omega). ((0). V) = (0). ((0). V) by VECTSP_4:36;
hence dim ((0). V) = 0 by VECTSP_9:29; ::_thesis: verum
end;
theorem Th17: :: RANKNULL:17
for F being Field
for W, V being VectSp of F
for 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 Field; ::_thesis: for W, V being VectSp of F
for 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
let W, V be VectSp of F; ::_thesis: for 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
let T be linear-transformation of V,W; ::_thesis: for x, y being Element of V st T . x = T . y holds
x - y in ker T
let x, y be Element of V; ::_thesis: ( T . x = T . y implies x - y in ker T )
assume A1: T . x = T . y ; ::_thesis: x - y in ker T
T . (x - y) = (T . x) - (T . y) by Th8
.= 0. W by A1, VECTSP_1:19 ;
hence x - y in ker T by Th10; ::_thesis: verum
end;
theorem Th18: :: RANKNULL:18
for F being Field
for V being VectSp of F
for A being Subset of V
for x, y being Element of V st x - y in Lin A holds
x in Lin (A \/ {y})
proof
let F be Field; ::_thesis: for V being VectSp of F
for A being Subset of V
for x, y being Element of V st x - y in Lin A holds
x in Lin (A \/ {y})
let V be VectSp of F; ::_thesis: for A being Subset of V
for x, y being Element of V st x - y in Lin A holds
x in Lin (A \/ {y})
let A be Subset of V; ::_thesis: for x, y being Element of V st x - y in Lin A holds
x in Lin (A \/ {y})
let x, y be Element of V; ::_thesis: ( x - y in Lin A implies x in Lin (A \/ {y}) )
assume A1: x - y in Lin A ; ::_thesis: x in Lin (A \/ {y})
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 x in Lin (A \/ {y}) by A1, A3, A2, VECTSP_5:1; ::_thesis: verum
end;
begin
theorem Th19: :: RANKNULL:19
for F being Field
for 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 Field; ::_thesis: for V, W being VectSp of F
for X being Subset of V st V is Subspace of W holds
X is Subset of W
let V, W be VectSp of F; ::_thesis: for X being Subset of V st V is Subspace of W holds
X is Subset of W
let X be Subset of V; ::_thesis: ( V is Subspace of W implies X is Subset of W )
assume V is Subspace of W ; ::_thesis: X is Subset of W
then A1: [#] V c= [#] W by VECTSP_4:def_2;
X c= [#] W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in [#] W )
assume x in X ; ::_thesis: x in [#] W
then x in [#] V ;
hence x in [#] W by A1; ::_thesis: verum
end;
hence X is Subset of W ; ::_thesis: verum
end;
theorem Th20: :: RANKNULL:20
for F being Field
for V being VectSp of F
for A being Subset of V st A is linearly-independent holds
A is Basis of Lin A
proof
let F be Field; ::_thesis: for V being VectSp of F
for A being Subset of V st A is linearly-independent holds
A is Basis of Lin A
let V be VectSp of F; ::_thesis: for A being Subset of V st A is linearly-independent holds
A is Basis of Lin A
let A be Subset of V; ::_thesis: ( A is linearly-independent implies A is Basis of Lin A )
assume A1: A is linearly-independent ; ::_thesis: A is Basis of Lin A
A c= [#] (Lin A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in [#] (Lin A) )
assume A2: x in A ; ::_thesis: x in [#] (Lin A)
reconsider x = x as Element of V by A2;
x in Lin A by A2, VECTSP_7:8;
hence x in [#] (Lin A) by STRUCT_0:def_5; ::_thesis: verum
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 A is Basis of Lin A by A3, VECTSP_7:def_3; ::_thesis: verum
end;
theorem Th21: :: RANKNULL:21
for F being Field
for V being VectSp of F
for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent
proof
let F be Field; ::_thesis: for V being VectSp of F
for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent
let V be VectSp of F; ::_thesis: for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent
let A be Subset of V; ::_thesis: for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent
let x be Element of V; ::_thesis: ( x in Lin A & not x in A implies A \/ {x} is linearly-dependent )
assume that
A1: x in Lin A and
A2: not x in A ; ::_thesis: A \/ {x} is linearly-dependent
percases ( A is linearly-independent or A is linearly-dependent ) ;
supposeA3: A is linearly-independent ; ::_thesis: A \/ {x} is linearly-dependent
x in [#] (Lin A) by A1, STRUCT_0:def_5;
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 ; ::_thesis: contradiction
then ex y being set st
( y in X & y in A9 ) by XBOOLE_0:3;
hence contradiction by A2, TARSKI:def_1; ::_thesis: verum
end;
then B is linearly-dependent by VECTSP_9:15;
hence A \/ {x} is linearly-dependent by VECTSP_9:12; ::_thesis: verum
end;
suppose A is linearly-dependent ; ::_thesis: A \/ {x} is linearly-dependent
hence A \/ {x} is linearly-dependent by VECTSP_7:1, XBOOLE_1:7; ::_thesis: verum
end;
end;
end;
theorem Th22: :: RANKNULL:22
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for 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 F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V st A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V st A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
let T be linear-transformation of V,W; ::_thesis: for A being Subset of V
for B being Basis of V st A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
let A be Subset of V; ::_thesis: for B being Basis of V st A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
let B be Basis of V; ::_thesis: ( A is Basis of ker T & A c= B implies T | (B \ A) is one-to-one )
assume that
A1: A is Basis of ker T and
A2: A c= B ; ::_thesis: T | (B \ A) is one-to-one
reconsider A9 = A as Subset of V ;
set f = T | (B \ A);
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (T | (B \ A)) or not x2 in dom (T | (B \ A)) or not (T | (B \ A)) . x1 = (T | (B \ A)) . x2 or x1 = x2 )
assume that
A3: x1 in dom (T | (B \ A)) and
A4: x2 in dom (T | (B \ A)) and
A5: (T | (B \ A)) . x1 = (T | (B \ A)) . x2 and
A6: x1 <> x2 ; ::_thesis: contradiction
x2 in dom T by A4, RELAT_1:57;
then reconsider x2 = x2 as Element of V ;
x1 in dom T by A3, RELAT_1:57;
then reconsider x1 = 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} ; ::_thesis: contradiction
percases ( x1 in A9 or x1 in {x2} ) by A9, XBOOLE_0:def_3;
suppose x1 in A9 ; ::_thesis: contradiction
hence contradiction by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose x1 in {x2} ; ::_thesis: contradiction
hence contradiction by A6, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
A10: x2 in B \ A by A4;
then A11: (T | (B \ A)) . x2 = T . x2 by FUNCT_1:49;
reconsider A = A as Basis of ker T by A1;
A12: ker T = Lin A by VECTSP_7:def_3;
(T | (B \ A)) . 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x1,x2} or z in B )
assume A15: z in {x1,x2} ; ::_thesis: z in B
percases ( z = x1 or z = x2 ) by A15, TARSKI:def_2;
suppose z = x1 ; ::_thesis: z in B
hence z in B by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose z = x2 ; ::_thesis: z in B
hence z in B by A10, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
then A16: A9 \/ {x1,x2} c= B by A2, XBOOLE_1:8;
B is linearly-independent by VECTSP_7:def_3;
hence contradiction by A13, A14, A8, A16, Th21, VECTSP_7:1; ::_thesis: verum
end;
theorem :: RANKNULL:23
for F being Field
for V being VectSp of F
for A being Subset of V
for l being Linear_Combination of A
for x being Element of V
for a being Element of F holds l +* (x,a) is Linear_Combination of A \/ {x}
proof
let F be Field; ::_thesis: for V being VectSp of F
for A being Subset of V
for l being Linear_Combination of A
for x being Element of V
for a being Element of F holds l +* (x,a) is Linear_Combination of A \/ {x}
let V be VectSp of F; ::_thesis: for A being Subset of V
for l being Linear_Combination of A
for x being Element of V
for a being Element of F holds l +* (x,a) is Linear_Combination of A \/ {x}
let A be Subset of V; ::_thesis: for l being Linear_Combination of A
for x being Element of V
for a being Element of F holds l +* (x,a) is Linear_Combination of A \/ {x}
let l be Linear_Combination of A; ::_thesis: for x being Element of V
for a being Element of F holds l +* (x,a) is Linear_Combination of A \/ {x}
let x be Element of V; ::_thesis: for a being Element of F holds l +* (x,a) is Linear_Combination of A \/ {x}
let a be Element of F; ::_thesis: l +* (x,a) is Linear_Combination of A \/ {x}
set m = l +* (x,a);
A1: dom (l +* (x,a)) = [#] V by FUNCT_2:def_1;
rng (l +* (x,a)) c= [#] F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (l +* (x,a)) or y in [#] F )
assume y in rng (l +* (x,a)) ; ::_thesis: y in [#] F
then consider x9 being set such that
A2: x9 in dom (l +* (x,a)) and
A3: (l +* (x,a)) . x9 = y by FUNCT_1:def_3;
A4: x9 in dom l by A1, A2, FUNCT_2:92;
percases ( x9 = x or x9 <> x ) ;
suppose x9 = x ; ::_thesis: y in [#] F
then (l +* (x,a)) . x9 = a by A4, FUNCT_7:31;
hence y in [#] F by A3; ::_thesis: verum
end;
supposeA5: x9 <> x ; ::_thesis: y in [#] F
A6: ( l . x9 in rng l & rng l c= [#] F ) by A4, FUNCT_1:3, FUNCT_2:92;
(l +* (x,a)) . x9 = l . x9 by A5, FUNCT_7:32;
hence y in [#] F by A3, A6; ::_thesis: verum
end;
end;
end;
then reconsider m = l +* (x,a) 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 (Carrier l) \/ {x} holds
m . v = 0. F
proof
let v be Element of V; ::_thesis: ( not v in (Carrier l) \/ {x} implies m . v = 0. F )
assume A7: not v in (Carrier l) \/ {x} ; ::_thesis: m . v = 0. F
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 m . v = 0. F by A8; ::_thesis: verum
end;
then reconsider m = m as Linear_Combination of V by VECTSP_6:def_1;
A9: Carrier m c= (Carrier l) \/ {x}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Carrier m or y in (Carrier l) \/ {x} )
assume y in Carrier m ; ::_thesis: y in (Carrier l) \/ {x}
then consider z being Element of V such that
A10: y = z and
A11: m . z <> 0. F ;
percases ( z = x or z <> x ) ;
supposeA12: z = x ; ::_thesis: y in (Carrier l) \/ {x}
( x in {x} & {x} c= (Carrier l) \/ {x} ) by TARSKI:def_1, XBOOLE_1:7;
hence y in (Carrier l) \/ {x} by A10, A12; ::_thesis: verum
end;
suppose z <> x ; ::_thesis: y in (Carrier l) \/ {x}
then m . z = l . z by FUNCT_7:32;
then A13: z in Carrier l by A11;
Carrier l c= (Carrier l) \/ {x} by XBOOLE_1:7;
hence y in (Carrier l) \/ {x} by A10, A13; ::_thesis: verum
end;
end;
end;
Carrier l c= A by VECTSP_6:def_4;
then (Carrier l) \/ {x} c= A \/ {x} by XBOOLE_1:9;
then Carrier m c= A \/ {x} by A9, XBOOLE_1:1;
hence l +* (x,a) is Linear_Combination of A \/ {x} by VECTSP_6:def_4; ::_thesis: verum
end;
definition
let V be 1-sorted ;
let X be Subset of V;
funcV \ X -> Subset of V equals :: RANKNULL:def 3
([#] V) \ X;
coherence
([#] V) \ X is Subset of V ;
end;
:: deftheorem defines \ RANKNULL:def_3_:_
for V being 1-sorted
for X being Subset of V holds V \ X = ([#] V) \ X;
definition
let F be Field;
let V be VectSp of F;
let l be Linear_Combination of V;
let X be Subset of V;
:: original: .:
redefine funcl .: X -> Subset of F;
coherence
l .: X is Subset of F
proof
l .: X c= [#] F ;
hence l .: X is Subset of F ; ::_thesis: verum
end;
end;
registration
let F be Field;
let V be VectSp of F;
cluster linearly-dependent for Element of K6( the carrier of V);
existence
ex b1 being Subset of V st b1 is linearly-dependent
proof
reconsider S = {(0. V)} as Subset of V ;
take S ; ::_thesis: S is linearly-dependent
0. V in S by TARSKI:def_1;
hence S is linearly-dependent by VECTSP_7:2; ::_thesis: verum
end;
end;
definition
let F be Field;
let V be VectSp of F;
let l be Linear_Combination of V;
let A be Subset of V;
funcl ! A -> Linear_Combination of A equals :: RANKNULL:def 4
(l | A) +* ((V \ A) --> (0. F));
coherence
(l | A) +* ((V \ A) --> (0. F)) is Linear_Combination of A
proof
set f = (l | A) +* ((V \ A) --> (0. F));
A1: dom ((l | A) +* ((V \ A) --> (0. F))) = (dom (l | A)) \/ (dom ((V \ A) --> (0. F))) by FUNCT_4:def_1;
A2: dom ((V \ A) --> (0. F)) = V \ A by FUNCOP_1:13;
dom l = [#] V by FUNCT_2:92;
then A3: dom (l | A) = A by RELAT_1:62;
then A4: dom ((l | A) +* ((V \ A) --> (0. F))) = [#] V by A1, A2, XBOOLE_1:45;
A5: A \/ (([#] V) \ A) = [#] V by XBOOLE_1:45;
rng ((l | A) +* ((V \ A) --> (0. F))) c= [#] F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((l | A) +* ((V \ A) --> (0. F))) or y in [#] F )
assume y in rng ((l | A) +* ((V \ A) --> (0. F))) ; ::_thesis: y in [#] F
then consider x being set such that
A6: x in dom ((l | A) +* ((V \ A) --> (0. F))) and
A7: y = ((l | A) +* ((V \ A) --> (0. F))) . x by FUNCT_1:def_3;
reconsider x = x as Element of V by A1, A3, A2, A6, XBOOLE_1:45;
percases ( x in A or x in V \ A ) by A5, XBOOLE_0:def_3;
supposeA8: x in A ; ::_thesis: y in [#] F
then not x in dom ((V \ A) --> (0. F)) by XBOOLE_0:def_5;
then A9: ((l | A) +* ((V \ A) --> (0. F))) . x = (l | A) . x by FUNCT_4:11;
(l | A) . x = l . x by A8, FUNCT_1:49;
hence y in [#] F by A7, A9; ::_thesis: verum
end;
supposeA10: x in V \ A ; ::_thesis: y in [#] F
then x in dom ((V \ A) --> (0. F)) by FUNCOP_1:13;
then ((l | A) +* ((V \ A) --> (0. F))) . x = ((V \ A) --> (0. F)) . x by FUNCT_4:13
.= 0. F by A10, FUNCOP_1:7 ;
hence y in [#] F by A7; ::_thesis: verum
end;
end;
end;
then reconsider f = (l | A) +* ((V \ A) --> (0. 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 } ;
{ v where v is Element of V : f . v <> 0. F } c= [#] V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Element of V : f . v <> 0. F } or x in [#] V )
assume x in { v where v is Element of V : f . v <> 0. F } ; ::_thesis: x in [#] V
then ex v being Element of V st
( x = v & f . v <> 0. F ) ;
hence x in [#] V ; ::_thesis: verum
end;
then reconsider D = { v where v is Element of V : f . v <> 0. F } as Subset of V ;
set C = Carrier l;
D c= Carrier l
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in Carrier l )
assume x in D ; ::_thesis: x in Carrier l
then consider v being Element of V such that
A11: x = v and
A12: f . v <> 0. F ;
A13: dom ((V \ A) --> (0. F)) = V \ A by FUNCOP_1:13;
A14: now__::_thesis:_not_v_in_V_\_A
assume A15: v in V \ A ; ::_thesis: contradiction
then f . v = ((V \ A) --> (0. F)) . v by A1, A4, A13, FUNCT_4:def_1
.= 0. F by A15, FUNCOP_1:7 ;
hence contradiction by A12; ::_thesis: verum
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 x in Carrier l by A11, A12, A16; ::_thesis: verum
end;
then reconsider D = D as finite Subset of V ;
take D ; ::_thesis: for v being Element of V st not v in D holds
f . v = 0. F
thus for v being Element of V st not v in D holds
f . v = 0. F ; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
Carrier f c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in A )
assume A17: x in Carrier f ; ::_thesis: x in A
reconsider x = x as Element of V by A17;
A18: f . x <> 0. F by A17, VECTSP_6:2;
now__::_thesis:_x_in_A
assume not x in A ; ::_thesis: contradiction
then A19: x in V \ A by XBOOLE_0:def_5;
then x in (dom (l | A)) \/ (dom ((V \ A) --> (0. F))) by A2, XBOOLE_0:def_3;
then f . x = ((V \ A) --> (0. F)) . x by A2, A19, FUNCT_4:def_1;
hence contradiction by A18, A19, FUNCOP_1:7; ::_thesis: verum
end;
hence x in A ; ::_thesis: verum
end;
hence (l | A) +* ((V \ A) --> (0. F)) is Linear_Combination of A by VECTSP_6:def_4; ::_thesis: verum
end;
end;
:: deftheorem defines ! RANKNULL:def_4_:_
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for A being Subset of V holds l ! A = (l | A) +* ((V \ A) --> (0. F));
theorem Th24: :: RANKNULL:24
for F being Field
for V being VectSp of F
for l being Linear_Combination of V holds l = l ! (Carrier l)
proof
let F be Field; ::_thesis: for V being VectSp of F
for l being Linear_Combination of V holds l = l ! (Carrier l)
let V be VectSp of F; ::_thesis: for l being Linear_Combination of V holds l = l ! (Carrier l)
let l be Linear_Combination of V; ::_thesis: l = l ! (Carrier l)
set f = l | (Carrier l);
set g = (V \ (Carrier l)) --> (0. F);
set m = (l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F));
A1: dom ((V \ (Carrier l)) --> (0. F)) = V \ (Carrier l) by FUNCOP_1:13;
A2: dom l = [#] V by FUNCT_2:92;
then dom (l | (Carrier l)) = Carrier l by RELAT_1:62;
then A3: (dom (l | (Carrier l))) \/ (dom ((V \ (Carrier l)) --> (0. F))) = [#] V by A1, XBOOLE_1:45;
A4: for x being set st x in dom l holds
l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x
proof
let x be set ; ::_thesis: ( x in dom l implies l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x )
assume x in dom l ; ::_thesis: l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x
then reconsider x = x as Element of V ;
percases ( x in Carrier l or not x in Carrier l ) ;
supposeA5: x in Carrier l ; ::_thesis: l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x
then not x in dom ((V \ (Carrier l)) --> (0. F)) by XBOOLE_0:def_5;
then ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x = (l | (Carrier l)) . x by A3, FUNCT_4:def_1;
hence l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x by A5, FUNCT_1:49; ::_thesis: verum
end;
supposeA6: not x in Carrier l ; ::_thesis: l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x
then x in V \ (Carrier l) by XBOOLE_0:def_5;
then ( ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x = ((V \ (Carrier l)) --> (0. F)) . x & ((V \ (Carrier l)) --> (0. F)) . x = 0. F ) by A1, A3, FUNCOP_1:7, FUNCT_4:def_1;
hence l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x by A6; ::_thesis: verum
end;
end;
end;
dom l = dom ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) by A2, A3, FUNCT_4:def_1;
hence l = l ! (Carrier l) by A4, FUNCT_1:def_11; ::_thesis: verum
end;
Lm1: for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite
proof
let F be Field; ::_thesis: for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite
let V be VectSp of F; ::_thesis: for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite
let l be Linear_Combination of V; ::_thesis: for X being Subset of V holds l .: X is finite
let X be Subset of V; ::_thesis: l .: X is finite
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 l .: X is finite by FINSET_1:1, RELAT_1:111; ::_thesis: verum
end;
theorem Th25: :: RANKNULL:25
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st v in A holds
(l ! A) . v = l . v
proof
let F be Field; ::_thesis: for V being VectSp of F
for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st v in A holds
(l ! A) . v = l . v
let V be VectSp of F; ::_thesis: for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st v in A holds
(l ! A) . v = l . v
let l be Linear_Combination of V; ::_thesis: for A being Subset of V
for v being Element of V st v in A holds
(l ! A) . v = l . v
let A be Subset of V; ::_thesis: for v being Element of V st v in A holds
(l ! A) . v = l . v
let v be Element of V; ::_thesis: ( v in A implies (l ! A) . v = l . v )
assume A1: v in A ; ::_thesis: (l ! A) . v = l . v
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 (l ! A) . v = l . v ; ::_thesis: verum
end;
theorem Th26: :: RANKNULL:26
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st not v in A holds
(l ! A) . v = 0. F
proof
let F be Field; ::_thesis: for V being VectSp of F
for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st not v in A holds
(l ! A) . v = 0. F
let V be VectSp of F; ::_thesis: for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st not v in A holds
(l ! A) . v = 0. F
let l be Linear_Combination of V; ::_thesis: for A being Subset of V
for v being Element of V st not v in A holds
(l ! A) . v = 0. F
let A be Subset of V; ::_thesis: for v being Element of V st not v in A holds
(l ! A) . v = 0. F
let v be Element of V; ::_thesis: ( not v in A implies (l ! A) . v = 0. F )
assume not v in A ; ::_thesis: (l ! A) . v = 0. F
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 FUNCOP_1:13, 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 (l ! A) . v = 0. F ; ::_thesis: verum
end;
theorem Th27: :: RANKNULL:27
for F being Field
for V being VectSp of F
for A, B being Subset of V
for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
proof
let F be Field; ::_thesis: for V being VectSp of F
for A, B being Subset of V
for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
let V be VectSp of F; ::_thesis: for A, B being Subset of V
for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
let A, B be Subset of V; ::_thesis: for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
let l be Linear_Combination of B; ::_thesis: ( A c= B implies l = (l ! A) + (l ! (B \ A)) )
assume A1: A c= B ; ::_thesis: l = (l ! A) + (l ! (B \ A))
set r = (l ! A) + (l ! (B \ A));
let v be Element of V; :: according to FUNCT_2:def_8 ::_thesis: l . v = ((l ! A) + (l ! (B \ A))) . v
A2: ( not v in B or v in A or v in B \ A )
proof
assume A3: v in B ; ::_thesis: ( v in A or v in B \ A )
B = A \/ (B \ A) by A1, XBOOLE_1:45;
hence ( v in A or v in B \ A ) by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
percases ( v in A or v in B \ A or not v in B ) by A2;
supposeA4: v in A ; ::_thesis: l . v = ((l ! A) + (l ! (B \ A))) . v
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 ((l ! A) + (l ! (B \ A))) . v = (l . v) + (0. F) by A5, VECTSP_6:22
.= l . v by RLVECT_1:4 ;
hence l . v = ((l ! A) + (l ! (B \ A))) . v ; ::_thesis: verum
end;
supposeA6: v in B \ A ; ::_thesis: l . v = ((l ! A) + (l ! (B \ A))) . v
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 ((l ! A) + (l ! (B \ A))) . v = (0. F) + (l . v) by A7, VECTSP_6:22
.= l . v by RLVECT_1:4 ;
hence l . v = ((l ! A) + (l ! (B \ A))) . v ; ::_thesis: verum
end;
supposeA8: not v in B ; ::_thesis: l . v = ((l ! A) + (l ! (B \ A))) . v
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 ((l ! A) + (l ! (B \ A))) . v = (0. F) + (0. F) by A10, VECTSP_6:22
.= 0. F by RLVECT_1:4 ;
hence l . v = ((l ! A) + (l ! (B \ A))) . v by A9; ::_thesis: verum
end;
end;
end;
registration
let F be Field;
let V be VectSp of F;
let l be Linear_Combination of V;
let X be Subset of V;
clusterl .: X -> finite ;
coherence
l .: X is finite by Lm1;
end;
definition
let V, W be non empty 1-sorted ;
let T be Function of V,W;
let X be Subset of W;
:: original: "
redefine funcT " X -> Subset of V;
coherence
T " X is Subset of V
proof
dom T = [#] V by Th7;
hence T " X is Subset of V by RELAT_1:132; ::_thesis: verum
end;
end;
theorem Th28: :: RANKNULL:28
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. F)}
proof
let F be Field; ::_thesis: for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. F)}
let V be VectSp of F; ::_thesis: for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. F)}
let l be Linear_Combination of V; ::_thesis: for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. F)}
let X be Subset of V; ::_thesis: ( X misses Carrier l implies l .: X c= {(0. F)} )
assume A1: X misses Carrier l ; ::_thesis: l .: X c= {(0. F)}
set M = l .: X;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in l .: X or y in {(0. F)} )
assume y in l .: X ; ::_thesis: y in {(0. F)}
then consider x being set such that
A2: x in dom l and
A3: x in X and
A4: y = l . x by FUNCT_1:def_6;
reconsider x = x as Element of V by A2;
now__::_thesis:_not_l_._x_<>_0._F
assume l . x <> 0. F ; ::_thesis: contradiction
then x in Carrier l ;
then x in (Carrier l) /\ X by A3, XBOOLE_0:def_4;
hence contradiction by A1, XBOOLE_0:def_7; ::_thesis: verum
end;
hence y in {(0. F)} by A4, TARSKI:def_1; ::_thesis: verum
end;
definition
let F be Field;
let V, W be VectSp of F;
let l be Linear_Combination of V;
let T be linear-transformation of V,W;
funcT @ l -> Linear_Combination of W means :Def5: :: RANKNULL:def 5
for w being Element of W holds it . w = Sum (l .: (T " {w}));
existence
ex b1 being Linear_Combination of W st
for w being Element of W holds b1 . w = Sum (l .: (T " {w}))
proof
defpred S1[ set , set ] means ex w being Element of W st
( $1 = w & $2 = Sum (l .: (T " {w})) );
A1: for x being set st x in [#] W holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in [#] W implies ex y being set st S1[x,y] )
assume x in [#] W ; ::_thesis: ex y being set st S1[x,y]
then reconsider x = x as Element of W ;
take Sum (l .: (T " {x})) ; ::_thesis: S1[x, Sum (l .: (T " {x}))]
thus S1[x, Sum (l .: (T " {x}))] ; ::_thesis: verum
end;
consider f being Function such that
A2: dom f = [#] W and
A3: for x being set st x in [#] W holds
S1[x,f . x] from CLASSES1:sch_1(A1);
A4: rng f c= [#] F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in [#] F )
assume y in rng f ; ::_thesis: y in [#] F
then consider x being set 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 y in [#] F by A6; ::_thesis: verum
end;
A7: for w being Element of W holds f . w = Sum (l .: (T " {w}))
proof
let w be Element of W; ::_thesis: f . w = Sum (l .: (T " {w}))
ex w9 being Element of W st
( w = w9 & f . w = Sum (l .: (T " {w9})) ) by A3;
hence f . w = Sum (l .: (T " {w})) ; ::_thesis: verum
end;
reconsider f = 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 } ;
{ w where w is Element of W : f . w <> 0. F } c= [#] W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { w where w is Element of W : f . w <> 0. F } or x in [#] W )
assume x in { w where w is Element of W : f . w <> 0. F } ; ::_thesis: x in [#] W
then ex w being Element of W st
( x = w & f . w <> 0. F ) ;
hence x in [#] W ; ::_thesis: verum
end;
then reconsider X = { w where w is Element of W : f . w <> 0. F } as Subset of W ;
set C = Carrier l;
reconsider TC = T .: (Carrier l) as Subset of W ;
X c= TC
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in TC )
assume x in X ; ::_thesis: x in TC
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 ; ::_thesis: contradiction
then A11: l .: (T " {w}) c= {(0. F)} by Th28;
Sum (l .: (T " {w})) = 0. F
proof
percases ( l .: (T " {w}) = {} F or l .: (T " {w}) <> {} F ) ;
suppose l .: (T " {w}) = {} F ; ::_thesis: Sum (l .: (T " {w})) = 0. F
hence Sum (l .: (T " {w})) = 0. F by RLVECT_2:8; ::_thesis: verum
end;
supposeA12: l .: (T " {w}) <> {} F ; ::_thesis: Sum (l .: (T " {w})) = 0. F
A13: {(0. F)} c= l .: (T " {w})
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {(0. F)} or y in l .: (T " {w}) )
assume y in {(0. F)} ; ::_thesis: y in l .: (T " {w})
then A14: y = 0. F by TARSKI:def_1;
ex z being set st z in l .: (T " {w}) by A12, XBOOLE_0:def_1;
hence y in l .: (T " {w}) by A11, A14, TARSKI:def_1; ::_thesis: verum
end;
l .: (T " {w}) c= {(0. F)} by A10, Th28;
then l .: (T " {w}) = {(0. F)} by A13, XBOOLE_0:def_10;
hence Sum (l .: (T " {w})) = 0. F by RLVECT_2:9; ::_thesis: verum
end;
end;
end;
hence contradiction by A7, A9; ::_thesis: verum
end;
then consider y being set 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 = 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 x in TC by A8, A16, A17, FUNCT_1:def_6; ::_thesis: verum
end;
then reconsider X = X as finite Subset of W ;
take X ; ::_thesis: for w being Element of W st not w in X holds
f . w = 0. F
thus for w being Element of W st not w in X holds
f . w = 0. F ; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of W by VECTSP_6:def_1;
take f ; ::_thesis: for w being Element of W holds f . w = Sum (l .: (T " {w}))
for w being Element of W holds f . w = Sum (l .: (T " {w}))
proof
let w be Element of W; ::_thesis: f . w = Sum (l .: (T " {w}))
ex w9 being Element of W st
( w = w9 & f . w = Sum (l .: (T " {w9})) ) by A3;
hence f . w = Sum (l .: (T " {w})) ; ::_thesis: verum
end;
hence for w being Element of W holds f . w = Sum (l .: (T " {w})) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Linear_Combination of W st ( for w being Element of W holds b1 . w = Sum (l .: (T " {w})) ) & ( for w being Element of W holds b2 . w = Sum (l .: (T " {w})) ) holds
b1 = b2
proof
let f, g be Linear_Combination of W; ::_thesis: ( ( for w being Element of W holds f . w = Sum (l .: (T " {w})) ) & ( for w being Element of W holds g . w = Sum (l .: (T " {w})) ) implies f = g )
assume 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})) ; ::_thesis: f = g
A20: for x being set st x in dom f holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume x in dom f ; ::_thesis: f . x = g . x
then reconsider x = x as Element of W ;
f . x = Sum (l .: (T " {x})) by A18;
hence f . x = g . x by A19; ::_thesis: verum
end;
( dom f = [#] W & dom g = [#] W ) by FUNCT_2:92;
hence f = g by A20, FUNCT_1:def_11; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines @ RANKNULL:def_5_:_
for F being Field
for V, W being VectSp of F
for l being Linear_Combination of V
for T being linear-transformation of V,W
for b6 being Linear_Combination of W holds
( b6 = T @ l iff for w being Element of W holds b6 . w = Sum (l .: (T " {w})) );
theorem Th29: :: RANKNULL:29
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V holds T @ l is Linear_Combination of T .: (Carrier l)
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V holds T @ l is Linear_Combination of T .: (Carrier l)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V holds T @ l is Linear_Combination of T .: (Carrier l)
let T be linear-transformation of V,W; ::_thesis: for l being Linear_Combination of V holds T @ l is Linear_Combination of T .: (Carrier l)
let l be Linear_Combination of V; ::_thesis: T @ l is Linear_Combination of T .: (Carrier l)
Carrier (T @ l) c= T .: (Carrier l)
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in Carrier (T @ l) or w in T .: (Carrier l) )
assume A1: w in Carrier (T @ l) ; ::_thesis: w in T .: (Carrier l)
reconsider w = w as Element of W by A1;
A2: (T @ l) . w <> 0. F by A1, VECTSP_6:2;
now__::_thesis:_not_T_"_{w}_misses_Carrier_l
assume A3: T " {w} misses Carrier l ; ::_thesis: contradiction
then A4: l .: (T " {w}) c= {(0. F)} by Th28;
Sum (l .: (T " {w})) = 0. F
proof
percases ( l .: (T " {w}) = {} F or l .: (T " {w}) <> {} F ) ;
suppose l .: (T " {w}) = {} F ; ::_thesis: Sum (l .: (T " {w})) = 0. F
hence Sum (l .: (T " {w})) = 0. F by RLVECT_2:8; ::_thesis: verum
end;
supposeA5: l .: (T " {w}) <> {} F ; ::_thesis: Sum (l .: (T " {w})) = 0. F
A6: {(0. F)} c= l .: (T " {w})
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {(0. F)} or y in l .: (T " {w}) )
assume y in {(0. F)} ; ::_thesis: y in l .: (T " {w})
then A7: y = 0. F by TARSKI:def_1;
ex z being set st z in l .: (T " {w}) by A5, XBOOLE_0:def_1;
hence y in l .: (T " {w}) by A4, A7, TARSKI:def_1; ::_thesis: verum
end;
l .: (T " {w}) c= {(0. F)} by A3, Th28;
then l .: (T " {w}) = {(0. F)} by A6, XBOOLE_0:def_10;
hence Sum (l .: (T " {w})) = 0. F by RLVECT_2:9; ::_thesis: verum
end;
end;
end;
hence contradiction by A2, Def5; ::_thesis: verum
end;
then consider x being set 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 = x as Element of V by A8;
T . x = w by A11, TARSKI:def_1;
hence w in T .: (Carrier l) by A9, A10, FUNCT_1:def_6; ::_thesis: verum
end;
hence T @ l is Linear_Combination of T .: (Carrier l) by VECTSP_6:def_4; ::_thesis: verum
end;
theorem Th30: :: RANKNULL:30
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V holds Carrier (T @ l) c= T .: (Carrier l)
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V holds Carrier (T @ l) c= T .: (Carrier l)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V holds Carrier (T @ l) c= T .: (Carrier l)
let T be linear-transformation of V,W; ::_thesis: for l being Linear_Combination of V holds Carrier (T @ l) c= T .: (Carrier l)
let l be Linear_Combination of V; ::_thesis: Carrier (T @ l) c= T .: (Carrier l)
T @ l is Linear_Combination of T .: (Carrier l) by Th29;
hence Carrier (T @ l) c= T .: (Carrier l) by VECTSP_6:def_4; ::_thesis: verum
end;
theorem Th31: :: RANKNULL:31
for F being Field
for V being VectSp of F
for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l + m) = (Carrier l) \/ (Carrier m)
proof
let F be Field; ::_thesis: for V being VectSp of F
for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l + m) = (Carrier l) \/ (Carrier m)
let V be VectSp of F; ::_thesis: for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l + m) = (Carrier l) \/ (Carrier m)
let l, m be Linear_Combination of V; ::_thesis: ( Carrier l misses Carrier m implies Carrier (l + m) = (Carrier l) \/ (Carrier m) )
assume A1: Carrier l misses Carrier m ; ::_thesis: Carrier (l + m) = (Carrier l) \/ (Carrier m)
thus Carrier (l + m) c= (Carrier l) \/ (Carrier m) by VECTSP_6:23; :: according to XBOOLE_0:def_10 ::_thesis: (Carrier l) \/ (Carrier m) c= Carrier (l + m)
thus (Carrier l) \/ (Carrier m) c= Carrier (l + m) ::_thesis: verum
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in (Carrier l) \/ (Carrier m) or v in Carrier (l + m) )
assume A2: v in (Carrier l) \/ (Carrier m) ; ::_thesis: v in Carrier (l + m)
percases ( v in Carrier l or v in Carrier m ) by A2, XBOOLE_0:def_3;
supposeA3: v in Carrier l ; ::_thesis: v in Carrier (l + m)
then reconsider v = 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 v in Carrier (l + m) by A4; ::_thesis: verum
end;
supposeA5: v in Carrier m ; ::_thesis: v in Carrier (l + m)
then reconsider v = 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 v in Carrier (l + m) by A6; ::_thesis: verum
end;
end;
end;
end;
theorem Th32: :: RANKNULL:32
for F being Field
for V being VectSp of F
for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l - m) = (Carrier l) \/ (Carrier m)
proof
let F be Field; ::_thesis: for V being VectSp of F
for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l - m) = (Carrier l) \/ (Carrier m)
let V be VectSp of F; ::_thesis: for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l - m) = (Carrier l) \/ (Carrier m)
let l, m be Linear_Combination of V; ::_thesis: ( Carrier l misses Carrier m implies Carrier (l - m) = (Carrier l) \/ (Carrier m) )
assume A1: Carrier l misses Carrier m ; ::_thesis: Carrier (l - m) = (Carrier l) \/ (Carrier m)
Carrier (- m) = Carrier m by VECTSP_6:38;
hence Carrier (l - m) = (Carrier l) \/ (Carrier m) by A1, Th31; ::_thesis: verum
end;
theorem Th33: :: RANKNULL:33
for F being Field
for V being VectSp of F
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 F be Field; ::_thesis: for V being VectSp of F
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)
let V be VectSp of F; ::_thesis: 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)
let A, B be Subset of V; ::_thesis: ( A c= B & B is Basis of V implies V is_the_direct_sum_of Lin A, Lin (B \ A) )
assume that
A1: A c= B and
A2: B is Basis of V ; ::_thesis: V is_the_direct_sum_of Lin A, Lin (B \ A)
A3: (Lin A) /\ (Lin (B \ A)) = (0). V
proof
set U = (Lin A) /\ (Lin (B \ A));
reconsider W = (0). V as strict Subspace of (Lin A) /\ (Lin (B \ A)) by VECTSP_4:39;
for v being Element of ((Lin A) /\ (Lin (B \ A))) holds v in W
proof
let v be Element of ((Lin A) /\ (Lin (B \ A))); ::_thesis: v in W
A4: B is linearly-independent by A2, VECTSP_7:def_3;
A5: v in (Lin A) /\ (Lin (B \ A)) by STRUCT_0:def_5;
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, XBOOLE_1:1;
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 v in W by A6, VECTSP_4:35; ::_thesis: verum
end;
hence (Lin A) /\ (Lin (B \ A)) = (0). V by VECTSP_4:32; ::_thesis: verum
end;
(Omega). V = (Lin A) + (Lin (B \ A))
proof
set U = (Lin A) + (Lin (B \ A));
A11: [#] V c= [#] ((Lin A) + (Lin (B \ A)))
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in [#] V or v in [#] ((Lin A) + (Lin (B \ A))) )
assume v in [#] V ; ::_thesis: v in [#] ((Lin A) + (Lin (B \ A)))
then reconsider v = 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 = (l ! A) + (l ! (B \ A)) 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 (l ! A) ; ::_thesis: ex v2 being Element of V st
( Sum (l ! A) in Lin A & v2 in Lin (B \ A) & v = (Sum (l ! A)) + v2 )
take Sum (l ! (B \ A)) ; ::_thesis: ( Sum (l ! A) in Lin A & Sum (l ! (B \ A)) in Lin (B \ A) & v = (Sum (l ! A)) + (Sum (l ! (B \ A))) )
thus ( Sum (l ! A) in Lin A & Sum (l ! (B \ A)) in Lin (B \ A) & v = (Sum (l ! A)) + (Sum (l ! (B \ A))) ) by A12, A13, VECTSP_6:44, VECTSP_7:7; ::_thesis: verum
end;
then v in (Lin A) + (Lin (B \ A)) by VECTSP_5:1;
hence v in [#] ((Lin A) + (Lin (B \ A))) by STRUCT_0:def_5; ::_thesis: verum
end;
[#] ((Lin A) + (Lin (B \ A))) c= [#] V by VECTSP_4:def_2;
then [#] ((Lin A) + (Lin (B \ A))) = [#] V by A11, XBOOLE_0:def_10;
hence (Omega). V = (Lin A) + (Lin (B \ A)) by VECTSP_4:29; ::_thesis: verum
end;
hence V is_the_direct_sum_of Lin A, Lin (B \ A) by A3, VECTSP_5:def_4; ::_thesis: verum
end;
theorem Th34: :: RANKNULL:34
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for l being Linear_Combination of A
for 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 F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for l being Linear_Combination of A
for 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 )
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for A being Subset of V
for l being Linear_Combination of A
for 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 )
let T be linear-transformation of V,W; ::_thesis: for A being Subset of V
for l being Linear_Combination of A
for 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 )
let A be Subset of V; ::_thesis: for l being Linear_Combination of A
for 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 )
let l be Linear_Combination of A; ::_thesis: for 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 )
let v be Element of V; ::_thesis: ( T | A is one-to-one & v in A implies ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X ) )
assume that
A1: T | A is one-to-one and
A2: v in A ; ::_thesis: ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
set X = (T " {(T . v)}) \ {v};
A3: (T " {(T . v)}) \ {v} misses A
proof
dom T = [#] V by Th7;
then A4: dom (T | A) = A by RELAT_1:62;
assume (T " {(T . v)}) \ {v} meets A ; ::_thesis: contradiction
then consider x being set such that
A5: x in (T " {(T . v)}) \ {v} 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, A6, A7, A4, FUNCT_1:def_4; ::_thesis: verum
end;
take (T " {(T . v)}) \ {v} ; ::_thesis: ( (T " {(T . v)}) \ {v} misses A & T " {(T . v)} = {v} \/ ((T " {(T . v)}) \ {v}) )
{v} c= T " {(T . v)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in T " {(T . v)} )
assume x in {v} ; ::_thesis: x in T " {(T . v)}
then A9: x = v by TARSKI:def_1;
( dom T = [#] V & T . v in {(T . v)} ) by Th7, TARSKI:def_1;
hence x in T " {(T . v)} by A9, FUNCT_1:def_7; ::_thesis: verum
end;
hence ( (T " {(T . v)}) \ {v} misses A & T " {(T . v)} = {v} \/ ((T " {(T . v)}) \ {v}) ) by A3, XBOOLE_1:45; ::_thesis: verum
end;
theorem Th35: :: RANKNULL:35
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {(0. F)}
proof
let F be Field; ::_thesis: for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {(0. F)}
let V be VectSp of F; ::_thesis: for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {(0. F)}
let l be Linear_Combination of V; ::_thesis: for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {(0. F)}
let X be Subset of V; ::_thesis: ( X misses Carrier l & X <> {} implies l .: X = {(0. F)} )
assume that
A1: X misses Carrier l and
A2: X <> {} ; ::_thesis: l .: X = {(0. F)}
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 l .: X = {(0. F)} by A3, ZFMISC_1:33; ::_thesis: verum
end;
theorem Th36: :: RANKNULL:36
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
for w being Element of W st w in Carrier (T @ l) holds
T " {w} meets Carrier l
proof
let F be Field; ::_thesis: for V, W being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
for w being Element of W st w in Carrier (T @ l) holds
T " {w} meets Carrier l
let V, W be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V
for w being Element of W st w in Carrier (T @ l) holds
T " {w} meets Carrier l
let T be linear-transformation of V,W; ::_thesis: for l being Linear_Combination of V
for w being Element of W st w in Carrier (T @ l) holds
T " {w} meets Carrier l
let l be Linear_Combination of V; ::_thesis: for w being Element of W st w in Carrier (T @ l) holds
T " {w} meets Carrier l
let w be Element of W; ::_thesis: ( w in Carrier (T @ l) implies T " {w} meets Carrier l )
assume w in Carrier (T @ l) ; ::_thesis: T " {w} meets Carrier l
then A1: (T @ l) . w <> 0. F by VECTSP_6:2;
assume A2: T " {w} misses Carrier l ; ::_thesis: contradiction
percases ( T " {w} = {} or T " {w} <> {} ) ;
suppose T " {w} = {} ; ::_thesis: contradiction
then Sum (l .: (T " {w})) = Sum ({} F)
.= 0. F by RLVECT_2:8 ;
hence contradiction by A1, Def5; ::_thesis: verum
end;
suppose T " {w} <> {} ; ::_thesis: contradiction
then l .: (T " {w}) = {(0. F)} by A2, Th35;
then Sum (l .: (T " {w})) = 0. F by RLVECT_2:9;
hence contradiction by A1, Def5; ::_thesis: verum
end;
end;
end;
theorem Th37: :: RANKNULL:37
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
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 F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
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
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V
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
let T be linear-transformation of V,W; ::_thesis: for l being Linear_Combination of V
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
let l be Linear_Combination of V; ::_thesis: 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
let v be Element of V; ::_thesis: ( T | (Carrier l) is one-to-one & v in Carrier l implies (T @ l) . (T . v) = l . v )
assume that
A1: T | (Carrier l) is one-to-one and
A2: v in Carrier l ; ::_thesis: (T @ l) . (T . v) = l . v
consider X being Subset of V such that
A3: X misses Carrier l and
A4: T " {(T . v)} = {v} \/ X by A1, A2, Th34;
percases ( X = {} or X <> {} ) ;
supposeA5: X = {} ; ::_thesis: (T @ l) . (T . v) = l . v
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 (T @ l) . (T . v) = l . v by Def5; ::_thesis: verum
end;
supposeA7: X <> {} ; ::_thesis: (T @ l) . (T . v) = l . v
A8: l .: X c= {(0. F)}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in l .: X or y in {(0. F)} )
assume y in l .: X ; ::_thesis: y in {(0. F)}
then consider x being set such that
A9: x in dom l and
A10: x in X and
A11: y = l . x by FUNCT_1:def_6;
A12: now__::_thesis:_not_x_in_Carrier_l
assume x in Carrier l ; ::_thesis: contradiction
then x in (Carrier l) /\ X by A10, XBOOLE_0:def_4;
hence contradiction by A3, XBOOLE_0:def_7; ::_thesis: verum
end;
reconsider x = x as Element of V by A9;
l . x = 0. F by A12;
hence y in {(0. F)} by A11, TARSKI:def_1; ::_thesis: verum
end;
A13: l .: X misses l .: {v}
proof
assume l .: X meets l .: {v} ; ::_thesis: contradiction
then consider x being set 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 contradiction by A2, A17, VECTSP_6:2; ::_thesis: verum
end;
A18: dom l = [#] V by FUNCT_2:92;
{(0. F)} c= l .: X
proof
consider y being set such that
A19: y in X by A7, XBOOLE_0:def_1;
A20: now__::_thesis:_not_y_in_Carrier_l
assume y in Carrier l ; ::_thesis: contradiction
then y in (Carrier l) /\ X by A19, XBOOLE_0:def_4;
hence contradiction by A3, XBOOLE_0:def_7; ::_thesis: verum
end;
reconsider y = y as Element of V by A19;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. F)} or x in l .: X )
assume x in {(0. F)} ; ::_thesis: x in l .: X
then x = 0. F by TARSKI:def_1;
then l . y = x by A20;
hence x in l .: X by A18, A19, FUNCT_1:def_6; ::_thesis: verum
end;
then A21: l .: X = {(0. F)} by A8, XBOOLE_0:def_10;
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 (T @ l) . (T . v) = l . v by Def5; ::_thesis: verum
end;
end;
end;
theorem Th38: :: RANKNULL:38
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
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 F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
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)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V
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)
let T be linear-transformation of V,W; ::_thesis: for l being Linear_Combination of V
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)
let l be Linear_Combination of V; ::_thesis: 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)
let G be FinSequence of V; ::_thesis: ( rng G = Carrier l & T | (Carrier l) is one-to-one implies T * (l (#) G) = (T @ l) (#) (T * G) )
assume that
A1: rng G = Carrier l and
A2: T | (Carrier l) is one-to-one ; ::_thesis: T * (l (#) G) = (T @ l) (#) (T * G)
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; ::_thesis: ( 1 <= k & k <= len L implies L . k = R . k )
assume A6: ( 1 <= k & k <= len L ) ; ::_thesis: L . k = R . k
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;
k in NAT by ORDINAL1:def_12;
then 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, FUNCT_1: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 L . k = R . k by A7, A8, A11, A5, A12, VECTSP_6:def_5; ::_thesis: verum
end;
hence T * (l (#) G) = (T @ l) (#) (T * G) by A4, A3, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th39: :: RANKNULL:39
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @ l)
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @ l)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @ l)
let T be linear-transformation of V,W; ::_thesis: for l being Linear_Combination of V st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @ l)
let l be Linear_Combination of V; ::_thesis: ( T | (Carrier l) is one-to-one implies T .: (Carrier l) = Carrier (T @ l) )
assume A1: T | (Carrier l) is one-to-one ; ::_thesis: T .: (Carrier l) = Carrier (T @ l)
A2: T .: (Carrier l) c= Carrier (T @ l)
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in T .: (Carrier l) or w in Carrier (T @ l) )
assume w in T .: (Carrier l) ; ::_thesis: w in Carrier (T @ l)
then consider v being set 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 = 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 w in Carrier (T @ l) by A5; ::_thesis: verum
end;
Carrier (T @ l) c= T .: (Carrier l) by Th30;
hence T .: (Carrier l) = Carrier (T @ l) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th40: :: RANKNULL:40
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V
for 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 F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V
for l being Linear_Combination of B \ A st A is Basis of ker T & A c= B holds
T . (Sum l) = Sum (T @ l)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V
for l being Linear_Combination of B \ A st A is Basis of ker T & A c= B holds
T . (Sum l) = Sum (T @ l)
let T be linear-transformation of V,W; ::_thesis: for A being Subset of V
for B being Basis of V
for l being Linear_Combination of B \ A st A is Basis of ker T & A c= B holds
T . (Sum l) = Sum (T @ l)
let A be Subset of V; ::_thesis: for B being Basis of V
for l being Linear_Combination of B \ A st A is Basis of ker T & A c= B holds
T . (Sum l) = Sum (T @ l)
let B be Basis of V; ::_thesis: for l being Linear_Combination of B \ A st A is Basis of ker T & A c= B holds
T . (Sum l) = Sum (T @ l)
let l be Linear_Combination of B \ A; ::_thesis: ( A is Basis of ker T & A c= B implies T . (Sum l) = Sum (T @ l) )
assume ( A is Basis of ker T & A c= B ) ; ::_thesis: T . (Sum l) = Sum (T @ l)
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 = T * G 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 T . (Sum l) = Sum (T @ l) by A6, A8, MATRLIN:16; ::_thesis: verum
end;
theorem Th41: :: RANKNULL:41
for F being Field
for V being VectSp of F
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 F be Field; ::_thesis: for V being VectSp of F
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 )
let V be VectSp of F; ::_thesis: 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 )
let X be Subset of V; ::_thesis: ( X is linearly-dependent implies ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V ) )
assume X is linearly-dependent ; ::_thesis: ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V )
then ex l being Linear_Combination of X st
( Sum l = 0. V & not Carrier l = {} ) by VECTSP_7:def_1;
hence ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V ) ; ::_thesis: verum
end;
definition
let F be Field;
let V, W be VectSp of F;
let X be Subset of V;
let T be linear-transformation of V,W;
let l be Linear_Combination of T .: X;
assume A1: T | X is one-to-one ;
funcT # l -> Linear_Combination of X equals :Def6: :: RANKNULL:def 6
(l * T) +* ((V \ X) --> (0. F));
coherence
(l * T) +* ((V \ X) --> (0. F)) is Linear_Combination of X
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 by XBOOLE_1:1;
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 by FUNCOP_1:13;
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 ((l * T) +* ((V \ X) --> (0. 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 ((l * T) +* ((V \ X) --> (0. F))) c= [#] F by XBOOLE_1:1;
( dom T = [#] V & ([#] V) \/ (([#] V) \ X) = [#] V ) by Th7, XBOOLE_1:12;
then dom ((l * T) +* ((V \ X) --> (0. F))) = [#] V by A3, A4, FUNCT_4:def_1;
then reconsider f = (l * T) +* ((V \ X) --> (0. 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 } ;
{ v where v is Element of V : f . v <> 0. F } c= [#] V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Element of V : f . v <> 0. F } or x in [#] V )
assume x in { v where v is Element of V : f . v <> 0. F } ; ::_thesis: x in [#] V
then ex v being Element of V st
( v = x & f . v <> 0. F ) ;
hence x in [#] V ; ::_thesis: verum
end;
then reconsider C = { v where v is Element of V : f . v <> 0. F } 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 | ((T " (Carrier l)) /\ X);
take T | ((T " (Carrier l)) /\ X) ; ::_thesis: ( T | ((T " (Carrier l)) /\ X) is one-to-one & dom (T | ((T " (Carrier l)) /\ X)) = C & rng (T | ((T " (Carrier l)) /\ X)) c= Carrier l )
A6: C c= (T " (Carrier l)) /\ X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in (T " (Carrier l)) /\ X )
assume A7: x in C ; ::_thesis: x in (T " (Carrier l)) /\ X
A8: ex v being Element of V st
( v = x & f . v <> 0. F ) by A7;
reconsider x = x as Element of V by A7;
A9: now__::_thesis:_x_in_X
assume not x in X ; ::_thesis: contradiction
then A10: x in V \ X by XBOOLE_0:def_5;
then x in dom ((V \ X) --> (0. F)) by FUNCOP_1:13;
then f . x = ((V \ X) --> (0. F)) . x by FUNCT_4:13;
hence contradiction by A8, A10, FUNCOP_1:7; ::_thesis: verum
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 x in (T " (Carrier l)) /\ X by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
A13: dom T = [#] V by Th7;
A14: rng (T | ((T " (Carrier l)) /\ X)) c= Carrier l
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (T | ((T " (Carrier l)) /\ X)) or y in Carrier l )
assume y in rng (T | ((T " (Carrier l)) /\ X)) ; ::_thesis: y in Carrier l
then consider x being set such that
A15: x in dom (T | ((T " (Carrier l)) /\ X)) and
A16: y = (T | ((T " (Carrier l)) /\ X)) . 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 y in Carrier l by A15, A16, FUNCT_1:49; ::_thesis: verum
end;
(T " (Carrier l)) /\ X c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (T " (Carrier l)) /\ X or x in C )
assume A17: x in (T " (Carrier l)) /\ X ; ::_thesis: x in C
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 = 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 x in C by A23, A22; ::_thesis: verum
end;
then (T " (Carrier l)) /\ X = C by A6, XBOOLE_0:def_10;
hence ( T | ((T " (Carrier l)) /\ X) is one-to-one & dom (T | ((T " (Carrier l)) /\ X)) = C & rng (T | ((T " (Carrier l)) /\ X)) c= Carrier l ) by A1, A13, A14, Th2, RELAT_1:62, XBOOLE_1:17; ::_thesis: verum
end;
then card C c= card (Carrier l) by CARD_1:10;
then reconsider C = C as finite Subset of V ;
take C ; ::_thesis: for v being Element of V st not v in C holds
f . v = 0. F
thus for v being Element of V st not v in C holds
f . v = 0. F ; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
Carrier f c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in X )
assume A24: x in Carrier f ; ::_thesis: x in X
reconsider x = x as Element of V by A24;
now__::_thesis:_x_in_X
assume not x in X ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence x in X ; ::_thesis: verum
end;
hence (l * T) +* ((V \ X) --> (0. F)) is Linear_Combination of X by VECTSP_6:def_4; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines # RANKNULL:def_6_:_
for F being Field
for V, W being VectSp of F
for X being Subset of V
for T being linear-transformation of V,W
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T # l = (l * T) +* ((V \ X) --> (0. F));
theorem Th42: :: RANKNULL:42
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X
for v being Element of V st v in X & T | X is one-to-one holds
(T # l) . v = l . (T . v)
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X
for v being Element of V st v in X & T | X is one-to-one holds
(T # l) . v = l . (T . v)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X
for v being Element of V st v in X & T | X is one-to-one holds
(T # l) . v = l . (T . v)
let T be linear-transformation of V,W; ::_thesis: for X being Subset of V
for l being Linear_Combination of T .: X
for v being Element of V st v in X & T | X is one-to-one holds
(T # l) . v = l . (T . v)
let X be Subset of V; ::_thesis: for l being Linear_Combination of T .: X
for v being Element of V st v in X & T | X is one-to-one holds
(T # l) . v = l . (T . v)
let l be Linear_Combination of T .: X; ::_thesis: for v being Element of V st v in X & T | X is one-to-one holds
(T # l) . v = l . (T . v)
let v be Element of V; ::_thesis: ( v in X & T | X is one-to-one implies (T # l) . v = l . (T . v) )
assume ( v in X & T | X is one-to-one ) ; ::_thesis: (T # l) . v = l . (T . v)
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 (T # l) . v = l . (T . v) by A1, FUNCT_1:13; ::_thesis: verum
end;
theorem Th43: :: RANKNULL:43
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l
let T be linear-transformation of V,W; ::_thesis: for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l
let X be Subset of V; ::_thesis: for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l
let l be Linear_Combination of T .: X; ::_thesis: ( T | X is one-to-one implies T @ (T # l) = l )
assume A1: T | X is one-to-one ; ::_thesis: T @ (T # l) = l
let w be Element of W; :: according to FUNCT_2:def_8 ::_thesis: (T @ (T # l)) . w = l . w
set m = T @ (T # l);
percases ( w in Carrier l or not w in Carrier l ) ;
supposeA2: w in Carrier l ; ::_thesis: (T @ (T # l)) . w = l . w
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 set 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 = 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: (T @ (T # l)) . w = Sum ((T # l) .: (T " {(T . v)})) by A7, Def5
.= Sum ({(l . (T . v))} \/ ((T # l) .: B)) by A9, A10, A11, RELAT_1:120 ;
percases ( B = {} or B <> {} ) ;
suppose B = {} ; ::_thesis: (T @ (T # l)) . w = l . w
then (T @ (T # l)) . w = Sum ({(l . (T . v))} \/ ({} F)) by A12
.= l . w by A7, RLVECT_2:9 ;
hence (T @ (T # l)) . w = l . w ; ::_thesis: verum
end;
supposeA13: B <> {} ; ::_thesis: (T @ (T # l)) . w = l . w
Carrier (T # l) c= X by VECTSP_6:def_4;
then B misses Carrier (T # l) by A8, XBOOLE_1:63;
then (T @ (T # l)) . 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 (T @ (T # l)) . w = l . w ; ::_thesis: verum
end;
end;
end;
supposeA14: not w in Carrier l ; ::_thesis: (T @ (T # l)) . w = l . w
then A15: l . w = 0. F ;
now__::_thesis:_not_(T_@_(T_#_l))_._w_<>_0._F
assume A16: (T @ (T # l)) . w <> 0. F ; ::_thesis: contradiction
then w in Carrier (T @ (T # l)) ;
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 (T @ (T # l)) . w = (T # l) . v by A18, A19, Th37
.= 0. F by A1, A15, A18, A19, A20, Th42 ;
hence contradiction by A16; ::_thesis: verum
end;
hence (T @ (T # l)) . w = l . w by A14; ::_thesis: verum
end;
end;
end;
begin
definition
let F be Field;
let V, W be finite-dimensional VectSp of F;
let T be linear-transformation of V,W;
func rank T -> Nat equals :: RANKNULL:def 7
dim (im T);
coherence
dim (im T) is Nat ;
func nullity T -> Nat equals :: RANKNULL:def 8
dim (ker T);
coherence
dim (ker T) is Nat ;
end;
:: deftheorem defines rank RANKNULL:def_7_:_
for F being Field
for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W holds rank T = dim (im T);
:: deftheorem defines nullity RANKNULL:def_8_:_
for F being Field
for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W holds nullity T = dim (ker T);
theorem Th44: :: RANKNULL:44
for F being Field
for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W holds dim V = (rank T) + (nullity T)
proof
let F be Field; ::_thesis: for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W holds dim V = (rank T) + (nullity T)
let V, W be finite-dimensional VectSp of F; ::_thesis: for T being linear-transformation of V,W holds dim V = (rank T) + (nullity T)
let T be linear-transformation of V,W; ::_thesis: dim V = (rank T) + (nullity T)
set A = the finite Basis of ker T;
reconsider A9 = the finite Basis of ker T as Subset of V by Th19;
consider B being Basis of V such that
A1: the finite Basis of ker T c= B by VECTSP_9:13;
reconsider B = B as finite Subset of V by VECTSP_9:20;
reconsider X = B \ A9 as finite Subset of B by XBOOLE_1:36;
reconsider X = X as finite Subset of V ;
A2: B = the finite Basis of ker T \/ X by A1, XBOOLE_1:45;
reconsider B = B as finite Basis of V ;
reconsider A = the finite Basis of ker T 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 ; ::_thesis: contradiction
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 T # l9 ; ::_thesis: l = T @ (T # l9)
thus l = T @ (T # l9) by A3, Th43; ::_thesis: verum
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, XBOOLE_1:1;
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 contradiction by A5, A7, Th30, XBOOLE_1:3; ::_thesis: verum
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 = 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); ::_thesis: v in L
reconsider v9 = v as Element of W by VECTSP_4:10;
reconsider C9 = C as Subset of W ;
v in im T by STRUCT_0:def_5;
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 by STRUCT_0:def_5;
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 ; ::_thesis: v = Sum m
thus v = Sum m by A1, A14, A21, A19, Th40; ::_thesis: verum
end;
then v in Lin C9 by VECTSP_7:7;
hence v in L by VECTSP_9:17; ::_thesis: verum
end;
then A22: Lin C = im T by VECTSP_4:32;
reconsider C = C as linearly-independent Subset of (im T) by A4, VECTSP_9:12;
reconsider C = 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 dim V = (rank T) + (nullity T) ; ::_thesis: verum
end;
theorem :: RANKNULL:45
for F being Field
for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W st T is one-to-one holds
dim V = rank T
proof
let F be Field; ::_thesis: for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W st T is one-to-one holds
dim V = rank T
let V, W be finite-dimensional VectSp of F; ::_thesis: for T being linear-transformation of V,W st T is one-to-one holds
dim V = rank T
let T be linear-transformation of V,W; ::_thesis: ( T is one-to-one implies dim V = rank T )
assume T is one-to-one ; ::_thesis: dim V = rank T
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 dim V = rank T ; ::_thesis: verum
end;