:: Domains of Submodules, Join and Meet of Finite Sequences of Submodules and Quotient Modules
:: by Micha{\l} Muzalewski
::
:: Received March 29, 1993
:: Copyright (c) 1993-2021 Association of Mizar Users

scheme :: LMOD_7:sch 1
ElementEq{ F₁() -> set , P₁[ object ] } :

for X1, X2 being Element of F₁() st ( for x being object holds
( x in X1 iff P₁[x] ) ) & ( for x being object holds
( x in X2 iff P₁[x] ) ) holds
X1 = X2

proof end;

scheme :: LMOD_7:sch 2
UnOpEq{ F₁() -> non empty set , F₂( Element of F₁()) -> object } :

for f1, f2 being UnOp of F₁() st ( for a being Element of F₁() holds f1 . a = F₂(a) ) & ( for a being Element of F₁() holds f2 . a = F₂(a) ) holds
f1 = f2

proof end;

scheme :: LMOD_7:sch 3
TriOpEq{ F₁() -> non empty set , F₂( Element of F₁(), Element of F₁(), Element of F₁()) -> object } :

for f1, f2 being TriOp of F₁() st ( for a, b, c being Element of F₁() holds f1 . (a,b,c) = F₂(a,b,c) ) & ( for a, b, c being Element of F₁() holds f2 . (a,b,c) = F₂(a,b,c) ) holds
f1 = f2

proof end;

scheme :: LMOD_7:sch 4
QuaOpEq{ F₁() -> non empty set , F₂( Element of F₁(), Element of F₁(), Element of F₁(), Element of F₁()) -> object } :

for f1, f2 being QuaOp of F₁() st ( for a, b, c, d being Element of F₁() holds f1 . (a,b,c,d) = F₂(a,b,c,d) ) & ( for a, b, c, d being Element of F₁() holds f2 . (a,b,c,d) = F₂(a,b,c,d) ) holds
f1 = f2

proof end;

scheme :: LMOD_7:sch 5
Fraenkel1Ex{ F₁() -> non empty set , F₂() -> non empty set , F₃( object ) -> Element of F₂(), P₁[ object ] } :

ex S being Subset of F₂() st S = { F₃(x) where x is Element of F₁() : P₁[x] }

proof end;

scheme :: LMOD_7:sch 6
Fr0{ F₁() -> non empty set , F₂() -> Element of F₁(), P₁[ object ] } :

P₁[F₂()]

provided

A1: F₂() in { a where a is Element of F₁() : P₁[a] }

proof end;

scheme :: LMOD_7:sch 7
Fr1{ F₁() -> set , F₂() -> non empty set , F₃() -> Element of F₂(), P₁[ object ] } :

( F₃() in F₁() iff P₁[F₃()] )

provided

A1: F₁() = { a where a is Element of F₂() : P₁[a] }

proof end;

scheme :: LMOD_7:sch 8
Fr2{ F₁() -> set , F₂() -> non empty set , F₃() -> Element of F₂(), P₁[ object ] } :

P₁[F₃()]

provided

A1: F₃() in F₁() and
A2: F₁() = { a where a is Element of F₂() : P₁[a] }

proof end;

scheme :: LMOD_7:sch 9
Fr3{ F₁() -> set , F₂() -> set , F₃() -> non empty set , P₁[ object ] } :

( F₁() in F₂() iff ex a being Element of F₃() st
( F₁() = a & P₁[a] ) )

provided

A1: F₂() = { a where a is Element of F₃() : P₁[a] }

proof end;

scheme :: LMOD_7:sch 10
Fr4{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> set , F₄() -> Element of F₁(), F₅( object ) -> set , P₁[ object , object ], P₂[ object , object ] } :

( F₄() in F₅(F₃()) iff for b being Element of F₂() st b in F₃() holds
P₁[F₄(),b] )

provided

A1: F₅(F₃()) = { a where a is Element of F₁() : P₂[a,F₃()] } and
A2: ( P₂[F₄(),F₃()] iff for b being Element of F₂() st b in F₃() holds
P₁[F₄(),b] )

proof end;

Lm1: for G being AbGroup
for a, b, c being Element of G holds
( - (a - b) = (- a) - (- b) & (a - b) + c = (a + c) - b )

proof end;

:: 1. Auxiliary theorems about free-modules

theorem Th1: :: LMOD_7:1

for K being Ring
for V being LeftMod of K
for A being Subset of V st not K is trivial & A is linearly-independent holds
not 0. V in A

proof end;

theorem Th2: :: LMOD_7:2

for K being Ring
for V being LeftMod of K
for a being Vector of V
for A being Subset of V
for l being Linear_Combination of A st not a in A holds
l . a = 0. K

proof end;

theorem :: LMOD_7:3

for K being Ring
for V being LeftMod of K
for A being Subset of V st K is trivial holds
( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial )

proof end;

theorem Th4: :: LMOD_7:4

for K being Ring
for V being LeftMod of K st not V is trivial holds
for A being Subset of V st A is base holds
A <> {}

proof end;

theorem Th5: :: LMOD_7:5

for K being Ring
for V being LeftMod of K
for A1, A2 being Subset of V st A1 \/ A2 is linearly-independent & A1 misses A2 holds
(Lin A1) /\ (Lin A2) = (0). V

proof end;

theorem Th6: :: LMOD_7:6

for K being Ring
for V being LeftMod of K
for A, A1, A2 being Subset of V st A is base & A = A1 \/ A2 & A1 misses A2 holds
V is_the_direct_sum_of Lin A1, Lin A2

proof end;

definition

let K be Ring;
let V be LeftMod of K;

mode SUBMODULE_DOMAIN of V -> non empty set means :Def1: :: LMOD_7:def 1
for x being set st x in it holds
x is strict Subspace of V;

existence
ex b₁ being non empty set st
for x being set st x in b₁ holds
x is strict Subspace of V

proof end;

end;

:: deftheorem Def1 defines SUBMODULE_DOMAIN LMOD_7:def 1 :
for K being Ring
for V being LeftMod of K
for b₃ being non empty set holds
( b₃ is SUBMODULE_DOMAIN of V iff for x being set st x in b₃ holds
x is strict Subspace of V );

definition

let K be Ring;
let V be LeftMod of K;
:: original: Subspaces
redefine func Submodules V -> SUBMODULE_DOMAIN of V;
coherence
Subspaces V is SUBMODULE_DOMAIN of V

proof end;

end;

definition

let K be Ring;
let V be LeftMod of K;
let D be SUBMODULE_DOMAIN of V;
:: original: Element
redefine mode Element of D -> strict Subspace of V;
coherence
for b₁ being Element of D holds b₁ is strict Subspace of V by Def1;

end;

registration

let K be Ring;
let V be LeftMod of K;
let D be SUBMODULE_DOMAIN of V;

cluster non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed for Element of D;

existence
ex b₁ being Element of D st b₁ is strict

proof end;

end;

definition

let K be Ring;
let V be LeftMod of K;
assume A1: not V is trivial ;

mode LINE of V -> strict Subspace of V means :: LMOD_7:def 2
ex a being Vector of V st
( a <> 0. V & it = <:a:> );

existence
ex b₁ being strict Subspace of V ex a being Vector of V st
( a <> 0. V & b₁ = <:a:> )

proof end;

end;

:: deftheorem defines LINE LMOD_7:def 2 :
for K being Ring
for V being LeftMod of K st not V is trivial holds
for b₃ being strict Subspace of V holds
( b₃ is LINE of V iff ex a being Vector of V st
( a <> 0. V & b₃ = <:a:> ) );

definition

let K be Ring;
let V be LeftMod of K;

mode LINE_DOMAIN of V -> non empty set means :Def3: :: LMOD_7:def 3
for x being set st x in it holds
x is LINE of V;

existence
ex b₁ being non empty set st
for x being set st x in b₁ holds
x is LINE of V

proof end;

end;

:: deftheorem Def3 defines LINE_DOMAIN LMOD_7:def 3 :
for K being Ring
for V being LeftMod of K
for b₃ being non empty set holds
( b₃ is LINE_DOMAIN of V iff for x being set st x in b₃ holds
x is LINE of V );

definition

let K be Ring;
let V be LeftMod of K;

func lines V -> LINE_DOMAIN of V means :: LMOD_7:def 4
for x being object holds
( x in it iff x is LINE of V );

existence
ex b₁ being LINE_DOMAIN of V st
for x being object holds
( x in b₁ iff x is LINE of V )

proof end;

uniqueness
for b₁, b₂ being LINE_DOMAIN of V st ( for x being object holds
( x in b₁ iff x is LINE of V ) ) & ( for x being object holds
( x in b₂ iff x is LINE of V ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines lines LMOD_7:def 4 :
for K being Ring
for V being LeftMod of K
for b₃ being LINE_DOMAIN of V holds
( b₃ = lines V iff for x being object holds
( x in b₃ iff x is LINE of V ) );

definition

let K be Ring;
let V be LeftMod of K;
let D be LINE_DOMAIN of V;
:: original: Element
redefine mode Element of D -> LINE of V;
coherence
for b₁ being Element of D holds b₁ is LINE of V by Def3;

end;

definition

let K be Ring;
let V be LeftMod of K;
assume that
A1: not V is trivial and
A2: V is free ;

mode HIPERPLANE of V -> strict Subspace of V means :: LMOD_7:def 5
ex a being Vector of V st
( a <> 0. V & V is_the_direct_sum_of <:a:>,it );

existence
ex b₁ being strict Subspace of V ex a being Vector of V st
( a <> 0. V & V is_the_direct_sum_of <:a:>,b₁ )

proof end;

end;

:: deftheorem defines HIPERPLANE LMOD_7:def 5 :
for K being Ring
for V being LeftMod of K st not V is trivial & V is free holds
for b₃ being strict Subspace of V holds
( b₃ is HIPERPLANE of V iff ex a being Vector of V st
( a <> 0. V & V is_the_direct_sum_of <:a:>,b₃ ) );

definition

let K be Ring;
let V be LeftMod of K;

mode HIPERPLANE_DOMAIN of V -> non empty set means :Def6: :: LMOD_7:def 6
for x being set st x in it holds
x is HIPERPLANE of V;

existence
ex b₁ being non empty set st
for x being set st x in b₁ holds
x is HIPERPLANE of V

proof end;

end;

:: deftheorem Def6 defines HIPERPLANE_DOMAIN LMOD_7:def 6 :
for K being Ring
for V being LeftMod of K
for b₃ being non empty set holds
( b₃ is HIPERPLANE_DOMAIN of V iff for x being set st x in b₃ holds
x is HIPERPLANE of V );

definition

let K be Ring;
let V be LeftMod of K;

func hiperplanes V -> HIPERPLANE_DOMAIN of V means :: LMOD_7:def 7
for x being object holds
( x in it iff x is HIPERPLANE of V );

existence
ex b₁ being HIPERPLANE_DOMAIN of V st
for x being object holds
( x in b₁ iff x is HIPERPLANE of V )

proof end;

uniqueness
for b₁, b₂ being HIPERPLANE_DOMAIN of V st ( for x being object holds
( x in b₁ iff x is HIPERPLANE of V ) ) & ( for x being object holds
( x in b₂ iff x is HIPERPLANE of V ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines hiperplanes LMOD_7:def 7 :
for K being Ring
for V being LeftMod of K
for b₃ being HIPERPLANE_DOMAIN of V holds
( b₃ = hiperplanes V iff for x being object holds
( x in b₃ iff x is HIPERPLANE of V ) );

definition

let K be Ring;
let V be LeftMod of K;
let D be HIPERPLANE_DOMAIN of V;
:: original: Element
redefine mode Element of D -> HIPERPLANE of V;
coherence
for b₁ being Element of D holds b₁ is HIPERPLANE of V by Def6;

end;

definition

let K be Ring;
let V be LeftMod of K;
let Li be FinSequence of Submodules V;

func Sum Li -> Element of Submodules V equals :: LMOD_7:def 8
(SubJoin V) $$ Li;

coherence
(SubJoin V) $$ Li is Element of Submodules V ;

func /\ Li -> Element of Submodules V equals :: LMOD_7:def 9
(SubMeet V) $$ Li;

coherence
(SubMeet V) $$ Li is Element of Submodules V ;

end;

:: deftheorem defines Sum LMOD_7:def 8 :
for K being Ring
for V being LeftMod of K
for Li being FinSequence of Submodules V holds Sum Li = (SubJoin V) $$ Li;

:: deftheorem defines /\ LMOD_7:def 9 :
for K being Ring
for V being LeftMod of K
for Li being FinSequence of Submodules V holds /\ Li = (SubMeet V) $$ Li;

theorem :: LMOD_7:7

for K being Ring
for V being LeftMod of K holds
( SubJoin V is commutative & SubJoin V is associative & SubJoin V is having_a_unity & (0). V = the_unity_wrt (SubJoin V) )

proof end;

theorem :: LMOD_7:8

for K being Ring
for V being LeftMod of K holds
( SubMeet V is commutative & SubMeet V is associative & SubMeet V is having_a_unity & (Omega). V = the_unity_wrt (SubMeet V) )

proof end;

definition

let K be Ring;
let V be LeftMod of K;
let A1, A2 be Subset of V;

func A1 + A2 -> Subset of V means :: LMOD_7:def 10
for x being set holds
( x in it iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) );

existence
ex b₁ being Subset of V st
for x being set holds
( x in b₁ iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) )

proof end;

uniqueness
for b₁, b₂ being Subset of V st ( for x being set holds
( x in b₁ iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) ) & ( for x being set holds
( x in b₂ iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines + LMOD_7:def 10 :
for K being Ring
for V being LeftMod of K
for A1, A2, b₅ being Subset of V holds
( b₅ = A1 + A2 iff for x being set holds
( x in b₅ iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) );

definition

let K be Ring;
let V be LeftMod of K;
let A be Subset of V;
assume A1: A <> {} ;

mode Vector of A -> Vector of V means :Def11: :: LMOD_7:def 11
it is Element of A;

existence
ex b₁ being Vector of V st b₁ is Element of A

proof end;

end;

:: deftheorem Def11 defines Vector LMOD_7:def 11 :
for K being Ring
for V being LeftMod of K
for A being Subset of V st A <> {} holds
for b₄ being Vector of V holds
( b₄ is Vector of A iff b₄ is Element of A );

theorem :: LMOD_7:9

for K being Ring
for V being LeftMod of K
for A1, A2 being Subset of V st A1 <> {} & A1 c= A2 holds
for x being set st x is Vector of A1 holds
x is Vector of A2

proof end;

:: 6. Quotient modules

theorem Th10: :: LMOD_7:10

for K being Ring
for V being LeftMod of K
for a1, a2 being Vector of V
for W being Subspace of V holds
( a2 in a1 + W iff a1 - a2 in W )

proof end;

theorem Th11: :: LMOD_7:11

for K being Ring
for V being LeftMod of K
for a1, a2 being Vector of V
for W being Subspace of V holds
( a1 + W = a2 + W iff a1 - a2 in W ) by VECTSP_4:55, Th10;

definition

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;

func V .. W -> set means :Def12: :: LMOD_7:def 12
for x being set holds
( x in it iff ex a being Vector of V st x = a + W );

existence
ex b₁ being set st
for x being set holds
( x in b₁ iff ex a being Vector of V st x = a + W )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff ex a being Vector of V st x = a + W ) ) & ( for x being set holds
( x in b₂ iff ex a being Vector of V st x = a + W ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines .. LMOD_7:def 12 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for b₄ being set holds
( b₄ = V .. W iff for x being set holds
( x in b₄ iff ex a being Vector of V st x = a + W ) );

registration

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;

cluster V .. W -> non empty ;

coherence
not V .. W is empty

proof end;

end;

definition

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let a be Vector of V;

func a .. W -> Element of V .. W equals :: LMOD_7:def 13
a + W;

coherence
a + W is Element of V .. W by Def12;

end;

:: deftheorem defines .. LMOD_7:def 13 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for a being Vector of V holds a .. W = a + W;

theorem Th12: :: LMOD_7:12

for K being Ring
for V being LeftMod of K
for W being Subspace of V
for x being Element of V .. W ex a being Vector of V st x = a .. W

proof end;

theorem :: LMOD_7:13

for K being Ring
for V being LeftMod of K
for a1, a2 being Vector of V
for W being Subspace of V holds
( a1 .. W = a2 .. W iff a1 - a2 in W ) by Th11;

definition

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let S1 be Element of V .. W;

func - S1 -> Element of V .. W means :: LMOD_7:def 14
for a being Vector of V st S1 = a .. W holds
it = (- a) .. W;

existence
ex b₁ being Element of V .. W st
for a being Vector of V st S1 = a .. W holds
b₁ = (- a) .. W

proof end;

uniqueness
for b₁, b₂ being Element of V .. W st ( for a being Vector of V st S1 = a .. W holds
b₁ = (- a) .. W ) & ( for a being Vector of V st S1 = a .. W holds
b₂ = (- a) .. W ) holds
b₁ = b₂

proof end;

let S2 be Element of V .. W;

func S1 + S2 -> Element of V .. W means :Def15: :: LMOD_7:def 15
for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
it = (a1 + a2) .. W;

existence
ex b₁ being Element of V .. W st
for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
b₁ = (a1 + a2) .. W

proof end;

uniqueness
for b₁, b₂ being Element of V .. W st ( for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
b₁ = (a1 + a2) .. W ) & ( for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
b₂ = (a1 + a2) .. W ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines - LMOD_7:def 14 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for S1, b₅ being Element of V .. W holds
( b₅ = - S1 iff for a being Vector of V st S1 = a .. W holds
b₅ = (- a) .. W );

:: deftheorem Def15 defines + LMOD_7:def 15 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for S1, S2, b₆ being Element of V .. W holds
( b₆ = S1 + S2 iff for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
b₆ = (a1 + a2) .. W );

definition

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
deffunc H₁( Element of V .. W) -> Element of V .. W = - $1;

func COMPL W -> UnOp of (V .. W) means :: LMOD_7:def 16
for S1 being Element of V .. W holds it . S1 = - S1;

existence
ex b₁ being UnOp of (V .. W) st
for S1 being Element of V .. W holds b₁ . S1 = - S1

proof end;

uniqueness
for b₁, b₂ being UnOp of (V .. W) st ( for S1 being Element of V .. W holds b₁ . S1 = - S1 ) & ( for S1 being Element of V .. W holds b₂ . S1 = - S1 ) holds
b₁ = b₂

proof end;

deffunc H₂( Element of V .. W, Element of V .. W) -> Element of V .. W = $1 + $2;

func ADD W -> BinOp of (V .. W) means :Def17: :: LMOD_7:def 17
for S1, S2 being Element of V .. W holds it . (S1,S2) = S1 + S2;

existence
ex b₁ being BinOp of (V .. W) st
for S1, S2 being Element of V .. W holds b₁ . (S1,S2) = S1 + S2

proof end;

uniqueness
for b₁, b₂ being BinOp of (V .. W) st ( for S1, S2 being Element of V .. W holds b₁ . (S1,S2) = S1 + S2 ) & ( for S1, S2 being Element of V .. W holds b₂ . (S1,S2) = S1 + S2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines COMPL LMOD_7:def 16 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for b₄ being UnOp of (V .. W) holds
( b₄ = COMPL W iff for S1 being Element of V .. W holds b₄ . S1 = - S1 );

:: deftheorem Def17 defines ADD LMOD_7:def 17 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for b₄ being BinOp of (V .. W) holds
( b₄ = ADD W iff for S1, S2 being Element of V .. W holds b₄ . (S1,S2) = S1 + S2 );

definition

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;

func V . W -> strict addLoopStr equals :: LMOD_7:def 18
addLoopStr(# (V .. W),(ADD W),((0. V) .. W) #);

coherence
addLoopStr(# (V .. W),(ADD W),((0. V) .. W) #) is strict addLoopStr ;

end;

:: deftheorem defines . LMOD_7:def 18 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V holds V . W = addLoopStr(# (V .. W),(ADD W),((0. V) .. W) #);

registration

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;

cluster V . W -> non empty strict ;

coherence
not V . W is empty ;

end;

theorem :: LMOD_7:14

for K being Ring
for V being LeftMod of K
for a being Vector of V
for W being Subspace of V holds a .. W is Element of (V . W) ;

definition

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let a be Vector of V;

func a . W -> Element of (V . W) equals :: LMOD_7:def 19
a .. W;

coherence
a .. W is Element of (V . W) ;

end;

:: deftheorem defines . LMOD_7:def 19 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for a being Vector of V holds a . W = a .. W;

theorem Th15: :: LMOD_7:15

for K being Ring
for V being LeftMod of K
for W being Subspace of V
for x being Element of (V . W) ex a being Vector of V st x = a . W

proof end;

theorem :: LMOD_7:16

for K being Ring
for V being LeftMod of K
for a1, a2 being Vector of V
for W being Subspace of V holds
( a1 . W = a2 . W iff a1 - a2 in W ) by Th11;

theorem Th17: :: LMOD_7:17

for K being Ring
for V being LeftMod of K
for a, b being Vector of V
for W being Subspace of V holds
( (a . W) + (b . W) = (a + b) . W & 0. (V . W) = (0. V) . W )

proof end;

registration

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;

cluster V . W -> strict right_complementable Abelian add-associative right_zeroed ;

coherence
( V . W is Abelian & V . W is add-associative & V . W is right_zeroed & V . W is right_complementable )

proof end;

end;

definition

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let r be Scalar of K;
let S be Element of (V . W);

func r * S -> Element of (V . W) means :Def20: :: LMOD_7:def 20
for a being Vector of V st S = a . W holds
it = (r * a) . W;

existence
ex b₁ being Element of (V . W) st
for a being Vector of V st S = a . W holds
b₁ = (r * a) . W

proof end;

uniqueness
for b₁, b₂ being Element of (V . W) st ( for a being Vector of V st S = a . W holds
b₁ = (r * a) . W ) & ( for a being Vector of V st S = a . W holds
b₂ = (r * a) . W ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines * LMOD_7:def 20 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for r being Scalar of K
for S, b₆ being Element of (V . W) holds
( b₆ = r * S iff for a being Vector of V st S = a . W holds
b₆ = (r * a) . W );

definition

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;

func LMULT W -> Function of [: the carrier of K, the carrier of (V . W):], the carrier of (V . W) means :Def21: :: LMOD_7:def 21
for r being Scalar of K
for S being Element of (V . W) holds it . (r,S) = r * S;

existence
ex b₁ being Function of [: the carrier of K, the carrier of (V . W):], the carrier of (V . W) st
for r being Scalar of K
for S being Element of (V . W) holds b₁ . (r,S) = r * S

proof end;

uniqueness
for b₁, b₂ being Function of [: the carrier of K, the carrier of (V . W):], the carrier of (V . W) st ( for r being Scalar of K
for S being Element of (V . W) holds b₁ . (r,S) = r * S ) & ( for r being Scalar of K
for S being Element of (V . W) holds b₂ . (r,S) = r * S ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def21 defines LMULT LMOD_7:def 21 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for b₄ being Function of [: the carrier of K, the carrier of (V . W):], the carrier of (V . W) holds
( b₄ = LMULT W iff for r being Scalar of K
for S being Element of (V . W) holds b₄ . (r,S) = r * S );

definition

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;

func V / W -> strict ModuleStr over K equals :: LMOD_7:def 22
ModuleStr(# the carrier of (V . W), the addF of (V . W),((0. V) . W),(LMULT W) #);

coherence
ModuleStr(# the carrier of (V . W), the addF of (V . W),((0. V) . W),(LMULT W) #) is strict ModuleStr over K ;

end;

:: deftheorem defines / LMOD_7:def 22 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V holds V / W = ModuleStr(# the carrier of (V . W), the addF of (V . W),((0. V) . W),(LMULT W) #);

registration

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;

cluster V / W -> non empty strict ;

coherence
not V / W is empty ;

end;

theorem :: LMOD_7:18

for K being Ring
for V being LeftMod of K
for a being Vector of V
for W being Subspace of V holds a . W is Vector of (V / W) ;

theorem :: LMOD_7:19

for K being Ring
for V being LeftMod of K
for W being Subspace of V
for x being Vector of (V / W) holds x is Element of (V . W) ;

definition

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let a be Vector of V;

func a / W -> Vector of (V / W) equals :: LMOD_7:def 23
a . W;

coherence
a . W is Vector of (V / W) ;

end;

:: deftheorem defines / LMOD_7:def 23 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for a being Vector of V holds a / W = a . W;

theorem Th20: :: LMOD_7:20

for K being Ring
for V being LeftMod of K
for W being Subspace of V
for x being Vector of (V / W) ex a being Vector of V st x = a / W

proof end;

theorem :: LMOD_7:21

for K being Ring
for V being LeftMod of K
for a1, a2 being Vector of V
for W being Subspace of V holds
( a1 / W = a2 / W iff a1 - a2 in W ) by Th11;

theorem Th22: :: LMOD_7:22

for K being Ring
for r being Scalar of K
for V being LeftMod of K
for a, b being Vector of V
for W being Subspace of V holds
( (a / W) + (b / W) = (a + b) / W & r * (a / W) = (r * a) / W )

proof end;

Lm2: for K being Ring
for V being LeftMod of K
for W being Subspace of V holds
( V / W is Abelian & V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )

proof end;

theorem Th23: :: LMOD_7:23

for K being Ring
for V being LeftMod of K
for W being Subspace of V holds V / W is strict LeftMod of K

proof end;

registration

let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;

cluster V / W -> strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence
( V / W is vector-distributive & V / W is scalar-distributive & V / W is scalar-associative & V / W is scalar-unital ) by Th23;

end;