:: by Micha{\l} Muzalewski

::

:: Received March 29, 1993

:: Copyright (c) 1993-2016 Association of Mizar Users

scheme :: LMOD_7:sch 3

TriOpEq{ F_{1}() -> non empty set , F_{2}( Element of F_{1}(), Element of F_{1}(), Element of F_{1}()) -> object } :

TriOpEq{ F

for f1, f2 being TriOp of F_{1}() st ( for a, b, c being Element of F_{1}() holds f1 . (a,b,c) = F_{2}(a,b,c) ) & ( for a, b, c being Element of F_{1}() holds f2 . (a,b,c) = F_{2}(a,b,c) ) holds

f1 = f2

f1 = f2

proof end;

scheme :: LMOD_7:sch 4

QuaOpEq{ F_{1}() -> non empty set , F_{2}( Element of F_{1}(), Element of F_{1}(), Element of F_{1}(), Element of F_{1}()) -> object } :

QuaOpEq{ F

for f1, f2 being QuaOp of F_{1}() st ( for a, b, c, d being Element of F_{1}() holds f1 . (a,b,c,d) = F_{2}(a,b,c,d) ) & ( for a, b, c, d being Element of F_{1}() holds f2 . (a,b,c,d) = F_{2}(a,b,c,d) ) holds

f1 = f2

f1 = f2

proof end;

scheme :: LMOD_7:sch 10

Fr4{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> set , F_{4}() -> Element of F_{1}(), F_{5}( object ) -> set , P_{1}[ object , object ], P_{2}[ object , object ] } :

Fr4{ F

( F_{4}() in F_{5}(F_{3}()) iff for b being Element of F_{2}() st b in F_{3}() holds

P_{1}[F_{4}(),b] )

providedP

A1:
F_{5}(F_{3}()) = { a where a is Element of F_{1}() : P_{2}[a,F_{3}()] }
and

A2: ( P_{2}[F_{4}(),F_{3}()] iff for b being Element of F_{2}() st b in F_{3}() holds

P_{1}[F_{4}(),b] )

A2: ( P

P

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

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

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 )

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 <> {}

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

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

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;

ex b_{1} being non empty set st

for x being set st x in b_{1} holds

x is strict Subspace of V

end;
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 for x being set st x in it holds

x is strict Subspace of V;

ex b

for x being set st x in b

x is strict Subspace of V

proof end;

:: deftheorem Def1 defines SUBMODULE_DOMAIN LMOD_7:def 1 :

for K being Ring

for V being LeftMod of K

for b_{3} being non empty set holds

( b_{3} is SUBMODULE_DOMAIN of V iff for x being set st x in b_{3} holds

x is strict Subspace of V );

for K being Ring

for V being LeftMod of K

for b

( b

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

end;
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;

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_{1} being Element of D holds b_{1} is strict Subspace of V
by Def1;

end;
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

registration

let K be Ring;

let V be LeftMod of K;

let D be SUBMODULE_DOMAIN of V;

ex b_{1} being Element of D st b_{1} is strict

end;
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

proof end;

definition

let K be Ring;

let V be LeftMod of K;

assume A1: not V is trivial ;

ex b_{1} being strict Subspace of V ex a being Vector of V st

( a <> 0. V & b_{1} = <:a:> )

end;
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 a being Vector of V st

( a <> 0. V & it = <:a:> );

ex b

( a <> 0. V & b

proof 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_{3} being strict Subspace of V holds

( b_{3} is LINE of V iff ex a being Vector of V st

( a <> 0. V & b_{3} = <:a:> ) );

for K being Ring

for V being LeftMod of K st not V is trivial holds

for b

( b

( a <> 0. V & b

definition

let K be Ring;

let V be LeftMod of K;

ex b_{1} being non empty set st

for x being set st x in b_{1} holds

x is LINE of V

end;
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 for x being set st x in it holds

x is LINE of V;

ex b

for x being set st x in b

x is LINE of V

proof end;

:: deftheorem Def3 defines LINE_DOMAIN LMOD_7:def 3 :

for K being Ring

for V being LeftMod of K

for b_{3} being non empty set holds

( b_{3} is LINE_DOMAIN of V iff for x being set st x in b_{3} holds

x is LINE of V );

for K being Ring

for V being LeftMod of K

for b

( b

x is LINE of V );

definition

let K be Ring;

let V be LeftMod of K;

ex b_{1} being LINE_DOMAIN of V st

for x being object holds

( x in b_{1} iff x is LINE of V )

for b_{1}, b_{2} being LINE_DOMAIN of V st ( for x being object holds

( x in b_{1} iff x is LINE of V ) ) & ( for x being object holds

( x in b_{2} iff x is LINE of V ) ) holds

b_{1} = b_{2}

end;
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 for x being object holds

( x in it iff x is LINE of V );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem defines lines LMOD_7:def 4 :

for K being Ring

for V being LeftMod of K

for b_{3} being LINE_DOMAIN of V holds

( b_{3} = lines V iff for x being object holds

( x in b_{3} iff x is LINE of V ) );

for K being Ring

for V being LeftMod of K

for b

( b

( x in b

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_{1} being Element of D holds b_{1} is LINE of V
by Def3;

end;
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

definition

let K be Ring;

let V be LeftMod of K;

assume that

A1: not V is trivial and

A2: V is free ;

ex b_{1} being strict Subspace of V ex a being Vector of V st

( a <> 0. V & V is_the_direct_sum_of <:a:>,b_{1} )

end;
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 a being Vector of V st

( a <> 0. V & V is_the_direct_sum_of <:a:>,it );

ex b

( a <> 0. V & V is_the_direct_sum_of <:a:>,b

proof 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_{3} being strict Subspace of V holds

( b_{3} is HIPERPLANE of V iff ex a being Vector of V st

( a <> 0. V & V is_the_direct_sum_of <:a:>,b_{3} ) );

for K being Ring

for V being LeftMod of K st not V is trivial & V is free holds

for b

( b

( a <> 0. V & V is_the_direct_sum_of <:a:>,b

definition

let K be Ring;

let V be LeftMod of K;

ex b_{1} being non empty set st

for x being set st x in b_{1} holds

x is HIPERPLANE of V

end;
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 for x being set st x in it holds

x is HIPERPLANE of V;

ex b

for x being set st x in b

x is HIPERPLANE of V

proof end;

:: deftheorem Def6 defines HIPERPLANE_DOMAIN LMOD_7:def 6 :

for K being Ring

for V being LeftMod of K

for b_{3} being non empty set holds

( b_{3} is HIPERPLANE_DOMAIN of V iff for x being set st x in b_{3} holds

x is HIPERPLANE of V );

for K being Ring

for V being LeftMod of K

for b

( b

x is HIPERPLANE of V );

definition

let K be Ring;

let V be LeftMod of K;

ex b_{1} being HIPERPLANE_DOMAIN of V st

for x being object holds

( x in b_{1} iff x is HIPERPLANE of V )

for b_{1}, b_{2} being HIPERPLANE_DOMAIN of V st ( for x being object holds

( x in b_{1} iff x is HIPERPLANE of V ) ) & ( for x being object holds

( x in b_{2} iff x is HIPERPLANE of V ) ) holds

b_{1} = b_{2}

end;
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 for x being object holds

( x in it iff x is HIPERPLANE of V );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem defines hiperplanes LMOD_7:def 7 :

for K being Ring

for V being LeftMod of K

for b_{3} being HIPERPLANE_DOMAIN of V holds

( b_{3} = hiperplanes V iff for x being object holds

( x in b_{3} iff x is HIPERPLANE of V ) );

for K being Ring

for V being LeftMod of K

for b

( b

( x in b

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_{1} being Element of D holds b_{1} is HIPERPLANE of V
by Def6;

end;
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

definition

let K be Ring;

let V be LeftMod of K;

let Li be FinSequence of Submodules V;

coherence

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

coherence

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

end;
let V be LeftMod of K;

let Li be FinSequence of Submodules V;

coherence

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

coherence

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

:: 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;

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;

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) )

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) )

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;

ex b_{1} being Subset of V st

for x being set holds

( x in b_{1} iff ex a1, a2 being Vector of V st

( a1 in A1 & a2 in A2 & x = a1 + a2 ) )

for b_{1}, b_{2} being Subset of V st ( for x being set holds

( x in b_{1} 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_{2} iff ex a1, a2 being Vector of V st

( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) );

ex b

for x being set holds

( x in b

( a1 in A1 & a2 in A2 & x = a1 + a2 ) )

proof end;

uniqueness for b

( x in b

( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) ) & ( for x being set holds

( x in b

( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) ) holds

b

proof end;

:: deftheorem defines + LMOD_7:def 10 :

for K being Ring

for V being LeftMod of K

for A1, A2, b_{5} being Subset of V holds

( b_{5} = A1 + A2 iff for x being set holds

( x in b_{5} iff ex a1, a2 being Vector of V st

( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) );

for K being Ring

for V being LeftMod of K

for A1, A2, b

( b

( x in b

( 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 <> {} ;

existence

ex b_{1} being Vector of V st b_{1} is Element of A

end;
let V be LeftMod of K;

let A be Subset of V;

assume A1: A <> {} ;

existence

ex b

proof 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_{4} being Vector of V holds

( b_{4} is Vector of A iff b_{4} is Element of A );

for K being Ring

for V being LeftMod of K

for A being Subset of V st A <> {} holds

for b

( b

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

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 )

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;

definition

let K be Ring;

let V be LeftMod of K;

let W be Subspace of V;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex a being Vector of V st x = a + W )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex a being Vector of V st x = a + W ) ) & ( for x being set holds

( x in b_{2} iff ex a being Vector of V st x = a + W ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff ex a being Vector of V st x = a + W );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof 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_{4} being set holds

( b_{4} = V .. W iff for x being set holds

( x in b_{4} iff ex a being Vector of V st x = a + W ) );

for K being Ring

for V being LeftMod of K

for W being Subspace of V

for b

( b

( x in b

registration

let K be Ring;

let V be LeftMod of K;

let W be Subspace of V;

coherence

not V .. W is empty

end;
let V be LeftMod of K;

let W be Subspace of V;

coherence

not V .. W is empty

proof end;

definition

let K be Ring;

let V be LeftMod of K;

let W be Subspace of V;

let a be Vector of V;

coherence

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

end;
let V be LeftMod of K;

let W be Subspace of V;

let a be Vector of V;

coherence

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

:: 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;

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

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

definition

let K be Ring;

let V be LeftMod of K;

let W be Subspace of V;

let S1 be Element of V .. W;

ex b_{1} being Element of V .. W st

for a being Vector of V st S1 = a .. W holds

b_{1} = (- a) .. W

for b_{1}, b_{2} being Element of V .. W st ( for a being Vector of V st S1 = a .. W holds

b_{1} = (- a) .. W ) & ( for a being Vector of V st S1 = a .. W holds

b_{2} = (- a) .. W ) holds

b_{1} = b_{2}

ex b_{1} being Element of V .. W st

for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds

b_{1} = (a1 + a2) .. W

for b_{1}, b_{2} being Element of V .. W st ( for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds

b_{1} = (a1 + a2) .. W ) & ( for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds

b_{2} = (a1 + a2) .. W ) holds

b_{1} = b_{2}

end;
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 for a being Vector of V st S1 = a .. W holds

it = (- a) .. W;

ex b

for a being Vector of V st S1 = a .. W holds

b

proof end;

uniqueness for b

b

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 for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds

it = (a1 + a2) .. W;

ex b

for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds

b

proof end;

uniqueness for b

b

b

b

proof 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_{5} being Element of V .. W holds

( b_{5} = - S1 iff for a being Vector of V st S1 = a .. W holds

b_{5} = (- a) .. W );

for K being Ring

for V being LeftMod of K

for W being Subspace of V

for S1, b

( b

b

:: 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_{6} being Element of V .. W holds

( b_{6} = S1 + S2 iff for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds

b_{6} = (a1 + a2) .. W );

for K being Ring

for V being LeftMod of K

for W being Subspace of V

for S1, S2, b

( b

b

definition

let K be Ring;

let V be LeftMod of K;

let W be Subspace of V;

deffunc H_{1}( Element of V .. W) -> Element of V .. W = - $1;

ex b_{1} being UnOp of (V .. W) st

for S1 being Element of V .. W holds b_{1} . S1 = - S1

for b_{1}, b_{2} being UnOp of (V .. W) st ( for S1 being Element of V .. W holds b_{1} . S1 = - S1 ) & ( for S1 being Element of V .. W holds b_{2} . S1 = - S1 ) holds

b_{1} = b_{2}
_{2}( Element of V .. W, Element of V .. W) -> Element of V .. W = $1 + $2;

ex b_{1} being BinOp of (V .. W) st

for S1, S2 being Element of V .. W holds b_{1} . (S1,S2) = S1 + S2

for b_{1}, b_{2} being BinOp of (V .. W) st ( for S1, S2 being Element of V .. W holds b_{1} . (S1,S2) = S1 + S2 ) & ( for S1, S2 being Element of V .. W holds b_{2} . (S1,S2) = S1 + S2 ) holds

b_{1} = b_{2}

end;
let V be LeftMod of K;

let W be Subspace of V;

deffunc H

func COMPL W -> UnOp of (V .. W) means :: LMOD_7:def 16

for S1 being Element of V .. W holds it . S1 = - S1;

existence for S1 being Element of V .. W holds it . S1 = - S1;

ex b

for S1 being Element of V .. W holds b

proof end;

uniqueness for b

b

proof end;

deffunc H
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 for S1, S2 being Element of V .. W holds it . (S1,S2) = S1 + S2;

ex b

for S1, S2 being Element of V .. W holds b

proof end;

uniqueness for b

b

proof 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_{4} being UnOp of (V .. W) holds

( b_{4} = COMPL W iff for S1 being Element of V .. W holds b_{4} . S1 = - S1 );

for K being Ring

for V being LeftMod of K

for W being Subspace of V

for b

( b

:: 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_{4} being BinOp of (V .. W) holds

( b_{4} = ADD W iff for S1, S2 being Element of V .. W holds b_{4} . (S1,S2) = S1 + S2 );

for K being Ring

for V being LeftMod of K

for W being Subspace of V

for b

( b

definition

let K be Ring;

let V be LeftMod of K;

let W be Subspace of V;

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

end;
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) #);

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

:: 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) #);

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
end;

theorem :: LMOD_7:14

definition

let K be Ring;

let V be LeftMod of K;

let W be Subspace of V;

let a be Vector of V;

coherence

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

end;
let V be LeftMod of K;

let W be Subspace of V;

let a be Vector of V;

coherence

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

:: 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;

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

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

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 )

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;

coherence

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

end;
let V be LeftMod of K;

let W be Subspace of V;

coherence

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

proof 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);

ex b_{1} being Element of (V . W) st

for a being Vector of V st S = a . W holds

b_{1} = (r * a) . W

for b_{1}, b_{2} being Element of (V . W) st ( for a being Vector of V st S = a . W holds

b_{1} = (r * a) . W ) & ( for a being Vector of V st S = a . W holds

b_{2} = (r * a) . W ) holds

b_{1} = b_{2}

end;
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 for a being Vector of V st S = a . W holds

it = (r * a) . W;

ex b

for a being Vector of V st S = a . W holds

b

proof end;

uniqueness for b

b

b

b

proof 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_{6} being Element of (V . W) holds

( b_{6} = r * S iff for a being Vector of V st S = a . W holds

b_{6} = (r * a) . W );

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

( b

b

definition

let K be Ring;

let V be LeftMod of K;

let W be Subspace of V;

ex b_{1} 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_{1} . (r,S) = r * S

for b_{1}, b_{2} 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_{1} . (r,S) = r * S ) & ( for r being Scalar of K

for S being Element of (V . W) holds b_{2} . (r,S) = r * S ) holds

b_{1} = b_{2}

end;
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 for r being Scalar of K

for S being Element of (V . W) holds it . (r,S) = r * S;

ex b

for r being Scalar of K

for S being Element of (V . W) holds b

proof end;

uniqueness for b

for S being Element of (V . W) holds b

for S being Element of (V . W) holds b

b

proof 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_{4} being Function of [: the carrier of K, the carrier of (V . W):], the carrier of (V . W) holds

( b_{4} = LMULT W iff for r being Scalar of K

for S being Element of (V . W) holds b_{4} . (r,S) = r * S );

for K being Ring

for V being LeftMod of K

for W being Subspace of V

for b

( b

for S being Element of (V . W) holds b

definition

let K be Ring;

let V be LeftMod of K;

let W be Subspace of V;

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

end;
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) #);

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

:: 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) #);

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
end;

theorem :: LMOD_7:18

theorem :: LMOD_7:19

definition

let K be Ring;

let V be LeftMod of K;

let W be Subspace of V;

let a be Vector of V;

coherence

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

end;
let V be LeftMod of K;

let W be Subspace of V;

let a be Vector of V;

coherence

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

:: 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;

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

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

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 )

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

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;

coherence

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

end;
let V be LeftMod of K;

let W be Subspace of V;

coherence

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