:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received September 5, 2011

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

registration

let a, b be Element of INT.Ring;

let c, d be Integer;

compatibility

( a = c & b = d implies a * b = c * d )

( a = c & b = d implies a + b = c + d )

end;
let c, d be Integer;

compatibility

( a = c & b = d implies a * b = c * d )

proof end;

compatibility ( a = c & b = d implies a + b = c + d )

proof end;

registration
end;

definition
end;

registration

coherence

( TrivialLMod INT.Ring is trivial & not TrivialLMod INT.Ring is empty & TrivialLMod INT.Ring is strict )

end;
( TrivialLMod INT.Ring is trivial & not TrivialLMod INT.Ring is empty & TrivialLMod INT.Ring is strict )

proof end;

registration

ex b_{1} being Z_Module st b_{1} is strict
end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V140() V141() V142() V143() strict vector-distributive scalar-distributive scalar-associative scalar-unital for ModuleStr over INT.Ring ;

existence ex b

proof end;

:: deftheorem defines Mult-cancelable ZMODUL01:def 7 :

for IT being Z_Module holds

( IT is Mult-cancelable iff for a being Element of INT.Ring

for v being Vector of IT holds

( not a * v = 0. IT or a = 0. INT.Ring or v = 0. IT ) );

for IT being Z_Module holds

( IT is Mult-cancelable iff for a being Element of INT.Ring

for v being Vector of IT holds

( not a * v = 0. IT or a = 0. INT.Ring or v = 0. IT ) );

theorem Th1: :: ZMODUL01:1

for a being Element of INT.Ring

for V being Z_Module

for v being Vector of V st ( a = 0. INT.Ring or v = 0. V ) holds

a * v = 0. V

for V being Z_Module

for v being Vector of V st ( a = 0. INT.Ring or v = 0. V ) holds

a * v = 0. V

proof end;

theorem Th5: :: ZMODUL01:5

for a being Element of INT.Ring

for V being Z_Module

for v being Vector of V holds a * (- v) = (- a) * v

for V being Z_Module

for v being Vector of V holds a * (- v) = (- a) * v

proof end;

theorem Th6: :: ZMODUL01:6

for a being Element of INT.Ring

for V being Z_Module

for v being Vector of V holds a * (- v) = - (a * v)

for V being Z_Module

for v being Vector of V holds a * (- v) = - (a * v)

proof end;

theorem :: ZMODUL01:7

for a being Element of INT.Ring

for V being Z_Module

for v being Vector of V holds (- a) * (- v) = a * v

for V being Z_Module

for v being Vector of V holds (- a) * (- v) = a * v

proof end;

theorem Th8: :: ZMODUL01:8

for a being Element of INT.Ring

for V being Z_Module

for v, w being Vector of V holds a * (v - w) = (a * v) - (a * w)

for V being Z_Module

for v, w being Vector of V holds a * (v - w) = (a * v) - (a * w)

proof end;

theorem Th9: :: ZMODUL01:9

for a, b being Element of INT.Ring

for V being Z_Module

for v being Vector of V holds (a - b) * v = (a * v) - (b * v)

for V being Z_Module

for v being Vector of V holds (a - b) * v = (a * v) - (b * v)

proof end;

theorem :: ZMODUL01:10

for a being Element of INT.Ring

for V being Z_Module

for v, w being Vector of V st V is Mult-cancelable & a <> 0. INT.Ring & a * v = a * w holds

v = w

for V being Z_Module

for v, w being Vector of V st V is Mult-cancelable & a <> 0. INT.Ring & a * v = a * w holds

v = w

proof end;

theorem :: ZMODUL01:11

for a, b being Element of INT.Ring

for V being Z_Module

for v being Vector of V st V is Mult-cancelable & v <> 0. V & a * v = b * v holds

a = b

for V being Z_Module

for v being Vector of V st V is Mult-cancelable & v <> 0. V & a * v = b * v holds

a = b

proof end;

Lm1: for V being Z_Module holds Sum (<*> the carrier of V) = 0. V

proof end;

Lm2: for V being Z_Module

for F being FinSequence of V st len F = 0 holds

Sum F = 0. V

proof end;

theorem Th12: :: ZMODUL01:12

for a being Element of INT.Ring

for V being Z_Module

for F, G being FinSequence of V st len F = len G & ( for k being Nat

for v being Vector of V st k in dom F & v = G . k holds

F . k = a * v ) holds

Sum F = a * (Sum G)

for V being Z_Module

for F, G being FinSequence of V st len F = len G & ( for k being Nat

for v being Vector of V st k in dom F & v = G . k holds

F . k = a * v ) holds

Sum F = a * (Sum G)

proof end;

theorem :: ZMODUL01:13

theorem :: ZMODUL01:14

for V being Z_Module

for a being Element of INT.Ring

for v, u being Vector of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)

for a being Element of INT.Ring

for v, u being Vector of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)

proof end;

theorem :: ZMODUL01:15

for V being Z_Module

for a being Element of INT.Ring

for v, u, w being Vector of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)

for a being Element of INT.Ring

for v, u, w being Vector of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)

proof end;

theorem :: ZMODUL01:16

for a being Element of INT.Ring

for V being Z_Module

for v being Vector of V holds (- a) * v = - (a * v)

for V being Z_Module

for v being Vector of V holds (- a) * v = - (a * v)

proof end;

theorem :: ZMODUL01:17

for a being Element of INT.Ring

for V being Z_Module

for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds

G . k = a * (F /. k) ) holds

Sum G = a * (Sum F)

for V being Z_Module

for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds

G . k = a * (F /. k) ) holds

Sum G = a * (Sum F)

proof end;

theorem :: ZMODUL01:18

for V being Z_Module

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

0. V in V1 by VECTSP_4:1;

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

0. V in V1 by VECTSP_4:1;

theorem :: ZMODUL01:19

for V being Z_Module

for V1 being Subset of V st V1 is linearly-closed holds

for v being Vector of V st v in V1 holds

- v in V1 by VECTSP_4:2;

for V1 being Subset of V st V1 is linearly-closed holds

for v being Vector of V st v in V1 holds

- v in V1 by VECTSP_4:2;

theorem :: ZMODUL01:20

for V being Z_Module

for V1 being Subset of V st V1 is linearly-closed holds

for v, u being Vector of V st v in V1 & u in V1 holds

v - u in V1 by VECTSP_4:3;

for V1 being Subset of V st V1 is linearly-closed holds

for v, u being Vector of V st v in V1 & u in V1 holds

v - u in V1 by VECTSP_4:3;

theorem :: ZMODUL01:21

for V being Z_Module

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

V1 is linearly-closed ;

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

V1 is linearly-closed ;

theorem :: ZMODUL01:22

for V being Z_Module

for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where u, v is Vector of V : ( v in V1 & u in V2 ) } holds

V3 is linearly-closed

for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where u, v is Vector of V : ( v in V1 & u in V2 ) } holds

V3 is linearly-closed

proof end;

registration

let V be Z_Module;

coherence

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

b_{1} is linearly-closed
by VECTSP_4:4;

end;
coherence

for b

b

registration
end;

registration

let V be Z_Module;

let V1, V2 be linearly-closed Subset of V;

coherence

for b_{1} being Subset of V st b_{1} = V1 /\ V2 holds

b_{1} is linearly-closed
by VECTSP_4:7;

end;
let V1, V2 be linearly-closed Subset of V;

coherence

for b

b

definition
end;

theorem :: ZMODUL01:23

theorem Th25: :: ZMODUL01:25

for V being Z_Module

for W being Submodule of V

for w being Vector of W holds w is Vector of V by VECTSP_4:10;

for W being Submodule of V

for w being Vector of W holds w is Vector of V by VECTSP_4:10;

theorem :: ZMODUL01:26

theorem :: ZMODUL01:27

theorem :: ZMODUL01:28

theorem :: ZMODUL01:29

theorem :: ZMODUL01:30

theorem :: ZMODUL01:31

theorem :: ZMODUL01:34

theorem :: ZMODUL01:35

theorem :: ZMODUL01:37

theorem :: ZMODUL01:38

theorem Th40: :: ZMODUL01:40

for V being Z_Module

for V1 being Subset of V

for D being non empty set

for d1 being Element of D

for A being BinOp of D

for M being Function of [: the carrier of INT.Ring,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the lmult of V | [: the carrier of INT.Ring,V1:] holds

ModuleStr(# D,A,d1,M #) is Submodule of V

for V1 being Subset of V

for D being non empty set

for d1 being Element of D

for A being BinOp of D

for M being Function of [: the carrier of INT.Ring,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the lmult of V | [: the carrier of INT.Ring,V1:] holds

ModuleStr(# D,A,d1,M #) is Submodule of V

proof end;

theorem :: ZMODUL01:41

theorem Th42: :: ZMODUL01:42

for V, X, Y being Z_Module st V is Submodule of X & X is Submodule of Y holds

V is Submodule of Y by VECTSP_4:26;

V is Submodule of Y by VECTSP_4:26;

theorem :: ZMODUL01:44

registration

let V be Z_Module;

ex b_{1} being Submodule of V st b_{1} is strict

end;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V140() V141() V142() V143() strict vector-distributive scalar-distributive scalar-associative scalar-unital for Subspace of V;

existence ex b

proof end;

theorem :: ZMODUL01:47

theorem :: ZMODUL01:48

for V being strict Z_Module

for W being strict Submodule of V st ( for v being Vector of V holds

( v in W iff v in V ) ) holds

W = V

for W being strict Submodule of V st ( for v being Vector of V holds

( v in W iff v in V ) ) holds

W = V

proof end;

theorem :: ZMODUL01:49

for V being Z_Module

for V1 being Subset of V

for W being Submodule of V st the carrier of W = V1 holds

V1 is linearly-closed by VECTSP_4:33;

for V1 being Subset of V

for W being Submodule of V st the carrier of W = V1 holds

V1 is linearly-closed by VECTSP_4:33;

theorem :: ZMODUL01:50

for V being Z_Module

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

ex W being strict Submodule of V st V1 = the carrier of W by VECTSP_4:34;

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

ex W being strict Submodule of V st V1 = the carrier of W by VECTSP_4:34;

theorem :: ZMODUL01:51

theorem :: ZMODUL01:52

theorem :: ZMODUL01:53

theorem :: ZMODUL01:55

for V being Z_Module

for W1, W2 being Submodule of V holds (0). W1 is Submodule of W2 by VECTSP_4:40;

for W1, W2 being Submodule of V holds (0). W1 is Submodule of W2 by VECTSP_4:40;

definition
end;

theorem :: ZMODUL01:57

theorem :: ZMODUL01:59

theorem :: ZMODUL01:60

theorem :: ZMODUL01:61

theorem :: ZMODUL01:62

theorem :: ZMODUL01:63

theorem :: ZMODUL01:64

theorem :: ZMODUL01:65

theorem :: ZMODUL01:66

theorem :: ZMODUL01:67

theorem :: ZMODUL01:68

theorem :: ZMODUL01:69

theorem :: ZMODUL01:70

theorem :: ZMODUL01:71

theorem :: ZMODUL01:72

for V being Z_Module

for u, v being Vector of V

for W being Submodule of V holds

( u in v + W iff ex v1 being Vector of V st

( v1 in W & u = v + v1 ) )

for u, v being Vector of V

for W being Submodule of V holds

( u in v + W iff ex v1 being Vector of V st

( v1 in W & u = v + v1 ) )

proof end;

theorem :: ZMODUL01:73

theorem :: ZMODUL01:74

theorem :: ZMODUL01:75

theorem :: ZMODUL01:76

theorem :: ZMODUL01:77

theorem :: ZMODUL01:78

theorem :: ZMODUL01:79

for V being Z_Module

for W being Submodule of V

for C being Coset of W holds

( C is linearly-closed iff C = the carrier of W ) by VECTSP_4:69;

for W being Submodule of V

for C being Coset of W holds

( C is linearly-closed iff C = the carrier of W ) by VECTSP_4:69;

theorem :: ZMODUL01:80

theorem :: ZMODUL01:81

theorem :: ZMODUL01:82

theorem :: ZMODUL01:83

for V being Z_Module

for W being Submodule of V holds the carrier of W is Coset of W by VECTSP_4:73;

for W being Submodule of V holds the carrier of W is Coset of W by VECTSP_4:73;

theorem :: ZMODUL01:84

theorem :: ZMODUL01:85

theorem :: ZMODUL01:86

theorem :: ZMODUL01:87

theorem :: ZMODUL01:88

theorem :: ZMODUL01:89

theorem :: ZMODUL01:90

theorem :: ZMODUL01:91

definition

let GF be non empty right_complementable associative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;

let M be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over GF;

let W1, W2 be Subspace of M;

:: original: +

redefine func W1 + W2 -> Subspace of M;

commutativity

for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1 by VECTSP_5:5;

end;
let M be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over GF;

let W1, W2 be Subspace of M;

:: original: +

redefine func W1 + W2 -> Subspace of M;

commutativity

for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1 by VECTSP_5:5;

theorem :: ZMODUL01:93

Lm6: for V being Z_Module

for W1, W2 being Submodule of V holds the carrier of W1 c= the carrier of (W1 + W2)

proof end;

theorem :: ZMODUL01:95

theorem :: ZMODUL01:96

theorem :: ZMODUL01:97

for V being Z_Module

for W1, W2 being Submodule of V holds W1 is Submodule of W1 + W2 by VECTSP_5:7;

for W1, W2 being Submodule of V holds W1 is Submodule of W1 + W2 by VECTSP_5:7;

theorem :: ZMODUL01:100

theorem :: ZMODUL01:103

theorem :: ZMODUL01:104

Lm8: for V being Z_Module

for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of W1

proof end;

theorem :: ZMODUL01:105

for V being Z_Module

for W1, W2 being Submodule of V holds W1 /\ W2 is Submodule of W1 by VECTSP_5:15;

for W1, W2 being Submodule of V holds W1 /\ W2 is Submodule of W1 by VECTSP_5:15;

theorem :: ZMODUL01:110

Lm9: for V being Z_Module

for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)

proof end;

theorem :: ZMODUL01:111

Lm10: for V being Z_Module

for W1, W2 being Submodule of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2

proof end;

theorem :: ZMODUL01:112

Lm11: for V being Z_Module

for W1, W2 being Submodule of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1

proof end;

theorem :: ZMODUL01:113

Lm12: for V being Z_Module

for W1, W2, W3 being Submodule of V holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))

proof end;

theorem :: ZMODUL01:114

Lm13: for V being Z_Module

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

the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))

by VECTSP_5:27;

theorem :: ZMODUL01:115

Lm14: for V being Z_Module

for W1, W2, W3 being Submodule of V holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))

proof end;

theorem :: ZMODUL01:116

Lm15: for V being Z_Module

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

the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))

proof end;

theorem :: ZMODUL01:117

theorem :: ZMODUL01:118

theorem :: ZMODUL01:119

for V being Z_Module

for W1, W2 being strict Submodule of V holds

( W1 + W2 = W2 iff W1 /\ W2 = W1 )

for W1, W2 being strict Submodule of V holds

( W1 + W2 = W2 iff W1 /\ W2 = W1 )

proof end;

theorem :: ZMODUL01:120

theorem :: ZMODUL01:121

notation

let GF be non empty right_complementable associative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;

let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over GF;

synonym Submodules V for Subspaces V;

end;
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over GF;

synonym Submodules V for Subspaces V;

Lm16: for V being Z_Module

for W being strict Submodule of V st ( for v being Vector of V holds v in W ) holds

W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)

proof end;

Lm17: for V being Z_Module

for W1, W2 being Submodule of V holds

( W1 + W2 = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) iff for v being Vector of V ex v1, v2 being Vector of V st

( v1 in W1 & v2 in W2 & v = v1 + v2 ) )

proof end;

definition

let V be Z_Module;

let W be Submodule of V;

end;
let W be Submodule of V;

attr W is with_Linear_Compl means :: ZMODUL01:def 17

ex C being Submodule of V st V is_the_direct_sum_of C,W;

ex C being Submodule of V st V is_the_direct_sum_of C,W;

:: deftheorem defines with_Linear_Compl ZMODUL01:def 17 :

for V being Z_Module

for W being Submodule of V holds

( W is with_Linear_Compl iff ex C being Submodule of V st V is_the_direct_sum_of C,W );

for V being Z_Module

for W being Submodule of V holds

( W is with_Linear_Compl iff ex C being Submodule of V st V is_the_direct_sum_of C,W );

registration

let V be Z_Module;

existence

ex b_{1} being Submodule of V st b_{1} is with_Linear_Compl ;

end;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V140() V141() V142() V143() vector-distributive scalar-distributive scalar-associative scalar-unital with_Linear_Compl for Subspace of V;

correctness existence

ex b

proof end;

definition

let V be Z_Module;

let W be Submodule of V;

assume A1: W is with_Linear_Compl ;

ex b_{1} being Submodule of V st V is_the_direct_sum_of b_{1},W
by A1;

end;
let W be Submodule of V;

assume A1: W is with_Linear_Compl ;

mode Linear_Compl of W -> Submodule of V means :Def19: :: ZMODUL01:def 18

V is_the_direct_sum_of it,W;

existence V is_the_direct_sum_of it,W;

ex b

:: deftheorem Def19 defines Linear_Compl ZMODUL01:def 18 :

for V being Z_Module

for W being Submodule of V st W is with_Linear_Compl holds

for b_{3} being Submodule of V holds

( b_{3} is Linear_Compl of W iff V is_the_direct_sum_of b_{3},W );

for V being Z_Module

for W being Submodule of V st W is with_Linear_Compl holds

for b

( b

theorem :: ZMODUL01:123

for V being Z_Module

for W1, W2 being Submodule of V st V is_the_direct_sum_of W1,W2 holds

W2 is Linear_Compl of W1

for W1, W2 being Submodule of V st V is_the_direct_sum_of W1,W2 holds

W2 is Linear_Compl of W1

proof end;

theorem Th124: :: ZMODUL01:124

for V being Z_Module

for W being with_Linear_Compl Submodule of V

for L being Linear_Compl of W holds

( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L )

for W being with_Linear_Compl Submodule of V

for L being Linear_Compl of W holds

( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L )

proof end;

theorem :: ZMODUL01:125

for V being Z_Module

for W being with_Linear_Compl Submodule of V

for L being Linear_Compl of W holds W + L = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)

for W being with_Linear_Compl Submodule of V

for L being Linear_Compl of W holds W + L = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)

proof end;

theorem :: ZMODUL01:126

for V being Z_Module

for W being with_Linear_Compl Submodule of V

for L being Linear_Compl of W holds W /\ L = (0). V

for W being with_Linear_Compl Submodule of V

for L being Linear_Compl of W holds W /\ L = (0). V

proof end;

theorem :: ZMODUL01:127

for V being Z_Module

for W1, W2 being Submodule of V st V is_the_direct_sum_of W1,W2 holds

V is_the_direct_sum_of W2,W1 by VECTSP_5:41;

for W1, W2 being Submodule of V st V is_the_direct_sum_of W1,W2 holds

V is_the_direct_sum_of W2,W1 by VECTSP_5:41;

theorem :: ZMODUL01:128

for V being Z_Module

for W being with_Linear_Compl Submodule of V

for L being Linear_Compl of W holds W is Linear_Compl of L

for W being with_Linear_Compl Submodule of V

for L being Linear_Compl of W holds W is Linear_Compl of L

proof end;

theorem Th129: :: ZMODUL01:129

for V being Z_Module holds

( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V )

( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V )

proof end;

theorem :: ZMODUL01:130

for V being Z_Module holds

( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V )

( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V )

proof end;

theorem :: ZMODUL01:131

Lm18: for V being Z_Module

for W being Submodule of V

for v being Vector of V ex C being Coset of W st v in C

proof end;

theorem :: ZMODUL01:132

theorem :: ZMODUL01:133

theorem :: ZMODUL01:134

theorem :: ZMODUL01:135

for V being Z_Module

for W1, W2 being Submodule of V st V = W1 + W2 & ex v being Vector of V st

for v1, v2, u1, u2 being Vector of V st v1 + v2 = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 ) holds

V is_the_direct_sum_of W1,W2

for W1, W2 being Submodule of V st V = W1 + W2 & ex v being Vector of V st

for v1, v2, u1, u2 being Vector of V st v1 + v2 = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 ) holds

V is_the_direct_sum_of W1,W2

proof end;

definition
end;

theorem Th136: :: ZMODUL01:136

for V being Z_Module

for W1, W2 being Submodule of V

for v being Vector of V st V is_the_direct_sum_of W1,W2 holds

(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 by VECTSP_5:50;

for W1, W2 being Submodule of V

for v being Vector of V st V is_the_direct_sum_of W1,W2 holds

(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 by VECTSP_5:50;

theorem Th137: :: ZMODUL01:137

for V being Z_Module

for W1, W2 being Submodule of V

for v being Vector of V st V is_the_direct_sum_of W1,W2 holds

(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 by VECTSP_5:51;

for W1, W2 being Submodule of V

for v being Vector of V st V is_the_direct_sum_of W1,W2 holds

(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 by VECTSP_5:51;

theorem :: ZMODUL01:138

for V being Z_Module

for W being with_Linear_Compl Submodule of V

for L being Linear_Compl of W

for v being Vector of V

for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds

t = v |-- (W,L)

for W being with_Linear_Compl Submodule of V

for L being Linear_Compl of W

for v being Vector of V

for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds

t = v |-- (W,L)

proof end;

theorem :: ZMODUL01:139

for V being Z_Module

for W being with_Linear_Compl Submodule of V

for L being Linear_Compl of W

for v being Vector of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v

for W being with_Linear_Compl Submodule of V

for L being Linear_Compl of W

for v being Vector of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v

proof end;

theorem :: ZMODUL01:140

for V being Z_Module

for W being with_Linear_Compl Submodule of V

for L being Linear_Compl of W

for v being Vector of V holds

( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )

for W being with_Linear_Compl Submodule of V

for L being Linear_Compl of W

for v being Vector of V holds

( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )

proof end;

theorem :: ZMODUL01:141

theorem :: ZMODUL01:142

theorem Th143: :: ZMODUL01:143

for V being Z_Module holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice by VECTSP_5:57;

registration

let V be Z_Module;

coherence

LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice-like by Th143;

end;
coherence

LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice-like by Th143;

theorem Th144: :: ZMODUL01:144

for V being Z_Module holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is lower-bounded by VECTSP_5:58;

theorem Th145: :: ZMODUL01:145

for V being Z_Module holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is upper-bounded by VECTSP_5:59;

theorem :: ZMODUL01:147

for V being Z_Module holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is modular by VECTSP_5:61;

theorem :: ZMODUL01:148

for V being Z_Module

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

W1 /\ W3 is Submodule of W2 /\ W3

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

W1 /\ W3 is Submodule of W2 /\ W3

proof end;

theorem :: ZMODUL01:149

theorem :: ZMODUL01:150

definition

let AG be non empty addLoopStr ;

ex b_{1} being Function of [: the carrier of INT.Ring, the carrier of AG:], the carrier of AG st

for i being Element of INT.Ring

for a being Element of AG holds

( ( i >= 0 implies b_{1} . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies b_{1} . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) )

for b_{1}, b_{2} being Function of [: the carrier of INT.Ring, the carrier of AG:], the carrier of AG st ( for i being Element of INT.Ring

for a being Element of AG holds

( ( i >= 0 implies b_{1} . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies b_{1} . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) ) & ( for i being Element of INT.Ring

for a being Element of AG holds

( ( i >= 0 implies b_{2} . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies b_{2} . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) ) holds

b_{1} = b_{2}

end;
func Int-mult-left AG -> Function of [: the carrier of INT.Ring, the carrier of AG:], the carrier of AG means :Def23: :: ZMODUL01:def 20

for i being Element of INT.Ring

for a being Element of AG holds

( ( i >= 0 implies it . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies it . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) );

existence for i being Element of INT.Ring

for a being Element of AG holds

( ( i >= 0 implies it . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies it . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) );

ex b

for i being Element of INT.Ring

for a being Element of AG holds

( ( i >= 0 implies b

proof end;

uniqueness for b

for a being Element of AG holds

( ( i >= 0 implies b

for a being Element of AG holds

( ( i >= 0 implies b

b

proof end;

:: deftheorem Def23 defines Int-mult-left ZMODUL01:def 20 :

for AG being non empty addLoopStr

for b_{2} being Function of [: the carrier of INT.Ring, the carrier of AG:], the carrier of AG holds

( b_{2} = Int-mult-left AG iff for i being Element of INT.Ring

for a being Element of AG holds

( ( i >= 0 implies b_{2} . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies b_{2} . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) );

for AG being non empty addLoopStr

for b

( b

for a being Element of AG holds

( ( i >= 0 implies b

theorem :: ZMODUL01:151

theorem Th152: :: ZMODUL01:152

for R being non empty addLoopStr

for a being Element of R

for i being Integer st i = 0 holds

(Int-mult-left R) . (i,a) = 0. R

for a being Element of R

for i being Integer st i = 0 holds

(Int-mult-left R) . (i,a) = 0. R

proof end;

theorem Th153: :: ZMODUL01:153

for R being non empty right_complementable add-associative right_zeroed addLoopStr

for i being Element of NAT holds (Nat-mult-left R) . (i,(0. R)) = 0. R

for i being Element of NAT holds (Nat-mult-left R) . (i,(0. R)) = 0. R

proof end;

theorem Th154: :: ZMODUL01:154

for R being non empty right_complementable add-associative right_zeroed addLoopStr

for i being Element of INT.Ring holds (Int-mult-left R) . (i,(0. R)) = 0. R

for i being Element of INT.Ring holds (Int-mult-left R) . (i,(0. R)) = 0. R

proof end;

theorem Th155: :: ZMODUL01:155

for R being non empty right_zeroed addLoopStr

for a being Element of R

for i being Integer st i = 1 holds

(Int-mult-left R) . (i,a) = a

for a being Element of R

for i being Integer st i = 1 holds

(Int-mult-left R) . (i,a) = a

proof end;

theorem Th156: :: ZMODUL01:156

for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for a being Element of R

for i, j, k being Element of NAT st i <= j & k = j - i holds

(Nat-mult-left R) . (k,a) = ((Nat-mult-left R) . (j,a)) - ((Nat-mult-left R) . (i,a))

for a being Element of R

for i, j, k being Element of NAT st i <= j & k = j - i holds

(Nat-mult-left R) . (k,a) = ((Nat-mult-left R) . (j,a)) - ((Nat-mult-left R) . (i,a))

proof end;

theorem Th157: :: ZMODUL01:157

for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for a being Element of R

for i being Element of NAT holds - ((Nat-mult-left R) . (i,a)) = (Nat-mult-left R) . (i,(- a))

for a being Element of R

for i being Element of NAT holds - ((Nat-mult-left R) . (i,a)) = (Nat-mult-left R) . (i,(- a))

proof end;

theorem Th158: :: ZMODUL01:158

for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for a being Element of R

for i, j being Element of INT.Ring st i in NAT & not j in NAT holds

(Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))

for a being Element of R

for i, j being Element of INT.Ring st i in NAT & not j in NAT holds

(Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))

proof end;

theorem Th159: :: ZMODUL01:159

for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for a being Element of R

for i, j being Element of INT.Ring holds (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))

for a being Element of R

for i, j being Element of INT.Ring holds (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))

proof end;

theorem Th160: :: ZMODUL01:160

for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for a, b being Element of R

for i being Element of NAT holds (Nat-mult-left R) . (i,(a + b)) = ((Nat-mult-left R) . (i,a)) + ((Nat-mult-left R) . (i,b))

for a, b being Element of R

for i being Element of NAT holds (Nat-mult-left R) . (i,(a + b)) = ((Nat-mult-left R) . (i,a)) + ((Nat-mult-left R) . (i,b))

proof end;

theorem Th161: :: ZMODUL01:161

for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for a, b being Element of R

for i being Element of INT.Ring holds (Int-mult-left R) . (i,(a + b)) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b))

for a, b being Element of R

for i being Element of INT.Ring holds (Int-mult-left R) . (i,(a + b)) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b))

proof end;

theorem Th162: :: ZMODUL01:162

for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for a being Element of R

for i, j being Element of NAT holds (Nat-mult-left R) . ((i * j),a) = (Nat-mult-left R) . (i,((Nat-mult-left R) . (j,a)))

for a being Element of R

for i, j being Element of NAT holds (Nat-mult-left R) . ((i * j),a) = (Nat-mult-left R) . (i,((Nat-mult-left R) . (j,a)))

proof end;

Lm19: for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for a being Element of R

for i, j being Element of INT.Ring st i <> 0 & j <> 0 holds

(Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))

proof end;

Lm20: for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for a being Element of R

for i, j being Element of INT.Ring st ( i = 0 or j = 0 ) holds

(Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))

proof end;

theorem Th163: :: ZMODUL01:163

for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for a being Element of R

for i, j being Element of INT.Ring holds (Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))

for a being Element of R

for i, j being Element of INT.Ring holds (Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))

proof end;

theorem :: ZMODUL01:164

for AG being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds ModuleStr(# the carrier of AG, the addF of AG, the ZeroF of AG,(Int-mult-left AG) #) is Z_Module

proof end;