:: LMOD_7 semantic presentation

scheme :: LMOD_7:sch 1
s1{ F1() -> set , P1[ set ] } :
for b1, b2 being Element of F1() st ( for b3 being set holds
( b3 in b1 iff P1[b3] ) ) & ( for b3 being set holds
( b3 in b2 iff P1[b3] ) ) holds
b1 = b2
proof end;

scheme :: LMOD_7:sch 2
s2{ F1() -> non empty set , F2( Element of F1()) -> set } :
for b1, b2 being UnOp of F1() st ( for b3 being Element of F1() holds b1 . b3 = F2(b3) ) & ( for b3 being Element of F1() holds b2 . b3 = F2(b3) ) holds
b1 = b2
proof end;

scheme :: LMOD_7:sch 3
s3{ F1() -> non empty set , F2( Element of F1(), Element of F1(), Element of F1()) -> set } :
for b1, b2 being TriOp of F1() st ( for b3, b4, b5 being Element of F1() holds b1 . b3,b4,b5 = F2(b3,b4,b5) ) & ( for b3, b4, b5 being Element of F1() holds b2 . b3,b4,b5 = F2(b3,b4,b5) ) holds
b1 = b2
proof end;

scheme :: LMOD_7:sch 4
s4{ F1() -> non empty set , F2( Element of F1(), Element of F1(), Element of F1(), Element of F1()) -> set } :
for b1, b2 being QuaOp of F1() st ( for b3, b4, b5, b6 being Element of F1() holds b1 . b3,b4,b5,b6 = F2(b3,b4,b5,b6) ) & ( for b3, b4, b5, b6 being Element of F1() holds b2 . b3,b4,b5,b6 = F2(b3,b4,b5,b6) ) holds
b1 = b2
proof end;

scheme :: LMOD_7:sch 5
s5{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> Element of F2(), P1[ set ] } :
ex b1 being Subset of F2() st b1 = { F3(b2) where B is Element of F1() : P1[b2] }
proof end;

scheme :: LMOD_7:sch 6
s6{ F1() -> non empty set , F2() -> Element of F1(), P1[ set ] } :
P1[F2()]
provided
E1: F2() in { b1 where B is Element of F1() : P1[b1] }
proof end;

scheme :: LMOD_7:sch 7
s7{ F1() -> set , F2() -> non empty set , F3() -> Element of F2(), P1[ set ] } :
( F3() in F1() iff P1[F3()] )
provided
E1: F1() = { b1 where B is Element of F2() : P1[b1] }
proof end;

scheme :: LMOD_7:sch 8
s8{ F1() -> set , F2() -> non empty set , F3() -> Element of F2(), P1[ set ] } :
P1[F3()]
provided
E1: F3() in F1() and
E2: F1() = { b1 where B is Element of F2() : P1[b1] }
proof end;

scheme :: LMOD_7:sch 9
s9{ F1() -> set , F2() -> set , F3() -> non empty set , P1[ set ] } :
( F1() in F2() iff ex b1 being Element of F3() st
( F1() = b1 & P1[b1] ) )
provided
E1: F2() = { b1 where B is Element of F3() : P1[b1] }
proof end;

scheme :: LMOD_7:sch 10
s10{ F1() -> non empty set , F2() -> non empty set , F3() -> set , F4() -> Element of F1(), F5( set ) -> set , P1[ set , set ], P2[ set , set ] } :
( F4() in F5(F3()) iff for b1 being Element of F2() st b1 in F3() holds
P1[F4(),b1] )
provided
E1: F5(F3()) = { b1 where B is Element of F1() : P2[b1,F3()] } and
E2: ( P2[F4(),F3()] iff for b1 being Element of F2() st b1 in F3() holds
P1[F4(),b1] )
proof end;

Lemma1: for b1 being AbGroup
for b2, b3, b4 being Element of b1 holds
( - (b2 - b3) = (- b2) - (- b3) & (b2 - b3) + b4 = (b2 + b4) - b3 )
proof end;

theorem Th1: :: LMOD_7:1
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subset of b2 st not b1 is trivial & b3 is linearly-independent holds
not 0. b2 in b3
proof end;

theorem Th2: :: LMOD_7:2
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Vector of b2
for b4 being Subset of b2
for b5 being Linear_Combination of b4 st not b3 in b4 holds
b5 . b3 = 0. b1
proof end;

theorem Th3: :: LMOD_7:3
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subset of b2 st b1 is trivial holds
( ( for b4 being Linear_Combination of b3 holds Carrier b4 = {} ) & Lin b3 is trivial )
proof end;

theorem Th4: :: LMOD_7:4
for b1 being Ring
for b2 being LeftMod of b1 st not b2 is trivial holds
for b3 being Subset of b2 st b3 is base holds
b3 <> {}
proof end;

theorem Th5: :: LMOD_7:5
for b1 being Ring
for b2 being LeftMod of b1
for b3, b4 being Subset of b2 st b3 \/ b4 is linearly-independent & b3 misses b4 holds
(Lin b3) /\ (Lin b4) = (0). b2
proof end;

theorem Th6: :: LMOD_7:6
for b1 being Ring
for b2 being LeftMod of b1
for b3, b4, b5 being Subset of b2 st b3 is base & b3 = b4 \/ b5 & b4 misses b5 holds
b2 is_the_direct_sum_of Lin b4, Lin b5
proof end;

definition
let c1 be Ring;
let c2 be LeftMod of c1;
mode SUBMODULE_DOMAIN of c2 -> non empty set means :Def1: :: LMOD_7:def 1
for b1 being set st b1 in a3 holds
b1 is strict Subspace of a2;
existence
ex b1 being non empty set st
for b2 being set st b2 in b1 holds
b2 is strict Subspace of c2
proof end;
end;

:: deftheorem Def1 defines SUBMODULE_DOMAIN LMOD_7:def 1 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being non empty set holds
( b3 is SUBMODULE_DOMAIN of b2 iff for b4 being set st b4 in b3 holds
b4 is strict Subspace of b2 );

definition
let c1 be Ring;
let c2 be LeftMod of c1;
redefine func Subspaces as Submodules c2 -> SUBMODULE_DOMAIN of a2;
coherence
Subspaces c2 is SUBMODULE_DOMAIN of c2
proof end;
end;

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be SUBMODULE_DOMAIN of c2;
redefine mode Element as Element of c3 -> strict Subspace of a2;
coherence
for b1 being Element of c3 holds b1 is strict Subspace of c2 by Def1;
end;

registration
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be SUBMODULE_DOMAIN of c2;
cluster strict Element of a3;
existence
ex b1 being Element of c3 st b1 is strict
proof end;
end;

definition
let c1 be Ring;
let c2 be LeftMod of c1;
assume E8: not c2 is trivial ;
mode LINE of c2 -> strict Subspace of a2 means :: LMOD_7:def 2
ex b1 being Vector of a2 st
( b1 <> 0. a2 & a3 = <:b1:> );
existence
ex b1 being strict Subspace of c2ex b2 being Vector of c2 st
( b2 <> 0. c2 & b1 = <:b2:> )
proof end;
end;

:: deftheorem Def2 defines LINE LMOD_7:def 2 :
for b1 being Ring
for b2 being LeftMod of b1 st not b2 is trivial holds
for b3 being strict Subspace of b2 holds
( b3 is LINE of b2 iff ex b4 being Vector of b2 st
( b4 <> 0. b2 & b3 = <:b4:> ) );

definition
let c1 be Ring;
let c2 be LeftMod of c1;
mode LINE_DOMAIN of c2 -> non empty set means :Def3: :: LMOD_7:def 3
for b1 being set st b1 in a3 holds
b1 is LINE of a2;
existence
ex b1 being non empty set st
for b2 being set st b2 in b1 holds
b2 is LINE of c2
proof end;
end;

:: deftheorem Def3 defines LINE_DOMAIN LMOD_7:def 3 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being non empty set holds
( b3 is LINE_DOMAIN of b2 iff for b4 being set st b4 in b3 holds
b4 is LINE of b2 );

definition
let c1 be Ring;
let c2 be LeftMod of c1;
func lines c2 -> LINE_DOMAIN of a2 means :: LMOD_7:def 4
for b1 being set holds
( b1 in a3 iff b1 is LINE of a2 );
existence
ex b1 being LINE_DOMAIN of c2 st
for b2 being set holds
( b2 in b1 iff b2 is LINE of c2 )
proof end;
uniqueness
for b1, b2 being LINE_DOMAIN of c2 st ( for b3 being set holds
( b3 in b1 iff b3 is LINE of c2 ) ) & ( for b3 being set holds
( b3 in b2 iff b3 is LINE of c2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines lines LMOD_7:def 4 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being LINE_DOMAIN of b2 holds
( b3 = lines b2 iff for b4 being set holds
( b4 in b3 iff b4 is LINE of b2 ) );

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be LINE_DOMAIN of c2;
redefine mode Element as Element of c3 -> LINE of a2;
coherence
for b1 being Element of c3 holds b1 is LINE of c2 by Def3;
end;

definition
let c1 be Ring;
let c2 be LeftMod of c1;
assume that
E9: not c2 is trivial and
E10: c2 is free ;
mode HIPERPLANE of c2 -> strict Subspace of a2 means :: LMOD_7:def 5
ex b1 being Vector of a2 st
( b1 <> 0. a2 & a2 is_the_direct_sum_of <:b1:>,a3 );
existence
ex b1 being strict Subspace of c2ex b2 being Vector of c2 st
( b2 <> 0. c2 & c2 is_the_direct_sum_of <:b2:>,b1 )
proof end;
end;

:: deftheorem Def5 defines HIPERPLANE LMOD_7:def 5 :
for b1 being Ring
for b2 being LeftMod of b1 st not b2 is trivial & b2 is free holds
for b3 being strict Subspace of b2 holds
( b3 is HIPERPLANE of b2 iff ex b4 being Vector of b2 st
( b4 <> 0. b2 & b2 is_the_direct_sum_of <:b4:>,b3 ) );

definition
let c1 be Ring;
let c2 be LeftMod of c1;
mode HIPERPLANE_DOMAIN of c2 -> non empty set means :Def6: :: LMOD_7:def 6
for b1 being set st b1 in a3 holds
b1 is HIPERPLANE of a2;
existence
ex b1 being non empty set st
for b2 being set st b2 in b1 holds
b2 is HIPERPLANE of c2
proof end;
end;

:: deftheorem Def6 defines HIPERPLANE_DOMAIN LMOD_7:def 6 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being non empty set holds
( b3 is HIPERPLANE_DOMAIN of b2 iff for b4 being set st b4 in b3 holds
b4 is HIPERPLANE of b2 );

definition
let c1 be Ring;
let c2 be LeftMod of c1;
func hiperplanes c2 -> HIPERPLANE_DOMAIN of a2 means :: LMOD_7:def 7
for b1 being set holds
( b1 in a3 iff b1 is HIPERPLANE of a2 );
existence
ex b1 being HIPERPLANE_DOMAIN of c2 st
for b2 being set holds
( b2 in b1 iff b2 is HIPERPLANE of c2 )
proof end;
uniqueness
for b1, b2 being HIPERPLANE_DOMAIN of c2 st ( for b3 being set holds
( b3 in b1 iff b3 is HIPERPLANE of c2 ) ) & ( for b3 being set holds
( b3 in b2 iff b3 is HIPERPLANE of c2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines hiperplanes LMOD_7:def 7 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being HIPERPLANE_DOMAIN of b2 holds
( b3 = hiperplanes b2 iff for b4 being set holds
( b4 in b3 iff b4 is HIPERPLANE of b2 ) );

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be HIPERPLANE_DOMAIN of c2;
redefine mode Element as Element of c3 -> HIPERPLANE of a2;
coherence
for b1 being Element of c3 holds b1 is HIPERPLANE of c2 by Def6;
end;

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be FinSequence of Submodules c2;
func Sum c3 -> Element of Submodules a2 equals :: LMOD_7:def 8
(SubJoin a2) $$ a3;
coherence
(SubJoin c2) $$ c3 is Element of Submodules c2 ;
func /\ c3 -> Element of Submodules a2 equals :: LMOD_7:def 9
(SubMeet a2) $$ a3;
coherence
(SubMeet c2) $$ c3 is Element of Submodules c2 ;
end;

:: deftheorem Def8 defines Sum LMOD_7:def 8 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being FinSequence of Submodules b2 holds Sum b3 = (SubJoin b2) $$ b3;

:: deftheorem Def9 defines /\ LMOD_7:def 9 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being FinSequence of Submodules b2 holds /\ b3 = (SubMeet b2) $$ b3;

theorem Th7: :: LMOD_7:7
canceled;

theorem Th8: :: LMOD_7:8
canceled;

theorem Th9: :: LMOD_7:9
canceled;

theorem Th10: :: LMOD_7:10
canceled;

theorem Th11: :: LMOD_7:11
canceled;

theorem Th12: :: LMOD_7:12
canceled;

theorem Th13: :: LMOD_7:13
canceled;

theorem Th14: :: LMOD_7:14
for b1 being Ring
for b2 being LeftMod of b1 holds
( SubJoin b2 is commutative & SubJoin b2 is associative & SubJoin b2 has_a_unity & (0). b2 = the_unity_wrt (SubJoin b2) )
proof end;

theorem Th15: :: LMOD_7:15
for b1 being Ring
for b2 being LeftMod of b1 holds
( SubMeet b2 is commutative & SubMeet b2 is associative & SubMeet b2 has_a_unity & (Omega). b2 = the_unity_wrt (SubMeet b2) )
proof end;

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3, c4 be Subset of c2;
func c3 + c4 -> Subset of a2 means :: LMOD_7:def 10
for b1 being set holds
( b1 in a5 iff ex b2, b3 being Vector of a2 st
( b2 in a3 & b3 in a4 & b1 = b2 + b3 ) );
existence
ex b1 being Subset of c2 st
for b2 being set holds
( b2 in b1 iff ex b3, b4 being Vector of c2 st
( b3 in c3 & b4 in c4 & b2 = b3 + b4 ) )
proof end;
uniqueness
for b1, b2 being Subset of c2 st ( for b3 being set holds
( b3 in b1 iff ex b4, b5 being Vector of c2 st
( b4 in c3 & b5 in c4 & b3 = b4 + b5 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4, b5 being Vector of c2 st
( b4 in c3 & b5 in c4 & b3 = b4 + b5 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines + LMOD_7:def 10 :
for b1 being Ring
for b2 being LeftMod of b1
for b3, b4, b5 being Subset of b2 holds
( b5 = b3 + b4 iff for b6 being set holds
( b6 in b5 iff ex b7, b8 being Vector of b2 st
( b7 in b3 & b8 in b4 & b6 = b7 + b8 ) ) );

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subset of c2;
assume E10: c3 <> {} ;
mode Vector of c3 -> Vector of a2 means :Def11: :: LMOD_7:def 11
a4 is Element of a3;
existence
ex b1 being Vector of c2 st b1 is Element of c3
proof end;
end;

:: deftheorem Def11 defines Vector LMOD_7:def 11 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subset of b2 st b3 <> {} holds
for b4 being Vector of b2 holds
( b4 is Vector of b3 iff b4 is Element of b3 );

theorem Th16: :: LMOD_7:16
for b1 being Ring
for b2 being LeftMod of b1
for b3, b4 being Subset of b2 st b3 <> {} & b3 c= b4 holds
for b5 being set st b5 is Vector of b3 holds
b5 is Vector of b4
proof end;

theorem Th17: :: LMOD_7:17
for b1 being Ring
for b2 being LeftMod of b1
for b3, b4 being Vector of b2
for b5 being Subspace of b2 holds
( b3 in b4 + b5 iff b4 - b3 in b5 )
proof end;

theorem Th18: :: LMOD_7:18
for b1 being Ring
for b2 being LeftMod of b1
for b3, b4 being Vector of b2
for b5 being Subspace of b2 holds
( b3 + b5 = b4 + b5 iff b3 - b4 in b5 )
proof end;

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
func c2 .. c3 -> set means :Def12: :: LMOD_7:def 12
for b1 being set holds
( b1 in a4 iff ex b2 being Vector of a2 st b1 = b2 + a3 );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ex b3 being Vector of c2 st b2 = b3 + c3 )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ex b4 being Vector of c2 st b3 = b4 + c3 ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being Vector of c2 st b3 = b4 + c3 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines .. LMOD_7:def 12 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2
for b4 being set holds
( b4 = b2 .. b3 iff for b5 being set holds
( b5 in b4 iff ex b6 being Vector of b2 st b5 = b6 + b3 ) );

registration
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
cluster a2 .. a3 -> non empty ;
coherence
not c2 .. c3 is empty
proof end;
end;

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
let c4 be Vector of c2;
func c4 .. c3 -> Element of a2 .. a3 equals :: LMOD_7:def 13
a4 + a3;
coherence
c4 + c3 is Element of c2 .. c3 by Def12;
end;

:: deftheorem Def13 defines .. LMOD_7:def 13 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2
for b4 being Vector of b2 holds b4 .. b3 = b4 + b3;

theorem Th19: :: LMOD_7:19
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2
for b4 being Element of b2 .. b3 ex b5 being Vector of b2 st b4 = b5 .. b3
proof end;

theorem Th20: :: LMOD_7:20
for b1 being Ring
for b2 being LeftMod of b1
for b3, b4 being Vector of b2
for b5 being Subspace of b2 holds
( b3 .. b5 = b4 .. b5 iff b3 - b4 in b5 ) by Th18;

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
let c4 be Element of c2 .. c3;
func - c4 -> Element of a2 .. a3 means :: LMOD_7:def 14
for b1 being Vector of a2 st a4 = b1 .. a3 holds
a5 = (- b1) .. a3;
existence
ex b1 being Element of c2 .. c3 st
for b2 being Vector of c2 st c4 = b2 .. c3 holds
b1 = (- b2) .. c3
proof end;
uniqueness
for b1, b2 being Element of c2 .. c3 st ( for b3 being Vector of c2 st c4 = b3 .. c3 holds
b1 = (- b3) .. c3 ) & ( for b3 being Vector of c2 st c4 = b3 .. c3 holds
b2 = (- b3) .. c3 ) holds
b1 = b2
proof end;
let c5 be Element of c2 .. c3;
func c4 + c5 -> Element of a2 .. a3 means :Def15: :: LMOD_7:def 15
for b1, b2 being Vector of a2 st a4 = b1 .. a3 & a5 = b2 .. a3 holds
a6 = (b1 + b2) .. a3;
existence
ex b1 being Element of c2 .. c3 st
for b2, b3 being Vector of c2 st c4 = b2 .. c3 & c5 = b3 .. c3 holds
b1 = (b2 + b3) .. c3
proof end;
uniqueness
for b1, b2 being Element of c2 .. c3 st ( for b3, b4 being Vector of c2 st c4 = b3 .. c3 & c5 = b4 .. c3 holds
b1 = (b3 + b4) .. c3 ) & ( for b3, b4 being Vector of c2 st c4 = b3 .. c3 & c5 = b4 .. c3 holds
b2 = (b3 + b4) .. c3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines - LMOD_7:def 14 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2
for b4, b5 being Element of b2 .. b3 holds
( b5 = - b4 iff for b6 being Vector of b2 st b4 = b6 .. b3 holds
b5 = (- b6) .. b3 );

:: deftheorem Def15 defines + LMOD_7:def 15 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2
for b4, b5, b6 being Element of b2 .. b3 holds
( b6 = b4 + b5 iff for b7, b8 being Vector of b2 st b4 = b7 .. b3 & b5 = b8 .. b3 holds
b6 = (b7 + b8) .. b3 );

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
deffunc H1( Element of c2 .. c3) -> Element of c2 .. c3 = - a1;
func COMPL c3 -> UnOp of a2 .. a3 means :: LMOD_7:def 16
for b1 being Element of a2 .. a3 holds a4 . b1 = - b1;
existence
ex b1 being UnOp of c2 .. c3 st
for b2 being Element of c2 .. c3 holds b1 . b2 = - b2
proof end;
uniqueness
for b1, b2 being UnOp of c2 .. c3 st ( for b3 being Element of c2 .. c3 holds b1 . b3 = - b3 ) & ( for b3 being Element of c2 .. c3 holds b2 . b3 = - b3 ) holds
b1 = b2
proof end;
deffunc H2( Element of c2 .. c3, Element of c2 .. c3) -> Element of c2 .. c3 = a1 + a2;
func ADD c3 -> BinOp of a2 .. a3 means :Def17: :: LMOD_7:def 17
for b1, b2 being Element of a2 .. a3 holds a4 . b1,b2 = b1 + b2;
existence
ex b1 being BinOp of c2 .. c3 st
for b2, b3 being Element of c2 .. c3 holds b1 . b2,b3 = b2 + b3
proof end;
uniqueness
for b1, b2 being BinOp of c2 .. c3 st ( for b3, b4 being Element of c2 .. c3 holds b1 . b3,b4 = b3 + b4 ) & ( for b3, b4 being Element of c2 .. c3 holds b2 . b3,b4 = b3 + b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines COMPL LMOD_7:def 16 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2
for b4 being UnOp of b2 .. b3 holds
( b4 = COMPL b3 iff for b5 being Element of b2 .. b3 holds b4 . b5 = - b5 );

:: deftheorem Def17 defines ADD LMOD_7:def 17 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2
for b4 being BinOp of b2 .. b3 holds
( b4 = ADD b3 iff for b5, b6 being Element of b2 .. b3 holds b4 . b5,b6 = b5 + b6 );

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
func c2 . c3 -> strict LoopStr equals :: LMOD_7:def 18
 LoopStr(# (a2 .. a3),(ADD a3),((0. a2) .. a3) #);
coherence
LoopStr(# (c2 .. c3),(ADD c3),((0. c2) .. c3) #) is strict LoopStr ;
end;

:: deftheorem Def18 defines . LMOD_7:def 18 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2 holds b2 . b3 = LoopStr(# (b2 .. b3),(ADD b3),((0. b2) .. b3) #);

registration
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
cluster a2 . a3 -> non empty strict ;
coherence
not c2 . c3 is empty
proof end;
end;

theorem Th21: :: LMOD_7:21
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Vector of b2
for b4 being Subspace of b2 holds b3 .. b4 is Element of (b2 . b4) ;

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
let c4 be Vector of c2;
func c4 . c3 -> Element of (a2 . a3) equals :: LMOD_7:def 19
a4 .. a3;
coherence
c4 .. c3 is Element of (c2 . c3) ;
end;

:: deftheorem Def19 defines . LMOD_7:def 19 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2
for b4 being Vector of b2 holds b4 . b3 = b4 .. b3;

theorem Th22: :: LMOD_7:22
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2
for b4 being Element of (b2 . b3) ex b5 being Vector of b2 st b4 = b5 . b3
proof end;

theorem Th23: :: LMOD_7:23
for b1 being Ring
for b2 being LeftMod of b1
for b3, b4 being Vector of b2
for b5 being Subspace of b2 holds
( b3 . b5 = b4 . b5 iff b3 - b4 in b5 ) by Th20;

theorem Th24: :: LMOD_7:24
for b1 being Ring
for b2 being LeftMod of b1
for b3, b4 being Vector of b2
for b5 being Subspace of b2 holds
( (b3 . b5) + (b4 . b5) = (b3 + b4) . b5 & 0. (b2 . b5) = (0. b2) . b5 )
proof end;

registration
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
cluster a2 . a3 -> non empty strict Abelian add-associative right_zeroed right_complementable ;
coherence
( c2 . c3 is Abelian & c2 . c3 is add-associative & c2 . c3 is right_zeroed & c2 . c3 is right_complementable )
proof end;
end;

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
let c4 be Scalar of c1;
let c5 be Element of (c2 . c3);
func c4 * c5 -> Element of (a2 . a3) means :Def20: :: LMOD_7:def 20
for b1 being Vector of a2 st a5 = b1 . a3 holds
a6 = (a4 * b1) . a3;
existence
ex b1 being Element of (c2 . c3) st
for b2 being Vector of c2 st c5 = b2 . c3 holds
b1 = (c4 * b2) . c3
proof end;
uniqueness
for b1, b2 being Element of (c2 . c3) st ( for b3 being Vector of c2 st c5 = b3 . c3 holds
b1 = (c4 * b3) . c3 ) & ( for b3 being Vector of c2 st c5 = b3 . c3 holds
b2 = (c4 * b3) . c3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines * LMOD_7:def 20 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2
for b4 being Scalar of b1
for b5, b6 being Element of (b2 . b3) holds
( b6 = b4 * b5 iff for b7 being Vector of b2 st b5 = b7 . b3 holds
b6 = (b4 * b7) . b3 );

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
func LMULT c3 -> Function of [:the carrier of a1,the carrier of (a2 . a3):],the carrier of (a2 . a3) means :Def21: :: LMOD_7:def 21
for b1 being Scalar of a1
for b2 being Element of (a2 . a3) holds a4 . b1,b2 = b1 * b2;
existence
ex b1 being Function of [:the carrier of c1,the carrier of (c2 . c3):],the carrier of (c2 . c3) st
for b2 being Scalar of c1
for b3 being Element of (c2 . c3) holds b1 . b2,b3 = b2 * b3
proof end;
uniqueness
for b1, b2 being Function of [:the carrier of c1,the carrier of (c2 . c3):],the carrier of (c2 . c3) st ( for b3 being Scalar of c1
for b4 being Element of (c2 . c3) holds b1 . b3,b4 = b3 * b4 ) & ( for b3 being Scalar of c1
for b4 being Element of (c2 . c3) holds b2 . b3,b4 = b3 * b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines LMULT LMOD_7:def 21 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2
for b4 being Function of [:the carrier of b1,the carrier of (b2 . b3):],the carrier of (b2 . b3) holds
( b4 = LMULT b3 iff for b5 being Scalar of b1
for b6 being Element of (b2 . b3) holds b4 . b5,b6 = b5 * b6 );

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
func c2 / c3 -> strict VectSpStr of a1 equals :: LMOD_7:def 22
 VectSpStr(# the carrier of (a2 . a3),the add of (a2 . a3),the Zero of (a2 . a3),(LMULT a3) #);
coherence
VectSpStr(# the carrier of (c2 . c3),the add of (c2 . c3),the Zero of (c2 . c3),(LMULT c3) #) is strict VectSpStr of c1 ;
end;

:: deftheorem Def22 defines / LMOD_7:def 22 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2 holds b2 / b3 = VectSpStr(# the carrier of (b2 . b3),the add of (b2 . b3),the Zero of (b2 . b3),(LMULT b3) #);

registration
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
cluster a2 / a3 -> non empty strict ;
coherence
not c2 / c3 is empty ;
end;

theorem Th25: :: LMOD_7:25
canceled;

theorem Th26: :: LMOD_7:26
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Vector of b2
for b4 being Subspace of b2 holds b3 . b4 is Vector of (b2 / b4) ;

theorem Th27: :: LMOD_7:27
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2
for b4 being Vector of (b2 / b3) holds b4 is Element of (b2 . b3) ;

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
let c4 be Vector of c2;
func c4 / c3 -> Vector of (a2 / a3) equals :: LMOD_7:def 23
a4 . a3;
coherence
c4 . c3 is Vector of (c2 / c3) ;
end;

:: deftheorem Def23 defines / LMOD_7:def 23 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2
for b4 being Vector of b2 holds b4 / b3 = b4 . b3;

theorem Th28: :: LMOD_7:28
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2
for b4 being Vector of (b2 / b3) ex b5 being Vector of b2 st b4 = b5 / b3
proof end;

theorem Th29: :: LMOD_7:29
for b1 being Ring
for b2 being LeftMod of b1
for b3, b4 being Vector of b2
for b5 being Subspace of b2 holds
( b3 / b5 = b4 / b5 iff b3 - b4 in b5 ) by Th23;

theorem Th30: :: LMOD_7:30
for b1 being Ring
for b2 being Scalar of b1
for b3 being LeftMod of b1
for b4, b5 being Vector of b3
for b6 being Subspace of b3 holds
( (b4 / b6) + (b5 / b6) = (b4 + b5) / b6 & b2 * (b4 / b6) = (b2 * b4) / b6 )
proof end;

Lemma25: for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2 holds
( b2 / b3 is Abelian & b2 / b3 is add-associative & b2 / b3 is right_zeroed & b2 / b3 is right_complementable )
proof end;

theorem Th31: :: LMOD_7:31
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Subspace of b2 holds b2 / b3 is strict LeftMod of b1
proof end;

registration
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Subspace of c2;
cluster a2 / a3 -> non empty strict VectSp-like ;
coherence
c2 / c3 is VectSp-like by Th31;
end;