:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received May 7, 2012

:: Copyright (c) 2012-2014 Association of Mizar Users

definition

let V be Z_Module;

let a be Element of INT.Ring;

coherence

{ (a * v) where v is Element of V : verum } is non empty Subset of V;

end;
let a be Element of INT.Ring;

func a * V -> non empty Subset of V equals :: ZMODUL02:def 1

{ (a * v) where v is Element of V : verum } ;

correctness { (a * v) where v is Element of V : verum } ;

coherence

{ (a * v) where v is Element of V : verum } is non empty Subset of V;

proof end;

:: deftheorem defines * ZMODUL02:def 1 :

for V being Z_Module

for a being Element of INT.Ring holds a * V = { (a * v) where v is Element of V : verum } ;

for V being Z_Module

for a being Element of INT.Ring holds a * V = { (a * v) where v is Element of V : verum } ;

definition

let V be Z_Module;

let a be Element of INT.Ring;

correctness

coherence

0. V is Element of a * V;

end;
let a be Element of INT.Ring;

correctness

coherence

0. V is Element of a * V;

proof end;

:: deftheorem defines Zero_ ZMODUL02:def 2 :

for V being Z_Module

for a being Element of INT.Ring holds Zero_ (a,V) = 0. V;

for V being Z_Module

for a being Element of INT.Ring holds Zero_ (a,V) = 0. V;

definition

let V be Z_Module;

let a be Element of INT.Ring;

coherence

the addF of V | [:(a * V),(a * V):] is Function of [:(a * V),(a * V):],(a * V);

end;
let a be Element of INT.Ring;

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 the addF of V | [:(a * V),(a * V):];

coherence

the addF of V | [:(a * V),(a * V):] is Function of [:(a * V),(a * V):],(a * V);

proof end;

:: deftheorem defines Add_ ZMODUL02:def 3 :

for V being Z_Module

for a being Element of INT.Ring holds Add_ (a,V) = the addF of V | [:(a * V),(a * V):];

for V being Z_Module

for a being Element of INT.Ring holds Add_ (a,V) = the addF of V | [:(a * V),(a * V):];

definition

let V be Z_Module;

let a be Element of INT.Ring;

coherence

the lmult of V | [:INT,(a * V):] is Function of [: the carrier of INT.Ring,(a * V):],(a * V);

end;
let a be Element of INT.Ring;

func Mult_ (a,V) -> Function of [: the carrier of INT.Ring,(a * V):],(a * V) equals :: ZMODUL02:def 4

the lmult of V | [:INT,(a * V):];

correctness the lmult of V | [:INT,(a * V):];

coherence

the lmult of V | [:INT,(a * V):] is Function of [: the carrier of INT.Ring,(a * V):],(a * V);

proof end;

:: deftheorem defines Mult_ ZMODUL02:def 4 :

for V being Z_Module

for a being Element of INT.Ring holds Mult_ (a,V) = the lmult of V | [:INT,(a * V):];

for V being Z_Module

for a being Element of INT.Ring holds Mult_ (a,V) = the lmult of V | [:INT,(a * V):];

definition

let V be Z_Module;

let a be Element of INT.Ring;

ModuleStr(# (a * V),(Add_ (a,V)),(Zero_ (a,V)),(Mult_ (a,V)) #) is Submodule of V

end;
let a be Element of INT.Ring;

func a (*) V -> Submodule of V equals :: ZMODUL02:def 5

ModuleStr(# (a * V),(Add_ (a,V)),(Zero_ (a,V)),(Mult_ (a,V)) #);

coherence ModuleStr(# (a * V),(Add_ (a,V)),(Zero_ (a,V)),(Mult_ (a,V)) #);

ModuleStr(# (a * V),(Add_ (a,V)),(Zero_ (a,V)),(Mult_ (a,V)) #) is Submodule of V

proof end;

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

for V being Z_Module

for a being Element of INT.Ring holds a (*) V = ModuleStr(# (a * V),(Add_ (a,V)),(Zero_ (a,V)),(Mult_ (a,V)) #);

for V being Z_Module

for a being Element of INT.Ring holds a (*) V = ModuleStr(# (a * V),(Add_ (a,V)),(Zero_ (a,V)),(Mult_ (a,V)) #);

definition

let V be Z_Module;

let W be Submodule of V;

coherence

{ A where A is Coset of W : verum } is non empty Subset-Family of V;

end;
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 { A where A is Coset of W : verum } ;

coherence

{ A where A is Coset of W : verum } is non empty Subset-Family of V;

proof end;

:: deftheorem defines CosetSet ZMODUL02:def 6 :

for V being Z_Module

for W being Submodule of V holds CosetSet (V,W) = { A where A is Coset of W : verum } ;

for V being Z_Module

for W being Submodule of V holds CosetSet (V,W) = { A where A is Coset of W : verum } ;

definition

let V be Z_Module;

let W be Submodule of V;

ex b_{1} being BinOp of (CosetSet (V,W)) st

for A, B being Element of CosetSet (V,W)

for a, b being VECTOR of V st A = a + W & B = b + W holds

b_{1} . (A,B) = (a + b) + W

for b_{1}, b_{2} being BinOp of (CosetSet (V,W)) st ( for A, B being Element of CosetSet (V,W)

for a, b being VECTOR of V st A = a + W & B = b + W holds

b_{1} . (A,B) = (a + b) + W ) & ( for A, B being Element of CosetSet (V,W)

for a, b being VECTOR of V st A = a + W & B = b + W holds

b_{2} . (A,B) = (a + b) + W ) holds

b_{1} = b_{2}

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

ex b

for A, B being Element of CosetSet (V,W)

for a, b being VECTOR of V st A = a + W & B = b + W holds

b

proof end;

uniqueness for b

for a, b being VECTOR of V st A = a + W & B = b + W holds

b

for a, b being VECTOR of V st A = a + W & B = b + W holds

b

b

proof end;

:: deftheorem Def7 defines addCoset ZMODUL02:def 7 :

for V being Z_Module

for W being Submodule of V

for b_{3} being BinOp of (CosetSet (V,W)) holds

( b_{3} = addCoset (V,W) iff for A, B being Element of CosetSet (V,W)

for a, b being VECTOR of V st A = a + W & B = b + W holds

b_{3} . (A,B) = (a + b) + W );

for V being Z_Module

for W being Submodule of V

for b

( b

for a, b being VECTOR of V st A = a + W & B = b + W holds

b

definition

let V be Z_Module;

let W be Submodule of V;

coherence

the carrier of W is Element of CosetSet (V,W)

end;
let W be Submodule of V;

coherence

the carrier of W is Element of CosetSet (V,W)

proof end;

:: deftheorem defines zeroCoset ZMODUL02:def 8 :

for V being Z_Module

for W being Submodule of V holds zeroCoset (V,W) = the carrier of W;

for V being Z_Module

for W being Submodule of V holds zeroCoset (V,W) = the carrier of W;

definition

let V be Z_Module;

let W be Submodule of V;

ex b_{1} being Function of [: the carrier of INT.Ring,(CosetSet (V,W)):],(CosetSet (V,W)) st

for z being Element of INT.Ring

for A being Element of CosetSet (V,W)

for a being VECTOR of V st A = a + W holds

b_{1} . (z,A) = (z * a) + W

for b_{1}, b_{2} being Function of [: the carrier of INT.Ring,(CosetSet (V,W)):],(CosetSet (V,W)) st ( for z being Element of INT.Ring

for A being Element of CosetSet (V,W)

for a being VECTOR of V st A = a + W holds

b_{1} . (z,A) = (z * a) + W ) & ( for z being Element of INT.Ring

for A being Element of CosetSet (V,W)

for a being VECTOR of V st A = a + W holds

b_{2} . (z,A) = (z * a) + W ) holds

b_{1} = b_{2}

end;
let W be Submodule of V;

func lmultCoset (V,W) -> Function of [: the carrier of INT.Ring,(CosetSet (V,W)):],(CosetSet (V,W)) means :Def9: :: ZMODUL02:def 9

for z being Element of INT.Ring

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 for z being Element of INT.Ring

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;

ex b

for z being Element of INT.Ring

for A being Element of CosetSet (V,W)

for a being VECTOR of V st A = a + W holds

b

proof end;

uniqueness for b

for A being Element of CosetSet (V,W)

for a being VECTOR of V st A = a + W holds

b

for A being Element of CosetSet (V,W)

for a being VECTOR of V st A = a + W holds

b

b

proof end;

:: deftheorem Def9 defines lmultCoset ZMODUL02:def 9 :

for V being Z_Module

for W being Submodule of V

for b_{3} being Function of [: the carrier of INT.Ring,(CosetSet (V,W)):],(CosetSet (V,W)) holds

( b_{3} = lmultCoset (V,W) iff for z being Element of INT.Ring

for A being Element of CosetSet (V,W)

for a being VECTOR of V st A = a + W holds

b_{3} . (z,A) = (z * a) + W );

for V being Z_Module

for W being Submodule of V

for b

( b

for A being Element of CosetSet (V,W)

for a being VECTOR of V st A = a + W holds

b

definition

let V be Z_Module;

let W be Submodule of V;

ex b_{1} being strict Z_Module st

( the carrier of b_{1} = CosetSet (V,W) & the addF of b_{1} = addCoset (V,W) & 0. b_{1} = zeroCoset (V,W) & the lmult of b_{1} = lmultCoset (V,W) )

for b_{1}, b_{2} being strict Z_Module st the carrier of b_{1} = CosetSet (V,W) & the addF of b_{1} = addCoset (V,W) & 0. b_{1} = zeroCoset (V,W) & the lmult of b_{1} = lmultCoset (V,W) & the carrier of b_{2} = CosetSet (V,W) & the addF of b_{2} = addCoset (V,W) & 0. b_{2} = zeroCoset (V,W) & the lmult of b_{2} = lmultCoset (V,W) holds

b_{1} = b_{2}
;

end;
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 lmult of it = lmultCoset (V,W) );

existence ( the carrier of it = CosetSet (V,W) & the addF of it = addCoset (V,W) & 0. it = zeroCoset (V,W) & the lmult of it = lmultCoset (V,W) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines Z_ModuleQuot ZMODUL02:def 10 :

for V being Z_Module

for W being Submodule of V

for b_{3} being strict Z_Module holds

( b_{3} = Z_ModuleQuot (V,W) iff ( the carrier of b_{3} = CosetSet (V,W) & the addF of b_{3} = addCoset (V,W) & 0. b_{3} = zeroCoset (V,W) & the lmult of b_{3} = lmultCoset (V,W) ) );

for V being Z_Module

for W being Submodule of V

for b

( b

theorem Th1: :: ZMODUL02:1

for p being Element of INT.Ring

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

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

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

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;

Lem1: for i being Integer holds i in the carrier of INT.Ring

proof end;

theorem :: ZMODUL02:3

for p, q being Element of INT.Ring

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

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;

registration

ex b_{1} being Element of INT.Ring st b_{1} is prime
end;

cluster ext-real V50() right_complementable V102() integer V115() prime for Element of the carrier of INT.Ring;

existence ex b

proof end;

registration
end;

definition

let p be prime Element of INT.Ring;

let V be Z_Module;

ex b_{1} being Function of [: the carrier of (GF p), the carrier of (Z_ModuleQuot (V,(p (*) V))):], the carrier of (Z_ModuleQuot (V,(p (*) V))) st

for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds

b_{1} . (a,x) = (i mod p) * x

for b_{1}, b_{2} being Function of [: the carrier of (GF p), the carrier of (Z_ModuleQuot (V,(p (*) V))):], the carrier of (Z_ModuleQuot (V,(p (*) V))) st ( for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds

b_{1} . (a,x) = (i mod p) * x ) & ( for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds

b_{2} . (a,x) = (i mod p) * x ) holds

b_{1} = b_{2}

end;
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 Element of INT.Ring

for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds

it . (a,x) = (i mod p) * x;

existence for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds

it . (a,x) = (i mod p) * x;

ex b

for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds

b

proof end;

uniqueness for b

for i being Element of INT.Ring

for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds

b

for i being Element of INT.Ring

for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds

b

b

proof end;

:: deftheorem Def11 defines Mult_Mod_pV ZMODUL02:def 11 :

for p being prime Element of INT.Ring

for V being Z_Module

for b_{3} being Function of [: the carrier of (GF p), the carrier of (Z_ModuleQuot (V,(p (*) V))):], the carrier of (Z_ModuleQuot (V,(p (*) V))) holds

( b_{3} = Mult_Mod_pV (V,p) iff for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds

b_{3} . (a,x) = (i mod p) * x );

for p being prime Element of INT.Ring

for V being Z_Module

for b

( b

for i being Element of INT.Ring

for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds

b

definition

let p be prime Element of INT.Ring;

let V be Z_Module;

ModuleStr(# 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)) #) is non empty strict ModuleStr over GF p ;

end;
let V be Z_Module;

func Z_MQ_VectSp (V,p) -> non empty strict ModuleStr over GF p equals :: ZMODUL02:def 12

ModuleStr(# 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 ModuleStr(# 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)) #);

ModuleStr(# 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)) #) is non empty strict ModuleStr over GF p ;

:: deftheorem defines Z_MQ_VectSp ZMODUL02:def 12 :

for p being prime Element of INT.Ring

for V being Z_Module holds Z_MQ_VectSp (V,p) = ModuleStr(# 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)) #);

for p being prime Element of INT.Ring

for V being Z_Module holds Z_MQ_VectSp (V,p) = ModuleStr(# 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)) #);

registration

let p be prime Element of INT.Ring;

let V be Z_Module;

( Z_MQ_VectSp (V,p) is scalar-distributive & Z_MQ_VectSp (V,p) is vector-distributive & Z_MQ_VectSp (V,p) is scalar-associative & Z_MQ_VectSp (V,p) is scalar-unital & Z_MQ_VectSp (V,p) is add-associative & Z_MQ_VectSp (V,p) is right_zeroed & Z_MQ_VectSp (V,p) is right_complementable & Z_MQ_VectSp (V,p) is Abelian )

end;
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 ( Z_MQ_VectSp (V,p) is scalar-distributive & Z_MQ_VectSp (V,p) is vector-distributive & Z_MQ_VectSp (V,p) is scalar-associative & Z_MQ_VectSp (V,p) is scalar-unital & Z_MQ_VectSp (V,p) is add-associative & Z_MQ_VectSp (V,p) is right_zeroed & Z_MQ_VectSp (V,p) is right_complementable & Z_MQ_VectSp (V,p) is Abelian )

proof end;

definition

let p be prime Element of INT.Ring;

let V be Z_Module;

let v be VECTOR of V;

correctness

coherence

v + (p (*) V) is Vector of (Z_MQ_VectSp (V,p));

end;
let V be Z_Module;

let v be VECTOR of V;

correctness

coherence

v + (p (*) V) is Vector of (Z_MQ_VectSp (V,p));

proof end;

:: deftheorem defines ZMtoMQV ZMODUL02:def 13 :

for p being prime Element of INT.Ring

for V being Z_Module

for v being VECTOR of V holds ZMtoMQV (V,p,v) = v + (p (*) V);

for p being prime Element of INT.Ring

for V being Z_Module

for v being VECTOR of V holds ZMtoMQV (V,p,v) = v + (p (*) V);

definition

let X be Z_Module;

coherence

the lmult of X is Function of [: the carrier of INT.Ring, the carrier of X:], the carrier of X;

;

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

the lmult of X;

correctness the lmult of X;

coherence

the lmult of X is Function of [: the carrier of INT.Ring, the carrier of X:], the carrier of X;

;

:: deftheorem defines Mult_INT* ZMODUL02:def 14 :

for X being Z_Module holds Mult_INT* X = the lmult of X;

for X being Z_Module holds Mult_INT* X = the lmult of X;

definition

let X be Z_Module;

ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) is non empty strict ModuleStr over INT.Ring ;

end;
func modetrans X -> non empty strict ModuleStr over INT.Ring equals :: ZMODUL02:def 15

ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #);

coherence ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #);

ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) is non empty strict ModuleStr over INT.Ring ;

:: deftheorem defines modetrans ZMODUL02:def 15 :

for X being Z_Module holds modetrans X = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #);

for X being Z_Module holds modetrans X = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #);

registration

let X be Z_Module;

( modetrans X is Abelian & modetrans X is add-associative & modetrans X is right_zeroed & modetrans X is right_complementable & modetrans X is vector-distributive & modetrans X is scalar-distributive & modetrans X is scalar-associative & modetrans X is scalar-unital )

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

coherence ( modetrans X is Abelian & modetrans X is add-associative & modetrans X is right_zeroed & modetrans X is right_complementable & modetrans X is vector-distributive & modetrans X is scalar-distributive & modetrans X is scalar-associative & modetrans X is scalar-unital )

proof end;

definition

let X be LeftMod of INT.Ring ;

the lmult of X is Function of [: the carrier of INT.Ring, the carrier of X:], the carrier of X ;

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

the lmult of X;

coherence the lmult of X;

the lmult of X is Function of [: the carrier of INT.Ring, the carrier of X:], the carrier of X ;

:: deftheorem defines Mult_INT* ZMODUL02:def 16 :

for X being LeftMod of INT.Ring holds Mult_INT* X = the lmult of X;

for X being LeftMod of INT.Ring holds Mult_INT* X = the lmult of X;

definition

let X be LeftMod of INT.Ring ;

coherence

ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) is non empty strict ModuleStr over INT.Ring ;

;

end;
func modetrans X -> non empty strict ModuleStr over INT.Ring equals :: ZMODUL02:def 17

ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #);

correctness ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #);

coherence

ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) is non empty strict ModuleStr over INT.Ring ;

;

:: deftheorem defines modetrans ZMODUL02:def 17 :

for X being LeftMod of INT.Ring holds modetrans X = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #);

for X being LeftMod of INT.Ring holds modetrans X = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #);

registration

let X be LeftMod of INT.Ring ;

( modetrans X is Abelian & modetrans X is add-associative & modetrans X is right_zeroed & modetrans X is right_complementable & modetrans X is scalar-distributive & modetrans X is vector-distributive & modetrans X is scalar-associative & modetrans X is scalar-unital )

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

coherence ( modetrans X is Abelian & modetrans X is add-associative & modetrans X is right_zeroed & modetrans X is right_complementable & modetrans X is scalar-distributive & modetrans X is vector-distributive & modetrans X is scalar-associative & modetrans X is scalar-unital )

proof end;

definition
end;

theorem :: ZMODUL02:8

for V being Z_Module

for L being Linear_Combination of V

for v being Element of V holds

( L . v = 0. INT.Ring iff not v in Carrier L )

for L being Linear_Combination of V

for v being Element of V holds

( L . v = 0. INT.Ring iff not v in Carrier L )

proof end;

theorem :: ZMODUL02:10

for V being Z_Module

for A, B being Subset of V

for l being Linear_Combination of A st A c= B holds

l is Linear_Combination of B by VECTSP_6:4;

for A, B being Subset of V

for l being Linear_Combination of A st A c= B holds

l is Linear_Combination of B by VECTSP_6:4;

theorem Th11: :: ZMODUL02:11

for V being Z_Module

for A being Subset of V holds ZeroLC V is Linear_Combination of A by VECTSP_6:5;

for A being Subset of V holds ZeroLC V is Linear_Combination of A by VECTSP_6:5;

theorem :: ZMODUL02:12

for V being Z_Module

for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V by VECTSP_6:6;

for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V by VECTSP_6:6;

theorem :: ZMODUL02:13

theorem :: ZMODUL02:14

theorem :: ZMODUL02:15

theorem :: ZMODUL02:16

theorem :: ZMODUL02:17

theorem :: ZMODUL02:18

for V being Z_Module

for A being Subset of V holds

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

for A being Subset of V holds

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

proof end;

theorem :: ZMODUL02:20

for V being Z_Module

for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V by VECTSP_6:16;

for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V by VECTSP_6:16;

theorem :: ZMODUL02:21

for V being Z_Module

for v being VECTOR of V

for l being Linear_Combination of {v} holds Sum l = (l . v) * v by VECTSP_6:17;

for v being VECTOR of V

for l being Linear_Combination of {v} holds Sum l = (l . v) * v by VECTSP_6:17;

theorem :: ZMODUL02:23

for V being Z_Module

for L being Linear_Combination of V st Carrier L = {} holds

Sum L = 0. V by VECTSP_6:19;

for L being Linear_Combination of V st Carrier L = {} holds

Sum L = 0. V by VECTSP_6:19;

theorem :: ZMODUL02:25

definition
end;

theorem :: ZMODUL02:26

for V being Z_Module

for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) by VECTSP_6:23;

for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) by VECTSP_6:23;

theorem Th27: :: ZMODUL02:27

for V being Z_Module

for L1, L2 being Linear_Combination of V

for A being Subset of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds

L1 + L2 is Linear_Combination of A by VECTSP_6:24;

for L1, L2 being Linear_Combination of V

for A being Subset of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds

L1 + L2 is Linear_Combination of A by VECTSP_6:24;

theorem Th28: :: ZMODUL02:28

for V being Z_Module

for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3 by VECTSP_6:26;

for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3 by VECTSP_6:26;

registration
end;

theorem :: ZMODUL02:29

for V being Z_Module

for L being Linear_Combination of V

for a being Element of INT.Ring st a <> 0. INT.Ring holds

Carrier (a * L) = Carrier L

for L being Linear_Combination of V

for a being Element of INT.Ring st a <> 0. INT.Ring holds

Carrier (a * L) = Carrier L

proof end;

theorem :: ZMODUL02:30

for V being Z_Module

for L being Linear_Combination of V holds (0. INT.Ring) * L = ZeroLC V by VECTSP_6:30;

for L being Linear_Combination of V holds (0. INT.Ring) * L = ZeroLC V by VECTSP_6:30;

theorem Th31: :: ZMODUL02:31

for V being Z_Module

for L being Linear_Combination of V

for a being Element of INT.Ring

for A being Subset of V st L is Linear_Combination of A holds

a * L is Linear_Combination of A by VECTSP_6:31;

for L being Linear_Combination of V

for a being Element of INT.Ring

for A being Subset of V st L is Linear_Combination of A holds

a * L is Linear_Combination of A by VECTSP_6:31;

theorem Th34: :: ZMODUL02:34

for V being Z_Module

for L being Linear_Combination of V

for a, b being Element of INT.Ring holds a * (b * L) = (a * b) * L by VECTSP_6:34;

for L being Linear_Combination of V

for a, b being Element of INT.Ring holds a * (b * L) = (a * b) * L by VECTSP_6:34;

registration

let V be Z_Module;

let L be Linear_Combination of V;

reducibility

(1. INT.Ring) * L = L by VECTSP_6:35;

end;
let L be Linear_Combination of V;

reducibility

(1. INT.Ring) * L = L by VECTSP_6:35;

definition
end;

theorem :: ZMODUL02:35

for V being Z_Module

for v being VECTOR of V

for L being Linear_Combination of V holds (- L) . v = - (L . v) by VECTSP_6:36;

for v being VECTOR of V

for L being Linear_Combination of V holds (- L) . v = - (L . v) by VECTSP_6:36;

theorem :: ZMODUL02:36

for V being Z_Module

for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds

L2 = - L1 by VECTSP_6:37;

for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds

L2 = - L1 by VECTSP_6:37;

theorem :: ZMODUL02:37

for V being Z_Module

for L being Linear_Combination of V holds Carrier (- L) = Carrier L by VECTSP_6:38;

for L being Linear_Combination of V holds Carrier (- L) = Carrier L by VECTSP_6:38;

theorem :: ZMODUL02:38

for V being Z_Module

for L being Linear_Combination of V

for A being Subset of V st L is Linear_Combination of A holds

- L is Linear_Combination of A by VECTSP_6:39;

for L being Linear_Combination of V

for A being Subset of V st L is Linear_Combination of A holds

- L is Linear_Combination of A by VECTSP_6:39;

theorem :: ZMODUL02:39

for V being Z_Module

for v being VECTOR of V

for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) by VECTSP_6:40;

for v being VECTOR of V

for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) by VECTSP_6:40;

theorem :: ZMODUL02:40

for V being Z_Module

for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) by VECTSP_6:41;

for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) by VECTSP_6:41;

theorem :: ZMODUL02:41

for V being Z_Module

for L1, L2 being Linear_Combination of V

for A being Subset of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds

L1 - L2 is Linear_Combination of A by VECTSP_6:42;

for L1, L2 being Linear_Combination of V

for A being Subset of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds

L1 - L2 is Linear_Combination of A by VECTSP_6:42;

definition

let V be Z_Module;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is Linear_Combination of V )

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

( x in b_{1} iff x is Linear_Combination of V ) ) & ( for x being set holds

( x in b_{2} iff x is Linear_Combination of V ) ) holds

b_{1} = b_{2}

end;
func LinComb V -> set means :Def29: :: ZMODUL02:def 29

for x being set holds

( x in it iff x is Linear_Combination of V );

existence for x being set holds

( x in it iff x is Linear_Combination of V );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def29 defines LinComb ZMODUL02:def 29 :

for V being Z_Module

for b_{2} being set holds

( b_{2} = LinComb V iff for x being set holds

( x in b_{2} iff x is Linear_Combination of V ) );

for V being Z_Module

for b

( b

( x in b

registration
end;

definition
end;

:: deftheorem defines @ ZMODUL02:def 30 :

for V being Z_Module

for e being Element of LinComb V holds @ e = e;

for V being Z_Module

for e being Element of LinComb V holds @ e = e;

definition
end;

:: deftheorem defines @ ZMODUL02:def 31 :

for V being Z_Module

for L being Linear_Combination of V holds @ L = L;

for V being Z_Module

for L being Linear_Combination of V holds @ L = L;

definition

let V be Z_Module;

ex b_{1} being BinOp of (LinComb V) st

for e1, e2 being Element of LinComb V holds b_{1} . (e1,e2) = (@ e1) + (@ e2)

for b_{1}, b_{2} being BinOp of (LinComb V) st ( for e1, e2 being Element of LinComb V holds b_{1} . (e1,e2) = (@ e1) + (@ e2) ) & ( for e1, e2 being Element of LinComb V holds b_{2} . (e1,e2) = (@ e1) + (@ e2) ) holds

b_{1} = b_{2}

end;
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 for e1, e2 being Element of LinComb V holds it . (e1,e2) = (@ e1) + (@ e2);

ex b

for e1, e2 being Element of LinComb V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def32 defines LCAdd ZMODUL02:def 32 :

for V being Z_Module

for b_{2} being BinOp of (LinComb V) holds

( b_{2} = LCAdd V iff for e1, e2 being Element of LinComb V holds b_{2} . (e1,e2) = (@ e1) + (@ e2) );

for V being Z_Module

for b

( b

definition

let V be Z_Module;

ex b_{1} being Function of [: the carrier of INT.Ring,(LinComb V):],(LinComb V) st

for a being Element of INT.Ring

for e being Element of LinComb V holds b_{1} . [a,e] = a * (@ e)

for b_{1}, b_{2} being Function of [: the carrier of INT.Ring,(LinComb V):],(LinComb V) st ( for a being Element of INT.Ring

for e being Element of LinComb V holds b_{1} . [a,e] = a * (@ e) ) & ( for a being Element of INT.Ring

for e being Element of LinComb V holds b_{2} . [a,e] = a * (@ e) ) holds

b_{1} = b_{2}

end;
func LCMult V -> Function of [: the carrier of INT.Ring,(LinComb V):],(LinComb V) means :Def33: :: ZMODUL02:def 33

for a being Element of INT.Ring

for e being Element of LinComb V holds it . [a,e] = a * (@ e);

existence for a being Element of INT.Ring

for e being Element of LinComb V holds it . [a,e] = a * (@ e);

ex b

for a being Element of INT.Ring

for e being Element of LinComb V holds b

proof end;

uniqueness for b

for e being Element of LinComb V holds b

for e being Element of LinComb V holds b

b

proof end;

:: deftheorem Def33 defines LCMult ZMODUL02:def 33 :

for V being Z_Module

for b_{2} being Function of [: the carrier of INT.Ring,(LinComb V):],(LinComb V) holds

( b_{2} = LCMult V iff for a being Element of INT.Ring

for e being Element of LinComb V holds b_{2} . [a,e] = a * (@ e) );

for V being Z_Module

for b

( b

for e being Element of LinComb V holds b

definition

let V be Z_Module;

ModuleStr(# (LinComb V),(LCAdd V),(@ (ZeroLC V)),(LCMult V) #) is ModuleStr over INT.Ring ;

end;
func LC_Z_Module V -> ModuleStr over INT.Ring equals :: ZMODUL02:def 34

ModuleStr(# (LinComb V),(LCAdd V),(@ (ZeroLC V)),(LCMult V) #);

coherence ModuleStr(# (LinComb V),(LCAdd V),(@ (ZeroLC V)),(LCMult V) #);

ModuleStr(# (LinComb V),(LCAdd V),(@ (ZeroLC V)),(LCMult V) #) is ModuleStr over INT.Ring ;

:: deftheorem defines LC_Z_Module ZMODUL02:def 34 :

for V being Z_Module holds LC_Z_Module V = ModuleStr(# (LinComb V),(LCAdd V),(@ (ZeroLC V)),(LCMult V) #);

for V being Z_Module holds LC_Z_Module V = ModuleStr(# (LinComb V),(LCAdd V),(@ (ZeroLC V)),(LCMult V) #);

registration
end;

registration

let V be Z_Module;

( LC_Z_Module V is Abelian & LC_Z_Module V is add-associative & LC_Z_Module V is right_zeroed & LC_Z_Module V is right_complementable & LC_Z_Module V is vector-distributive & LC_Z_Module V is scalar-distributive & LC_Z_Module V is scalar-associative & LC_Z_Module V is scalar-unital )

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

coherence ( LC_Z_Module V is Abelian & LC_Z_Module V is add-associative & LC_Z_Module V is right_zeroed & LC_Z_Module V is right_complementable & LC_Z_Module V is vector-distributive & LC_Z_Module V is scalar-distributive & LC_Z_Module V is scalar-associative & LC_Z_Module V is scalar-unital )

proof end;

theorem Th47: :: ZMODUL02:47

for V being Z_Module

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

for L1, L2 being 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 Linear_Combination of V

for a being Element of INT.Ring holds a * (vector ((LC_Z_Module V),L)) = a * L

for L being Linear_Combination of V

for a being Element of INT.Ring holds a * (vector ((LC_Z_Module V),L)) = a * L

proof end;

theorem :: ZMODUL02:50

for V being Z_Module

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

for L1, L2 being 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;

ex b_{1} being strict Submodule of LC_Z_Module V st the carrier of b_{1} = { l where l is Linear_Combination of A : verum }

for b_{1}, b_{2} being strict Submodule of LC_Z_Module V st the carrier of b_{1} = { l where l is Linear_Combination of A : verum } & the carrier of b_{2} = { l where l is Linear_Combination of A : verum } holds

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

end;
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 Linear_Combination of A : verum } ;

existence the carrier of it = { l where l is Linear_Combination of A : verum } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem defines LC_Z_Module ZMODUL02:def 35 :

for V being Z_Module

for A being Subset of V

for b_{3} being strict Submodule of LC_Z_Module V holds

( b_{3} = LC_Z_Module A iff the carrier of b_{3} = { l where l is Linear_Combination of A : verum } );

for V being Z_Module

for A being Subset of V

for b

( b

theorem :: ZMODUL02:51

theorem :: ZMODUL02:52

for V being Z_Module

for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2) by VECTSP_6:44;

for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2) by VECTSP_6:44;

theorem :: ZMODUL02:53

theorem :: ZMODUL02:54

for V being Z_Module

for L being Linear_Combination of V holds Sum (- L) = - (Sum L) by VECTSP_6:46;

for L being Linear_Combination of V holds Sum (- L) = - (Sum L) by VECTSP_6:46;

theorem :: ZMODUL02:55

for V being Z_Module

for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2) by VECTSP_6:47;

for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2) by VECTSP_6:47;

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 by VECTSP_7:1;

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

A is linearly-independent by VECTSP_7:1;

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 by VECTSP_7:2;

for A being Subset of V st A is linearly-independent holds

not 0. V in A by VECTSP_7:2;

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

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;

coherence

for b_{1} being Subset of V st b_{1} = {(0. V)} holds

not b_{1} is linearly-independent

end;
coherence

for b

not b

proof 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 by VECTSP_7:4;

for v1, v2 being Vector of V st {v1,v2} is linearly-independent holds

v1 <> 0. V by VECTSP_7:4;

theorem :: ZMODUL02:61

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 Element of INT.Ring st b <> 0. INT.Ring holds

b * v1 <> a * v2 ) ) )

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 Element of INT.Ring st b <> 0. INT.Ring 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 Element of INT.Ring st (a * v1) + (b * v2) = 0. V holds

( a = 0 & b = 0 ) )

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 Element of INT.Ring st (a * v1) + (b * v2) = 0. V holds

( a = 0 & b = 0 ) )

proof end;

theorem :: ZMODUL02:64

theorem :: ZMODUL02:68

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 :: ZMODUL02:70

theorem :: ZMODUL02:71

theorem :: ZMODUL02:72

theorem :: ZMODUL02:73

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

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

theorem :: ZMODUL02:76

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

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

W1 is Submodule of W2 + W3

proof end;