LMOD_7: Domains of Submodules, Join and Meet of Finite Sequences of Submodules and Quotient Modules

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

proof end;

end;

:: deftheorem Def1 defines SUBMODULE_DOMAIN LMOD_7:def 1 :

definition

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

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

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

proof end;

end;

:: deftheorem defines LINE LMOD_7:def 2 :

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;

proof end;

end;

:: deftheorem Def3 defines LINE_DOMAIN LMOD_7:def 3 :

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

proof end;

proof end;

end;

:: deftheorem defines lines LMOD_7:def 4 :

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

proof end;

end;

:: deftheorem defines HIPERPLANE LMOD_7:def 5 :

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;

proof end;

end;

:: deftheorem Def6 defines HIPERPLANE_DOMAIN LMOD_7:def 6 :

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

proof end;

proof end;

end;

:: deftheorem defines hiperplanes LMOD_7:def 7 :

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

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

end;

:: deftheorem defines Sum LMOD_7:def 8 :

:: deftheorem defines /\ LMOD_7:def 9 :

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

proof end;

proof end;

end;

:: deftheorem defines + LMOD_7:def 10 :

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;

proof end;

end;

:: deftheorem Def11 defines Vector LMOD_7:def 11 :

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

proof end;

proof end;

end;

:: deftheorem Def12 defines .. LMOD_7:def 12 :

registration

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

cluster V .. W -> non 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 by Def12;

end;

:: deftheorem defines .. LMOD_7:def 13 :

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;

proof end;

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;

proof end;

proof end;

end;

:: deftheorem defines - LMOD_7:def 14 :

:: deftheorem Def15 defines + LMOD_7:def 15 :

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;

proof end;

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;

proof end;

proof end;

end;

:: deftheorem defines COMPL LMOD_7:def 16 :

:: deftheorem Def17 defines ADD LMOD_7:def 17 :

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

end;

:: deftheorem defines . LMOD_7:def 18 :

registration

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

cluster V . W -> non empty strict ;

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;

end;

:: deftheorem defines . LMOD_7:def 19 :

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 ;

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;

proof end;

proof end;

end;

:: deftheorem Def20 defines * LMOD_7:def 20 :

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;

proof end;

proof end;

end;

:: deftheorem Def21 defines LMULT LMOD_7:def 21 :

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

end;

:: deftheorem defines / LMOD_7:def 22 :

registration

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

cluster V / W -> non empty strict ;

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;

end;

:: deftheorem defines / LMOD_7:def 23 :

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 by Th23;

end;