:: MOD_3 semantic presentation

Lemma1: for b₁ being Ring
for b₂ being Scalar of b₁ st - b₂ = 0. b₁ holds
b₂ = 0. b₁

proof end;

theorem Th1: :: MOD_3:1

canceled;

theorem Th2: :: MOD_3:2

for b₁ being non empty add-associative right_zeroed right_complementable non degenerated doubleLoopStr holds 0. b₁ <> - (1. b₁)

proof end;

theorem Th3: :: MOD_3:3

canceled;

theorem Th4: :: MOD_3:4

canceled;

theorem Th5: :: MOD_3:5

canceled;

theorem Th6: :: MOD_3:6

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃ being Linear_Combination of b₂
for b₄ being finite Subset of b₂ st Carrier b₃ c= b₄ holds
ex b₅ being FinSequence of the carrier of b₂ st
( b₅ is one-to-one & rng b₅ = b₄ & Sum b₃ = Sum (b₃ (#) b₅) )

proof end;

theorem Th7: :: MOD_3:7

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

proof end;

definition

let c₁ be Ring;
let c₂ be LeftMod of c₁;
let c₃ be Subset of c₂;
func Lin c₃ -> strict Subspace of a₂ means :Def1: :: MOD_3:def 1
the carrier of a₄ = { (Sum b₁) where B is Linear_Combination of a₃ : verum } ;
existence

proof end;

uniqueness by VECTSP_4:37;

end;

:: deftheorem Def1 defines Lin MOD_3:def 1 :

theorem Th8: :: MOD_3:8

canceled;

theorem Th9: :: MOD_3:9

canceled;

theorem Th10: :: MOD_3:10

canceled;

theorem Th11: :: MOD_3:11

for b₁ being set
for b₂ being Ring
for b₃ being LeftMod 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 Th12: :: MOD_3:12

for b₁ being set
for b₂ being Ring
for b₃ being LeftMod of b₂
for b₄ being Subset of b₃ st b₁ in b₄ holds
b₁ in Lin b₄

proof end;

theorem Th13: :: MOD_3:13

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

proof end;

theorem Th14: :: MOD_3:14

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

proof end;

theorem Th15: :: MOD_3:15

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃ being Subset of b₂
for b₄ being strict Subspace of b₂ st 0. b₁ <> 1. b₁ & b₃ = the carrier of b₄ holds
Lin b₃ = b₄

proof end;

theorem Th16: :: MOD_3:16

for b₁ being Ring
for b₂ being strict LeftMod 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 Th17: :: MOD_3:17

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

proof end;

theorem Th18: :: MOD_3:18

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

proof end;

theorem Th19: :: MOD_3:19

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

proof end;

theorem Th20: :: MOD_3:20

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

proof end;

definition

let c₁ be Ring;
let c₂ be LeftMod of c₁;
let c₃ be Subset of c₂;
attr a₃ is base means :Def2: :: MOD_3:def 2
( a₃ is linearly-independent & Lin a₃ = VectSpStr(# the carrier of a₂,the add of a₂,the Zero of a₂,the lmult of a₂ #) );

end;

:: deftheorem Def2 defines base MOD_3:def 2 :

definition

let c₁ be Ring;
let c₂ be LeftMod of c₁;
attr a₂ is free means :Def3: :: MOD_3:def 3
ex b₁ being Subset of a₂ st b₁ is base;

end;

:: deftheorem Def3 defines free MOD_3:def 3 :

theorem Th21: :: MOD_3:21

for b₁ being Ring
for b₂ being LeftMod of b₁ holds (0). b₂ is free

proof end;

registration

let c₁ be Ring;
cluster strict free VectSpStr of a₁;
existence

proof end;

end;

Lemma14: for b₁ being Skew-Field
for b₂ being Scalar of b₁
for b₃ being LeftMod of b₁
for b₄ being Vector of b₃ st b₂ <> 0. b₁ holds
( (b₂ " ) * (b₂ * b₄) = (1. b₁) * b₄ & ((b₂ " ) * b₂) * b₄ = (1. b₁) * b₄ )

proof end;

theorem Th22: :: MOD_3:22

canceled;

theorem Th23: :: MOD_3:23

for b₁ being Skew-Field
for b₂ being LeftMod of b₁
for b₃ being Vector of b₂ holds
( {b₃} is linearly-independent iff b₃ <> 0. b₂ )

proof end;

theorem Th24: :: MOD_3:24

for b₁ being Skew-Field
for b₂ being LeftMod of b₁
for b₃, b₄ being Vector of b₂ holds
( b₃ <> b₄ & {b₃,b₄} is linearly-independent iff ( b₄ <> 0. b₂ & ( for b₅ being Scalar of b₁ holds b₃ <> b₅ * b₄ ) ) )

proof end;

theorem Th25: :: MOD_3:25

for b₁ being Skew-Field
for b₂ being LeftMod of b₁
for b₃, b₄ being Vector of b₂ holds
( ( b₃ <> b₄ & {b₃,b₄} is linearly-independent ) iff for b₅, b₆ being Scalar of b₁ st (b₅ * b₃) + (b₆ * b₄) = 0. b₂ holds
( b₅ = 0. b₁ & b₆ = 0. b₁ ) )

proof end;

theorem Th26: :: MOD_3:26

for b₁ being Skew-Field
for b₂ being LeftMod of b₁
for b₃ being Subset of b₂ st b₃ is linearly-independent holds
ex b₄ being Subset of b₂ st
( b₃ c= b₄ & b₄ is base )

proof end;

theorem Th27: :: MOD_3:27

for b₁ being Skew-Field
for b₂ being LeftMod of b₁
for b₃ being Subset of b₂ st Lin b₃ = b₂ holds
ex b₄ being Subset of b₂ st
( b₄ c= b₃ & b₄ is base )

proof end;

Lemma18: for b₁ being Skew-Field
for b₂ being LeftMod of b₁ ex b₃ being Subset of b₂ st b₃ is base

proof end;

theorem Th28: :: MOD_3:28

for b₁ being Skew-Field
for b₂ being LeftMod of b₁ holds b₂ is free

proof end;

definition

let c₁ be Skew-Field;
let c₂ be LeftMod of c₁;
canceled;
mode Basis of c₂ -> Subset of a₂ means :Def5: :: MOD_3:def 5
a₃ is base;
existence by Lemma18;

end;

:: deftheorem Def4 MOD_3:def 4 :

:: deftheorem Def5 defines Basis MOD_3:def 5 :

theorem Th29: :: MOD_3:29

for b₁ being Skew-Field
for b₂ being LeftMod of b₁
for b₃ being Subset of b₂ st b₃ is linearly-independent holds
ex b₄ being Basis of b₂ st b₃ c= b₄

proof end;

theorem Th30: :: MOD_3:30

for b₁ being Skew-Field
for b₂ being LeftMod of b₁
for b₃ being Subset of b₂ st Lin b₃ = b₂ holds
ex b₄ being Basis of b₂ st b₄ c= b₃

proof end;