:: RMOD_4 semantic presentation

Lemma1: for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄, b₅ being FinSequence of the carrier of b₂ st len b₄ = (len b₅) + 1 & b₅ = b₄ | (Seg (len b₅)) & b₃ = b₄ . (len b₄) holds
Sum b₄ = (Sum b₅) + b₃

proof end;

theorem Th1: :: RMOD_4:1

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Scalar of b₁
for b₄, b₅ being FinSequence of the carrier of b₂ st len b₄ = len b₅ & ( for b₆ being Nat
for b₇ being Vector of b₂ st b₆ in dom b₄ & b₇ = b₅ . b₆ holds
b₄ . b₆ = b₇ * b₃ ) holds
Sum b₄ = (Sum b₅) * b₃

proof end;

Lemma3: for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Scalar of b₁
for b₄, b₅ being FinSequence of the carrier of b₂ st len b₄ = len b₅ & ( for b₆ being Nat st b₆ in dom b₄ holds
b₅ . b₆ = (b₄ /. b₆) * b₃ ) holds
Sum b₅ = (Sum b₄) * b₃

proof end;

theorem Th2: :: RMOD_4:2

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Scalar of b₁ holds (Sum (<*> the carrier of b₂)) * b₃ = 0. b₂

proof end;

theorem Th3: :: RMOD_4:3

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Scalar of b₁
for b₄, b₅ being Vector of b₂ holds (Sum <*b₄,b₅*>) * b₃ = (b₄ * b₃) + (b₅ * b₃)

proof end;

theorem Th4: :: RMOD_4:4

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Scalar of b₁
for b₄, b₅, b₆ being Vector of b₂ holds (Sum <*b₄,b₅,b₆*>) * b₃ = ((b₄ * b₃) + (b₅ * b₃)) + (b₆ * b₃)

proof end;

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃ be finite Subset of c₂;
canceled;
canceled;
func Sum c₃ -> Vector of a₂ means :Def3: :: RMOD_4:def 3
ex b₁ being FinSequence of the carrier of a₂ st
( rng b₁ = a₃ & b₁ is one-to-one & a₄ = Sum b₁ );
existence

proof end;

uniqueness by RLVECT_1:59;

end;

:: deftheorem Def1 RMOD_4:def 1 :

:: deftheorem Def2 RMOD_4:def 2 :

:: deftheorem Def3 defines Sum RMOD_4:def 3 :

theorem Th5: :: RMOD_4:5

for b₁ being Ring
for b₂ being RightMod of b₁ holds Sum ({} b₂) = 0. b₂

proof end;

theorem Th6: :: RMOD_4:6

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂ holds Sum {b₃} = b₃

proof end;

theorem Th7: :: RMOD_4:7

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂ st b₃ <> b₄ holds
Sum {b₃,b₄} = b₃ + b₄

proof end;

theorem Th8: :: RMOD_4:8

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄, b₅ being Vector of b₂ st b₃ <> b₄ & b₄ <> b₅ & b₃ <> b₅ holds
Sum {b₃,b₄,b₅} = (b₃ + b₄) + b₅

proof end;

theorem Th9: :: RMOD_4:9

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being finite Subset of b₂ st b₃ misses b₄ holds
Sum (b₃ \/ b₄) = (Sum b₃) + (Sum b₄)

proof end;

theorem Th10: :: RMOD_4:10

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being finite Subset of b₂ holds Sum (b₃ \/ b₄) = ((Sum b₃) + (Sum b₄)) - (Sum (b₃ /\ b₄))

proof end;

theorem Th11: :: RMOD_4:11

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being finite Subset of b₂ holds Sum (b₃ /\ b₄) = ((Sum b₃) + (Sum b₄)) - (Sum (b₃ \/ b₄))

proof end;

theorem Th12: :: RMOD_4:12

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being finite Subset of b₂ holds Sum (b₃ \ b₄) = (Sum (b₃ \/ b₄)) - (Sum b₄)

proof end;

theorem Th13: :: RMOD_4:13

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being finite Subset of b₂ holds Sum (b₃ \ b₄) = (Sum b₃) - (Sum (b₃ /\ b₄))

proof end;

theorem Th14: :: RMOD_4:14

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being finite Subset of b₂ holds Sum (b₃ \+\ b₄) = (Sum (b₃ \/ b₄)) - (Sum (b₃ /\ b₄))

proof end;

theorem Th15: :: RMOD_4:15

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being finite Subset of b₂ holds Sum (b₃ \+\ b₄) = (Sum (b₃ \ b₄)) + (Sum (b₄ \ b₃))

proof end;

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
mode Linear_Combination of c₂ -> Element of Funcs the carrier of a₂,the carrier of a₁ means :Def4: :: RMOD_4:def 4
ex b₁ being finite Subset of a₂ st
for b₂ being Vector of a₂ st not b₂ in b₁ holds
a₃ . b₂ = 0. a₁;
existence

proof end;

end;

:: deftheorem Def4 defines Linear_Combination RMOD_4:def 4 :

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃ be Linear_Combination of c₂;
func Carrier c₃ -> finite Subset of a₂ equals :: RMOD_4:def 5
{ b₁ where B is Vector of a₂ : a₃ . b₁ <> 0. a₁ } ;
coherence

proof end;

end;

:: deftheorem Def5 defines Carrier RMOD_4:def 5 :

theorem Th16: :: RMOD_4:16

canceled;

theorem Th17: :: RMOD_4:17

canceled;

theorem Th18: :: RMOD_4:18

canceled;

theorem Th19: :: RMOD_4:19

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being set
for b₄ being Linear_Combination of b₂ holds
( b₃ in Carrier b₄ iff ex b₅ being Vector of b₂ st
( b₃ = b₅ & b₄ . b₅ <> 0. b₁ ) ) ;

theorem Th20: :: RMOD_4:20

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Linear_Combination of b₂ holds
( b₄ . b₃ = 0. b₁ iff not b₃ in Carrier b₄ )

proof end;

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
func ZeroLC c₂ -> Linear_Combination of a₂ means :Def6: :: RMOD_4:def 6
Carrier a₃ = {} ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines ZeroLC RMOD_4:def 6 :

theorem Th21: :: RMOD_4:21

canceled;

theorem Th22: :: RMOD_4:22

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂ holds (ZeroLC b₂) . b₃ = 0. b₁

proof end;

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃ be Subset of c₂;
mode Linear_Combination of c₃ -> Linear_Combination of a₂ means :Def7: :: RMOD_4:def 7
Carrier a₄ c= a₃;
existence

proof end;

end;

:: deftheorem Def7 defines Linear_Combination RMOD_4:def 7 :

theorem Th23: :: RMOD_4:23

canceled;

theorem Th24: :: RMOD_4:24

canceled;

theorem Th25: :: RMOD_4:25

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Subset of b₂
for b₅ being Linear_Combination of b₃ st b₃ c= b₄ holds
b₅ is Linear_Combination of b₄

proof end;

theorem Th26: :: RMOD_4:26

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Subset of b₂ holds ZeroLC b₂ is Linear_Combination of b₃

proof end;

theorem Th27: :: RMOD_4:27

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Linear_Combination of {} the carrier of b₂ holds b₃ = ZeroLC b₂

proof end;

theorem Th28: :: RMOD_4:28

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Linear_Combination of b₂ holds b₃ is Linear_Combination of Carrier b₃ by Def7;

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃ be FinSequence of the carrier of c₂;
let c₄ be Function of the carrier of c₂,the carrier of c₁;
func c₄ (#) c₃ -> FinSequence of the carrier of a₂ means :Def8: :: RMOD_4:def 8
( len a₅ = len a₃ & ( for b₁ being Nat st b₁ in dom a₅ holds
a₅ . b₁ = (a₃ /. b₁) * (a₄ . (a₃ /. b₁)) ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th29: :: RMOD_4:29

canceled;

theorem Th30: :: RMOD_4:30

canceled;

theorem Th31: :: RMOD_4:31

canceled;

theorem Th32: :: RMOD_4:32

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Nat
for b₄ being Vector of b₂
for b₅ being FinSequence of the carrier of b₂
for b₆ being Function of the carrier of b₂,the carrier of b₁ st b₃ in dom b₅ & b₄ = b₅ . b₃ holds
(b₆ (#) b₅) . b₃ = b₄ * (b₆ . b₄)

proof end;

theorem Th33: :: RMOD_4:33

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Function of the carrier of b₂,the carrier of b₁ holds b₃ (#) (<*> the carrier of b₂) = <*> the carrier of b₂

proof end;

theorem Th34: :: RMOD_4:34

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Function of the carrier of b₂,the carrier of b₁ holds b₄ (#) <*b₃*> = <*(b₃ * (b₄ . b₃))*>

proof end;

theorem Th35: :: RMOD_4:35

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Function of the carrier of b₂,the carrier of b₁ holds b₅ (#) <*b₃,b₄*> = <*(b₃ * (b₅ . b₃)),(b₄ * (b₅ . b₄))*>

proof end;

theorem Th36: :: RMOD_4:36

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄, b₅ being Vector of b₂
for b₆ being Function of the carrier of b₂,the carrier of b₁ holds b₆ (#) <*b₃,b₄,b₅*> = <*(b₃ * (b₆ . b₃)),(b₄ * (b₆ . b₄)),(b₅ * (b₆ . b₅))*>

proof end;

theorem Th37: :: RMOD_4:37

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being FinSequence of the carrier of b₂
for b₅ being Function of the carrier of b₂,the carrier of b₁ holds b₅ (#) (b₃ ^ b₄) = (b₅ (#) b₃) ^ (b₅ (#) b₄)

proof end;

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃ be Linear_Combination of c₂;
func Sum c₃ -> Vector of a₂ means :Def9: :: RMOD_4:def 9
ex b₁ being FinSequence of the carrier of a₂ st
( b₁ is one-to-one & rng b₁ = Carrier a₃ & a₄ = Sum (a₃ (#) b₁) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Sum RMOD_4:def 9 :

Lemma22: for b₁ being Ring
for b₂ being RightMod of b₁ holds Sum (ZeroLC b₂) = 0. b₂

proof end;

theorem Th38: :: RMOD_4:38

canceled;

theorem Th39: :: RMOD_4:39

canceled;

theorem Th40: :: RMOD_4:40

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Subset of b₂ st 0. b₁ <> 1. b₁ holds
( ( b₃ <> {} & b₃ is lineary-closed ) iff for b₄ being Linear_Combination of b₃ holds Sum b₄ in b₃ )

proof end;

theorem Th41: :: RMOD_4:41

for b₁ being Ring
for b₂ being RightMod of b₁ holds Sum (ZeroLC b₂) = 0. b₂ by Lemma22;

theorem Th42: :: RMOD_4:42

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Linear_Combination of {} the carrier of b₂ holds Sum b₃ = 0. b₂

proof end;

theorem Th43: :: RMOD_4:43

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Linear_Combination of {b₃} holds Sum b₄ = b₃ * (b₄ . b₃)

proof end;

theorem Th44: :: RMOD_4:44

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂ st b₃ <> b₄ holds
for b₅ being Linear_Combination of {b₃,b₄} holds Sum b₅ = (b₃ * (b₅ . b₃)) + (b₄ * (b₅ . b₄))

proof end;

theorem Th45: :: RMOD_4:45

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Linear_Combination of b₂ st Carrier b₃ = {} holds
Sum b₃ = 0. b₂

proof end;

theorem Th46: :: RMOD_4:46

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Linear_Combination of b₂ st Carrier b₄ = {b₃} holds
Sum b₄ = b₃ * (b₄ . b₃)

proof end;

theorem Th47: :: RMOD_4:47

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Linear_Combination of b₂ st Carrier b₅ = {b₃,b₄} & b₃ <> b₄ holds
Sum b₅ = (b₃ * (b₅ . b₃)) + (b₄ * (b₅ . b₄))

proof end;

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃, c₄ be Linear_Combination of c₂;
redefine pred = as c₃ = c₄ means :: RMOD_4:def 10
for b₁ being Vector of a₂ holds a₃ . b₁ = a₄ . b₁;
compatibility by FUNCT_2:113;

end;

:: deftheorem Def10 defines = RMOD_4:def 10 :

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃, c₄ be Linear_Combination of c₂;
func c₃ + c₄ -> Linear_Combination of a₂ means :Def11: :: RMOD_4:def 11
for b₁ being Vector of a₂ holds a₅ . b₁ = (a₃ . b₁) + (a₄ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines + RMOD_4:def 11 :

theorem Th48: :: RMOD_4:48

canceled;

theorem Th49: :: RMOD_4:49

canceled;

theorem Th50: :: RMOD_4:50

canceled;

theorem Th51: :: RMOD_4:51

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Linear_Combination of b₂ holds Carrier (b₃ + b₄) c= (Carrier b₃) \/ (Carrier b₄)

proof end;

theorem Th52: :: RMOD_4:52

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Subset of b₂
for b₄, b₅ being Linear_Combination of b₂ st b₄ is Linear_Combination of b₃ & b₅ is Linear_Combination of b₃ holds
b₄ + b₅ is Linear_Combination of b₃

proof end;

theorem Th53: :: RMOD_4:53

for b₁ being comRing
for b₂ being RightMod of b₁
for b₃, b₄ being Linear_Combination of b₂ holds b₃ + b₄ = b₄ + b₃

proof end;

theorem Th54: :: RMOD_4:54

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄, b₅ being Linear_Combination of b₂ holds b₃ + (b₄ + b₅) = (b₃ + b₄) + b₅

proof end;

theorem Th55: :: RMOD_4:55

for b₁ being comRing
for b₂ being RightMod of b₁
for b₃ being Linear_Combination of b₂ holds
( b₃ + (ZeroLC b₂) = b₃ & (ZeroLC b₂) + b₃ = b₃ )

proof end;

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃ be Scalar of c₁;
let c₄ be Linear_Combination of c₂;
func c₄ * c₃ -> Linear_Combination of a₂ means :Def12: :: RMOD_4:def 12
for b₁ being Vector of a₂ holds a₅ . b₁ = (a₄ . b₁) * a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines * RMOD_4:def 12 :

theorem Th56: :: RMOD_4:56

canceled;

theorem Th57: :: RMOD_4:57

canceled;

theorem Th58: :: RMOD_4:58

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Scalar of b₁
for b₄ being Linear_Combination of b₂ holds Carrier (b₄ * b₃) c= Carrier b₄

proof end;

theorem Th59: :: RMOD_4:59

for b₁ being domRing
for b₂ being RightMod of b₁
for b₃ being Linear_Combination of b₂
for b₄ being Scalar of b₁ st b₄ <> 0. b₁ holds
Carrier (b₃ * b₄) = Carrier b₃

proof end;

theorem Th60: :: RMOD_4:60

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Linear_Combination of b₂ holds b₃ * (0. b₁) = ZeroLC b₂

proof end;

theorem Th61: :: RMOD_4:61

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Scalar of b₁
for b₄ being Subset of b₂
for b₅ being Linear_Combination of b₂ st b₅ is Linear_Combination of b₄ holds
b₅ * b₃ is Linear_Combination of b₄

proof end;

theorem Th62: :: RMOD_4:62

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Scalar of b₁
for b₅ being Linear_Combination of b₂ holds b₅ * (b₃ + b₄) = (b₅ * b₃) + (b₅ * b₄)

proof end;

theorem Th63: :: RMOD_4:63

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Scalar of b₁
for b₄, b₅ being Linear_Combination of b₂ holds (b₄ + b₅) * b₃ = (b₄ * b₃) + (b₅ * b₃)

proof end;

theorem Th64: :: RMOD_4:64

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Scalar of b₁
for b₅ being Linear_Combination of b₂ holds (b₅ * b₃) * b₄ = b₅ * (b₃ * b₄)

proof end;

theorem Th65: :: RMOD_4:65

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Linear_Combination of b₂ holds b₃ * (1. b₁) = b₃

proof end;

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃ be Linear_Combination of c₂;
func - c₃ -> Linear_Combination of a₂ equals :: RMOD_4:def 13
a₃ * (- (1. a₁));
correctness ;
involutiveness

proof end;

end;

:: deftheorem Def13 defines - RMOD_4:def 13 :

theorem Th66: :: RMOD_4:66

canceled;

theorem Th67: :: RMOD_4:67

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Linear_Combination of b₂ holds (- b₄) . b₃ = - (b₄ . b₃)

proof end;

theorem Th68: :: RMOD_4:68

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Linear_Combination of b₂ st b₃ + b₄ = ZeroLC b₂ holds
b₄ = - b₃

proof end;

theorem Th69: :: RMOD_4:69

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Linear_Combination of b₂ holds Carrier (- b₃) = Carrier b₃

proof end;

theorem Th70: :: RMOD_4:70

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Subset of b₂
for b₄ being Linear_Combination of b₂ st b₄ is Linear_Combination of b₃ holds
- b₄ is Linear_Combination of b₃ by Th61;

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃, c₄ be Linear_Combination of c₂;
func c₃ - c₄ -> Linear_Combination of a₂ equals :: RMOD_4:def 14
a₃ + (- a₄);
correctness ;

end;

:: deftheorem Def14 defines - RMOD_4:def 14 :

theorem Th71: :: RMOD_4:71

canceled;

theorem Th72: :: RMOD_4:72

canceled;

theorem Th73: :: RMOD_4:73

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄, b₅ being Linear_Combination of b₂ holds (b₄ - b₅) . b₃ = (b₄ . b₃) - (b₅ . b₃)

proof end;

theorem Th74: :: RMOD_4:74

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Linear_Combination of b₂ holds Carrier (b₃ - b₄) c= (Carrier b₃) \/ (Carrier b₄)

proof end;

theorem Th75: :: RMOD_4:75

proof end;

theorem Th76: :: RMOD_4:76

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Linear_Combination of b₂ holds b₃ - b₃ = ZeroLC b₂

proof end;

theorem Th77: :: RMOD_4:77

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Linear_Combination of b₂ holds Sum (b₃ + b₄) = (Sum b₃) + (Sum b₄)

proof end;

theorem Th78: :: RMOD_4:78

for b₁ being domRing
for b₂ being RightMod of b₁
for b₃ being Linear_Combination of b₂
for b₄ being Scalar of b₁ holds Sum (b₃ * b₄) = (Sum b₃) * b₄

proof end;

theorem Th79: :: RMOD_4:79

for b₁ being domRing
for b₂ being RightMod of b₁
for b₃ being Linear_Combination of b₂ holds Sum (- b₃) = - (Sum b₃)

proof end;

theorem Th80: :: RMOD_4:80

for b₁ being domRing
for b₂ being RightMod of b₁
for b₃, b₄ being Linear_Combination of b₂ holds Sum (b₃ - b₄) = (Sum b₃) - (Sum b₄)

proof end;