:: by Michal Muzalewski and Wojciech Skaba

::

:: Received October 22, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

Lm1: for R being Ring

for V being RightMod of R

for v being Vector of V

for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds

Sum F = (Sum G) + v

proof end;

theorem Th1: :: RMOD_4:1

for R being Ring

for V being RightMod of R

for a being Scalar of R

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 = v * a ) holds

Sum F = (Sum G) * a

for V being RightMod of R

for a being Scalar of R

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 = v * a ) holds

Sum F = (Sum G) * a

proof end;

Lm2: for R being Ring

for V being RightMod of R

for a being Scalar of R

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

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

Sum G = (Sum F) * a

proof end;

theorem :: RMOD_4:2

for R being Ring

for V being RightMod of R

for a being Scalar of R holds (Sum (<*> the carrier of V)) * a = 0. V

for V being RightMod of R

for a being Scalar of R holds (Sum (<*> the carrier of V)) * a = 0. V

proof end;

theorem :: RMOD_4:3

for R being Ring

for V being RightMod of R

for a being Scalar of R

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

for V being RightMod of R

for a being Scalar of R

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

proof end;

theorem :: RMOD_4:4

for R being Ring

for V being RightMod of R

for a being Scalar of R

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

for V being RightMod of R

for a being Scalar of R

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

proof end;

definition

let R be Ring;

let V be RightMod of R;

let T be finite Subset of V;

ex b_{1} being Vector of V ex F being FinSequence of V st

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

for b_{1}, b_{2} being Vector of V st ex F being FinSequence of V st

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

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

b_{1} = b_{2}
by RLVECT_1:42;

end;
let V be RightMod of R;

let T be finite Subset of V;

func Sum T -> Vector of V means :Def1: :: RMOD_4:def 1

ex F being FinSequence of V st

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

existence ex F being FinSequence of V st

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

ex b

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

proof end;

uniqueness for b

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

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

b

:: deftheorem Def1 defines Sum RMOD_4:def 1 :

for R being Ring

for V being RightMod of R

for T being finite Subset of V

for b_{4} being Vector of V holds

( b_{4} = Sum T iff ex F being FinSequence of V st

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

for R being Ring

for V being RightMod of R

for T being finite Subset of V

for b

( b

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

theorem :: RMOD_4:7

for R being Ring

for V being RightMod of R

for v1, v2 being Vector of V st v1 <> v2 holds

Sum {v1,v2} = v1 + v2

for V being RightMod of R

for v1, v2 being Vector of V st v1 <> v2 holds

Sum {v1,v2} = v1 + v2

proof end;

theorem :: RMOD_4:8

for R being Ring

for V being RightMod of R

for v1, v2, v3 being Vector of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds

Sum {v1,v2,v3} = (v1 + v2) + v3

for V being RightMod of R

for v1, v2, v3 being Vector of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds

Sum {v1,v2,v3} = (v1 + v2) + v3

proof end;

theorem Th9: :: RMOD_4:9

for R being Ring

for V being RightMod of R

for S, T being finite Subset of V st T misses S holds

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

for V being RightMod of R

for S, T being finite Subset of V st T misses S holds

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

proof end;

theorem Th10: :: RMOD_4:10

for R being Ring

for V being RightMod of R

for S, T being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))

for V being RightMod of R

for S, T being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))

proof end;

theorem :: RMOD_4:11

for R being Ring

for V being RightMod of R

for S, T being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S))

for V being RightMod of R

for S, T being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S))

proof end;

theorem Th12: :: RMOD_4:12

for R being Ring

for V being RightMod of R

for S, T being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S)

for V being RightMod of R

for S, T being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S)

proof end;

theorem Th13: :: RMOD_4:13

for R being Ring

for V being RightMod of R

for S, T being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S))

for V being RightMod of R

for S, T being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S))

proof end;

theorem :: RMOD_4:14

for R being Ring

for V being RightMod of R

for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))

for V being RightMod of R

for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))

proof end;

theorem :: RMOD_4:15

definition

let R be Ring;

let V be RightMod of R;

ex b_{1} being Element of Funcs ( the carrier of V, the carrier of R) ex T being finite Subset of V st

for v being Vector of V st not v in T holds

b_{1} . v = 0. R

end;
let V be RightMod of R;

mode Linear_Combination of V -> Element of Funcs ( the carrier of V, the carrier of R) means :Def2: :: RMOD_4:def 2

ex T being finite Subset of V st

for v being Vector of V st not v in T holds

it . v = 0. R;

existence ex T being finite Subset of V st

for v being Vector of V st not v in T holds

it . v = 0. R;

ex b

for v being Vector of V st not v in T holds

b

proof end;

:: deftheorem Def2 defines Linear_Combination RMOD_4:def 2 :

for R being Ring

for V being RightMod of R

for b_{3} being Element of Funcs ( the carrier of V, the carrier of R) holds

( b_{3} is Linear_Combination of V iff ex T being finite Subset of V st

for v being Vector of V st not v in T holds

b_{3} . v = 0. R );

for R being Ring

for V being RightMod of R

for b

( b

for v being Vector of V st not v in T holds

b

definition

let R be Ring;

let V be RightMod of R;

let L be Linear_Combination of V;

{ v where v is Vector of V : L . v <> 0. R } is finite Subset of V

end;
let V be RightMod of R;

let L be Linear_Combination of V;

func Carrier L -> finite Subset of V equals :: RMOD_4:def 3

{ v where v is Vector of V : L . v <> 0. R } ;

coherence { v where v is Vector of V : L . v <> 0. R } ;

{ v where v is Vector of V : L . v <> 0. R } is finite Subset of V

proof end;

:: deftheorem defines Carrier RMOD_4:def 3 :

for R being Ring

for V being RightMod of R

for L being Linear_Combination of V holds Carrier L = { v where v is Vector of V : L . v <> 0. R } ;

for R being Ring

for V being RightMod of R

for L being Linear_Combination of V holds Carrier L = { v where v is Vector of V : L . v <> 0. R } ;

theorem :: RMOD_4:16

theorem :: RMOD_4:17

for R being Ring

for V being RightMod of R

for v being Vector of V

for L being Linear_Combination of V holds

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

for V being RightMod of R

for v being Vector of V

for L being Linear_Combination of V holds

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

proof end;

definition

let R be Ring;

let V be RightMod of R;

existence

ex b_{1} being Linear_Combination of V st Carrier b_{1} = {}

for b_{1}, b_{2} being Linear_Combination of V st Carrier b_{1} = {} & Carrier b_{2} = {} holds

b_{1} = b_{2}

end;
let V be RightMod of R;

existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines ZeroLC RMOD_4:def 4 :

for R being Ring

for V being RightMod of R

for b_{3} being Linear_Combination of V holds

( b_{3} = ZeroLC V iff Carrier b_{3} = {} );

for R being Ring

for V being RightMod of R

for b

( b

definition

let R be Ring;

let V be RightMod of R;

let A be Subset of V;

ex b_{1} being Linear_Combination of V st Carrier b_{1} c= A

end;
let V be RightMod of R;

let A be Subset of V;

mode Linear_Combination of A -> Linear_Combination of V means :Def5: :: RMOD_4:def 5

Carrier it c= A;

existence Carrier it c= A;

ex b

proof end;

:: deftheorem Def5 defines Linear_Combination RMOD_4:def 5 :

for R being Ring

for V being RightMod of R

for A being Subset of V

for b_{4} being Linear_Combination of V holds

( b_{4} is Linear_Combination of A iff Carrier b_{4} c= A );

for R being Ring

for V being RightMod of R

for A being Subset of V

for b

( b

theorem Th19: :: RMOD_4:19

for R being Ring

for V being RightMod 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

for V being RightMod 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

proof end;

theorem Th20: :: RMOD_4:20

for R being Ring

for V being RightMod of R

for A being Subset of V holds ZeroLC V is Linear_Combination of A

for V being RightMod of R

for A being Subset of V holds ZeroLC V is Linear_Combination of A

proof end;

theorem Th21: :: RMOD_4:21

for R being Ring

for V being RightMod of R

for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V

for V being RightMod of R

for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V

proof end;

theorem :: RMOD_4:22

for R being Ring

for V being RightMod of R

for L being Linear_Combination of V holds L is Linear_Combination of Carrier L by Def5;

for V being RightMod of R

for L being Linear_Combination of V holds L is Linear_Combination of Carrier L by Def5;

definition

let R be Ring;

let V be RightMod of R;

let F be FinSequence of V;

let f be Function of V,R;

ex b_{1} being FinSequence of V st

( len b_{1} = len F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (F /. i) * (f . (F /. i)) ) )

for b_{1}, b_{2} being FinSequence of V st len b_{1} = len F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (F /. i) * (f . (F /. i)) ) & len b_{2} = len F & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = (F /. i) * (f . (F /. i)) ) holds

b_{1} = b_{2}

end;
let V be RightMod of R;

let F be FinSequence of V;

let f be Function of V,R;

func f (#) F -> FinSequence of V means :Def6: :: RMOD_4:def 6

( len it = len F & ( for i being Nat st i in dom it holds

it . i = (F /. i) * (f . (F /. i)) ) );

existence ( len it = len F & ( for i being Nat st i in dom it holds

it . i = (F /. i) * (f . (F /. i)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines (#) RMOD_4:def 6 :

for R being Ring

for V being RightMod of R

for F being FinSequence of V

for f being Function of V,R

for b_{5} being FinSequence of V holds

( b_{5} = f (#) F iff ( len b_{5} = len F & ( for i being Nat st i in dom b_{5} holds

b_{5} . i = (F /. i) * (f . (F /. i)) ) ) );

for R being Ring

for V being RightMod of R

for F being FinSequence of V

for f being Function of V,R

for b

( b

b

theorem Th23: :: RMOD_4:23

for R being Ring

for V being RightMod of R

for i being Nat

for v being Vector of V

for F being FinSequence of V

for f being Function of V,R st i in dom F & v = F . i holds

(f (#) F) . i = v * (f . v)

for V being RightMod of R

for i being Nat

for v being Vector of V

for F being FinSequence of V

for f being Function of V,R st i in dom F & v = F . i holds

(f (#) F) . i = v * (f . v)

proof end;

theorem :: RMOD_4:24

for R being Ring

for V being RightMod of R

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

for V being RightMod of R

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

proof end;

theorem Th25: :: RMOD_4:25

for R being Ring

for V being RightMod of R

for v being Vector of V

for f being Function of V,R holds f (#) <*v*> = <*(v * (f . v))*>

for V being RightMod of R

for v being Vector of V

for f being Function of V,R holds f (#) <*v*> = <*(v * (f . v))*>

proof end;

theorem Th26: :: RMOD_4:26

for R being Ring

for V being RightMod of R

for v1, v2 being Vector of V

for f being Function of V,R holds f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*>

for V being RightMod of R

for v1, v2 being Vector of V

for f being Function of V,R holds f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*>

proof end;

theorem :: RMOD_4:27

for R being Ring

for V being RightMod of R

for v1, v2, v3 being Vector of V

for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*>

for V being RightMod of R

for v1, v2, v3 being Vector of V

for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*>

proof end;

theorem Th28: :: RMOD_4:28

for R being Ring

for V being RightMod of R

for F, G being FinSequence of V

for f being Function of V,R holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)

for V being RightMod of R

for F, G being FinSequence of V

for f being Function of V,R holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)

proof end;

definition

let R be Ring;

let V be RightMod of R;

let L be Linear_Combination of V;

ex b_{1} being Vector of V ex F being FinSequence of V st

( F is one-to-one & rng F = Carrier L & b_{1} = Sum (L (#) F) )

for b_{1}, b_{2} being Vector of V st ex F being FinSequence of V st

( F is one-to-one & rng F = Carrier L & b_{1} = Sum (L (#) F) ) & ex F being FinSequence of V st

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

b_{1} = b_{2}

end;
let V be RightMod of R;

let L be Linear_Combination of V;

func Sum L -> Vector of V means :Def7: :: RMOD_4:def 7

ex F being FinSequence of V st

( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) );

existence ex F being FinSequence of V st

( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) );

ex b

( F is one-to-one & rng F = Carrier L & b

proof end;

uniqueness for b

( F is one-to-one & rng F = Carrier L & b

( F is one-to-one & rng F = Carrier L & b

b

proof end;

:: deftheorem Def7 defines Sum RMOD_4:def 7 :

for R being Ring

for V being RightMod of R

for L being Linear_Combination of V

for b_{4} being Vector of V holds

( b_{4} = Sum L iff ex F being FinSequence of V st

( F is one-to-one & rng F = Carrier L & b_{4} = Sum (L (#) F) ) );

for R being Ring

for V being RightMod of R

for L being Linear_Combination of V

for b

( b

( F is one-to-one & rng F = Carrier L & b

Lm3: for R being Ring

for V being RightMod of R holds Sum (ZeroLC V) = 0. V

proof end;

theorem Th29: :: RMOD_4:29

for R being Ring

for V being RightMod of R

for A being Subset of V st 0. R <> 1_ R holds

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

for V being RightMod of R

for A being Subset of V st 0. R <> 1_ R holds

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

proof end;

theorem Th31: :: RMOD_4:31

for R being Ring

for V being RightMod of R

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

for V being RightMod of R

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

proof end;

theorem Th32: :: RMOD_4:32

for R being Ring

for V being RightMod of R

for v being Vector of V

for l being Linear_Combination of {v} holds Sum l = v * (l . v)

for V being RightMod of R

for v being Vector of V

for l being Linear_Combination of {v} holds Sum l = v * (l . v)

proof end;

theorem Th33: :: RMOD_4:33

for R being Ring

for V being RightMod of R

for v1, v2 being Vector of V st v1 <> v2 holds

for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2))

for V being RightMod of R

for v1, v2 being Vector of V st v1 <> v2 holds

for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2))

proof end;

theorem :: RMOD_4:34

for R being Ring

for V being RightMod of R

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

Sum L = 0. V

for V being RightMod of R

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

Sum L = 0. V

proof end;

theorem Th35: :: RMOD_4:35

for R being Ring

for V being RightMod of R

for v being Vector of V

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

Sum L = v * (L . v)

for V being RightMod of R

for v being Vector of V

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

Sum L = v * (L . v)

proof end;

theorem :: RMOD_4:36

for R being Ring

for V being RightMod of R

for v1, v2 being Vector of V

for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds

Sum L = (v1 * (L . v1)) + (v2 * (L . v2))

for V being RightMod of R

for v1, v2 being Vector of V

for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds

Sum L = (v1 * (L . v1)) + (v2 * (L . v2))

proof end;

definition

let R be Ring;

let V be RightMod of R;

let L1, L2 be Linear_Combination of V;

( L1 = L2 iff for v being Vector of V holds L1 . v = L2 . v ) by FUNCT_2:63;

end;
let V be RightMod of R;

let L1, L2 be Linear_Combination of V;

:: original: =

redefine pred L1 = L2 means :: RMOD_4:def 8

for v being Vector of V holds L1 . v = L2 . v;

compatibility redefine pred L1 = L2 means :: RMOD_4:def 8

for v being Vector of V holds L1 . v = L2 . v;

( L1 = L2 iff for v being Vector of V holds L1 . v = L2 . v ) by FUNCT_2:63;

:: deftheorem defines = RMOD_4:def 8 :

for R being Ring

for V being RightMod of R

for L1, L2 being Linear_Combination of V holds

( L1 = L2 iff for v being Vector of V holds L1 . v = L2 . v );

for R being Ring

for V being RightMod of R

for L1, L2 being Linear_Combination of V holds

( L1 = L2 iff for v being Vector of V holds L1 . v = L2 . v );

definition

let R be Ring;

let V be RightMod of R;

let L1, L2 be Linear_Combination of V;

ex b_{1} being Linear_Combination of V st

for v being Vector of V holds b_{1} . v = (L1 . v) + (L2 . v)

for b_{1}, b_{2} being Linear_Combination of V st ( for v being Vector of V holds b_{1} . v = (L1 . v) + (L2 . v) ) & ( for v being Vector of V holds b_{2} . v = (L1 . v) + (L2 . v) ) holds

b_{1} = b_{2}

end;
let V be RightMod of R;

let L1, L2 be Linear_Combination of V;

func L1 + L2 -> Linear_Combination of V means :Def9: :: RMOD_4:def 9

for v being Vector of V holds it . v = (L1 . v) + (L2 . v);

existence for v being Vector of V holds it . v = (L1 . v) + (L2 . v);

ex b

for v being Vector of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines + RMOD_4:def 9 :

for R being Ring

for V being RightMod of R

for L1, L2, b_{5} being Linear_Combination of V holds

( b_{5} = L1 + L2 iff for v being Vector of V holds b_{5} . v = (L1 . v) + (L2 . v) );

for R being Ring

for V being RightMod of R

for L1, L2, b

( b

theorem Th37: :: RMOD_4:37

for R being Ring

for V being RightMod of R

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

for V being RightMod of R

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

proof end;

theorem Th38: :: RMOD_4:38

for R being Ring

for V being RightMod of R

for A being Subset of V

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

L1 + L2 is Linear_Combination of A

for V being RightMod of R

for A being Subset of V

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

L1 + L2 is Linear_Combination of A

proof end;

theorem Th39: :: RMOD_4:39

for R being comRing

for V being RightMod of R

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

for V being RightMod of R

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

proof end;

theorem :: RMOD_4:40

for R being Ring

for V being RightMod of R

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

for V being RightMod of R

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

proof end;

theorem :: RMOD_4:41

for R being comRing

for V being RightMod of R

for L being Linear_Combination of V holds

( L + (ZeroLC V) = L & (ZeroLC V) + L = L )

for V being RightMod of R

for L being Linear_Combination of V holds

( L + (ZeroLC V) = L & (ZeroLC V) + L = L )

proof end;

definition

let R be Ring;

let V be RightMod of R;

let a be Scalar of R;

let L be Linear_Combination of V;

ex b_{1} being Linear_Combination of V st

for v being Vector of V holds b_{1} . v = (L . v) * a

for b_{1}, b_{2} being Linear_Combination of V st ( for v being Vector of V holds b_{1} . v = (L . v) * a ) & ( for v being Vector of V holds b_{2} . v = (L . v) * a ) holds

b_{1} = b_{2}

end;
let V be RightMod of R;

let a be Scalar of R;

let L be Linear_Combination of V;

func L * a -> Linear_Combination of V means :Def10: :: RMOD_4:def 10

for v being Vector of V holds it . v = (L . v) * a;

existence for v being Vector of V holds it . v = (L . v) * a;

ex b

for v being Vector of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines * RMOD_4:def 10 :

for R being Ring

for V being RightMod of R

for a being Scalar of R

for L, b_{5} being Linear_Combination of V holds

( b_{5} = L * a iff for v being Vector of V holds b_{5} . v = (L . v) * a );

for R being Ring

for V being RightMod of R

for a being Scalar of R

for L, b

( b

theorem Th42: :: RMOD_4:42

for R being Ring

for V being RightMod of R

for a being Scalar of R

for L being Linear_Combination of V holds Carrier (L * a) c= Carrier L

for V being RightMod of R

for a being Scalar of R

for L being Linear_Combination of V holds Carrier (L * a) c= Carrier L

proof end;

theorem Th43: :: RMOD_4:43

for RR being domRing

for VV being RightMod of RR

for LL being Linear_Combination of VV

for aa being Scalar of RR st aa <> 0. RR holds

Carrier (LL * aa) = Carrier LL

for VV being RightMod of RR

for LL being Linear_Combination of VV

for aa being Scalar of RR st aa <> 0. RR holds

Carrier (LL * aa) = Carrier LL

proof end;

theorem Th44: :: RMOD_4:44

for R being Ring

for V being RightMod of R

for L being Linear_Combination of V holds L * (0. R) = ZeroLC V

for V being RightMod of R

for L being Linear_Combination of V holds L * (0. R) = ZeroLC V

proof end;

theorem Th45: :: RMOD_4:45

for R being Ring

for V being RightMod of R

for a being Scalar of R

for A being Subset of V

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

L * a is Linear_Combination of A

for V being RightMod of R

for a being Scalar of R

for A being Subset of V

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

L * a is Linear_Combination of A

proof end;

theorem :: RMOD_4:46

for R being Ring

for V being RightMod of R

for a, b being Scalar of R

for L being Linear_Combination of V holds L * (a + b) = (L * a) + (L * b)

for V being RightMod of R

for a, b being Scalar of R

for L being Linear_Combination of V holds L * (a + b) = (L * a) + (L * b)

proof end;

theorem :: RMOD_4:47

for R being Ring

for V being RightMod of R

for a being Scalar of R

for L1, L2 being Linear_Combination of V holds (L1 + L2) * a = (L1 * a) + (L2 * a)

for V being RightMod of R

for a being Scalar of R

for L1, L2 being Linear_Combination of V holds (L1 + L2) * a = (L1 * a) + (L2 * a)

proof end;

theorem Th48: :: RMOD_4:48

for R being Ring

for V being RightMod of R

for a, b being Scalar of R

for L being Linear_Combination of V holds (L * b) * a = L * (b * a)

for V being RightMod of R

for a, b being Scalar of R

for L being Linear_Combination of V holds (L * b) * a = L * (b * a)

proof end;

definition

let R be Ring;

let V be RightMod of R;

let L be Linear_Combination of V;

correctness

coherence

L * (- (1_ R)) is Linear_Combination of V;

;

involutiveness

for b_{1}, b_{2} being Linear_Combination of V st b_{1} = b_{2} * (- (1_ R)) holds

b_{2} = b_{1} * (- (1_ R))

end;
let V be RightMod of R;

let L be Linear_Combination of V;

correctness

coherence

L * (- (1_ R)) is Linear_Combination of V;

;

involutiveness

for b

b

proof end;

:: deftheorem defines - RMOD_4:def 11 :

for R being Ring

for V being RightMod of R

for L being Linear_Combination of V holds - L = L * (- (1_ R));

for R being Ring

for V being RightMod of R

for L being Linear_Combination of V holds - L = L * (- (1_ R));

theorem Th50: :: RMOD_4:50

for R being Ring

for V being RightMod of R

for v being Vector of V

for L being Linear_Combination of V holds (- L) . v = - (L . v)

for V being RightMod of R

for v being Vector of V

for L being Linear_Combination of V holds (- L) . v = - (L . v)

proof end;

theorem :: RMOD_4:51

for R being Ring

for V being RightMod of R

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

L2 = - L1

for V being RightMod of R

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

L2 = - L1

proof end;

theorem Th52: :: RMOD_4:52

for R being Ring

for V being RightMod of R

for L being Linear_Combination of V holds Carrier (- L) = Carrier L

for V being RightMod of R

for L being Linear_Combination of V holds Carrier (- L) = Carrier L

proof end;

theorem :: RMOD_4:53

for R being Ring

for V being RightMod of R

for A being Subset of V

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

- L is Linear_Combination of A by Th45;

for V being RightMod of R

for A being Subset of V

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

- L is Linear_Combination of A by Th45;

definition

let R be Ring;

let V be RightMod of R;

let L1, L2 be Linear_Combination of V;

correctness

coherence

L1 + (- L2) is Linear_Combination of V;

;

end;
let V be RightMod of R;

let L1, L2 be Linear_Combination of V;

correctness

coherence

L1 + (- L2) is Linear_Combination of V;

;

:: deftheorem defines - RMOD_4:def 12 :

for R being Ring

for V being RightMod of R

for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);

for R being Ring

for V being RightMod of R

for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);

theorem Th54: :: RMOD_4:54

for R being Ring

for V being RightMod of R

for v being Vector of V

for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)

for V being RightMod of R

for v being Vector of V

for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)

proof end;

theorem :: RMOD_4:55

for R being Ring

for V being RightMod of R

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

for V being RightMod of R

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

proof end;

theorem :: RMOD_4:56

for R being Ring

for V being RightMod of R

for A being Subset of V

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

L1 - L2 is Linear_Combination of A

for V being RightMod of R

for A being Subset of V

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

L1 - L2 is Linear_Combination of A

proof end;

theorem :: RMOD_4:57

for R being Ring

for V being RightMod of R

for L being Linear_Combination of V holds L - L = ZeroLC V

for V being RightMod of R

for L being Linear_Combination of V holds L - L = ZeroLC V

proof end;

theorem Th58: :: RMOD_4:58

for R being Ring

for V being RightMod of R

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

for V being RightMod of R

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

proof end;

theorem Th59: :: RMOD_4:59

for R being domRing

for V being RightMod of R

for L being Linear_Combination of V

for a being Scalar of R holds Sum (L * a) = (Sum L) * a

for V being RightMod of R

for L being Linear_Combination of V

for a being Scalar of R holds Sum (L * a) = (Sum L) * a

proof end;

theorem Th60: :: RMOD_4:60

for R being domRing

for V being RightMod of R

for L being Linear_Combination of V holds Sum (- L) = - (Sum L)

for V being RightMod of R

for L being Linear_Combination of V holds Sum (- L) = - (Sum L)

proof end;

theorem :: RMOD_4:61

for R being domRing

for V being RightMod of R

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

for V being RightMod of R

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

proof end;

definition

let R be Ring;

let V be RightMod of R;

let IT be Subset of V;

end;
let V be RightMod of R;

let IT be Subset of V;

attr IT is linearly-independent means :: RMOD_4:def 13

for l being Linear_Combination of IT st Sum l = 0. V holds

Carrier l = {} ;

for l being Linear_Combination of IT st Sum l = 0. V holds

Carrier l = {} ;

:: deftheorem defines linearly-independent RMOD_4:def 13 :

for R being Ring

for V being RightMod of R

for IT being Subset of V holds

( IT is linearly-independent iff for l being Linear_Combination of IT st Sum l = 0. V holds

Carrier l = {} );

for R being Ring

for V being RightMod of R

for IT being Subset of V holds

( IT is linearly-independent iff for l being Linear_Combination of IT st Sum l = 0. V holds

Carrier l = {} );

notation

let R be Ring;

let V be RightMod of R;

let IT be Subset of V;

antonym linearly-dependent IT for linearly-independent ;

end;
let V be RightMod of R;

let IT be Subset of V;

antonym linearly-dependent IT for linearly-independent ;

theorem :: RMOD_4:62

for R being Ring

for V being RightMod of R

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

A is linearly-independent

for V being RightMod of R

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

A is linearly-independent

proof end;

theorem Th63: :: RMOD_4:63

for R being Ring

for V being RightMod of R

for A being Subset of V st 0. R <> 1_ R & A is linearly-independent holds

not 0. V in A

for V being RightMod of R

for A being Subset of V st 0. R <> 1_ R & A is linearly-independent holds

not 0. V in A

proof end;

theorem Th65: :: RMOD_4:65

for R being Ring

for V being RightMod of R

for v1, v2 being Vector of V st 0. R <> 1_ R & {v1,v2} is linearly-independent holds

( v1 <> 0. V & v2 <> 0. V )

for V being RightMod of R

for v1, v2 being Vector of V st 0. R <> 1_ R & {v1,v2} is linearly-independent holds

( v1 <> 0. V & v2 <> 0. V )

proof end;

theorem :: RMOD_4:66

definition

let R be domRing;

let V be RightMod of R;

let A be Subset of V;

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

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

b_{1} = b_{2}
by RMOD_2:29;

end;
let V be RightMod of R;

let A be Subset of V;

func Lin A -> strict Submodule of V means :Def14: :: RMOD_4:def 14

the carrier of it = { (Sum l) where l is Linear_Combination of A : verum } ;

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

ex b

proof end;

uniqueness for b

b

:: deftheorem Def14 defines Lin RMOD_4:def 14 :

for R being domRing

for V being RightMod of R

for A being Subset of V

for b_{4} being strict Submodule of V holds

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

for R being domRing

for V being RightMod of R

for A being Subset of V

for b

( b

theorem Th67: :: RMOD_4:67

for x being set

for R being domRing

for V being RightMod of R

for A being Subset of V holds

( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )

for R being domRing

for V being RightMod of R

for A being Subset of V holds

( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )

proof end;

theorem Th68: :: RMOD_4:68

for x being set

for R being domRing

for V being RightMod of R

for A being Subset of V st x in A holds

x in Lin A

for R being domRing

for V being RightMod of R

for A being Subset of V st x in A holds

x in Lin A

proof end;

theorem :: RMOD_4:70

for R being domRing

for V being RightMod of R

for A being Subset of V holds

( not Lin A = (0). V or A = {} or A = {(0. V)} )

for V being RightMod of R

for A being Subset of V holds

( not Lin A = (0). V or A = {} or A = {(0. V)} )

proof end;

theorem Th71: :: RMOD_4:71

for R being domRing

for V being RightMod of R

for A being Subset of V

for W being strict Submodule of V st 0. R <> 1_ R & A = the carrier of W holds

Lin A = W

for V being RightMod of R

for A being Subset of V

for W being strict Submodule of V st 0. R <> 1_ R & A = the carrier of W holds

Lin A = W

proof end;

theorem :: RMOD_4:72

for R being domRing

for V being strict RightMod of R

for A being Subset of V st 0. R <> 1_ R & A = the carrier of V holds

Lin A = V

for V being strict RightMod of R

for A being Subset of V st 0. R <> 1_ R & A = the carrier of V holds

Lin A = V

proof end;

theorem Th73: :: RMOD_4:73

for R being domRing

for V being RightMod of R

for A, B being Subset of V st A c= B holds

Lin A is Submodule of Lin B

for V being RightMod of R

for A, B being Subset of V st A c= B holds

Lin A is Submodule of Lin B

proof end;

theorem :: RMOD_4:74

for R being domRing

for V being strict RightMod of R

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

Lin B = V

for V being strict RightMod of R

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

Lin B = V

proof end;

theorem :: RMOD_4:75

for R being domRing

for V being RightMod of R

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

for V being RightMod of R

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

proof end;

theorem :: RMOD_4:76

for R being domRing

for V being RightMod of R

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

for V being RightMod of R

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

proof end;