:: RMOD_4 semantic presentation

Lm1: for R being Ring
for V being RightMod of R
for v being Vector of V
for F, G being FinSequence of the carrier 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 the carrier 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 the carrier 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

proof end;

theorem :: RMOD_4:3

for R being Ring
for V being RightMod of R
for a being Scalar of R
for v, u 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 v, u, 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;
canceled;
canceled;
func Sum T -> Vector of V means :Def3: :: RMOD_4:def 3
ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & it = Sum F );
existence

proof end;

uniqueness by RLVECT_1:59;

end;

:: deftheorem RMOD_4:def 1 :

:: deftheorem RMOD_4:def 2 :

:: deftheorem Def3 defines Sum RMOD_4:def 3 :

theorem Th5: :: RMOD_4:5

for R being Ring
for V being RightMod of R holds Sum ({} V) = 0. V

proof end;

theorem :: RMOD_4:6

for R being Ring
for V being RightMod of R
for v being Vector of V holds Sum {v} = v

proof end;

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

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

proof end;

theorem Th9: :: RMOD_4:9

for R being Ring
for V being RightMod of R
for T, S 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 T, S 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 T, S 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 T, S 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 T, S 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 T, S being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))

proof end;

theorem :: RMOD_4:15

for R being Ring
for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \+\ S) = (Sum (T \ S)) + (Sum (S \ T))

proof end;

definition

let R be Ring;
let V be RightMod of R;
mode Linear_Combination of V -> Element of Funcs the carrier of V,the carrier of R means :Def4: :: RMOD_4:def 4
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

proof end;

end;

:: deftheorem Def4 defines Linear_Combination RMOD_4:def 4 :

definition

let R be Ring;
let V be RightMod of R;
let L be Linear_Combination of V;
func Carrier L -> finite Subset of V equals :: RMOD_4:def 5
{ v where v is Vector of V : L . v <> 0. R } ;
coherence

proof end;

end;

:: deftheorem defines Carrier RMOD_4:def 5 :

theorem :: RMOD_4:16

canceled;

theorem :: RMOD_4:17

canceled;

theorem :: RMOD_4:18

canceled;

theorem :: RMOD_4:19

for R being Ring
for V being RightMod of R
for x being set
for L being Linear_Combination of V holds
( x in Carrier L iff ex v being Vector of V st
( x = v & L . v <> 0. R ) ) ;

theorem :: RMOD_4:20

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 )

proof end;

definition

let R be Ring;
let V be RightMod of R;
func ZeroLC V -> Linear_Combination of V means :Def6: :: RMOD_4:def 6
Carrier it = {} ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines ZeroLC RMOD_4:def 6 :

theorem :: RMOD_4:21

canceled;

theorem Th22: :: RMOD_4:22

for R being Ring
for V being RightMod of R
for v being Vector of V holds (ZeroLC V) . v = 0. R

proof end;

definition

let R be Ring;
let V be RightMod of R;
let A be Subset of V;
mode Linear_Combination of A -> Linear_Combination of V means :Def7: :: RMOD_4:def 7
Carrier it c= A;
existence

proof end;

end;

:: deftheorem Def7 defines Linear_Combination RMOD_4:def 7 :

theorem :: RMOD_4:23

canceled;

theorem :: RMOD_4:24

canceled;

theorem :: RMOD_4:25

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

proof end;

theorem Th26: :: RMOD_4:26

for R being Ring
for V being RightMod of R
for A being Subset of V holds ZeroLC V is Linear_Combination of A

proof end;

theorem Th27: :: RMOD_4:27

for R being Ring
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:28

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

definition

let R be Ring;
let V be RightMod of R;
let F be FinSequence of the carrier of V;
let f be Function of the carrier of V,the carrier of R;
func f (#) F -> FinSequence of the carrier of V means :Def8: :: RMOD_4:def 8
( len it = len F & ( for i being Nat st i in dom it holds
it . i = (F /. i) * (f . (F /. i)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines (#) RMOD_4:def 8 :

theorem :: RMOD_4:29

canceled;

theorem :: RMOD_4:30

canceled;

theorem :: RMOD_4:31

canceled;

theorem Th32: :: RMOD_4:32

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 the carrier of V
for f being Function of the carrier of V,the carrier of R st i in dom F & v = F . i holds
(f (#) F) . i = v * (f . v)

proof end;

theorem :: RMOD_4:33

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

proof end;

theorem Th34: :: RMOD_4:34

for R being Ring
for V being RightMod of R
for v being Vector of V
for f being Function of the carrier of V,the carrier of R holds f (#) <*v*> = <*(v * (f . v))*>

proof end;

theorem Th35: :: RMOD_4:35

for R being Ring
for V being RightMod of R
for v1, v2 being Vector of V
for f being Function of the carrier of V,the carrier of R holds f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*>

proof end;

theorem :: RMOD_4:36

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

proof end;

theorem Th37: :: RMOD_4:37

for R being Ring
for V being RightMod of R
for F, G being FinSequence of the carrier of V
for f being Function of the carrier of V,the carrier of 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;
func Sum L -> Vector of V means :Def9: :: RMOD_4:def 9
ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Sum RMOD_4:def 9 :

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

proof end;

theorem :: RMOD_4:38

canceled;

theorem :: RMOD_4:39

canceled;

theorem :: RMOD_4:40

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 lineary-closed ) iff for l being Linear_Combination of A holds Sum l in A )

proof end;

theorem :: RMOD_4:41

for R being Ring
for V being RightMod of R holds Sum (ZeroLC V) = 0. V by Lm3;

theorem :: RMOD_4:42

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

proof end;

theorem Th43: :: RMOD_4:43

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)

proof end;

theorem Th44: :: RMOD_4:44

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

proof end;

theorem :: RMOD_4:45

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

proof end;

theorem :: RMOD_4:46

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)

proof end;

theorem :: RMOD_4:47

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

proof end;

definition

let R be Ring;
let V be RightMod of R;
let L1, L2 be Linear_Combination of V;
:: original: =
redefine pred L1 = L2 means :: RMOD_4:def 10
for v being Vector of V holds L1 . v = L2 . v;
compatibility by FUNCT_2:113;

end;

:: deftheorem defines = RMOD_4:def 10 :

definition

let R be Ring;
let V be RightMod of R;
let L1, L2 be Linear_Combination of V;
func L1 + L2 -> Linear_Combination of V means :Def11: :: RMOD_4:def 11
for v being Vector of V holds it . v = (L1 . v) + (L2 . v);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines + RMOD_4:def 11 :

theorem :: RMOD_4:48

canceled;

theorem :: RMOD_4:49

canceled;

theorem :: RMOD_4:50

canceled;

theorem Th51: :: RMOD_4:51

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)

proof end;

theorem Th52: :: RMOD_4:52

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

proof end;

theorem Th53: :: RMOD_4:53

for R being comRing
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1

proof end;

theorem :: RMOD_4:54

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

proof end;

theorem :: RMOD_4:55

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 )

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;
func L * a -> Linear_Combination of V means :Def12: :: RMOD_4:def 12
for v being Vector of V holds it . v = (L . v) * a;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines * RMOD_4:def 12 :

theorem :: RMOD_4:56

canceled;

theorem :: RMOD_4:57

canceled;

theorem Th58: :: RMOD_4:58

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

proof end;

theorem Th59: :: RMOD_4:59

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

proof end;

theorem Th60: :: RMOD_4:60

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

proof end;

theorem Th61: :: RMOD_4:61

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

proof end;

theorem :: RMOD_4:62

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)

proof end;

theorem :: RMOD_4:63

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)

proof end;

theorem Th64: :: RMOD_4:64

for R being Ring
for V being RightMod of R
for b, a being Scalar of R
for L being Linear_Combination of V holds (L * b) * a = L * (b * a)

proof end;

theorem :: RMOD_4:65

for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds L * (1. R) = L

proof end;

definition

let R be Ring;
let V be RightMod of R;
let L be Linear_Combination of V;
func - L -> Linear_Combination of V equals :: RMOD_4:def 13
L * (- (1. R));
correctness ;
involutiveness

proof end;

end;

:: deftheorem defines - RMOD_4:def 13 :

theorem :: RMOD_4:66

canceled;

theorem Th67: :: RMOD_4:67

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)

proof end;

theorem :: RMOD_4:68

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

proof end;

theorem Th69: :: RMOD_4:69

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

proof end;

theorem Th70: :: RMOD_4:70

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

definition

let R be Ring;
let V be RightMod of R;
let L1, L2 be Linear_Combination of V;
func L1 - L2 -> Linear_Combination of V equals :: RMOD_4:def 14
L1 + (- L2);
correctness ;

end;

:: deftheorem defines - RMOD_4:def 14 :

theorem :: RMOD_4:71

canceled;

theorem :: RMOD_4:72

canceled;

theorem Th73: :: RMOD_4:73

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)

proof end;

theorem :: RMOD_4:74

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)

proof end;

theorem :: RMOD_4:75

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

proof end;

theorem :: RMOD_4:76

for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds L - L = ZeroLC V

proof end;

theorem Th77: :: RMOD_4:77

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)

proof end;

theorem Th78: :: RMOD_4:78

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

proof end;

theorem Th79: :: RMOD_4:79

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

proof end;

theorem :: RMOD_4:80

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)

proof end;