ZMODUL02: Quotient Module of $\mathbb Z$-module

:: Quotient Module of $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received May 7, 2012
:: Copyright (c) 2012-2013 Association of Mizar Users

definition

let V be Z_Module;
let a be Integer;

func a * V -> non empty Subset of V equals :: ZMODUL02:def 1
{ (a * v) where v is Element of V : verum } ;

correctness

proof end;

end;

:: deftheorem defines * ZMODUL02:def 1 :

definition

let V be Z_Module;
let a be Integer;

func Zero_ (a,V) -> Element of a * V equals :: ZMODUL02:def 2
0. V;

correctness

proof end;

end;

:: deftheorem defines Zero_ ZMODUL02:def 2 :

definition

let V be Z_Module;
let a be Integer;

func Add_ (a,V) -> Function of [:(a * V),(a * V):],(a * V) equals :: ZMODUL02:def 3
the addF of V | [:(a * V),(a * V):];

correctness

proof end;

end;

:: deftheorem defines Add_ ZMODUL02:def 3 :

definition

let V be Z_Module;
let a be Integer;

func Mult_ (a,V) -> Function of [:INT,(a * V):],(a * V) equals :: ZMODUL02:def 4
the Mult of V | [:INT,(a * V):];

correctness

proof end;

end;

:: deftheorem defines Mult_ ZMODUL02:def 4 :

definition

let V be Z_Module;
let a be Integer;

func a (*) V -> Submodule of V equals :: ZMODUL02:def 5
Z_ModuleStruct(# (a * V),(Zero_ (a,V)),(Add_ (a,V)),(Mult_ (a,V)) #);

coherence

proof end;

end;

:: deftheorem defines (*) ZMODUL02:def 5 :

definition

let V be Z_Module;
let W be Submodule of V;

func CosetSet (V,W) -> non empty Subset-Family of V equals :: ZMODUL02:def 6
{ A where A is Coset of W : verum } ;

correctness

proof end;

end;

:: deftheorem defines CosetSet ZMODUL02:def 6 :

definition

let V be Z_Module;
let W be Submodule of V;

func addCoset (V,W) -> BinOp of (CosetSet (V,W)) means :Def7: :: ZMODUL02:def 7
for A, B being Element of CosetSet (V,W)
for a, b being VECTOR of V st A = a + W & B = b + W holds
it . (A,B) = (a + b) + W;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines addCoset ZMODUL02:def 7 :

definition

let V be Z_Module;
let W be Submodule of V;

func zeroCoset (V,W) -> Element of CosetSet (V,W) equals :: ZMODUL02:def 8
the carrier of W;

coherence

proof end;

end;

:: deftheorem defines zeroCoset ZMODUL02:def 8 :

definition

let V be Z_Module;
let W be Submodule of V;

func lmultCoset (V,W) -> Function of [:INT,(CosetSet (V,W)):],(CosetSet (V,W)) means :Def9: :: ZMODUL02:def 9
for z being Integer
for A being Element of CosetSet (V,W)
for a being VECTOR of V st A = a + W holds
it . (z,A) = (z * a) + W;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines lmultCoset ZMODUL02:def 9 :

definition

let V be Z_Module;
let W be Submodule of V;

func Z_ModuleQuot (V,W) -> strict Z_Module means :Def10: :: ZMODUL02:def 10
( the carrier of it = CosetSet (V,W) & the addF of it = addCoset (V,W) & 0. it = zeroCoset (V,W) & the Mult of it = lmultCoset (V,W) );

existence

proof end;

uniqueness ;

end;

:: deftheorem Def10 defines Z_ModuleQuot ZMODUL02:def 10 :

theorem Th1: :: ZMODUL02:1

for p being Integer
for V being Z_Module
for W being Submodule of V
for x being VECTOR of (Z_ModuleQuot (V,W)) st W = p (*) V holds
p * x = 0. (Z_ModuleQuot (V,W))

proof end;

theorem Th2: :: ZMODUL02:2

for p, i being Integer
for V being Z_Module
for W being Submodule of V
for x being VECTOR of (Z_ModuleQuot (V,W)) st p <> 0 & W = p (*) V holds
i * x = (i mod p) * x

proof end;

theorem :: ZMODUL02:3

for p, q being Integer
for V being Z_Module
for W being Submodule of V
for v being VECTOR of V st W = p (*) V & p > 1 & q > 1 & p,q are_coprime & q * v = 0. V holds
v + W = 0. (Z_ModuleQuot (V,W))

proof end;

definition

let p be Prime;
let V be Z_Module;

func Mult_Mod_pV (V,p) -> Function of [: the carrier of (GF p), the carrier of (Z_ModuleQuot (V,(p (*) V))):], the carrier of (Z_ModuleQuot (V,(p (*) V))) means :Def11: :: ZMODUL02:def 11
for a being Element of (GF p)
for i being Integer
for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds
it . (a,x) = (i mod p) * x;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines Mult_Mod_pV ZMODUL02:def 11 :

definition

let p be Prime;
let V be Z_Module;

func Z_MQ_VectSp (V,p) -> non empty strict VectSpStr over GF p equals :: ZMODUL02:def 12
VectSpStr(# the carrier of (Z_ModuleQuot (V,(p (*) V))), the addF of (Z_ModuleQuot (V,(p (*) V))), the ZeroF of (Z_ModuleQuot (V,(p (*) V))),(Mult_Mod_pV (V,p)) #);

coherence ;

end;

:: deftheorem defines Z_MQ_VectSp ZMODUL02:def 12 :

registration

let p be Prime;
let V be Z_Module;

cluster Z_MQ_VectSp (V,p) -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence

proof end;

end;

definition

let p be Prime;
let V be Z_Module;
let v be VECTOR of V;

func ZMtoMQV (V,p,v) -> Vector of (Z_MQ_VectSp (V,p)) equals :: ZMODUL02:def 13
v + (p (*) V);

correctness

proof end;

end;

:: deftheorem defines ZMtoMQV ZMODUL02:def 13 :

definition

let X be Z_Module;

func Mult_INT* X -> Function of [: the carrier of INT.Ring, the carrier of X:], the carrier of X equals :: ZMODUL02:def 14
the Mult of X;

correctness ;

end;

:: deftheorem defines Mult_INT* ZMODUL02:def 14 :

definition

let X be Z_Module;

func modetrans X -> non empty strict VectSpStr over INT.Ring equals :: ZMODUL02:def 15
VectSpStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #);

coherence ;

end;

:: deftheorem defines modetrans ZMODUL02:def 15 :

registration

let X be Z_Module;

cluster modetrans X -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence

proof end;

end;

definition

let X be LeftMod of INT.Ring ;

func Mult_INT* X -> Function of [:INT, the carrier of X:], the carrier of X equals :: ZMODUL02:def 16
the lmult of X;

coherence ;

end;

:: deftheorem defines Mult_INT* ZMODUL02:def 16 :

definition

let X be LeftMod of INT.Ring ;

func modetrans X -> non empty strict Z_ModuleStruct equals :: ZMODUL02:def 17
Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #);

correctness ;

end;

:: deftheorem defines modetrans ZMODUL02:def 17 :

registration

let X be LeftMod of INT.Ring ;

cluster modetrans X -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence

proof end;

end;

theorem :: ZMODUL02:4

for X being Z_Module
for v, w being Element of X
for v1, w1 being Element of (modetrans X) st v = v1 & w = w1 holds
( v + w = v1 + w1 & v - w = v1 - w1 )

proof end;

theorem :: ZMODUL02:5

for X being Z_Module
for v being Element of X
for v1 being Element of (modetrans X)
for a being Integer
for a1 being Element of INT.Ring st v = v1 & a = a1 holds
a * v = a1 * v1 ;

theorem :: ZMODUL02:6

for X being LeftMod of INT.Ring
for v, w being Element of X
for v1, w1 being Element of (modetrans X) st v = v1 & w = w1 holds
( v + w = v1 + w1 & v - w = v1 - w1 )

proof end;

theorem :: ZMODUL02:7

for X being LeftMod of INT.Ring
for v being Element of X
for v1 being Element of (modetrans X)
for a being Element of INT.Ring
for a1 being Integer st v = v1 & a = a1 holds
a * v = a1 * v1 ;

definition

let V be non empty ZeroStr ;

mode Z_Linear_Combination of V -> Element of Funcs ( the carrier of V,INT) means :Def18: :: ZMODUL02:def 18
ex T being finite Subset of V st
for v being Element of V st not v in T holds
it . v = 0 ;

existence

proof end;

end;

:: deftheorem Def18 defines Z_Linear_Combination ZMODUL02:def 18 :

definition

let V be non empty addLoopStr ;
let L be Z_Linear_Combination of V;

func Carrier L -> finite Subset of V equals :: ZMODUL02:def 19
{ v where v is Element of V : L . v <> 0 } ;

coherence

proof end;

end;

:: deftheorem defines Carrier ZMODUL02:def 19 :

theorem :: ZMODUL02:8

for V being non empty addLoopStr
for L being Z_Linear_Combination of V
for v being Element of V holds
( L . v = 0 iff not v in Carrier L )

proof end;

definition

let V be non empty addLoopStr ;

func Z_ZeroLC V -> Z_Linear_Combination of V means :Def20: :: ZMODUL02:def 20
Carrier it = {} ;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines Z_ZeroLC ZMODUL02:def 20 :

theorem Th9: :: ZMODUL02:9

for V being non empty addLoopStr
for v being Element of V holds (Z_ZeroLC V) . v = 0

proof end;

definition

let V be non empty addLoopStr ;
let A be Subset of V;

mode Z_Linear_Combination of A -> Z_Linear_Combination of V means :Def21: :: ZMODUL02:def 21
Carrier it c= A;

existence

proof end;

end;

:: deftheorem Def21 defines Z_Linear_Combination ZMODUL02:def 21 :

theorem Th10: :: ZMODUL02:10

for V being Z_Module
for A, B being Subset of V
for l being Z_Linear_Combination of A st A c= B holds
l is Z_Linear_Combination of B

proof end;

theorem Th11: :: ZMODUL02:11

for V being Z_Module
for A being Subset of V holds Z_ZeroLC V is Z_Linear_Combination of A

proof end;

theorem Th12: :: ZMODUL02:12

for V being Z_Module
for l being Z_Linear_Combination of {} the carrier of V holds l = Z_ZeroLC V

proof end;

definition

let V be Z_Module;
let F be FinSequence of V;
let f be Function of the carrier of V,INT;

func f (#) F -> FinSequence of V means :Def22: :: ZMODUL02:def 22
( len it = len F & ( for i being Element of NAT st i in dom it holds
it . i = (f . (F /. i)) * (F /. i) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines (#) ZMODUL02:def 22 :

theorem Th13: :: ZMODUL02:13

for V being Z_Module
for v being VECTOR of V
for F being FinSequence of V
for f being Function of the carrier of V,INT
for i being Element of NAT st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v

proof end;

theorem :: ZMODUL02:14

for V being Z_Module
for f being Function of the carrier of V,INT holds f (#) (<*> the carrier of V) = <*> the carrier of V

proof end;

theorem Th15: :: ZMODUL02:15

for V being Z_Module
for v being VECTOR of V
for f being Function of the carrier of V,INT holds f (#) <*v*> = <*((f . v) * v)*>

proof end;

theorem Th16: :: ZMODUL02:16

for V being Z_Module
for v1, v2 being VECTOR of V
for f being Function of the carrier of V,INT holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>

proof end;

theorem :: ZMODUL02:17

for V being Z_Module
for v1, v2, v3 being VECTOR of V
for f being Function of the carrier of V,INT holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>

proof end;

definition

let V be Z_Module;
let L be Z_Linear_Combination of V;

func Sum L -> Element of V means :Def23: :: ZMODUL02:def 23
ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def23 defines Sum ZMODUL02:def 23 :

Lm1: for V being Z_Module holds Sum (Z_ZeroLC V) = 0. V

proof end;

theorem :: ZMODUL02:18

for V being Z_Module
for A being Subset of V holds
( ( A <> {} & A is linearly-closed ) iff for l being Z_Linear_Combination of A holds Sum l in A )

proof end;

theorem :: ZMODUL02:19

for V being Z_Module holds Sum (Z_ZeroLC V) = 0. V by Lm1;

theorem Th20: :: ZMODUL02:20

for V being Z_Module
for l being Z_Linear_Combination of {} the carrier of V holds Sum l = 0. V

proof end;

theorem Th21: :: ZMODUL02:21

for V being Z_Module
for v being VECTOR of V
for l being Z_Linear_Combination of {v} holds Sum l = (l . v) * v

proof end;

theorem Th22: :: ZMODUL02:22

for V being Z_Module
for v1, v2 being VECTOR of V st v1 <> v2 holds
for l being Z_Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)

proof end;

theorem :: ZMODUL02:23

for V being Z_Module
for L being Z_Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V

proof end;

theorem Th24: :: ZMODUL02:24

for V being Z_Module
for v being VECTOR of V
for L being Z_Linear_Combination of V st Carrier L = {v} holds
Sum L = (L . v) * v

proof end;

theorem :: ZMODUL02:25

for V being Z_Module
for L being Z_Linear_Combination of V
for v1, v2 being VECTOR of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = ((L . v1) * v1) + ((L . v2) * v2)

proof end;

definition

let V be non empty addLoopStr ;
let L1, L2 be Z_Linear_Combination of V;

:: original: =
redefine pred L1 = L2 means :: ZMODUL02:def 24
for v being Element of V holds L1 . v = L2 . v;

compatibility ;

end;

:: deftheorem defines = ZMODUL02:def 24 :

definition

let V be non empty addLoopStr ;
let L1, L2 be Z_Linear_Combination of V;

:: original: +
redefine func L1 + L2 -> Z_Linear_Combination of V means :Def25: :: ZMODUL02:def 25
for v being Element of V holds it . v = (L1 . v) + (L2 . v);

coherence

proof end;

compatibility

proof end;

commutativity ;

end;

:: deftheorem Def25 defines + ZMODUL02:def 25 :

theorem Th26: :: ZMODUL02:26

for V being Z_Module
for L1, L2 being Z_Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)

proof end;

theorem Th27: :: ZMODUL02:27

for V being Z_Module
for L1, L2 being Z_Linear_Combination of V
for A being Subset of V st L1 is Z_Linear_Combination of A & L2 is Z_Linear_Combination of A holds
L1 + L2 is Z_Linear_Combination of A

proof end;

theorem Th28: :: ZMODUL02:28

for V being Z_Module
for L1, L2, L3 being Z_Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3

proof end;

registration

let V be Z_Module;
let L be Z_Linear_Combination of V;

reduce L + (Z_ZeroLC V) to L;

reducibility

proof end;

end;

definition

let V be Z_Module;
let a be Integer;
let L be Z_Linear_Combination of V;

func a * L -> Z_Linear_Combination of V means :Def26: :: ZMODUL02:def 26
for v being VECTOR of V holds it . v = a * (L . v);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def26 defines * ZMODUL02:def 26 :

theorem Th29: :: ZMODUL02:29

for V being Z_Module
for L being Z_Linear_Combination of V
for a being Integer st a <> 0 holds
Carrier (a * L) = Carrier L

proof end;

theorem Th30: :: ZMODUL02:30

for V being Z_Module
for L being Z_Linear_Combination of V holds 0 * L = Z_ZeroLC V

proof end;

theorem Th31: :: ZMODUL02:31

for V being Z_Module
for L being Z_Linear_Combination of V
for a being Integer
for A being Subset of V st L is Z_Linear_Combination of A holds
a * L is Z_Linear_Combination of A

proof end;

theorem Th32: :: ZMODUL02:32

for V being Z_Module
for L being Z_Linear_Combination of V
for a, b being Integer holds (a + b) * L = (a * L) + (b * L)

proof end;

theorem Th33: :: ZMODUL02:33

for V being Z_Module
for L1, L2 being Z_Linear_Combination of V
for a being Integer holds a * (L1 + L2) = (a * L1) + (a * L2)

proof end;

theorem Th34: :: ZMODUL02:34

for V being Z_Module
for L being Z_Linear_Combination of V
for a, b being Integer holds a * (b * L) = (a * b) * L

proof end;

registration

let V be Z_Module;
let L be Z_Linear_Combination of V;

reduce 1 * L to L;

reducibility

proof end;

end;

definition

let V be Z_Module;
let L be Z_Linear_Combination of V;

func - L -> Z_Linear_Combination of V equals :: ZMODUL02:def 27
(- 1) * L;

coherence ;
involutiveness

proof end;

end;

:: deftheorem defines - ZMODUL02:def 27 :

theorem Th35: :: ZMODUL02:35

for V being Z_Module
for v being VECTOR of V
for L being Z_Linear_Combination of V holds (- L) . v = - (L . v)

proof end;

theorem :: ZMODUL02:36

for V being Z_Module
for L1, L2 being Z_Linear_Combination of V st L1 + L2 = Z_ZeroLC V holds
L2 = - L1

proof end;

theorem :: ZMODUL02:37

for V being Z_Module
for L being Z_Linear_Combination of V holds Carrier (- L) = Carrier L by Th29;

theorem :: ZMODUL02:38

for V being Z_Module
for L being Z_Linear_Combination of V
for A being Subset of V st L is Z_Linear_Combination of A holds
- L is Z_Linear_Combination of A by Th31;

definition

let V be Z_Module;
let L1, L2 be Z_Linear_Combination of V;

func L1 - L2 -> Z_Linear_Combination of V equals :: ZMODUL02:def 28
L1 + (- L2);

correctness ;

end;

:: deftheorem defines - ZMODUL02:def 28 :

theorem Th39: :: ZMODUL02:39

for V being Z_Module
for v being VECTOR of V
for L1, L2 being Z_Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)

proof end;

theorem :: ZMODUL02:40

for V being Z_Module
for L1, L2 being Z_Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)

proof end;

theorem :: ZMODUL02:41

for V being Z_Module
for L1, L2 being Z_Linear_Combination of V
for A being Subset of V st L1 is Z_Linear_Combination of A & L2 is Z_Linear_Combination of A holds
L1 - L2 is Z_Linear_Combination of A

proof end;

theorem Th42: :: ZMODUL02:42

for V being Z_Module
for L being Z_Linear_Combination of V holds L - L = Z_ZeroLC V

proof end;

definition

let V be Z_Module;

func LinComb V -> set means :Def29: :: ZMODUL02:def 29
for x being set holds
( x in it iff x is Z_Linear_Combination of V );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def29 defines LinComb ZMODUL02:def 29 :

registration

let V be Z_Module;

cluster LinComb V -> non empty ;

coherence

proof end;

end;

definition

let V be Z_Module;
let e be Element of LinComb V;

func @ e -> Z_Linear_Combination of V equals :: ZMODUL02:def 30
e;

coherence by Def29;

end;

:: deftheorem defines @ ZMODUL02:def 30 :

definition

let V be Z_Module;
let L be Z_Linear_Combination of V;

func @ L -> Element of LinComb V equals :: ZMODUL02:def 31
L;

coherence by Def29;

end;

:: deftheorem defines @ ZMODUL02:def 31 :

definition

let V be Z_Module;

func LCAdd V -> BinOp of (LinComb V) means :Def32: :: ZMODUL02:def 32
for e1, e2 being Element of LinComb V holds it . (e1,e2) = (@ e1) + (@ e2);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def32 defines LCAdd ZMODUL02:def 32 :

definition

let V be Z_Module;

func LCMult V -> Function of [:INT,(LinComb V):],(LinComb V) means :Def33: :: ZMODUL02:def 33
for a being Integer
for e being Element of LinComb V holds it . [a,e] = a * (@ e);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def33 defines LCMult ZMODUL02:def 33 :

definition

let V be Z_Module;

func LC_Z_Module V -> Z_ModuleStruct equals :: ZMODUL02:def 34
Z_ModuleStruct(# (LinComb V),(@ (Z_ZeroLC V)),(LCAdd V),(LCMult V) #);

coherence ;

end;

:: deftheorem defines LC_Z_Module ZMODUL02:def 34 :

registration

let V be Z_Module;

cluster LC_Z_Module V -> non empty strict ;

coherence ;

end;

registration

let V be Z_Module;

cluster LC_Z_Module V -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence

proof end;

end;

theorem :: ZMODUL02:43

for V being Z_Module holds the carrier of (LC_Z_Module V) = LinComb V ;

theorem :: ZMODUL02:44

for V being Z_Module holds 0. (LC_Z_Module V) = Z_ZeroLC V ;

theorem :: ZMODUL02:45

for V being Z_Module holds the addF of (LC_Z_Module V) = LCAdd V ;

theorem :: ZMODUL02:46

for V being Z_Module holds the Mult of (LC_Z_Module V) = LCMult V ;

theorem Th47: :: ZMODUL02:47

for V being Z_Module
for L1, L2 being Z_Linear_Combination of V holds (vector ((LC_Z_Module V),L1)) + (vector ((LC_Z_Module V),L2)) = L1 + L2

proof end;

theorem Th48: :: ZMODUL02:48

for V being Z_Module
for L being Z_Linear_Combination of V
for a being Integer holds a * (vector ((LC_Z_Module V),L)) = a * L

proof end;

theorem Th49: :: ZMODUL02:49

for V being Z_Module
for L being Z_Linear_Combination of V holds - (vector ((LC_Z_Module V),L)) = - L

proof end;

theorem :: ZMODUL02:50

for V being Z_Module
for L1, L2 being Z_Linear_Combination of V holds (vector ((LC_Z_Module V),L1)) - (vector ((LC_Z_Module V),L2)) = L1 - L2

proof end;

definition

let V be Z_Module;
let A be Subset of V;

func LC_Z_Module A -> strict Submodule of LC_Z_Module V means :: ZMODUL02:def 35
the carrier of it = { l where l is Z_Linear_Combination of A : verum } ;

existence

proof end;

uniqueness by ZMODUL01:45;

end;

:: deftheorem defines LC_Z_Module ZMODUL02:def 35 :

Lm2: for V being Z_Module
for F, G being FinSequence of the carrier of V
for f being Function of the carrier of V,INT holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)

proof end;

theorem :: ZMODUL02:51

for V being Z_Module
for F, G being FinSequence of the carrier of V
for f being Function of the carrier of V,INT holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G) by Lm2;

theorem Th52: :: ZMODUL02:52

for V being Z_Module
for L1, L2 being Z_Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)

proof end;

theorem Th53: :: ZMODUL02:53

for V being Z_Module
for a being Integer
for L being Z_Linear_Combination of V holds Sum (a * L) = a * (Sum L)

proof end;

theorem Th54: :: ZMODUL02:54

for V being Z_Module
for L being Z_Linear_Combination of V holds Sum (- L) = - (Sum L)

proof end;

theorem :: ZMODUL02:55

for V being Z_Module
for L1, L2 being Z_Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)

proof end;

definition

let V be Z_Module;
let A be Subset of V;

attr A is linearly-independent means :: ZMODUL02:def 36
for l being Z_Linear_Combination of A st Sum l = 0. V holds
Carrier l = {} ;

end;

:: deftheorem defines linearly-independent ZMODUL02:def 36 :

notation

let V be Z_Module;
let A be Subset of V;
antonym linearly-dependent A for linearly-independent ;

end;

theorem :: ZMODUL02:56

for V being Z_Module
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent

proof end;

theorem Th57: :: ZMODUL02:57

for V being Z_Module
for A being Subset of V st A is linearly-independent holds
not 0. V in A

proof end;

theorem Th58: :: ZMODUL02:58

for V being Z_Module holds {} the carrier of V is linearly-independent

proof end;

registration

let V be Z_Module;

cluster linearly-independent for Element of bool the carrier of V;

existence

proof end;

end;

theorem :: ZMODUL02:59

for V being Z_Module
for v being VECTOR of V st V is Mult-cancelable holds
( {v} is linearly-independent iff v <> 0. V )

proof end;

registration

let V be Z_Module;

cluster {(0. V)} -> linearly-dependent for Subset of V;

coherence

proof end;

end;

theorem Th60: :: ZMODUL02:60

for V being Z_Module
for v1, v2 being VECTOR of V st {v1,v2} is linearly-independent holds
v1 <> 0. V

proof end;

theorem :: ZMODUL02:61

for V being Z_Module
for v being VECTOR of V holds {v,(0. V)} is linearly-dependent by Th60;

theorem Th62: :: ZMODUL02:62

for V being Z_Module
for v1, v2 being VECTOR of V st V is Mult-cancelable holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a, b being Integer st b <> 0 holds
b * v1 <> a * v2 ) ) )

proof end;

theorem :: ZMODUL02:63

for V being Z_Module
for v1, v2 being VECTOR of V st V is Mult-cancelable holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Integer st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) )

proof end;

definition

let V be Z_Module;
let A be Subset of V;

func Lin A -> strict Submodule of V means :Def37: :: ZMODUL02:def 37
the carrier of it = { (Sum l) where l is Z_Linear_Combination of A : verum } ;

existence

proof end;

uniqueness by ZMODUL01:45;

end;

:: deftheorem Def37 defines Lin ZMODUL02:def 37 :

theorem Th64: :: ZMODUL02:64

for x being set
for V being Z_Module
for A being Subset of V holds
( x in Lin A iff ex l being Z_Linear_Combination of A st x = Sum l )

proof end;

theorem Th65: :: ZMODUL02:65

for x being set
for V being Z_Module
for A being Subset of V st x in A holds
x in Lin A

proof end;

theorem Th66: :: ZMODUL02:66

for V being Z_Module
for x being object holds
( x in (0). V iff x = 0. V )

proof end;

theorem :: ZMODUL02:67

for V being Z_Module holds Lin ({} the carrier of V) = (0). V

proof end;

theorem :: ZMODUL02:68

for V being Z_Module
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )

proof end;

theorem :: ZMODUL02:69

for V being strict Z_Module
for A being Subset of V st A = the carrier of V holds
Lin A = V

proof end;

Lm3: for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 & W1 is Submodule of W3 holds
W1 is Submodule of W2 /\ W3

proof end;

Lm4: for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 is Submodule of W3 & W2 is Submodule of W3 holds
W1 + W2 is Submodule of W3

proof end;

theorem Th70: :: ZMODUL02:70

for V being Z_Module
for A, B being Subset of V st A c= B holds
Lin A is Submodule of Lin B

proof end;

theorem :: ZMODUL02:71

for V being strict Z_Module
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V

proof end;

theorem :: ZMODUL02:72

for V being Z_Module
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)

proof end;

theorem :: ZMODUL02:73

for V being Z_Module
for A, B being Subset of V holds Lin (A /\ B) is Submodule of (Lin A) /\ (Lin B)

proof end;

theorem :: ZMODUL02:74

for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 is Submodule of W3 holds
W1 /\ W2 is Submodule of W3

proof end;

theorem :: ZMODUL02:75

for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 & W1 is Submodule of W3 holds
W1 is Submodule of W2 /\ W3 by Lm3;

theorem :: ZMODUL02:76

for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 is Submodule of W3 & W2 is Submodule of W3 holds
W1 + W2 is Submodule of W3 by Lm4;

theorem :: ZMODUL02:77

for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
W1 is Submodule of W2 + W3

proof end;