:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received May 7, 2012

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

definition

let R be Ring;

let V be LeftMod of R;

let a be Element of R;

coherence

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

end;
let V be LeftMod of R;

let a be Element of R;

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 R being Ring

for V being LeftMod of R

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

for R being Ring

for V being LeftMod of R

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

definition

let R be Ring;

let V be LeftMod of R;

let a be Element of R;

correctness

coherence

0. V is Element of a * V;

end;
let V be LeftMod of R;

let a be Element of R;

correctness

coherence

0. V is Element of a * V;

proof end;

:: deftheorem defines Zero_ ZMODUL02:def 2 :

for R being Ring

for V being LeftMod of R

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

for R being Ring

for V being LeftMod of R

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

definition

let R be Ring;

let V be LeftMod of R;

let a be Element of R;

coherence

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

end;
let V be LeftMod of R;

let a be Element of R;

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 R being Ring

for V being LeftMod of R

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

for R being Ring

for V being LeftMod of R

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

definition

let R be commutative Ring;

let V be VectSp of R;

let a be Element of R;

coherence

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

end;
let V be VectSp of R;

let a be Element of R;

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

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

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

coherence

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

proof end;

:: deftheorem defines Mult_ ZMODUL02:def 4 :

for R being commutative Ring

for V being VectSp of R

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

for R being commutative Ring

for V being VectSp of R

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

definition

let R be commutative Ring;

let V be LeftMod of R;

let a be Element of R;

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

end;
let V be LeftMod of R;

let a be Element of R;

func a (*) V -> Subspace 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 Subspace of V

proof end;

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

for R being commutative Ring

for V being LeftMod of R

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

for R being commutative Ring

for V being LeftMod of R

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

definition
end;

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 (VectQuot (V,W)) st W = p (*) V holds

p * x = 0. (VectQuot (V,W))

for V being Z_Module

for W being Submodule of V

for x being VECTOR of (VectQuot (V,W)) st W = p (*) V holds

p * x = 0. (VectQuot (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 (VectQuot (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 (VectQuot (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. (VectQuot (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. (VectQuot (V,W))

proof end;

registration

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

cluster ext-real complex 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 (VectQuot (V,(p (*) V))):], the carrier of (VectQuot (V,(p (*) V))) st

for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (VectQuot (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 (VectQuot (V,(p (*) V))):], the carrier of (VectQuot (V,(p (*) V))) st ( for a being Element of (GF p)

for i being Element of INT.Ring

for x being Element of (VectQuot (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 (VectQuot (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 (VectQuot (V,(p (*) V))):], the carrier of (VectQuot (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 (VectQuot (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 (VectQuot (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 (VectQuot (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 (VectQuot (V,(p (*) V))) st a = i mod p holds

b

for i being Element of INT.Ring

for x being Element of (VectQuot (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 (VectQuot (V,(p (*) V))):], the carrier of (VectQuot (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 (VectQuot (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 (VectQuot (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 (VectQuot (V,(p (*) V))), the addF of (VectQuot (V,(p (*) V))), the ZeroF of (VectQuot (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 (VectQuot (V,(p (*) V))), the addF of (VectQuot (V,(p (*) V))), the ZeroF of (VectQuot (V,(p (*) V))),(Mult_Mod_pV (V,p)) #);

coherence ModuleStr(# the carrier of (VectQuot (V,(p (*) V))), the addF of (VectQuot (V,(p (*) V))), the ZeroF of (VectQuot (V,(p (*) V))),(Mult_Mod_pV (V,p)) #);

ModuleStr(# the carrier of (VectQuot (V,(p (*) V))), the addF of (VectQuot (V,(p (*) V))), the ZeroF of (VectQuot (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 (VectQuot (V,(p (*) V))), the addF of (VectQuot (V,(p (*) V))), the ZeroF of (VectQuot (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 (VectQuot (V,(p (*) V))), the addF of (VectQuot (V,(p (*) V))), the ZeroF of (VectQuot (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 R be Ring;

let X be LeftMod of R;

coherence

the lmult of X is Function of [: the carrier of R, the carrier of X:], the carrier of X;

;

end;
let X be LeftMod of R;

func Mult_INT* X -> Function of [: the carrier of R, 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 R, the carrier of X:], the carrier of X;

;

:: deftheorem defines Mult_INT* ZMODUL02:def 14 :

for R being Ring

for X being LeftMod of R holds Mult_INT* X = the lmult of X;

for R being Ring

for X being LeftMod of R holds Mult_INT* X = the lmult of X;

definition

let R be Ring;

let X be LeftMod of R;

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

end;
let X be LeftMod of R;

func modetrans X -> non empty strict ModuleStr over R 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 R ;

:: deftheorem defines modetrans ZMODUL02:def 15 :

for R being Ring

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

for R being Ring

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

registration

let R be Ring;

let X be LeftMod of R;

( 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;
let X be LeftMod of R;

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

::$CD 13

::$CD 13

::$CD 13

::$CD 13

theorem :: ZMODUL02:8

for R being Ring

for V being LeftMod of R

for L being Linear_Combination of V

for v being Element of V holds

( L . v = 0. R iff not v in Carrier L )

for V being LeftMod of R

for L being Linear_Combination of V

for v being Element of V holds

( L . v = 0. R iff not v in Carrier L )

proof end;

theorem :: ZMODUL02:10

for R being Ring

for V being LeftMod of R

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 V being LeftMod of R

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 R being Ring

for V being LeftMod of R

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

for V being LeftMod of R

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

theorem :: ZMODUL02:12

for R being Ring

for V being LeftMod of R

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

for V being LeftMod of R

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 R being Ring

for V being LeftMod of R

for A being Subset of V st not R is degenerated holds

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

for V being LeftMod of R

for A being Subset of V st not R is degenerated holds

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

proof end;

theorem :: ZMODUL02:19

theorem :: ZMODUL02:20

for R being Ring

for V being LeftMod of R

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

for V being LeftMod of R

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

theorem :: ZMODUL02:21

theorem :: ZMODUL02:23

for R being Ring

for V being LeftMod of R

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

Sum L = 0. V by VECTSP_6:19;

for V being LeftMod of R

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

Sum L = 0. V by VECTSP_6:19;

theorem :: ZMODUL02:25

theorem :: ZMODUL02:26

for R being Ring

for V being LeftMod of R

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

for V being LeftMod of R

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 R being Ring

for V being LeftMod of R

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 V being LeftMod of R

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 R being Ring

for V being LeftMod of R

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

for V being LeftMod of R

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

registration

let R be Ring;

let V be LeftMod of R;

let L be Linear_Combination of V;

reducibility

L + (ZeroLC V) = L by VECTSP_6:27;

end;
let V be LeftMod of R;

let L be Linear_Combination of V;

reducibility

L + (ZeroLC V) = L by VECTSP_6:27;

theorem :: ZMODUL02:29

for V being Z_Module

for a being Element of INT.Ring

for L being Linear_Combination of V st a <> 0. INT.Ring holds

Carrier (a * L) = Carrier L

for a being Element of INT.Ring

for L being Linear_Combination of V st a <> 0. INT.Ring holds

Carrier (a * L) = Carrier L

proof end;

theorem :: ZMODUL02:30

for R being Ring

for V being LeftMod of R

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

for V being LeftMod of R

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

theorem Th31: :: ZMODUL02:31

for R being Ring

for V being LeftMod of R

for L being Linear_Combination of V

for a being Element of R

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 V being LeftMod of R

for L being Linear_Combination of V

for a being Element of R

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 R being Ring

for V being LeftMod of R

for L being Linear_Combination of V

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

for V being LeftMod of R

for L being Linear_Combination of V

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

registration

let R be Ring;

let V be LeftMod of R;

let L be Linear_Combination of V;

reducibility

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

end;
let V be LeftMod of R;

let L be Linear_Combination of V;

reducibility

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

theorem :: ZMODUL02:35

for R being Ring

for V being LeftMod of R

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 LeftMod of R

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 R being Ring

for V being LeftMod of R

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

L2 = - L1 by VECTSP_6:37;

for V being LeftMod of R

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

L2 = - L1 by VECTSP_6:37;

theorem :: ZMODUL02:37

for R being Ring

for V being LeftMod of R

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

for V being LeftMod of R

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

theorem :: ZMODUL02:38

for R being Ring

for V being LeftMod of R

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 V being LeftMod of R

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

theorem :: ZMODUL02:40

for R being Ring

for V being LeftMod of R

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

for V being LeftMod of R

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 R being Ring

for V being LeftMod of R

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 V being LeftMod of R

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;

theorem Th42: :: ZMODUL02:42

for R being Ring

for V being LeftMod of R

for L being Linear_Combination of V holds L - L = ZeroLC V by VECTSP_6:43;

for V being LeftMod of R

for L being Linear_Combination of V holds L - L = ZeroLC V by VECTSP_6:43;

definition

let R be Ring;

let V be LeftMod of R;

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;
let V be LeftMod of R;

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 R being Ring

for V being LeftMod of R

for b_{3} being set holds

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

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

for R being Ring

for V being LeftMod of R

for b

( b

( x in b

definition

let R be Ring;

let V be LeftMod of R;

let e be Element of LinComb V;

coherence

e is Linear_Combination of V by Def29;

end;
let V be LeftMod of R;

let e be Element of LinComb V;

coherence

e is Linear_Combination of V by Def29;

:: deftheorem defines @ ZMODUL02:def 30 :

for R being Ring

for V being LeftMod of R

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

for R being Ring

for V being LeftMod of R

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

definition

let R be Ring;

let V be LeftMod of R;

let L be Linear_Combination of V;

coherence

L is Element of LinComb V by Def29;

end;
let V be LeftMod of R;

let L be Linear_Combination of V;

coherence

L is Element of LinComb V by Def29;

:: deftheorem defines @ ZMODUL02:def 31 :

for R being Ring

for V being LeftMod of R

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

for R being Ring

for V being LeftMod of R

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

definition

let R be Ring;

let V be LeftMod of R;

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;
let V be LeftMod of R;

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 R being Ring

for V being LeftMod of R

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

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

for R being Ring

for V being LeftMod of R

for b

( b

definition

let R be Ring;

let V be LeftMod of R;

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

for a being Element of R

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 R,(LinComb V):],(LinComb V) st ( for a being Element of R

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

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

b_{1} = b_{2}

end;
let V be LeftMod of R;

func LCMult V -> Function of [: the carrier of R,(LinComb V):],(LinComb V) means :Def33: :: ZMODUL02:def 33

for a being Element of R

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

existence for a being Element of R

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

ex b

for a being Element of R

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 R being Ring

for V being LeftMod of R

for b_{3} being Function of [: the carrier of R,(LinComb V):],(LinComb V) holds

( b_{3} = LCMult V iff for a being Element of R

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

for R being Ring

for V being LeftMod of R

for b

( b

for e being Element of LinComb V holds b

definition

let R be Ring;

let V be LeftMod of R;

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

end;
let V be LeftMod of R;

func LC_Z_Module V -> ModuleStr over R 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 R ;

:: deftheorem defines LC_Z_Module ZMODUL02:def 34 :

for R being Ring

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

for R being Ring

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

registration

let R be Ring;

let V be LeftMod of R;

coherence

( LC_Z_Module V is strict & not LC_Z_Module V is empty ) ;

end;
let V be LeftMod of R;

coherence

( LC_Z_Module V is strict & not LC_Z_Module V is empty ) ;

registration

let R be Ring;

let V be LeftMod of R;

( 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;
let V be LeftMod of R;

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

theorem :: ZMODUL02:44

theorem :: ZMODUL02:45

theorem :: ZMODUL02:46

theorem Th47: :: ZMODUL02:47

for R being Ring

for V being LeftMod of R

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

for V being LeftMod of R

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 R being Ring

for V being LeftMod of R

for L being Linear_Combination of V

for a being Element of R holds a * (vector ((LC_Z_Module V),L)) = a * L

for V being LeftMod of R

for L being Linear_Combination of V

for a being Element of R holds a * (vector ((LC_Z_Module V),L)) = a * L

proof end;

theorem Th49: :: ZMODUL02:49

for R being Ring

for V being LeftMod of R

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

for V being LeftMod of R

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

proof end;

theorem :: ZMODUL02:50

for R being Ring

for V being LeftMod of R

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

for V being LeftMod of R

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 R be Ring;

let V be LeftMod of R;

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 V be LeftMod of R;

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 R being Ring

for V being LeftMod of R

for A being Subset of V

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

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

for R being Ring

for V being LeftMod of R

for A being Subset of V

for b

( b

theorem :: ZMODUL02:51

theorem :: ZMODUL02:52

for R being Ring

for V being LeftMod of R

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

for V being LeftMod of R

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 R being Ring

for V being LeftMod of R

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

for V being LeftMod of R

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

theorem :: ZMODUL02:55

for R being Ring

for V being LeftMod of R

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

for V being LeftMod of R

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

theorem :: ZMODUL02:56

for R being Ring

for V being LeftMod of R

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

A is linearly-independent by VECTSP_7:1;

for V being LeftMod of R

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

A is linearly-independent by VECTSP_7:1;

theorem Th57: :: ZMODUL02:57

for R being Ring

for V being LeftMod of R

for A being Subset of V st not R is degenerated & A is linearly-independent holds

not 0. V in A by VECTSP_7:2;

for V being LeftMod of R

for A being Subset of V st not R is degenerated & A is linearly-independent holds

not 0. V in A by VECTSP_7:2;

theorem :: ZMODUL02:58

registration

let R be Ring;

let V be LeftMod of R;

existence

ex b_{1} being Subset of V st b_{1} is linearly-independent

end;
let V be LeftMod of R;

existence

ex b

proof end;

theorem :: ZMODUL02:59

for R being Ring

for V being LeftMod of R

for v being Vector of V st not R is degenerated & V is Mult-cancelable holds

( {v} is linearly-independent iff v <> 0. V )

for V being LeftMod of R

for v being Vector of V st not R is degenerated & V is Mult-cancelable holds

( {v} is linearly-independent iff v <> 0. V )

proof end;

registration

let R be non degenerated Ring;

let V be LeftMod of R;

coherence

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

not b_{1} is linearly-independent

end;
let V be LeftMod of R;

coherence

for b

not b

proof end;

theorem Th60: :: ZMODUL02:60

for R being Ring

for V being LeftMod of R

for v1, v2 being Vector of V st R is commutative & not R is degenerated & {v1,v2} is linearly-independent holds

v1 <> 0. V by VECTSP_7:4;

for V being LeftMod of R

for v1, v2 being Vector of V st R is commutative & not R is degenerated & {v1,v2} is linearly-independent holds

v1 <> 0. V by VECTSP_7:4;

theorem :: ZMODUL02:61

for R being Ring

for V being LeftMod of R

for v being Vector of V st R is commutative & not R is degenerated holds

{v,(0. V)} is linearly-dependent by Th60;

for V being LeftMod of R

for v being Vector of V st R is commutative & not R is degenerated holds

{v,(0. V)} is linearly-dependent by Th60;

theorem Th62: :: ZMODUL02:62

for R being Ring

for V being LeftMod of R

for v1, v2 being Vector of V st R = INT.Ring & V is Mult-cancelable holds

( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) ) )

for V being LeftMod of R

for v1, v2 being Vector of V st R = INT.Ring & V is Mult-cancelable holds

( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a, b being Element of R st b <> 0. R holds

b * v1 <> a * v2 ) ) )

proof end;

theorem :: ZMODUL02:63

for R being Ring

for V being LeftMod of R

for v1, v2 being Vector of V st R = INT.Ring & V is Mult-cancelable holds

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

( a = 0. R & b = 0. R ) )

for V being LeftMod of R

for v1, v2 being Vector of V st R = INT.Ring & V is Mult-cancelable holds

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

( a = 0. R & b = 0. R ) )

proof end;

theorem :: ZMODUL02:64

theorem :: ZMODUL02:67

theorem :: ZMODUL02:68

theorem :: ZMODUL02:69

for R being Ring

for V being strict LeftMod of R

for A being Subset of V st A = the carrier of V holds

Lin A = V

for V being strict LeftMod of R

for A being Subset of V st A = the carrier of V holds

Lin A = V

proof end;

Lm3: for R being Ring

for V being LeftMod of R

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 R being Ring

for V being LeftMod of R

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 R being Ring

for V being LeftMod of R

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

W1 /\ W2 is Submodule of W3

for V being LeftMod of R

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 R being Ring

for V being LeftMod of R

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

W1 is Submodule of W2 + W3

for V being LeftMod of R

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

W1 is Submodule of W2 + W3

proof end;