:: by Kazuhisa Nakasho , Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received July 10, 2014

:: Copyright (c) 2014 Association of Mizar Users

registration

let V be Z_Module;

let A be finite Subset of V;

correctness

coherence

Lin A is finitely-generated ;

end;
let A be finite Subset of V;

correctness

coherence

Lin A is finitely-generated ;

proof end;

registration

let V be free finite-rank Z_Module;

existence

ex b_{1} being Basis of V st b_{1} is finite

end;
existence

ex b

proof end;

registration

let V be free finite-rank Z_Module;

correctness

coherence

for b_{1} being Basis of V holds b_{1} is finite ;

;

end;
correctness

coherence

for b

;

theorem RL5Th30: :: ZMODUL05:3

for V being Z_Module

for A being finite linearly-independent Subset of V holds card A = rank (Lin A)

for A being finite linearly-independent Subset of V holds card A = rank (Lin A)

proof end;

theorem :: ZMODUL05:5

for V being free finite-rank Z_Module holds

( rank V = 1 iff ex v being VECTOR of V st

( v <> 0. V & (Omega). V = Lin {v} ) )

( rank V = 1 iff ex v being VECTOR of V st

( v <> 0. V & (Omega). V = Lin {v} ) )

proof end;

theorem :: ZMODUL05:6

for V being free finite-rank Z_Module holds

( rank V = 2 iff ex u, v being VECTOR of V st

( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )

( rank V = 2 iff ex u, v being VECTOR of V st

( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )

proof end;

RL5Lm2: for V being free finite-rank Z_Module

for W being Submodule of V

for n being Nat st n <= rank V holds

ex W being strict free Submodule of V st rank W = n

proof end;

theorem :: ZMODUL05:7

definition

let V be free finite-rank Z_Module;

let n be Nat;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex W being strict free Submodule of V st

( W = x & rank W = n ) )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ex W being strict free Submodule of V st

( W = x & rank W = n ) ) ) & ( for x being object holds

( x in b_{2} iff ex W being strict free Submodule of V st

( W = x & rank W = n ) ) ) holds

b_{1} = b_{2}

end;
let n be Nat;

func n Submodules_of V -> set means :RL5Def4: :: ZMODUL05:def 1

for x being object holds

( x in it iff ex W being strict free Submodule of V st

( W = x & rank W = n ) );

existence for x being object holds

( x in it iff ex W being strict free Submodule of V st

( W = x & rank W = n ) );

ex b

for x being object holds

( x in b

( W = x & rank W = n ) )

proof end;

uniqueness for b

( x in b

( W = x & rank W = n ) ) ) & ( for x being object holds

( x in b

( W = x & rank W = n ) ) ) holds

b

proof end;

:: deftheorem RL5Def4 defines Submodules_of ZMODUL05:def 1 :

for V being free finite-rank Z_Module

for n being Nat

for b_{3} being set holds

( b_{3} = n Submodules_of V iff for x being object holds

( x in b_{3} iff ex W being strict free Submodule of V st

( W = x & rank W = n ) ) );

for V being free finite-rank Z_Module

for n being Nat

for b

( b

( x in b

( W = x & rank W = n ) ) );

theorem :: ZMODUL05:8

for V being free finite-rank Z_Module

for n being Nat st n <= rank V holds

not n Submodules_of V is empty

for n being Nat st n <= rank V holds

not n Submodules_of V is empty

proof end;

theorem :: ZMODUL05:10

for V being free finite-rank Z_Module

for W being Submodule of V

for n being Nat holds n Submodules_of W c= n Submodules_of V

for W being Submodule of V

for n being Nat holds n Submodules_of W c= n Submodules_of V

proof end;

theorem :: ZMODUL05:11

for F, G being FinSequence of INT

for v being Integer st len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) holds

Sum F = (Sum G) + v

for v being Integer st len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) holds

Sum F = (Sum G) + v

proof end;

theorem RLVECT142: :: ZMODUL05:12

for F, G being FinSequence of INT st rng F = rng G & F is one-to-one & G is one-to-one holds

Sum F = Sum G

Sum F = Sum G

proof end;

definition

let T be finite Subset of the carrier of INT.Ring;

ex b_{1} being Element of INT.Ring ex F being FinSequence of INT st

( rng F = T & F is one-to-one & b_{1} = Sum F )

for b_{1}, b_{2} being Element of INT.Ring st ex F being FinSequence of INT st

( rng F = T & F is one-to-one & b_{1} = Sum F ) & ex F being FinSequence of INT st

( rng F = T & F is one-to-one & b_{2} = Sum F ) holds

b_{1} = b_{2}
by RLVECT142;

end;
func Sum T -> Element of INT.Ring means :: ZMODUL05:def 2

ex F being FinSequence of INT st

( rng F = T & F is one-to-one & it = Sum F );

existence ex F being FinSequence of INT st

( rng F = T & F is one-to-one & it = Sum F );

ex b

( rng F = T & F is one-to-one & b

proof end;

uniqueness for b

( rng F = T & F is one-to-one & b

( rng F = T & F is one-to-one & b

b

:: deftheorem defines Sum ZMODUL05:def 2 :

for T being finite Subset of the carrier of INT.Ring

for b_{2} being Element of INT.Ring holds

( b_{2} = Sum T iff ex F being FinSequence of INT st

( rng F = T & F is one-to-one & b_{2} = Sum F ) );

for T being finite Subset of the carrier of INT.Ring

for b

( b

( rng F = T & F is one-to-one & b

definition
end;

registration

let V, W be Z_Module;

ex b_{1} being Function of V,W st

( b_{1} is additive & b_{1} is homogeneous )

end;
cluster non empty Relation-like the carrier of V -defined the carrier of W -valued Function-like total quasi_total additive homogeneous for Element of K10(K11( the carrier of V, the carrier of W));

existence ex b

( b

proof end;

theorem MATRLIN16: :: ZMODUL05:16

for V1, V2 being Z_Module

for f being Function of V1,V2

for p being FinSequence of V1 st f is additive & f is homogeneous holds

f . (Sum p) = Sum (f * p)

for f being Function of V1,V2

for p being FinSequence of V1 st f is additive & f is homogeneous holds

f . (Sum p) = Sum (f * p)

proof end;

definition
end;

theorem Th8: :: ZMODUL05:18

for V, W being Z_Module

for T being linear-transformation of V,W

for x, y being Element of V holds (T . x) - (T . y) = T . (x - y)

for T being linear-transformation of V,W

for x, y being Element of V holds (T . x) - (T . y) = T . (x - y)

proof end;

definition

let V, W be Z_Module;

let T be linear-transformation of V,W;

ex b_{1} being strict Submodule of V st [#] b_{1} = { u where u is Element of V : T . u = 0. W }

for b_{1}, b_{2} being strict Submodule of V st [#] b_{1} = { u where u is Element of V : T . u = 0. W } & [#] b_{2} = { u where u is Element of V : T . u = 0. W } holds

b_{1} = b_{2}
by ZMODUL01:45;

end;
let T be linear-transformation of V,W;

func ker T -> strict Submodule of V means :Def1: :: ZMODUL05:def 4

[#] it = { u where u is Element of V : T . u = 0. W } ;

existence [#] it = { u where u is Element of V : T . u = 0. W } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines ker ZMODUL05:def 4 :

for V, W being Z_Module

for T being linear-transformation of V,W

for b_{4} being strict Submodule of V holds

( b_{4} = ker T iff [#] b_{4} = { u where u is Element of V : T . u = 0. W } );

for V, W being Z_Module

for T being linear-transformation of V,W

for b

( b

theorem Th10: :: ZMODUL05:20

for V, W being Z_Module

for T being linear-transformation of V,W

for x being Element of V holds

( x in ker T iff T . x = 0. W )

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 end;

definition

let V, W be Z_Module;

let T be linear-transformation of V,W;

existence

ex b_{1} being strict Submodule of W st [#] b_{1} = T .: ([#] V)

for b_{1}, b_{2} being strict Submodule of W st [#] b_{1} = T .: ([#] V) & [#] b_{2} = T .: ([#] V) holds

b_{1} = b_{2}
by ZMODUL01:45;

end;
let T be linear-transformation of V,W;

existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def2 defines im ZMODUL05:def 5 :

for V, W being Z_Module

for T being linear-transformation of V,W

for b_{4} being strict Submodule of W holds

( b_{4} = im T iff [#] b_{4} = T .: ([#] V) );

for V, W being Z_Module

for T being linear-transformation of V,W

for b

( b

theorem :: ZMODUL05:22

for V, W being Z_Module

for T being linear-transformation of V,W

for X being Subset of V holds T .: X is Subset of (im T)

for T being linear-transformation of V,W

for X being Subset of V holds T .: X is Subset of (im T)

proof end;

theorem :: ZMODUL05:23

for V, W being Z_Module

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 )

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 end;

theorem :: ZMODUL05:24

for V, W being Z_Module

for T being linear-transformation of V,W

for x being Element of (ker T) holds T . x = 0. W

for T being linear-transformation of V,W

for x being Element of (ker T) holds T . x = 0. W

proof end;

theorem :: ZMODUL05:25

for V, W being Z_Module

for T being linear-transformation of V,W st T is one-to-one holds

ker T = (0). V

for T being linear-transformation of V,W st T is one-to-one holds

ker T = (0). V

proof end;

theorem Th17: :: ZMODUL05:27

for V, W being Z_Module

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

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 end;

theorem Th18: :: ZMODUL05:28

for V being Z_Module

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})

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 end;

:: combinations

:: Adjoining an element x to A that is already in its linear span

:: results in a linearly dependent set.

:: results in a linearly dependent set.

theorem Th21: :: ZMODUL05:32

for V being free finite-rank Z_Module

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

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 end;

registration

let V be free finite-rank Z_Module;

let W be Z_Module;

let T be linear-transformation of V,W;

correctness

coherence

( ker T is finite-rank & ker T is free );

;

end;
let W be Z_Module;

let T be linear-transformation of V,W;

correctness

coherence

( ker T is finite-rank & ker T is free );

;

theorem Th22: :: ZMODUL05:33

for W being Z_Module

for V being free finite-rank Z_Module

for A being Subset of V

for B being Basis of V

for T being linear-transformation of V,W st A is Basis of (ker T) & A c= B holds

T | (B \ A) is one-to-one

for V being free finite-rank Z_Module

for A being Subset of V

for B being Basis of V

for T being linear-transformation of V,W st A is Basis of (ker T) & A c= B holds

T | (B \ A) is one-to-one

proof end;

theorem :: ZMODUL05:34

for V being Z_Module

for A being Subset of V

for l being Linear_Combination of A

for x being Element of V

for a being Element of INT.Ring holds l +* (x,a) is Linear_Combination of A \/ {x}

for A being Subset of V

for l being Linear_Combination of A

for x being Element of V

for a being Element of INT.Ring holds l +* (x,a) is Linear_Combination of A \/ {x}

proof end;

registration
end;

:: Restricting a linear combination to a given set

definition

let V be Z_Module;

let l be Linear_Combination of V;

let A be Subset of V;

coherence

(l | A) +* ((A `) --> (0. INT.Ring)) is Linear_Combination of A

end;
let l be Linear_Combination of V;

let A be Subset of V;

coherence

(l | A) +* ((A `) --> (0. INT.Ring)) is Linear_Combination of A

proof end;

:: deftheorem defines ! ZMODUL05:def 6 :

for V being Z_Module

for l being Linear_Combination of V

for A being Subset of V holds l ! A = (l | A) +* ((A `) --> (0. INT.Ring));

for V being Z_Module

for l being Linear_Combination of V

for A being Subset of V holds l ! A = (l | A) +* ((A `) --> (0. INT.Ring));

Lm1: for V being Z_Module

for l being Linear_Combination of V

for X being Subset of V holds l .: X is finite

proof end;

theorem Th25: :: ZMODUL05:36

for V being Z_Module

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

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 end;

theorem Th26: :: ZMODUL05:37

for V being Z_Module

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. INT.Ring

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. INT.Ring

proof end;

theorem Th27: :: ZMODUL05:38

for V being Z_Module

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))

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 end;

registration

let V be Z_Module;

let l be Linear_Combination of V;

let X be Subset of V;

coherence

l .: X is finite by Lm1;

end;
let l be Linear_Combination of V;

let X be Subset of V;

coherence

l .: X is finite by Lm1;

theorem Th28: :: ZMODUL05:39

for V being Z_Module

for l being Linear_Combination of V

for X being Subset of V st X misses Carrier l holds

l .: X c= {(0. INT.Ring)}

for l being Linear_Combination of V

for X being Subset of V st X misses Carrier l holds

l .: X c= {(0. INT.Ring)}

proof end;

definition

let V, W be Z_Module;

let l be Linear_Combination of V;

let T be linear-transformation of V,W;

let w be Element of W;

coherence

l * (canFS ((T " {w}) /\ (Carrier l))) is the carrier of INT.Ring -valued FinSequence;

end;
let l be Linear_Combination of V;

let T be linear-transformation of V,W;

let w be Element of W;

func lCFST (l,T,w) -> the carrier of INT.Ring -valued FinSequence equals :: ZMODUL05:def 7

l * (canFS ((T " {w}) /\ (Carrier l)));

correctness l * (canFS ((T " {w}) /\ (Carrier l)));

coherence

l * (canFS ((T " {w}) /\ (Carrier l))) is the carrier of INT.Ring -valued FinSequence;

proof end;

:: deftheorem defines lCFST ZMODUL05:def 7 :

for V, W being Z_Module

for l being Linear_Combination of V

for T being linear-transformation of V,W

for w being Element of W holds lCFST (l,T,w) = l * (canFS ((T " {w}) /\ (Carrier l)));

for V, W being Z_Module

for l being Linear_Combination of V

for T being linear-transformation of V,W

for w being Element of W holds lCFST (l,T,w) = l * (canFS ((T " {w}) /\ (Carrier l)));

theorem ThTF3C0: :: ZMODUL05:40

for V, W being non empty set

for f being FinSequence

for l being Function of V,W st rng f c= V holds

( l * f is W -valued & l * f is FinSequence-like )

for f being FinSequence

for l being Function of V,W st rng f c= V holds

( l * f is W -valued & l * f is FinSequence-like )

proof end;

registration

let V, W be non empty set ;

let f be V -valued FinSequence;

let l be Function of V,W;

coherence

( l * f is W -valued & l * f is FinSequence-like )

end;
let f be V -valued FinSequence;

let l be Function of V,W;

coherence

( l * f is W -valued & l * f is FinSequence-like )

proof end;

ThTF3C1: for V, W being non empty set

for A being finite Subset of V

for l being Function of V,W holds

( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like )

proof end;

registration

let V, W be non empty set ;

let A be finite Subset of V;

let l be Function of V,W;

coherence

( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like ) by ThTF3C1;

end;
let A be finite Subset of V;

let l be Function of V,W;

coherence

( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like ) by ThTF3C1;

registration

let V be Z_Module;

let A be finite Subset of V;

let l be Linear_Combination of V;

coherence

( l * (canFS A) is the carrier of INT.Ring -valued & l * (canFS A) is FinSequence-like ) ;

end;
let A be finite Subset of V;

let l be Linear_Combination of V;

coherence

( l * (canFS A) is the carrier of INT.Ring -valued & l * (canFS A) is FinSequence-like ) ;

theorem ThTF3C3: :: ZMODUL05:41

for V, W being non empty set

for f, g being b_{1} -valued FinSequence

for l being Function of V,W holds l * (f ^ g) = (l * f) ^ (l * g)

for f, g being b

for l being Function of V,W holds l * (f ^ g) = (l * f) ^ (l * g)

proof end;

RF9: for R1, R2 being FinSequence of INT.Ring st R1,R2 are_fiberwise_equipotent holds

Sum R1 = Sum R2

proof end;

theorem ThTF3C2: :: ZMODUL05:42

for V being Z_Module

for A, B being finite Subset of V

for l being Linear_Combination of V

for l0, l1, l2 being FinSequence of INT.Ring st A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * (canFS A) & l2 = l * (canFS B) holds

Sum l0 = (Sum l1) + (Sum l2)

for A, B being finite Subset of V

for l being Linear_Combination of V

for l0, l1, l2 being FinSequence of INT.Ring st A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * (canFS A) & l2 = l * (canFS B) holds

Sum l0 = (Sum l1) + (Sum l2)

proof end;

theorem ThTF3C3: :: ZMODUL05:43

for V being Z_Module

for A being finite Subset of V

for l, l0 being Linear_Combination of V st l | (Carrier l0) = l0 | (Carrier l0) & Carrier l0 c= Carrier l & A c= Carrier l0 holds

Sum (l * (canFS A)) = Sum (l0 * (canFS A))

for A being finite Subset of V

for l, l0 being Linear_Combination of V st l | (Carrier l0) = l0 | (Carrier l0) & Carrier l0 c= Carrier l & A c= Carrier l0 holds

Sum (l * (canFS A)) = Sum (l0 * (canFS A))

proof end;

definition

let V, W be Z_Module;

let l be Linear_Combination of V;

let T be linear-transformation of V,W;

ex b_{1} being Linear_Combination of W st

( Carrier b_{1} c= T .: (Carrier l) & ( for w being Element of W holds b_{1} . w = Sum (lCFST (l,T,w)) ) )

for b_{1}, b_{2} being Linear_Combination of W st Carrier b_{1} c= T .: (Carrier l) & ( for w being Element of W holds b_{1} . w = Sum (lCFST (l,T,w)) ) & Carrier b_{2} c= T .: (Carrier l) & ( for w being Element of W holds b_{2} . w = Sum (lCFST (l,T,w)) ) holds

b_{1} = b_{2}

end;
let l be Linear_Combination of V;

let T be linear-transformation of V,W;

func T @* l -> Linear_Combination of W means :LDef5: :: ZMODUL05:def 8

( Carrier it c= T .: (Carrier l) & ( for w being Element of W holds it . w = Sum (lCFST (l,T,w)) ) );

existence ( Carrier it c= T .: (Carrier l) & ( for w being Element of W holds it . w = Sum (lCFST (l,T,w)) ) );

ex b

( Carrier b

proof end;

uniqueness for b

b

proof end;

:: deftheorem LDef5 defines @* ZMODUL05:def 8 :

for V, W being Z_Module

for l being Linear_Combination of V

for T being linear-transformation of V,W

for b_{5} being Linear_Combination of W holds

( b_{5} = T @* l iff ( Carrier b_{5} c= T .: (Carrier l) & ( for w being Element of W holds b_{5} . w = Sum (lCFST (l,T,w)) ) ) );

for V, W being Z_Module

for l being Linear_Combination of V

for T being linear-transformation of V,W

for b

( b

theorem LTh29: :: ZMODUL05:44

for V, W being Z_Module

for l being Linear_Combination of V

for T being linear-transformation of V,W holds T @* l is Linear_Combination of T .: (Carrier l)

for l being Linear_Combination of V

for T being linear-transformation of V,W holds T @* l is Linear_Combination of T .: (Carrier l)

proof end;

theorem ThTF3B2: :: ZMODUL05:45

for V, W being Z_Module

for T being linear-transformation of V,W

for s being VECTOR of W

for A being Subset of V

for l being Linear_Combination of A st ( for v being VECTOR of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

for T being linear-transformation of V,W

for s being VECTOR of W

for A being Subset of V

for l being Linear_Combination of A st ( for v being VECTOR of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

proof end;

theorem :: ZMODUL05:46

for V, W being Z_Module

for T being linear-transformation of V,W

for A being Subset of V

for l being Linear_Combination of A

for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l holds

T . (Sum l) = Sum Tl

for T being linear-transformation of V,W

for A being Subset of V

for l being Linear_Combination of A

for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l holds

T . (Sum l) = Sum Tl

proof end;

::: same as ZMODUL04:25

theorem Th31: :: ZMODUL05:47

for V being Z_Module

for l, m being Linear_Combination of V st Carrier l misses Carrier m holds

Carrier (l + m) = (Carrier l) \/ (Carrier m)

for l, m being Linear_Combination of V st Carrier l misses Carrier m holds

Carrier (l + m) = (Carrier l) \/ (Carrier m)

proof end;

theorem Th32: :: ZMODUL05:48

for V being Z_Module

for l, m being Linear_Combination of V st Carrier l misses Carrier m holds

Carrier (l - m) = (Carrier l) \/ (Carrier m)

for l, m being Linear_Combination of V st Carrier l misses Carrier m holds

Carrier (l - m) = (Carrier l) \/ (Carrier m)

proof end;

theorem :: ZMODUL05:49

for V being Z_Module

for A being Subset of V

for l1, l2 being Linear_Combination of A st Carrier l1 misses Carrier l2 holds

Carrier (l1 - l2) = (Carrier l1) \/ (Carrier l2)

for A being Subset of V

for l1, l2 being Linear_Combination of A st Carrier l1 misses Carrier l2 holds

Carrier (l1 - l2) = (Carrier l1) \/ (Carrier l2)

proof end;

theorem :: ZMODUL05:50

for V being free Z_Module

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)

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 end;

theorem :: ZMODUL05:51

for V, W being Z_Module

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 )

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 end;

theorem :: ZMODUL05:52

for V being Z_Module

for l being Linear_Combination of V

for X being Subset of V st X misses Carrier l & X <> {} holds

l .: X = {(0. INT.Ring)}

for l being Linear_Combination of V

for X being Subset of V st X misses Carrier l & X <> {} holds

l .: X = {(0. INT.Ring)}

proof end;

theorem Th36: :: ZMODUL05:53

for V, W being Z_Module

for l being Linear_Combination of V

for T being linear-transformation of V,W

for w being Element of W st w in Carrier (T @* l) holds

T " {w} meets Carrier l

for l being Linear_Combination of V

for T being linear-transformation of V,W

for w being Element of W st w in Carrier (T @* l) holds

T " {w} meets Carrier l

proof end;

theorem Th37: :: ZMODUL05:54

for V, W being Z_Module

for l being Linear_Combination of V

for T being linear-transformation of V,W

for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds

(T @* l) . (T . v) = l . v

for l being Linear_Combination of V

for T being linear-transformation of V,W

for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds

(T @* l) . (T . v) = l . v

proof end;

theorem Th38: :: ZMODUL05:55

for V, W being Z_Module

for l being Linear_Combination of V

for T being linear-transformation of V,W

for G being FinSequence of V st rng G = Carrier l & T | (Carrier l) is one-to-one holds

T * (l (#) G) = (T @* l) (#) (T * G)

for l being Linear_Combination of V

for T being linear-transformation of V,W

for G being FinSequence of V st rng G = Carrier l & T | (Carrier l) is one-to-one holds

T * (l (#) G) = (T @* l) (#) (T * G)

proof end;

theorem Th39: :: ZMODUL05:56

for V, W being Z_Module

for l being Linear_Combination of V

for T being linear-transformation of V,W st T | (Carrier l) is one-to-one holds

T .: (Carrier l) = Carrier (T @* l)

for l being Linear_Combination of V

for T being linear-transformation of V,W st T | (Carrier l) is one-to-one holds

T .: (Carrier l) = Carrier (T @* l)

proof end;

theorem :: ZMODUL05:57

for W being Z_Module

for V being free finite-rank Z_Module

for A being Subset of V

for B being Basis of V

for T being linear-transformation of V,W

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)

for V being free finite-rank Z_Module

for A being Subset of V

for B being Basis of V

for T being linear-transformation of V,W

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 end;

theorem :: ZMODUL05:58

for V being Z_Module

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 ) ;

for X being Subset of V st X is linearly-dependent holds

ex l being Linear_Combination of X st

( Carrier l <> {} & Sum l = 0. V ) ;

:: "Pulling back" a linear combination from the image space of a

:: linear transformation to the base space.

:: linear transformation to the base space.

definition

let V, W be Z_Module;

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 ;

(l * T) +* ((X `) --> (0. INT.Ring)) is Linear_Combination of X

end;
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 ;

func T # l -> Linear_Combination of X equals :Def6: :: ZMODUL05:def 9

(l * T) +* ((X `) --> (0. INT.Ring));

coherence (l * T) +* ((X `) --> (0. INT.Ring));

(l * T) +* ((X `) --> (0. INT.Ring)) is Linear_Combination of X

proof end;

:: deftheorem Def6 defines # ZMODUL05:def 9 :

for V, W being Z_Module

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) +* ((X `) --> (0. INT.Ring));

for V, W being Z_Module

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) +* ((X `) --> (0. INT.Ring));

theorem Th42: :: ZMODUL05:59

for V, W being Z_Module

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)

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 end;

:: # is a right inverse of @*

theorem :: ZMODUL05:60

for V, W being Z_Module

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

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 end;

::theorem

::: for X be finite Subset of INT st X = {}

::: holds Sum X = 0 by Def2,GR_CY_1:3,RELAT_1:38;

::theorem

:: for v be Element of INT holds Sum {v} = v

:: proof

:: let v be Element of INT;

:: A1: Sum <*v*> = v by RVSUM_1:73;

:: rng <*v*> = {v} & <*v*> is one-to-one by FINSEQ_1:39;

:: hence Sum {v} = v by A1,Def2;

:: end;

::theorem

:: for S, T being finite Subset of INT

:: st T misses S holds

:: Sum (T \/ S) = (Sum T) + (Sum S)

:: proof

:: let S, T be finite Subset of INT;

:: consider F being FinSequence of INT such that

:: A1: rng F = T \/ S and

:: A2: F is one-to-one & Sum (T \/ S) = Sum F by Def2;

:: consider G being FinSequence of INT such that

:: A3: rng G = T and

:: A4: G is one-to-one and

:: A5: Sum T = Sum G by Def2;

:: consider H being FinSequence of INT such that

:: A6: rng H = S and

:: A7: H is one-to-one and

:: A8: Sum S = Sum H by Def2;

:: set I = G ^ H;

:: reconsider G0 = G, H0 = H as real-valued FinSequence;

::: A9: Sum (G0 ^ H0) = Sum (G) + Sum (H) by RVSUM_1:75;

:: assume T misses S; then

:: A10: G ^ H is one-to-one by A3,A4,A6,A7,FINSEQ_3:91;

:: rng (G ^ H) = rng F by A1,A3,A6,FINSEQ_1:31;

:: hence Sum (T \/ S) = (Sum T) + (Sum S) by A2,A5,A8,A9,A10,RLVECT142;

:: end;