:: LMOD_6 semantic presentation

notation

let c₁ be Ring;
let c₂ be LeftMod of c₁;
synonym Submodules c₂ for Subspaces c₂;

end;

theorem Th1: :: LMOD_6:1

for b₁ being set
for b₂ being Ring
for b₃, b₄ being LeftMod of b₂ st b₃ = VectSpStr(# the carrier of b₄,the add of b₄,the Zero of b₄,the lmult of b₄ #) holds
( b₁ in b₃ iff b₁ in b₄ )

proof end;

theorem Th2: :: LMOD_6:2

for b₁ being Ring
for b₂ being Scalar of b₁
for b₃ being LeftMod of b₁
for b₄ being Vector of b₃
for b₅ being Vector of VectSpStr(# the carrier of b₃,the add of b₃,the Zero of b₃,the lmult of b₃ #) st b₄ = b₅ holds
b₂ * b₄ = b₂ * b₅

proof end;

theorem Th3: :: LMOD_6:3

for b₁ being Ring
for b₂ being LeftMod of b₁ holds VectSpStr(# the carrier of b₂,the add of b₂,the Zero of b₂,the lmult of b₂ #) is strict Subspace of b₂

proof end;

theorem Th4: :: LMOD_6:4

for b₁ being Ring
for b₂ being LeftMod of b₁ holds b₂ is Subspace of (Omega). b₂

proof end;

definition

let c₁ be Ring;
canceled;
redefine attr a₁ is trivial means :Def2: :: LMOD_6:def 2
0. a₁ = 1. a₁;
compatibility

proof end;

end;

:: deftheorem Def1 LMOD_6:def 1 :

:: deftheorem Def2 defines trivial LMOD_6:def 2 :

theorem Th5: :: LMOD_6:5

for b₁ being Ring
for b₂ being LeftMod of b₁ st b₁ is trivial holds
( ( for b₃ being Scalar of b₁ holds b₃ = 0. b₁ ) & ( for b₃ being Vector of b₂ holds b₃ = 0. b₂ ) )

proof end;

theorem Th6: :: LMOD_6:6

for b₁ being Ring
for b₂ being LeftMod of b₁ st b₁ is trivial holds
b₂ is trivial

proof end;

theorem Th7: :: LMOD_6:7

for b₁ being Ring
for b₂ being LeftMod of b₁ holds
( b₂ is trivial iff VectSpStr(# the carrier of b₂,the add of b₂,the Zero of b₂,the lmult of b₂ #) = (0). b₂ )

proof end;

definition

let c₁ be Ring;
let c₂ be LeftMod of c₁;
let c₃ be strict Subspace of c₂;
func @ c₃ -> Element of Submodules a₂ equals :: LMOD_6:def 3
a₃;
coherence by VECTSP_5:def 3;

end;

:: deftheorem Def3 defines @ LMOD_6:def 3 :

theorem Th8: :: LMOD_6:8

canceled;

theorem Th9: :: LMOD_6:9

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃ being Subspace of b₂
for b₄ being Subset of b₃ holds b₄ is Subset of b₂

proof end;

definition

let c₁ be Ring;
let c₂ be LeftMod of c₁;
let c₃ be Subspace of c₂;
let c₄ be Subset of c₃;
canceled;
func @ c₄ -> Subset of a₂ equals :: LMOD_6:def 5
a₄;
coherence by Th9;

end;

:: deftheorem Def4 LMOD_6:def 4 :

:: deftheorem Def5 defines @ LMOD_6:def 5 :

registration

let c₁ be Ring;
let c₂ be LeftMod of c₁;
let c₃ be Subspace of c₂;
let c₄ be non empty Subset of c₃;
cluster @ a₄ -> non empty ;
coherence ;

end;

theorem Th10: :: LMOD_6:10

for b₁ being set
for b₂ being Ring
for b₃ being LeftMod of b₂ holds
( b₁ in [#] b₃ iff b₁ in b₃ )

proof end;

theorem Th11: :: LMOD_6:11

for b₁ being set
for b₂ being Ring
for b₃ being LeftMod of b₂
for b₄ being Subspace of b₃ holds
( b₁ in @ ([#] b₄) iff b₁ in b₄ ) by Th10;

theorem Th12: :: LMOD_6:12

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃ being Subset of b₂ holds b₃ c= [#] (Lin b₃)

proof end;

theorem Th13: :: LMOD_6:13

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃ being Subset of b₂
for b₄ being Linear_Combination of b₃ st b₃ <> {} & b₃ is lineary-closed holds
Sum b₄ in b₃

proof end;

theorem Th14: :: LMOD_6:14

canceled;

theorem Th15: :: LMOD_6:15

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃ being Subset of b₂ st 0. b₂ in b₃ & b₃ is lineary-closed holds
b₃ = [#] (Lin b₃)

proof end;

definition

let c₁ be Ring;
let c₂ be LeftMod of c₁;
let c₃ be Vector of c₂;
redefine func { as {c₃} -> Subset of a₂;
coherence

proof end;

end;

definition

let c₁ be Ring;
let c₂ be LeftMod of c₁;
let c₃ be Vector of c₂;
func <:c₃:> -> strict Subspace of a₂ equals :: LMOD_6:def 6
Lin {a₃};
correctness ;

end;

:: deftheorem Def6 defines <: LMOD_6:def 6 :

definition

let c₁ be Ring;
let c₂, c₃ be LeftMod of c₁;
pred c₂ c= c₃ means :Def7: :: LMOD_6:def 7
a₂ is Subspace of a₃;
reflexivity by VECTSP_4:32;

end;

:: deftheorem Def7 defines c= LMOD_6:def 7 :

theorem Th16: :: LMOD_6:16

for b₁ being set
for b₂ being Ring
for b₃, b₄ being LeftMod of b₂ st b₃ c= b₄ holds
( ( b₁ in b₃ implies b₁ in b₄ ) & ( b₁ is Vector of b₃ implies b₁ is Vector of b₄ ) )

proof end;

theorem Th17: :: LMOD_6:17

for b₁ being Ring
for b₂ being Scalar of b₁
for b₃, b₄ being LeftMod of b₁
for b₅, b₆, b₇ being Vector of b₃
for b₈, b₉, b₁₀ being Vector of b₄ st b₃ c= b₄ holds
( 0. b₃ = 0. b₄ & ( b₅ = b₈ & b₆ = b₉ implies b₅ + b₆ = b₈ + b₉ ) & ( b₇ = b₁₀ implies b₂ * b₇ = b₂ * b₁₀ ) & ( b₇ = b₁₀ implies - b₁₀ = - b₇ ) & ( b₅ = b₈ & b₆ = b₉ implies b₅ - b₆ = b₈ - b₉ ) & 0. b₄ in b₃ & 0. b₃ in b₄ & ( b₈ in b₃ & b₉ in b₃ implies b₈ + b₉ in b₃ ) & ( b₁₀ in b₃ implies b₂ * b₁₀ in b₃ ) & ( b₁₀ in b₃ implies - b₁₀ in b₃ ) & ( b₈ in b₃ & b₉ in b₃ implies b₈ - b₉ in b₃ ) )

proof end;

theorem Th18: :: LMOD_6:18

for b₁ being Ring
for b₂, b₃, b₄ being LeftMod of b₁ st b₂ c= b₃ & b₄ c= b₃ holds
( 0. b₂ = 0. b₄ & 0. b₂ in b₄ & ( the carrier of b₂ c= the carrier of b₄ implies b₂ c= b₄ ) & ( ( for b₅ being Vector of b₃ st b₅ in b₂ holds
b₅ in b₄ ) implies b₂ c= b₄ ) & ( the carrier of b₂ = the carrier of b₄ & b₂ is strict & b₄ is strict implies b₂ = b₄ ) & (0). b₂ c= b₄ )

proof end;

theorem Th19: :: LMOD_6:19

canceled;

theorem Th20: :: LMOD_6:20

canceled;

theorem Th21: :: LMOD_6:21

for b₁ being Ring
for b₂, b₃ being strict LeftMod of b₁ st b₂ c= b₃ & b₃ c= b₂ holds
b₂ = b₃

proof end;

theorem Th22: :: LMOD_6:22

for b₁ being Ring
for b₂, b₃, b₄ being LeftMod of b₁ st b₂ c= b₃ & b₃ c= b₄ holds
b₂ c= b₄

proof end;

theorem Th23: :: LMOD_6:23

for b₁ being Ring
for b₂, b₃ being LeftMod of b₁ st b₂ c= b₃ holds
(0). b₂ c= b₃

proof end;

theorem Th24: :: LMOD_6:24

for b₁ being Ring
for b₂, b₃ being LeftMod of b₁ st b₂ c= b₃ holds
(0). b₃ c= b₂

proof end;

theorem Th25: :: LMOD_6:25

for b₁ being Ring
for b₂, b₃ being LeftMod of b₁ st b₂ c= b₃ holds
b₂ c= (Omega). b₃

proof end;

theorem Th26: :: LMOD_6:26

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄ being Subspace of b₂ holds
( b₃ c= b₃ + b₄ & b₄ c= b₃ + b₄ )

proof end;

theorem Th27: :: LMOD_6:27

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄ being Subspace of b₂ holds
( b₃ /\ b₄ c= b₃ & b₃ /\ b₄ c= b₄ )

proof end;

theorem Th28: :: LMOD_6:28

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄, b₅ being Subspace of b₂ st b₃ c= b₄ holds
b₃ /\ b₅ c= b₄ /\ b₅

proof end;

theorem Th29: :: LMOD_6:29

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄, b₅ being Subspace of b₂ st b₃ c= b₄ holds
b₃ /\ b₅ c= b₄

proof end;

theorem Th30: :: LMOD_6:30

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄, b₅ being Subspace of b₂ st b₃ c= b₄ & b₃ c= b₅ holds
b₃ c= b₄ /\ b₅

proof end;

theorem Th31: :: LMOD_6:31

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄ being Subspace of b₂ holds b₃ /\ b₄ c= b₃ + b₄

proof end;

theorem Th32: :: LMOD_6:32

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄, b₅ being Subspace of b₂ holds (b₃ /\ b₄) + (b₄ /\ b₅) c= b₄ /\ (b₃ + b₅)

proof end;

theorem Th33: :: LMOD_6:33

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄, b₅ being Subspace of b₂ st b₃ c= b₄ holds
b₄ /\ (b₃ + b₅) = (b₃ /\ b₄) + (b₄ /\ b₅)

proof end;

theorem Th34: :: LMOD_6:34

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄, b₅ being Subspace of b₂ holds b₃ + (b₄ /\ b₅) c= (b₄ + b₃) /\ (b₃ + b₅)

proof end;

theorem Th35: :: LMOD_6:35

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄, b₅ being Subspace of b₂ st b₃ c= b₄ holds
b₄ + (b₃ /\ b₅) = (b₃ + b₄) /\ (b₄ + b₅)

proof end;

theorem Th36: :: LMOD_6:36

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄, b₅ being Subspace of b₂ st b₃ c= b₄ holds
b₃ c= b₄ + b₅

proof end;

theorem Th37: :: LMOD_6:37

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄, b₅ being Subspace of b₂ st b₃ c= b₄ & b₅ c= b₄ holds
b₃ + b₅ c= b₄

proof end;

theorem Th38: :: LMOD_6:38

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄ being Subset of b₂ st b₃ c= b₄ holds
Lin b₃ c= Lin b₄

proof end;

theorem Th39: :: LMOD_6:39

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄ being Subset of b₂ holds Lin (b₃ /\ b₄) c= (Lin b₃) /\ (Lin b₄)

proof end;

theorem Th40: :: LMOD_6:40

for b₁ being Ring
for b₂, b₃ being LeftMod of b₁ st b₂ c= b₃ holds
[#] b₂ c= [#] b₃

proof end;

theorem Th41: :: LMOD_6:41

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄ being Subspace of b₂ holds
( b₃ c= b₄ iff for b₅ being Vector of b₂ st b₅ in b₃ holds
b₅ in b₄ )

proof end;

theorem Th42: :: LMOD_6:42

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄ being Subspace of b₂ holds
( b₃ c= b₄ iff [#] b₃ c= [#] b₄ )

proof end;

theorem Th43: :: LMOD_6:43

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄ being Subspace of b₂ holds
( b₃ c= b₄ iff @ ([#] b₃) c= @ ([#] b₄) ) by Th42;

theorem Th44: :: LMOD_6:44

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄, b₅ being Subspace of b₂ holds
( (0). b₃ c= b₂ & (0). b₂ c= b₃ & (0). b₄ c= b₅ )

proof end;