:: Operations on Subspaces in Vector Space
:: by Wojciech A. Trybulec
::
:: Received July 27, 1990
:: Copyright (c) 1990-2021 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 RLVECT_1, ALGSTR_0, BINOP_1, VECTSP_1, LATTICES, XBOOLE_0,
RLSUB_1, SUBSET_1, ARYTM_3, STRUCT_0, TARSKI, SUPINF_2, ARYTM_1, RLSUB_2,
ZFMISC_1, FUNCT_1, RELAT_1, GROUP_1, FINSEQ_4, MCART_1, EQREL_1, PBOOLE;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, RELAT_1, FUNCT_1,
STRUCT_0, ALGSTR_0, LATTICES, RELSET_1, RLVECT_1, GROUP_1, VECTSP_1,
DOMAIN_1, VECTSP_4;
constructors BINOP_1, REALSET1, LATTICES, VECTSP_4;
registrations SUBSET_1, STRUCT_0, LATTICES, VECTSP_1, VECTSP_4, RELAT_1,
XTUPLE_0;
requirements SUBSET, BOOLE;
begin
reserve GF for add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
reserve M for Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over GF;
reserve W,W1,W2,W3 for Subspace of M;
reserve u,u1,u2,v,v1,v2 for Element of M;
reserve X,Y for set, x,y,y1,y2 for object;
definition
let GF;
let M;
let W1,W2;
func W1 + W2 -> strict Subspace of M means
:: VECTSP_5:def 1
the carrier of it = {v + u : v in W1 & u in W2};
end;
definition
let GF;
let M;
let W1,W2;
func W1 /\ W2 -> strict Subspace of M means
:: VECTSP_5:def 2
the carrier of it = (the carrier of W1) /\ (the carrier of W2);
commutativity;
end;
theorem :: VECTSP_5:1
x in W1 + W2 iff ex v1,v2 st v1 in W1 & v2 in W2 & x = v1 + v2;
theorem :: VECTSP_5:2
v in W1 or v in W2 implies v in W1 + W2;
theorem :: VECTSP_5:3
x in W1 /\ W2 iff x in W1 & x in W2;
theorem :: VECTSP_5:4
for W being strict Subspace of M holds W + W = W;
theorem :: VECTSP_5:5
W1 + W2 = W2 + W1;
theorem :: VECTSP_5:6
W1 + (W2 + W3) = (W1 + W2) + W3;
theorem :: VECTSP_5:7
W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2;
theorem :: VECTSP_5:8
for W2 being strict Subspace of M holds W1 is Subspace of W2 iff W1 + W2 = W2
;
theorem :: VECTSP_5:9
for W being strict Subspace of M holds (0).M + W = W & W + (0).M = W;
theorem :: VECTSP_5:10
(0).M + (Omega).M = the ModuleStr of M & (Omega). M + (0).M = the
ModuleStr of M;
theorem :: VECTSP_5:11
(Omega).M + W = the ModuleStr of M & W + (Omega).M = the ModuleStr of M;
theorem :: VECTSP_5:12
for M being strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF holds (Omega).M
+ (Omega).M = M;
theorem :: VECTSP_5:13
for W being strict Subspace of M holds W /\ W = W;
theorem :: VECTSP_5:14
W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3;
theorem :: VECTSP_5:15
W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2;
theorem :: VECTSP_5:16
(for W1 being strict Subspace of M holds W1 is Subspace of W2
implies W1 /\ W2 = W1) & for W1 st W1 /\ W2 = W1 holds W1 is Subspace of W2;
theorem :: VECTSP_5:17
W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3;
theorem :: VECTSP_5:18
W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3;
theorem :: VECTSP_5:19
W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of
W2 /\ W3;
theorem :: VECTSP_5:20
(0).M /\ W = (0).M & W /\ (0).M = (0).M;
theorem :: VECTSP_5:21
for W being strict Subspace of M holds (Omega).M /\ W = W & W /\
(Omega).M = W;
theorem :: VECTSP_5:22
for M being strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF holds (Omega).M
/\ (Omega).M = M;
theorem :: VECTSP_5:23
W1 /\ W2 is Subspace of W1 + W2;
theorem :: VECTSP_5:24
for W2 being strict Subspace of M holds (W1 /\ W2) + W2 = W2;
theorem :: VECTSP_5:25
for W1 being strict Subspace of M holds W1 /\ (W1 + W2) = W1;
theorem :: VECTSP_5:26
(W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3);
theorem :: VECTSP_5:27
W1 is Subspace of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3);
theorem :: VECTSP_5:28
W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3);
theorem :: VECTSP_5:29
W1 is Subspace of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3);
theorem :: VECTSP_5:30
for W1 being strict Subspace of M holds W1 is Subspace of W3
implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3;
theorem :: VECTSP_5:31
for W1,W2 being strict Subspace of M holds W1 + W2 = W2 iff W1 /\ W2 = W1;
theorem :: VECTSP_5:32
for W2,W3 being strict Subspace of M holds W1 is Subspace of W2
implies W1 + W3 is Subspace of W2 + W3;
theorem :: VECTSP_5:33
W1 is Subspace of W2 implies W1 is Subspace of W2 + W3;
theorem :: VECTSP_5:34
W1 is Subspace of W3 & W2 is Subspace of W3 implies W1 + W2 is Subspace of W3
;
theorem :: VECTSP_5:35
(ex W st the carrier of W = (the carrier of W1) \/ (the carrier of W2)
) iff W1 is Subspace of W2 or W2 is Subspace of W1;
definition
let GF;
let M;
func Subspaces(M) -> set means
:: VECTSP_5:def 3
for x being object
holds x in it iff ex W being strict Subspace of M st W = x;
end;
registration
let GF;
let M;
cluster Subspaces(M) -> non empty;
end;
theorem :: VECTSP_5:36
for M being strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF holds M in
Subspaces(M);
definition
let GF;
let M;
let W1,W2;
pred M is_the_direct_sum_of W1,W2 means
:: VECTSP_5:def 4
the ModuleStr of M = W1 + W2 & W1 /\ W2 = (0).M;
end;
reserve F for Field;
reserve V for VectSp of F;
reserve W for Subspace of V;
definition
let F,V,W;
mode Linear_Compl of W -> Subspace of V means
:: VECTSP_5:def 5
V is_the_direct_sum_of it,W;
end;
reserve W,W1,W2 for Subspace of V;
theorem :: VECTSP_5:37
V is_the_direct_sum_of W1,W2 implies W2 is Linear_Compl of W1;
theorem :: VECTSP_5:38
for L being Linear_Compl of W holds V is_the_direct_sum_of L,W &
V is_the_direct_sum_of W,L;
theorem :: VECTSP_5:39
for L being Linear_Compl of W holds W + L = the ModuleStr of V &
L + W = the ModuleStr of V;
theorem :: VECTSP_5:40
for L being Linear_Compl of W holds W /\ L = (0).V & L /\ W = (0).V;
reserve W1,W2 for Subspace of M;
theorem :: VECTSP_5:41
M is_the_direct_sum_of W1,W2 implies M is_the_direct_sum_of W2,W1;
theorem :: VECTSP_5:42
M is_the_direct_sum_of (0).M,(Omega).M & M is_the_direct_sum_of
(Omega). M,(0).M;
reserve W for Subspace of V;
theorem :: VECTSP_5:43
for L being Linear_Compl of W holds W is Linear_Compl of L;
theorem :: VECTSP_5:44
(0).V is Linear_Compl of (Omega).V & (Omega).V is Linear_Compl of (0). V;
reserve W1,W2 for Subspace of M;
reserve u,u1,u2,v for Element of M;
reserve C1 for Coset of W1;
reserve C2 for Coset of W2;
theorem :: VECTSP_5:45
C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2;
theorem :: VECTSP_5:46
M is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1, C2
being Coset of W2 ex v being Element of M st C1 /\ C2 = {v};
theorem :: VECTSP_5:47
for M being strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital
non empty ModuleStr over GF, W1,W2 being
Subspace of M holds W1 + W2 = M iff for v being Element of M ex v1,v2 being
Element of M st v1 in W1 & v2 in W2 & v = v1 + v2;
theorem :: VECTSP_5:48
for v,v1,v2,u1,u2 being Element of M holds M
is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 &
v2 in W2 & u2 in W2 implies v1 = u1 & v2 = u2;
theorem :: VECTSP_5:49
M = W1 + W2 & (ex v st for v1,v2,u1,u2 being Element of M st v = v1 +
v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds v1 = u1 & v2
= u2) implies M is_the_direct_sum_of W1,W2;
reserve t1,t2 for Element of [:the carrier of M, the carrier of M:];
definition
let GF,M,v,W1,W2;
assume
M is_the_direct_sum_of W1,W2;
func v |-- (W1,W2) -> Element of [:the carrier of M,the carrier of M:] means
:: VECTSP_5:def 6
v = it`1 + it`2 & it`1 in W1 & it`2 in W2;
end;
theorem :: VECTSP_5:50
M is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`1 = (v |-- (W2,W1))`2;
theorem :: VECTSP_5:51
M is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`2 = (v |-- (W2,W1))`1;
reserve W for Subspace of V;
theorem :: VECTSP_5:52
for L being Linear_Compl of W, v being Element of V, t being Element
of [:the carrier of V,the carrier of V:] holds t`1 + t`2 = v & t`1 in W & t`2
in L implies t = v |-- (W,L);
theorem :: VECTSP_5:53
for L being Linear_Compl of W, v being Element of V holds (v |-- (W,L)
)`1 + (v |-- (W,L))`2 = v;
theorem :: VECTSP_5:54
for L being Linear_Compl of W, v being Element of V holds (v |-- (W,L)
)`1 in W & (v |-- (W,L))`2 in L;
theorem :: VECTSP_5:55
for L being Linear_Compl of W, v being Element of V holds (v |-- (W,L)
)`1 = (v |-- (L,W))`2;
theorem :: VECTSP_5:56
for L being Linear_Compl of W, v being Element of V holds (v |-- (W,L)
)`2 = (v |-- (L,W))`1;
reserve A1,A2,B for Element of Subspaces(M),
W1,W2 for Subspace of M;
definition
let GF;
let M;
func SubJoin M -> BinOp of Subspaces M means
:: VECTSP_5:def 7
for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 + W2;
end;
definition
let GF;
let M;
func SubMeet M -> BinOp of Subspaces M means
:: VECTSP_5:def 8
for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 /\ W2;
end;
theorem :: VECTSP_5:57
LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is Lattice;
theorem :: VECTSP_5:58
LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is 0_Lattice;
theorem :: VECTSP_5:59
LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is 1_Lattice;
theorem :: VECTSP_5:60
LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is 01_Lattice;
theorem :: VECTSP_5:61
LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is M_Lattice;
theorem :: VECTSP_5:62
for F being Field, V being VectSp of F holds LattStr (# Subspaces(V),
SubJoin(V), SubMeet(V) #) is C_Lattice;