Volume 5, 1993

University of Bialystok

Copyright (c) 1993 Association of Mizar Users

### The abstract of the Mizar article:

### Domains of Submodules, Join and Meet of Finite Sequences of Submodules and Quotient Modules

**by****Michal Muzalewski**- Received March 29, 1993
- MML identifier: LMOD_7

- [ Mizar article, MML identifier index ]

environ vocabulary BINOP_1, FUNCT_1, MULTOP_1, FUNCSDOM, VECTSP_1, VECTSP_2, RLVECT_2, FINSEQ_1, RMOD_3, ARYTM_1, RLVECT_1, REALSET1, RLVECT_3, BOOLE, MOD_3, RLSUB_1, RLSUB_2, INCSP_1, PARTFUN1, PRELAMB, SETWISEO, LATTICES, QC_LANG1, FINSEQ_4, ARYTM_3, LMOD_7; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, STRUCT_0, FUNCT_2, BINOP_1, FINSEQ_1, SETWISEO, SETWOP_2, LATTICES, MULTOP_1, RLVECT_1, ANPROJ_1, VECTSP_1, FUNCSDOM, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, LMOD_5, MOD_3, LMOD_6; constructors BINOP_1, DOMAIN_1, SETWISEO, MULTOP_1, ANPROJ_1, VECTSP_6, LMOD_5, MOD_3, LMOD_6, FINSOP_1, LATTICE2, MEMBERED, XBOOLE_0; clusters VECTSP_1, VECTSP_4, STRUCT_0, VECTSP_5, RELSET_1, SUBSET_1, LATTICES, LATTICE2, MEMBERED, ZFMISC_1, XBOOLE_0; requirements BOOLE, SUBSET; begin :: :: Schemes :: scheme ElementEq {A()->set,P[set]} : for X1,X2 being Element of A() st (for x being set holds x in X1 iff P[x]) & (for x being set holds x in X2 iff P[x]) holds X1 = X2; scheme UnOpEq {A() -> non empty set, F(Element of A()) -> set}: for f1,f2 being UnOp of A() st (for a being Element of A() holds f1.(a) = F(a)) & (for a being Element of A() holds f2.(a) = F(a)) holds f1 = f2; scheme TriOpEq {A() -> non empty set, F(Element of A(),Element of A(),Element of A()) -> set}: for f1,f2 being TriOp of A() st (for a,b,c being Element of A() holds f1.(a,b,c) = F(a,b,c)) & (for a,b,c being Element of A() holds f2.(a,b,c) = F(a,b,c)) holds f1 = f2; scheme QuaOpEq {A() -> non empty set, F(Element of A(),Element of A(),Element of A(),Element of A()) -> set}: for f1,f2 being QuaOp of A() st (for a,b,c,d being Element of A() holds f1.(a,b,c,d) = F(a,b,c,d)) & (for a,b,c,d being Element of A() holds f2.(a,b,c,d) = F(a,b,c,d)) holds f1 = f2; scheme Fraenkel1_Ex {A, D() -> non empty set, F(set) -> Element of D(), P[set]} : ex S being Subset of D() st S = {F(x) where x is Element of A() : P[x]}; scheme Fr_0 {A() -> non empty set, x() -> Element of A(), P[set]} : P[x()] provided x() in {a where a is Element of A() : P[a]}; scheme Fr_1 {X() -> set, A() -> non empty set, a() -> Element of A(), P[set]} : a() in X() iff P[a()] provided X() = {a where a is Element of A() : P[a]}; scheme Fr_2 {X() -> set, A() -> non empty set, a() -> Element of A(), P[set]}: P[a()] provided a() in X() and X() = {a where a is Element of A() : P[a]}; scheme Fr_3 {x() -> set, X() -> set, A() -> non empty set, P[set]} : x() in X() iff ex a being Element of A() st x()=a & P[a] provided X() = {a where a is Element of A() : P[a]}; scheme Fr_4 {D1,D2() -> non empty set, B() -> set, a() -> Element of D1(), F(set) -> set, P[set,set], Q[set,set]} : a() in F(B()) iff for b being Element of D2() st b in B() holds P[a(),b] provided F(B()) = {a where a is Element of D1() : Q[a,B()]} and Q[a(),B()] iff for b being Element of D2() st b in B() holds P[a(),b]; begin :: Main Part reserve x for set, K for Ring, r for Scalar of K, V for LeftMod of K, a,b,a1,a2 for Vector of V, A,A1,A2 for Subset of V, l for Linear_Combination of A, W for Subspace of V, Li for FinSequence of Submodules(V); :: :: 1. Auxiliary theorems about free-modules :: theorem :: LMOD_7:1 K is non trivial & A is linearly-independent implies not 0.V in A; theorem :: LMOD_7:2 not a in A implies l.a = 0.K; theorem :: LMOD_7:3 K is trivial implies (for l holds Carrier(l) = {}) & Lin A is trivial; theorem :: LMOD_7:4 V is non trivial implies for A st A is base holds A <> {}; theorem :: LMOD_7:5 A1 \/ A2 is linearly-independent & A1 misses A2 implies Lin A1 /\ Lin A2 = (0).V; theorem :: LMOD_7:6 A is base & A = A1 \/ A2 & A1 misses A2 implies V is_the_direct_sum_of Lin A1,Lin A2; begin :: :: 2. Domains of submodules :: definition let K,V; mode SUBMODULE_DOMAIN of V -> non empty set means :: LMOD_7:def 1 x in it implies x is strict Subspace of V; end; definition let K,V; redefine func Submodules(V) -> SUBMODULE_DOMAIN of V; end; definition let K,V; let D be SUBMODULE_DOMAIN of V; redefine mode Element of D -> strict Subspace of V; end; definition let K,V; let D be SUBMODULE_DOMAIN of V; cluster strict Element of D; end; definition let K,V; assume V is non trivial; mode LINE of V -> strict Subspace of V means :: LMOD_7:def 2 ex a st a<>0.V & it = <:a:>; end; definition let K,V; mode LINE_DOMAIN of V -> non empty set means :: LMOD_7:def 3 x in it implies x is LINE of V; end; definition let K,V; func lines(V) -> LINE_DOMAIN of V means :: LMOD_7:def 4 x in it iff x is LINE of V; end; definition let K,V; let D be LINE_DOMAIN of V; redefine mode Element of D -> LINE of V; end; definition let K,V; assume that V is non trivial and V is free; mode HIPERPLANE of V -> strict Subspace of V means :: LMOD_7:def 5 ex a st a<>0.V & V is_the_direct_sum_of <:a:>,it; end; definition let K,V; mode HIPERPLANE_DOMAIN of V -> non empty set means :: LMOD_7:def 6 x in it implies x is HIPERPLANE of V; end; definition let K,V; func hiperplanes(V) -> HIPERPLANE_DOMAIN of V means :: LMOD_7:def 7 x in it iff x is HIPERPLANE of V; end; definition let K,V; let D be HIPERPLANE_DOMAIN of V; redefine mode Element of D -> HIPERPLANE of V; end; begin :: :: 3. Join and meet of finite sequences of submodules :: definition let K,V,Li; 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; canceled 5; theorem :: LMOD_7:12 for G being Lattice holds the L_join of G is commutative associative & the L_meet of G is commutative associative; canceled; theorem :: LMOD_7:14 SubJoin(V) is commutative associative & SubJoin(V) has_a_unity & (0).V = the_unity_wrt SubJoin(V); theorem :: LMOD_7:15 SubMeet(V) is commutative associative & SubMeet(V) has_a_unity & (Omega).V = the_unity_wrt SubMeet(V); begin :: :: 4. Sum of subsets of module :: definition let K,V,A1,A2; func A1 + A2 -> Subset of V means :: LMOD_7:def 10 x in it iff ex a1,a2 st a1 in A1 & a2 in A2 & x = a1+a2; end; begin :: :: 5. Vector of subset :: definition let K,V,A; assume A <> {}; mode Vector of A -> Vector of V means :: LMOD_7:def 11 it is Element of A; end; theorem :: LMOD_7:16 A1 <> {} & A1 c= A2 implies for x st x is Vector of A1 holds x is Vector of A2; :: :: 6. Quotient modules :: theorem :: LMOD_7:17 a2 in a1 + W iff a1 - a2 in W; theorem :: LMOD_7:18 a1 + W = a2 + W iff a1 - a2 in W; definition let K,V,W; func V..W -> set means :: LMOD_7:def 12 x in it iff ex a st x = a + W; end; definition let K,V,W; cluster V..W -> non empty; end; definition let K,V,W,a; func a..W -> Element of V..W equals :: LMOD_7:def 13 a + W; end; theorem :: LMOD_7:19 for x being Element of V..W ex a st x = a..W; theorem :: LMOD_7:20 a1..W = a2..W iff a1 - a2 in W; reserve S1,S2 for Element of V..W; definition let K,V,W,S1; func -S1 -> Element of V..W means :: LMOD_7:def 14 S1 = a..W implies it = (-a)..W; let S2; func S1 + S2 -> Element of V..W means :: LMOD_7:def 15 S1 = a1..W & S2 = a2..W implies it = (a1+a2)..W; end; definition let K,V,W; func COMPL W -> UnOp of V..W means :: LMOD_7:def 16 it.S1 = -S1; func ADD W -> BinOp of V..W means :: LMOD_7:def 17 it.(S1,S2) = S1 + S2; end; definition let K,V,W; func V.W -> strict LoopStr equals :: LMOD_7:def 18 LoopStr(#V..W,ADD W,(0.V)..W#); end; definition let K,V,W; cluster V.W -> non empty; end; theorem :: LMOD_7:21 a..W is Element of V.W; definition let K,V,W,a; func a.W -> Element of V.W equals :: LMOD_7:def 19 a..W; end; theorem :: LMOD_7:22 for x being Element of V.W ex a st x = a.W; theorem :: LMOD_7:23 a1.W = a2.W iff a1 - a2 in W; theorem :: LMOD_7:24 a.W + b.W = (a+b).W & 0.(V.W) = (0.V).W; definition let K,V,W; cluster V.W -> Abelian add-associative right_zeroed right_complementable; end; reserve S for Element of V.W; definition let K,V,W,r,S; func r*S -> Element of V.W means :: LMOD_7:def 20 S = a.W implies it = (r*a).W; end; definition let K,V,W; func LMULT W -> Function of [:the carrier of K,the carrier of V.W:], the carrier of V.W means :: LMOD_7:def 21 it.(r,S) = r*S; end; begin definition let K,V,W; func V/W -> strict VectSpStr over K equals :: LMOD_7:def 22 VectSpStr(#the carrier of V.W,the add of V.W, the Zero of V.W,LMULT W#); end; definition let K,V,W; cluster V/W -> non empty; end; canceled; theorem :: LMOD_7:26 a.W is Vector of V/W; theorem :: LMOD_7:27 for x being Vector of V/W holds x is Element of V.W; definition let K,V,W,a; func a/W -> Vector of V/W equals :: LMOD_7:def 23 a.W; end; theorem :: LMOD_7:28 for x being Vector of V/W ex a st x = a/W; theorem :: LMOD_7:29 a1/W = a2/W iff a1 - a2 in W; theorem :: LMOD_7:30 a/W + b/W = (a+b)/W & r*(a/W) = (r*a)/W; theorem :: LMOD_7:31 V/W is strict LeftMod of K; definition let K,V,W; cluster V/W -> VectSp-like; end;

Back to top