:: 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-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, XBOOLE_0, BINOP_1, FUNCT_1, MULTOP_1, FUNCSDOM,
VECTSP_1, VECTSP_2, RLVECT_2, RLSUB_1, FINSEQ_1, RMOD_3, ARYTM_1,
ARYTM_3, ZFMISC_1, RLVECT_3, SUPINF_2, GROUP_1, TARSKI, CARD_3, MOD_3,
STRUCT_0, RLSUB_2, INCSP_1, PARTFUN1, PRELAMB, SETWISEO, LATTICES,
QC_LANG1, FINSEQ_4, ALGSTR_0, RLVECT_1, RELAT_1, LMOD_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, STRUCT_0, ALGSTR_0,
FUNCT_2, BINOP_1, FINSEQ_1, SETWISEO, SETWOP_2, LATTICES, MULTOP_1,
RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6,
VECTSP_7, LMOD_6;
constructors BINOP_1, DOMAIN_1, SETWISEO, MULTOP_1, FINSOP_1, LATTICES,
VECTSP_6, VECTSP_7, LMOD_6, RELSET_1;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, LATTICES, VECTSP_1, VECTSP_4,
VECTSP_5, LATTICE2, ALGSTR_0;
requirements BOOLE, SUBSET;
definitions RLVECT_1, XBOOLE_0, ALGSTR_0;
equalities STRUCT_0, ALGSTR_0;
expansions STRUCT_0;
theorems BINOP_1, FUNCT_2, RLVECT_1, VECTSP_7, LMOD_6, MOD_3, MULTOP_1,
SETWISEO, SUBSET_1, TARSKI, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6,
ZFMISC_1, XBOOLE_0, XBOOLE_1, ALGSTR_0;
schemes BINOP_1, DOMAIN_1, FUNCT_2, BINOP_2, XFAMILY;
begin :: Schemes
scheme ElementEq {A()->set,P[object]} :
for X1,X2 being Element of A() 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;
let X1,X2 be Element of A() such that
A1: for x being object holds x in X1 iff P[x] and
A2: for x being object holds x in X2 iff P[x];
for x being object holds x in X1 iff x in X2 by A1,A2;
hence thesis by TARSKI:2;
end;
scheme UnOpEq {A() -> non empty set, F(Element of A()) -> object}:
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
proof
let f1,f2 be UnOp of A() such that
A1: for a being Element of A() holds f1.(a) = F(a) and
A2: for a being Element of A() holds f2.(a) = F(a);
now
let a be Element of A();
thus f1.(a) = F(a) by A1
.= f2.(a) by A2;
end;
hence thesis by FUNCT_2:63;
end;
scheme TriOpEq {A() -> non empty set,
F(Element of A(),Element of A(),Element of A()) -> object}:
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
proof
let f1,f2 be TriOp of A() such that
A1: for a,b,c being Element of A() holds f1.(a,b,c) = F(a,b,c) and
A2: for a,b,c being Element of A() holds f2.(a,b,c) = F(a,b,c);
now
let a,b,c be Element of A();
thus f1.(a,b,c) = F(a,b,c) by A1
.= f2.(a,b,c) by A2;
end;
hence thesis by MULTOP_1:3;
end;
scheme QuaOpEq {A() -> non empty set,
F(Element of A(),Element of A(),Element of A(),Element of A()) -> object}:
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
proof
let f1,f2 be QuaOp of A() such that
A1: for a,b,c,d being Element of A() holds f1.(a,b,c,d) = F(a,b,c,d) and
A2: for a,b,c,d being Element of A() holds f2.(a,b,c,d) = F(a,b,c,d);
now
let a,b,c,d be Element of A();
thus f1.(a,b,c,d) = F(a,b,c,d) by A1
.= f2.(a,b,c,d) by A2;
end;
hence thesis by MULTOP_1:6;
end;
scheme Fraenkel1Ex {A, D() -> non empty set,
F(object) -> Element of D(), P[object]} : ex S being Subset of D()
st S = {F(x) where x is Element of A() : P[x]}
proof
reconsider S={F(x) where x is Element of A() : P[x]} as Subset of D()
from DOMAIN_1:sch 8;
take S;
thus thesis;
end;
scheme Fr0 {A() -> non empty set, x() -> Element of A(), P[object]} : P[x()]
provided
A1: x() in {a where a is Element of A() : P[a]}
proof
ex a being Element of A() st x()=a & P[a] by A1;
hence thesis;
end;
scheme Fr1
{X() -> set, A() -> non empty set, a() -> Element of A(), P[object]}:
a() in X() iff P[a()]
provided
A1: X() = {a where a is Element of A() : P[a]}
proof
thus a() in X() implies P[a()]
proof
assume a() in X();
then
A2: a() in {a where a is Element of A() : P[a]} by A1;
thus P[a()] from Fr0(A2);
end;
assume P[a()];
hence thesis by A1;
end;
scheme Fr2
{X() -> set, A() -> non empty set, a() -> Element of A(), P[object]}:
P[a()]
provided
A1: a() in X() and
A2: X() = {a where a is Element of A() : P[a]}
proof
A3: a() in {a where a is Element of A() : P[a]} by A1,A2;
thus P[a()] from Fr0(A3);
end;
scheme Fr3 {x() -> set, X() -> set, A() -> non empty set, P[object]} :
x() in X() iff ex a being Element of A() st x()=a & P[a]
provided
A1: X() = {a where a is Element of A() : P[a]}
proof
thus thesis by A1;
end;
scheme Fr4 {D1,D2() -> non empty set, B() -> set,
a() -> Element of D1(), F(object) -> set, P,Q[object,object]} :
a() in F(B()) iff for b being Element of D2() st b in B() holds P[a(),b]
provided
A1: F(B()) = {a where a is Element of D1() : Q[a,B()]} and
A2: Q[a(),B()] iff for b being Element of D2() st b in B() holds P[a(),b]
proof
thus a() in F(B()) implies for b being Element of D2() st b in
B() holds P[a(),b]
proof
defpred X[set] means Q[$1,B()];
assume a() in F(B());
then
A3: a() in {a where a is Element of D1() : X[a]} by A1;
X[a()] from Fr0(A3);
hence thesis by A2;
end;
assume for b being Element of D2() st b in B() holds P[a(),b];
hence thesis by A1,A2;
end;
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);
Lm1: for G being AbGroup, a,b,c being Element of G holds
-(a-b) = -a-(-b) & a-b+c = a+c-b
proof
let G be AbGroup, a,b,c be Element of G;
thus -(a-b) = -a+b by VECTSP_1:17
.= -a-(-b) by RLVECT_1:17;
thus thesis by RLVECT_1:def 3;
end;
:: 1. Auxiliary theorems about free-modules
theorem Th1:
K is non trivial & A is linearly-independent implies not 0.V in A
proof
assume that
A1: K is non trivial and
A2: A is linearly-independent;
0.K <> 1_K by A1,LMOD_6:def 1; then
K is non degenerated;
hence thesis by A2,VECTSP_7:2;
end;
theorem Th2:
not a in A implies l.a = 0.K
proof
assume
A1: not a in A;
Carrier l c= A by VECTSP_6:def 4;
then not a in Carrier l by A1;
hence thesis by VECTSP_6:2;
end;
theorem
K is trivial implies (for l holds Carrier(l) = {}) & Lin A is trivial
proof
assume
A1: K is trivial;
thus
A2: for l holds Carrier l = {}
proof
let l;
assume
A3: Carrier l <> {};
set x = the Element of Carrier l;
ex a st ( x = a)&( l.a <> 0.K) by A3,VECTSP_6:1;
hence contradiction by A1;
end;
now
let a be Vector of Lin A;
a in Lin A;
then consider l such that
A4: a = Sum(l) by MOD_3:4;
Carrier l = {} by A2;
then a = 0.V by A4,VECTSP_6:19;
hence a=0.(Lin A) by VECTSP_4:11;
end;
hence thesis;
end;
theorem Th4:
V is non trivial implies for A st A is base holds A <> {}
proof
assume
A1: V is non trivial;
let A such that
A2: A is base and
A3: A = {};
A4: A = {}(the carrier of V) by A3;
the ModuleStr of V = Lin A by A2,VECTSP_7:def 3
.= (0).V by A4,MOD_3:6;
hence contradiction by A1,LMOD_6:7;
end;
theorem Th5:
A1 \/ A2 is linearly-independent & A1 misses A2
implies Lin A1 /\ Lin A2 = (0).V
proof
assume that
A1: A1 \/ A2 is linearly-independent and
A2: A1 /\ A2 = {};
reconsider P=Lin A1 /\ Lin A2 as strict Subspace of V;
set Z=the carrier of P;
A3: Z=(the carrier of Lin A1)/\ (the carrier of Lin A2) by VECTSP_5:def 2;
A4: now
let x;
assume
A5: x in Z;
then
A6: x in the carrier of Lin A1 by A3,XBOOLE_0:def 4;
A7: x in the carrier of Lin A2 by A3,A5,XBOOLE_0:def 4;
A8: x in Lin A1 by A6;
A9: x in Lin A2 by A7;
consider l1 being Linear_Combination of A1 such that
A10: x = Sum(l1) by A8,MOD_3:4;
consider l2 being Linear_Combination of A2 such that
A11: x = Sum(l2) by A9,MOD_3:4;
A12: Carrier l1 c= A1 by VECTSP_6:def 4;
Carrier l2 c= A2 by VECTSP_6:def 4;
then
A13: Carrier l1 \/ Carrier l2 c= A1 \/ A2 by A12,XBOOLE_1:13;
Carrier(l1 - l2) c= Carrier l1 \/ Carrier l2 by VECTSP_6:41;
then Carrier(l1 - l2) c= A1 \/ A2 by A13,XBOOLE_1:1;
then reconsider l = l1 - l2 as Linear_Combination of A1 \/ A2
by VECTSP_6:def 4;
Sum(l) = Sum(l1) - Sum(l2) by VECTSP_6:47
.= 0.V by A10,A11,VECTSP_1:19;
then
A14: Carrier l = {} by A1,VECTSP_7:def 1;
Carrier l1 = {}
proof
assume
A15: Carrier l1 <> {};
set x = the Element of Carrier l1;
consider b such that
A16: x = b and
A17: l1.b <> 0.K by A15,VECTSP_6:1;
b in A1 by A12,A15,A16,TARSKI:def 3;
then
A18: not b in A2 by A2,XBOOLE_0:def 4;
0.K = l.b by A14,VECTSP_6:2
.= l1.b - l2.b by VECTSP_6:40;
then l1.b = l2.b by RLVECT_1:21
.= 0.K by A18,Th2;
hence contradiction by A17;
end;
hence x = 0.V by A10,VECTSP_6:19;
end;
0.V in Lin A1 /\ Lin A2 by VECTSP_4:17;
then for x be object holds x in Z iff x=0.V by A4;
then Z = {0.V} by TARSKI:def 1;
hence thesis by VECTSP_4:def 3;
end;
theorem Th6:
A is base & A = A1 \/ A2 & A1 misses A2 implies
V is_the_direct_sum_of Lin A1,Lin A2
proof
assume that
A1: A is base and
A2: A = A1 \/ A2 and
A3: A1 misses A2;
set W=the ModuleStr of V;
A4: A is linearly-independent by A1,VECTSP_7:def 3;
Lin A = W by A1,VECTSP_7:def 3;
then
A5: W = Lin A1 + Lin A2 by A2,MOD_3:12;
Lin A1 /\ Lin A2 = (0).V by A2,A3,A4,Th5;
hence thesis by A5,VECTSP_5:def 4;
end;
begin :: 2. Domains of submodules
definition
let K,V;
mode SUBMODULE_DOMAIN of V -> non empty set means
:Def1:
x in it implies x is strict Subspace of V;
existence
proof
set a = the strict Subspace of V;
set D = {a};
take D;
thus thesis by TARSKI:def 1;
end;
end;
definition
let K,V;
redefine func Submodules(V) -> SUBMODULE_DOMAIN of V; :: redefines Submodules (LMOD_6, synonym) → Subspaces (VECTSP_5, definition)
coherence
proof
now
let x;
assume x in Submodules(V);
then ex W being strict Subspace of V st ( W = x) by VECTSP_5:def 3;
hence x is strict Subspace of V;
end;
hence thesis by Def1;
end;
end;
definition
let K,V;
let D be SUBMODULE_DOMAIN of V;
redefine mode Element of D -> strict Subspace of V; :: redefines Element (SUBSET_1, definition)
coherence by Def1;
end;
registration
let K,V;
let D be SUBMODULE_DOMAIN of V;
cluster strict for Element of D;
existence
proof
set x = the Element of D;
take x;
thus thesis;
end;
end;
definition
let K,V;
assume
A1: V is non trivial;
mode LINE of V -> strict Subspace of V means
ex a st a<>0.V & it = <:a:>;
existence
proof consider a such that
A2: a<>0.V by A1;
take <:a:>;
thus thesis by A2;
end;
end;
definition
let K,V;
mode LINE_DOMAIN of V -> non empty set means
:Def3:
x in it implies x is LINE of V;
existence
proof
set a = the LINE of V;
set D = {a};
take D;
thus thesis by TARSKI:def 1;
end;
end;
definition
let K,V;
func lines(V) -> LINE_DOMAIN of V means
for x being object holds x in it iff x is LINE of V;
existence
proof
set D = {a where a is Element of Submodules(V): a is LINE of V};
set a1 = the LINE of V;
reconsider a2 = a1 as Element of Submodules(V) by VECTSP_5:def 3;
a2 in D;
then reconsider D as non empty set;
A1: now
let x;
assume x in D;
then ex a being Element of Submodules(V) st ( x = a)&( a is LINE of V);
hence x is LINE of V;
end;
then reconsider D9 = D as LINE_DOMAIN of V by Def3;
take D9;
now
let x be object;
thus x in D9 implies x is LINE of V by A1;
thus x is LINE of V implies x in D9
proof
assume
A2: x is LINE of V;
then reconsider x1 = x as Element of Submodules(V) by VECTSP_5:def 3;
x1 in D by A2;
hence thesis;
end;
end;
hence thesis;
end;
uniqueness
proof
let D1,D2 be LINE_DOMAIN of V such that
A3: for x being object holds x in D1 iff x is LINE of V and
A4: for x being object holds x in D2 iff x is LINE of V;
now
let x be object;
x in D1 iff x is LINE of V by A3;
hence x in D1 iff x in D2 by A4;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let K,V;
let D be LINE_DOMAIN of V;
redefine mode Element of D -> LINE of V; :: redefines Element (SUBSET_1, definition)
coherence by Def3;
end;
definition
let K,V;
assume that
A1: V is non trivial and
A2: V is free;
mode HIPERPLANE of V -> strict Subspace of V means
ex a st a<>0.V & V is_the_direct_sum_of <:a:>,it;
existence
proof
consider A being Subset of V such that
A3: A is base by A2,VECTSP_7:def 4;
reconsider A as Subset of V;
A4: A is linearly-independent by A3,VECTSP_7:def 3;
A5: A <> {} by A1,A3,Th4;
set x = the Element of A;
reconsider a = x as Vector of V by A5,TARSKI:def 3;
reconsider A1 = {a} as Subset of V;
set A2 = A\A1;
set H = Lin(A2);
A1 c= A by A5,ZFMISC_1:31;
then
A6: A = A1 \/ A2 by XBOOLE_1:45;
A1 misses A2 by XBOOLE_1:79;
then
A7: V is_the_direct_sum_of Lin(A1),H by A3,A6,Th6;
A8: ex a st a<>0.V & V is_the_direct_sum_of <:a:>,H
proof
take a;
thus thesis by A1,A4,A5,A7,Th1,LMOD_6:6,def 4;
end;
take H;
thus thesis by A8;
end;
end;
definition
let K,V;
mode HIPERPLANE_DOMAIN of V -> non empty set means
:Def6:
x in it implies x is HIPERPLANE of V;
existence
proof
set a = the HIPERPLANE of V;
set D = {a};
take D;
thus thesis by TARSKI:def 1;
end;
end;
definition
let K,V;
func hiperplanes(V) -> HIPERPLANE_DOMAIN of V means
for x being object holds x in it iff x is HIPERPLANE of V;
existence
proof
set D = {a where a is Element of Submodules(V): a is HIPERPLANE of V};
set a1 = the HIPERPLANE of V;
reconsider a2 = a1 as Element of Submodules(V) by VECTSP_5:def 3;
a2 in D;
then reconsider D as non empty set;
A1: now
let x;
assume x in D;
then ex a being Element of Submodules(V) st ( x = a)&( a is
HIPERPLANE of V);
hence x is HIPERPLANE of V;
end;
then reconsider D9 = D as HIPERPLANE_DOMAIN of V by Def6;
take D9;
now
let x be object;
thus x in D9 implies x is HIPERPLANE of V by A1;
thus x is HIPERPLANE of V implies x in D9
proof
assume x is HIPERPLANE of V;
then reconsider W=x as HIPERPLANE of V;
reconsider x1 = W as Element of Submodules(V) by VECTSP_5:def 3;
x1 in D;
hence thesis;
end;
end;
hence thesis;
end;
uniqueness
proof
let D1,D2 be HIPERPLANE_DOMAIN of V such that
A2: for x being object holds x in D1 iff x is HIPERPLANE of V and
A3: for x being object holds x in D2 iff x is HIPERPLANE of V;
now
let x be object;
x in D1 iff x is HIPERPLANE of V by A2;
hence x in D1 iff x in D2 by A3;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let K,V;
let D be HIPERPLANE_DOMAIN of V;
redefine mode Element of D -> HIPERPLANE of V; :: redefines Element (SUBSET_1, definition)
coherence by Def6;
end;
begin :: 3. Join and meet of finite sequences of submodules
definition
let K,V,Li;
func Sum Li -> Element of Submodules(V) equals
SubJoin(V) $$ Li;
coherence;
func /\ Li -> Element of Submodules(V) equals
SubMeet(V) $$ Li;
coherence;
end;
theorem
SubJoin(V) is commutative associative & SubJoin(V) is having_a_unity
& (0).V = the_unity_wrt SubJoin(V)
proof
set S0=Submodules(V), S1=SubJoin(V);
reconsider L=LattStr(#(S0 qua non empty set),(S1 qua BinOp of S0),
(SubMeet(V) qua BinOp of S0)#) as Lattice by VECTSP_5:57;
S1=the L_join of L;
hence S1 is commutative associative;
set e=(0).V;
reconsider e9=@e as Element of (S0 qua non empty set);
A1: e9=e by LMOD_6:def 2;
now
let a9 be Element of (S0 qua non empty set);
reconsider b=a9 as Element of S0;
reconsider a=b as strict Subspace of V;
thus S1.(e9,a9) = e+a by A1,VECTSP_5:def 7
.= a9 by VECTSP_5:9;
thus S1.(a9,e9) = a+e by A1,VECTSP_5:def 7
.= a9 by VECTSP_5:9;
end;
then
A2: e9 is_a_unity_wrt (S1 qua BinOp of S0) by BINOP_1:3;
hence S1 is having_a_unity by SETWISEO:def 2;
thus thesis by A1,A2,BINOP_1:def 8;
end;
theorem
SubMeet(V) is commutative associative & SubMeet(V)
is having_a_unity & (Omega).V = the_unity_wrt SubMeet(V)
proof
set S0=Submodules(V), S2=SubMeet(V);
reconsider L=LattStr(#(S0 qua non empty set),(SubJoin(V) qua BinOp of S0),
(S2 qua BinOp of S0)#) as Lattice by VECTSP_5:57;
S2=the L_meet of L;
hence S2 is commutative associative;
set e=(Omega).V;
reconsider e9=@e as Element of (S0 qua non empty set);
A1: e9=e by LMOD_6:def 2;
now
let a9 be Element of (S0 qua non empty set);
reconsider b=a9 as Element of S0;
reconsider a=b as strict Subspace of V;
thus (S2 qua BinOp of S0).(e9,a9) = e/\a by A1,VECTSP_5:def 8
.= a9 by VECTSP_5:21;
thus (S2 qua BinOp of S0).(a9,e9) = a/\e by A1,VECTSP_5:def 8
.= a9 by VECTSP_5:21;
end;
then
A2: e9 is_a_unity_wrt (S2 qua BinOp of S0) by BINOP_1:3;
hence S2 is having_a_unity by SETWISEO:def 2;
thus thesis by A1,A2,BINOP_1:def 8;
end;
begin :: 4. Sum of subsets of module
definition
let K,V,A1,A2;
func A1 + A2 -> Subset of V means
x in it iff ex a1,a2 st a1 in A1 & a2 in A2 & x = a1+a2;
existence
proof
set S = {a1+a2 : a1 in A1 & a2 in A2};
A1: now
let x;
assume x in S;
then ex a1,a2 st ( x = a1+a2)&( a1 in A1)&( a2 in A2);
hence ex a1,a2 st a1 in A1 & a2 in A2 & x = a1+a2;
end;
now
let x be object;
assume x in S;
then ex a1,a2 st ( x = a1+a2)&( a1 in A1)&( a2 in A2);
hence x in the carrier of V;
end;
then reconsider S9 = S as Subset of V by TARSKI:def 3;
take S9;
thus thesis by A1;
end;
uniqueness
proof
let D1,D2 be Subset of V such that
A2: x in D1 iff ex a1,a2 st a1 in A1 & a2 in A2 & x = a1+a2 and
A3: x in D2 iff ex a1,a2 st a1 in A1 & a2 in A2 & x = a1+a2;
now
let x be object;
x in D1 iff ex a1,a2 st a1 in A1 & a2 in A2 & x = a1+a2 by A2;
hence x in D1 iff x in D2 by A3;
end;
hence thesis by TARSKI:2;
end;
end;
begin :: 5. Vector of subset
definition
let K,V,A;
assume
A1: A <> {};
mode Vector of A -> Vector of V means
:Def11:
it is Element of A;
existence
proof
consider x being Element of V such that
A2: x in A by A1,SUBSET_1:4;
take x;
thus thesis by A2;
end;
end;
theorem
A1 <> {} & A1 c= A2 implies for x st x is Vector of A1 holds x is Vector of
A2
proof
assume that
A1: A1 <> {} and
A2: A1 c= A2;
let x;
assume x is Vector of A1;
then reconsider a=x as Vector of A1;
a is Element of A1 by A1,Def11;
then a in A2 by A1,A2,TARSKI:def 3;
hence thesis by Def11;
end;
:: 6. Quotient modules
theorem Th10:
a2 in a1 + W iff a1 - a2 in W
proof
a1 - (a1 - a2) = a1 - a1 + a2 by RLVECT_1:29
.= 0.V + a2 by VECTSP_1:19
.= a2 by RLVECT_1:def 4;
hence thesis by VECTSP_4:61;
end;
theorem Th11:
a1 + W = a2 + W iff a1 - a2 in W
by VECTSP_4:55,Th10;
definition
let K,V,W;
func V..W -> set means
:Def12:
x in it iff ex a st x = a + W;
existence
proof
take the set of all a + W ;
thus thesis;
end;
uniqueness
proof
defpred X[set] means ex a st $1 = a + W;
thus for S1,S2 being set st
(for x holds x in S1 iff X[x]) & (for x holds x in S2 iff X[x])
holds S1 = S2 from XFAMILY:sch 3;
end;
end;
registration
let K,V,W;
cluster V..W -> non empty;
coherence
proof
a + W in V..W by Def12;
hence thesis;
end;
end;
definition
let K,V,W,a;
func a..W -> Element of V..W equals
a + W;
coherence by Def12;
end;
theorem Th12:
for x being Element of V..W ex a st x = a..W
proof
let x be Element of V..W;
consider a such that
A1: x = a + W by Def12;
take a;
thus thesis by A1;
end;
theorem
a1..W = a2..W iff a1 - a2 in W by Th11;
reserve S1,S2 for Element of V..W;
definition
let K,V,W,S1;
func -S1 -> Element of V..W means
S1 = a..W implies it = (-a)..W;
existence
proof
consider a1 such that
A1: S1 = a1..W by Th12;
A2: now
let a be Vector of V;
assume S1 = a..W;
then a1 - a in W by A1,Th11;
then -(a1 -a) in W by VECTSP_4:22;
then -a1 - (-a) in W by Lm1;
hence (-a1)..W = (-a)..W by Th11;
end;
take (-a1)..W;
thus thesis by A2;
end;
uniqueness
proof
let S,T be Element of V..W such that
A3: S1 = a..W implies S = (-a)..W and
A4: S1 = a..W implies T = (-a)..W;
consider a1 such that
A5: S1 = a1..W by Th12;
thus S = (-a1)..W by A3,A5
.= T by A4,A5;
end;
let S2;
func S1 + S2 -> Element of V..W means
:Def15:
S1 = a1..W & S2 = a2..W implies it = (a1+a2)..W;
existence
proof
consider a1 such that
A6: S1 = a1..W by Th12;
consider a2 such that
A7: S2 = a2..W by Th12;
A8: now
let b1,b2 be Vector of V such that
A9: S1 = b1..W and
A10: S2 = b2..W;
A11: a1 - b1 in W by A6,A9,Th11;
a2 - b2 in W by A7,A10,Th11;
then
A12: (a1 - b1) + (a2 - b2) in W by A11,VECTSP_4:20;
(a1-b1) + (a2-b2) = a1-b1+a2-b2 by RLVECT_1:def 3
.= a1+a2-b1-b2 by Lm1
.= (a1+a2) - (b1 + b2) by VECTSP_1:17;
hence (a1 + a2)..W = (b1 + b2)..W by A12,Th11;
end;
take (a1 + a2)..W;
thus thesis by A8;
end;
uniqueness
proof
let S,T be Element of V..W such that
A13: S1 = a1..W & S2 = a2..W implies S = (a1+a2)..W and
A14: S1 = a1..W & S2 = a2..W implies T = (a1+a2)..W;
consider a1 such that
A15: S1 = a1..W by Th12;
consider a2 such that
A16: S2 = a2..W by Th12;
thus S = (a1+a2)..W by A13,A15,A16
.= T by A14,A15,A16;
end;
end;
definition
let K,V,W;
deffunc U(Element of V..W) = -$1;
func COMPL W -> UnOp of V..W means
it.S1 = -S1;
existence
proof
thus ex U being UnOp of V..W st
for S1 holds U.S1 = U(S1) from FUNCT_2:sch 4;
end;
uniqueness
proof
thus for U1,U2 being UnOp of V..W st
(for S1 holds U1.S1 = U(S1)) & (for S1 holds U2.S1 = U(S1))
holds U1 = U2 from UnOpEq;
end;
deffunc U(Element of V..W,Element of V..W) = $1 + $2;
func ADD W -> BinOp of V..W means
:Def17:
it.(S1,S2) = S1 + S2;
existence
proof
thus ex B being BinOp of V..W st
for S1,S2 holds B.(S1,S2) = U(S1,S2) from BINOP_1:sch 4;
end;
uniqueness
proof
thus for B1,B2 being BinOp of V..W st
(for S1,S2 holds B1.(S1,S2) = U(S1,S2)) &
(for S1,S2 holds B2.(S1,S2) = U(S1,S2)) holds B1 = B2 from BINOP_2:sch 2;
end;
end;
definition
let K,V,W;
func V.W -> strict addLoopStr equals
addLoopStr(#V..W,ADD W,(0.V)..W#);
coherence;
end;
registration
let K,V,W;
cluster V.W -> non empty;
coherence;
end;
theorem
a..W is Element of V.W;
definition
let K,V,W,a;
func a.W -> Element of V.W equals
a..W;
coherence;
end;
theorem Th15:
for x being Element of V.W ex a st x = a.W
proof
let x be Element of V.W;
consider a such that
A1: x = a..W by Th12;
take a;
thus thesis by A1;
end;
theorem
a1.W = a2.W iff a1 - a2 in W by Th11;
theorem Th17:
a.W + b.W = (a+b).W & 0.(V.W) = (0.V).W
proof
thus a.W + b.W = a..W + b..W by Def17
.= (a+b).W by Def15;
thus thesis;
end;
registration
let K,V,W;
cluster V.W -> Abelian add-associative right_zeroed right_complementable;
coherence
proof
set G = V.W;
hereby
let x,y be Element of G;
consider a being Vector of V such that
A1: x = a.W by Th15;
consider b being Vector of V such that
A2: y = b.W by Th15;
x+y = (a+b).W by A1,A2,Th17;
hence x+y = y+x by A1,A2,Th17;
end;
hereby
let x,y,z be Element of G;
consider a being Vector of V such that
A3: x = a.W by Th15;
consider b being Vector of V such that
A4: y = b.W by Th15;
consider c being Vector of V such that
A5: z = c.W by Th15;
A6: x+y = (a+b).W by A3,A4,Th17;
A7: y+z = (b+c).W by A4,A5,Th17;
thus (x+y)+z = (a+b+c).W by A5,A6,Th17
.= (a+(b+c)).W by RLVECT_1:def 3
.= x+(y+z) by A3,A7,Th17;
end;
hereby
let x be Element of G;
consider a being Vector of V such that
A8: x = a.W by Th15;
0.G = (0.V).W;
hence x+(0.G) = (a+0.V).W by A8,Th17
.= x by A8,RLVECT_1:4;
end;
let x be Element of G;
consider a being Vector of V such that
A9: x = a.W by Th15;
consider b being Vector of V such that
A10: a + b = 0.V by ALGSTR_0:def 11;
reconsider b9 = b.W as Element of G;
take b9;
thus x+b9 = (0.V).W by A9,A10,Th17
.= 0.G;
end;
end;
reserve S for Element of V.W;
definition
let K,V,W,r,S;
func r*S -> Element of V.W means
:Def20:
S = a.W implies it = (r*a).W;
existence
proof
consider a1 such that
A1: S = a1.W by Th15;
A2: now
let a;
assume S = a.W;
then a - a1 in W by A1,Th11;
then r*(a-a1) in W by VECTSP_4:21;
then r*a - r*a1 in W by VECTSP_1:23;
hence (r*a).W = (r*a1).W by Th11;
end;
take (r*a1).W;
thus thesis by A2;
end;
uniqueness
proof
let S1,S2 be Element of V.W such that
A3: S = a.W implies S1 = (r*a).W and
A4: S = a.W implies S2 = (r*a).W;
consider a1 such that
A5: S = a1.W by Th15;
thus S1 = (r*a1).W by A3,A5
.= S2 by A4,A5;
end;
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
:Def21:
it.(r,S) = r*S;
existence
proof
deffunc U(Scalar of K,Element of V.W) = $1 * $2;
consider F being Function of [:the carrier of K,the carrier of V.W:],
the carrier of V.W such that
A1: F.(r,S) = U(r,S) from BINOP_1:sch 4;
take F;
thus thesis by A1;
end;
uniqueness
proof
let F,G be Function of [:the carrier of K,the carrier of V.W:],
the carrier of V.W such that
A2: F.(r,S) = r*S and
A3: G.(r,S) = r*S;
now
let r,S;
thus F.(r,S) = r*S by A2
.= G.(r,S) by A3;
end;
hence thesis by BINOP_1:2;
end;
end;
begin
definition
let K,V,W;
func V/W -> strict ModuleStr over K equals
ModuleStr(#the carrier of V.W,the addF of V.W,0.V.W,LMULT W#);
coherence;
end;
registration
let K,V,W;
cluster V/W -> non empty;
coherence;
end;
theorem
a.W is Vector of V/W;
theorem
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
a.W;
coherence;
end;
theorem Th20:
for x being Vector of V/W ex a st x = a/W
proof
let x be Vector of V/W;
consider a such that
A1: x = a.W by Th15;
take a;
thus thesis by A1;
end;
theorem
a1/W = a2/W iff a1 - a2 in W by Th11;
theorem Th22:
a/W + b/W = (a+b)/W & r*(a/W) = (r*a)/W
proof
thus a/W + b/W = a.W + b.W .= (a+b)/W by Th17;
thus r*(a/W) = (LMULT W).(r,a.W) by VECTSP_1:def 12
.= r*(a.W qua Element of V.W) by Def21
.= (r*a)/W by Def20;
end;
Lm2: V/W is Abelian add-associative right_zeroed right_complementable
proof
A1: for x,y,z be Element of V.W, x9,y9,z9 be Vector of V/W
st x = x9 & y = y9 & z = z9 holds x + y = x9+ y9;
thus V/W is Abelian
proof
let x,y be Vector of V/W;
reconsider x9= x, y9= y as Element of V.W;
thus x+y = x9+ y9 .= y + x by A1;
end;
hereby
let x,y,z be Vector of V/W;
reconsider x9= x, y9= y, z9= z as Element of V.W;
thus (x+y)+z = (x9+ y9) + z9 .= x9+ (y9+ z9) by RLVECT_1:def 3
.=
x + (y + z);
end;
hereby
let x be Vector of V/W;
reconsider x9= x as Element of V.W;
thus x+(0.(V/W)) = x9+ (0.(V.W)) .= x by RLVECT_1:4;
end;
let x be Vector of V/W;
reconsider x9= x as Element of V.W;
consider b being Element of V.W such that
A2: x9 + b = 0.(V.W) by ALGSTR_0:def 11;
reconsider b9 = b as Vector of V/W;
take b9;
thus thesis by A2;
end;
theorem Th23:
V/W is strict LeftMod of K
proof
now
let x,y be Scalar of K, v,w be Vector of V/W;
consider a such that
A1: v = a/W by Th20;
consider b such that
A2: w = b/W by Th20;
A3: (x*a)/W = x*v by A1,Th22;
A4: (x*b)/W = x*w by A2,Th22;
A5: (y*a)/W = y*v by A1,Th22;
thus x*(v+w) = x*((a+b)/W) by A1,A2,Th22
.= (x*(a+b))/W by Th22
.= (x*a+x*b)/W by VECTSP_1:def 14
.= x*v+x*w by A3,A4,Th22;
thus (x+y)*v = ((x+y)*a)/W by A1,Th22
.= (x*a+y*a)/W by VECTSP_1:def 15
.= x*v+y*v by A3,A5,Th22;
thus (x*y)*v = ((x*y)*a)/W by A1,Th22
.= (x*(y*a))/W by VECTSP_1:def 16
.= x*((y*a)/W) by Th22
.= x*(y*v) by A1,Th22;
thus 1_K*v = (1_K*a)/W by A1,Th22
.= v by A1;
end;
hence thesis by Lm2,VECTSP_1:def 14,def 15,def 16,def 17;
end;
registration
let K,V,W;
cluster V/W -> vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence by Th23;
end;