:: RMOD_5 semantic presentation

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃ be Subset of c₂;
attr a₃ is linearly-independent means :Def1: :: RMOD_5:def 1
for b₁ being Linear_Combination of a₃ st Sum b₁ = 0. a₂ holds
Carrier b₁ = {} ;

end;

:: deftheorem Def1 defines linearly-independent RMOD_5:def 1 :

notation

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃ be Subset of c₂;
antonym linearly-dependent c₃ for linearly-independent c₃;

end;

theorem Th1: :: RMOD_5:1

canceled;

theorem Th2: :: RMOD_5:2

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Subset of b₂ st b₃ c= b₄ & b₄ is linearly-independent holds
b₃ is linearly-independent

proof end;

theorem Th3: :: RMOD_5:3

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Subset of b₂ st 0. b₁ <> 1. b₁ & b₃ is linearly-independent holds
not 0. b₂ in b₃

proof end;

theorem Th4: :: RMOD_5:4

for b₁ being Ring
for b₂ being RightMod of b₁ holds {} the carrier of b₂ is linearly-independent

proof end;

theorem Th5: :: RMOD_5:5

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂ st 0. b₁ <> 1. b₁ & {b₃,b₄} is linearly-independent holds
( b₃ <> 0. b₂ & b₄ <> 0. b₂ )

proof end;

theorem Th6: :: RMOD_5:6

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂ st 0. b₁ <> 1. b₁ holds
( not {b₃,(0. b₂)} is linearly-independent & not {(0. b₂),b₃} is linearly-independent ) by Th5;

definition

let c₁ be domRing;
let c₂ be RightMod of c₁;
let c₃ be Subset of c₂;
func Lin c₃ -> strict Submodule of a₂ means :Def2: :: RMOD_5:def 2
the carrier of a₄ = { (Sum b₁) where B is Linear_Combination of a₃ : verum } ;
existence

proof end;

uniqueness by RMOD_2:37;

end;

:: deftheorem Def2 defines Lin RMOD_5:def 2 :

theorem Th7: :: RMOD_5:7

canceled;

theorem Th8: :: RMOD_5:8

canceled;

theorem Th9: :: RMOD_5:9

for b₁ being set
for b₂ being domRing
for b₃ being RightMod of b₂
for b₄ being Subset of b₃ holds
( b₁ in Lin b₄ iff ex b₅ being Linear_Combination of b₄ st b₁ = Sum b₅ )

proof end;

theorem Th10: :: RMOD_5:10

for b₁ being set
for b₂ being domRing
for b₃ being RightMod of b₂
for b₄ being Subset of b₃ st b₁ in b₄ holds
b₁ in Lin b₄

proof end;

theorem Th11: :: RMOD_5:11

for b₁ being domRing
for b₂ being RightMod of b₁ holds Lin ({} the carrier of b₂) = (0). b₂

proof end;

theorem Th12: :: RMOD_5:12

for b₁ being domRing
for b₂ being RightMod of b₁
for b₃ being Subset of b₂ holds
( not Lin b₃ = (0). b₂ or b₃ = {} or b₃ = {(0. b₂)} )

proof end;

theorem Th13: :: RMOD_5:13

for b₁ being domRing
for b₂ being RightMod of b₁
for b₃ being Subset of b₂
for b₄ being strict Submodule of b₂ st 0. b₁ <> 1. b₁ & b₃ = the carrier of b₄ holds
Lin b₃ = b₄

proof end;

theorem Th14: :: RMOD_5:14

for b₁ being domRing
for b₂ being strict RightMod of b₁
for b₃ being Subset of b₂ st 0. b₁ <> 1. b₁ & b₃ = the carrier of b₂ holds
Lin b₃ = b₂

proof end;

theorem Th15: :: RMOD_5:15

for b₁ being domRing
for b₂ being RightMod of b₁
for b₃, b₄ being Subset of b₂ st b₃ c= b₄ holds
Lin b₃ is Submodule of Lin b₄

proof end;

theorem Th16: :: RMOD_5:16

for b₁ being domRing
for b₂ being strict RightMod of b₁
for b₃, b₄ being Subset of b₂ st Lin b₃ = b₂ & b₃ c= b₄ holds
Lin b₄ = b₂

proof end;

theorem Th17: :: RMOD_5:17

for b₁ being domRing
for b₂ being RightMod of b₁
for b₃, b₄ being Subset of b₂ holds Lin (b₃ \/ b₄) = (Lin b₃) + (Lin b₄)

proof end;

theorem Th18: :: RMOD_5:18

for b₁ being domRing
for b₂ being RightMod of b₁
for b₃, b₄ being Subset of b₂ holds Lin (b₃ /\ b₄) is Submodule of (Lin b₃) /\ (Lin b₄)

proof end;