:: Operations on Subspaces in Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received September 20, 1989
:: Copyright (c) 1990-2017 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, RLSUB_1, REAL_1, ARYTM_3, STRUCT_0, SUBSET_1, TARSKI,
SUPINF_2, XBOOLE_0, ARYTM_1, ZFMISC_1, FUNCT_1, RELAT_1, ALGSTR_0,
CARD_1, FINSEQ_4, MCART_1, BINOP_1, LATTICES, EQREL_1, PBOOLE, RLSUB_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, RELAT_1, FUNCT_1,
ORDINAL1, NUMBERS, LATTICES, XCMPLX_0, XREAL_0, REAL_1, RELSET_1,
STRUCT_0, ALGSTR_0, RLVECT_1, RLSUB_1, DOMAIN_1;
constructors BINOP_1, REAL_1, MEMBERED, REALSET1, LATTICES, RLSUB_1;
registrations SUBSET_1, MEMBERED, STRUCT_0, LATTICES, RLVECT_1, RLSUB_1,
RELAT_1, XREAL_0, XTUPLE_0;
requirements NUMERALS, SUBSET, BOOLE;
begin
reserve V for RealLinearSpace;
reserve W,W1,W2,W3 for Subspace of V;
reserve u,u1,u2,v,v1,v2 for VECTOR of V;
reserve a,a1,a2 for Real;
reserve X,Y,x,y,y1,y2 for set;
::
:: Definitions of sum and intersection of subspaces.
::
definition
let V;
let W1,W2;
func W1 + W2 -> strict Subspace of V means
:: RLSUB_2:def 1
the carrier of it = {v + u : v in W1 & u in W2};
end;
definition
let V;
let W1,W2;
func W1 /\ W2 -> strict Subspace of V means
:: RLSUB_2:def 2
the carrier of it = (the carrier of W1) /\ (the carrier of W2);
end;
::
:: Definitional theorems of sum and intersection of subspaces.
::
theorem :: RLSUB_2:1
for x being object holds
x in W1 + W2 iff ex v1,v2 st v1 in W1 & v2 in W2 & x = v1 + v2;
theorem :: RLSUB_2:2
v in W1 or v in W2 implies v in W1 + W2;
theorem :: RLSUB_2:3
for x being object holds x in W1 /\ W2 iff x in W1 & x in W2;
theorem :: RLSUB_2:4
for W being strict Subspace of V holds W + W = W;
theorem :: RLSUB_2:5
W1 + W2 = W2 + W1;
theorem :: RLSUB_2:6
W1 + (W2 + W3) = (W1 + W2) + W3;
theorem :: RLSUB_2:7
W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2;
theorem :: RLSUB_2:8
for W2 being strict Subspace of V holds W1 is Subspace of W2 iff W1 + W2 = W2
;
theorem :: RLSUB_2:9
for W being strict Subspace of V holds (0).V + W = W & W + (0).V = W;
theorem :: RLSUB_2:10
(0).V + (Omega).V = the RLSStruct of V & (Omega). V + (0).V = the
RLSStruct of V;
theorem :: RLSUB_2:11
(Omega).V + W = the RLSStruct of V & W + (Omega).V = the RLSStruct of V;
theorem :: RLSUB_2:12
for V being strict RealLinearSpace holds (Omega).V + (Omega).V = V;
theorem :: RLSUB_2:13
for W being strict Subspace of V holds W /\ W = W;
theorem :: RLSUB_2:14
W1 /\ W2 = W2 /\ W1;
theorem :: RLSUB_2:15
W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3;
theorem :: RLSUB_2:16
W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2;
theorem :: RLSUB_2:17
for W1 being strict Subspace of V holds W1 is Subspace of W2 iff
W1 /\ W2 = W1;
theorem :: RLSUB_2:18
(0).V /\ W = (0).V & W /\ (0).V = (0).V;
theorem :: RLSUB_2:19
(0).V /\ (Omega).V = (0).V & (Omega).V /\ (0).V = (0).V;
theorem :: RLSUB_2:20
for W being strict Subspace of V holds (Omega).V /\ W = W & W /\
(Omega).V = W;
theorem :: RLSUB_2:21
for V being strict RealLinearSpace holds (Omega).V /\ (Omega).V = V;
theorem :: RLSUB_2:22
W1 /\ W2 is Subspace of W1 + W2;
theorem :: RLSUB_2:23
for W2 being strict Subspace of V holds (W1 /\ W2) + W2 = W2;
theorem :: RLSUB_2:24
for W1 being strict Subspace of V holds W1 /\ (W1 + W2) = W1;
theorem :: RLSUB_2:25
(W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3);
theorem :: RLSUB_2:26
W1 is Subspace of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3);
theorem :: RLSUB_2:27
W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3);
theorem :: RLSUB_2:28
W1 is Subspace of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3);
theorem :: RLSUB_2:29
W1 is strict Subspace of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3;
theorem :: RLSUB_2:30
for W1,W2 being strict Subspace of V holds W1 + W2 = W2 iff W1 /\ W2 = W1;
theorem :: RLSUB_2:31
for W2,W3 being strict Subspace of V holds W1 is Subspace of W2
implies W1 + W3 is Subspace of W2 + W3;
theorem :: RLSUB_2:32
(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;
::
:: Introduction of a set of subspaces of real linear space.
::
definition
let V;
func Subspaces(V) -> set means
:: RLSUB_2:def 3
for x being object holds x in it iff x is strict Subspace of V;
end;
registration
let V;
cluster Subspaces(V) -> non empty;
end;
theorem :: RLSUB_2:33
for V being strict RealLinearSpace holds V in Subspaces(V);
::
:: Introduction of the direct sum of subspaces and
:: linear complement of subspace.
::
definition
let V;
let W1,W2;
pred V is_the_direct_sum_of W1,W2 means
:: RLSUB_2:def 4
the RLSStruct of V = W1 + W2 & W1 /\ W2 = (0).V;
end;
definition
let V be RealLinearSpace;
let W be Subspace of V;
mode Linear_Compl of W -> Subspace of V means
:: RLSUB_2:def 5
V is_the_direct_sum_of it,W;
end;
registration
let V be RealLinearSpace;
let W be Subspace of V;
cluster strict for Linear_Compl of W;
end;
theorem :: RLSUB_2:34
for V being RealLinearSpace, W1,W2 being Subspace of V holds V
is_the_direct_sum_of W1,W2 implies W2 is Linear_Compl of W1;
theorem :: RLSUB_2:35
for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W holds V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L
;
::
:: Theorems concerning the direct sum of a subspaces,
:: linear complement of a subspace and coset of a subspace.
::
theorem :: RLSUB_2:36
for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W holds W + L = the RLSStruct of V & L + W = the RLSStruct of V
;
theorem :: RLSUB_2:37
for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W holds W /\ L = (0).V & L /\ W = (0).V;
theorem :: RLSUB_2:38
V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2,W1;
theorem :: RLSUB_2:39
for V being RealLinearSpace holds V is_the_direct_sum_of (0).V,
(Omega).V & V is_the_direct_sum_of (Omega).V,(0).V;
theorem :: RLSUB_2:40
for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W holds W is Linear_Compl of L;
theorem :: RLSUB_2:41
for V being RealLinearSpace holds (0).V is Linear_Compl of (Omega).V &
(Omega).V is Linear_Compl of (0).V;
reserve C for Coset of W;
reserve C1 for Coset of W1;
reserve C2 for Coset of W2;
theorem :: RLSUB_2:42
C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2;
theorem :: RLSUB_2:43
for V being RealLinearSpace, W1,W2 being Subspace of V holds V
is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1, C2 being Coset of W2
ex v being VECTOR of V st C1 /\ C2 = {v};
::
:: Decomposition of a vector.
::
theorem :: RLSUB_2:44
for V being RealLinearSpace, W1,W2 being Subspace of V holds W1 + W2 =
the RLSStruct of V iff for v being VECTOR of V ex v1,v2 being VECTOR of V st v1
in W1 & v2 in W2 & v = v1 + v2;
theorem :: RLSUB_2:45
V 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 :: RLSUB_2:46
V = W1 + W2 & (ex v st for v1,v2,u1,u2 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 V
is_the_direct_sum_of W1,W2;
reserve t1,t2 for Element of [:the carrier of V, the carrier of V:];
definition
let V;
let v;
let W1,W2;
assume
V is_the_direct_sum_of W1,W2;
func v |-- (W1,W2) -> Element of [:the carrier of V, the carrier of V:]
means
:: RLSUB_2:def 6
v = it`1 + it`2 & it`1 in W1 & it`2 in W2;
end;
theorem :: RLSUB_2:47
V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`1 = (v |-- (W2,W1))`2;
theorem :: RLSUB_2:48
V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`2 = (v |-- (W2,W1))`1;
theorem :: RLSUB_2:49
for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W, v being VECTOR 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 :: RLSUB_2:50
for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W, v being VECTOR of V holds (v |-- (W,L))`1 + (v |-- (W,L))`2
= v;
theorem :: RLSUB_2:51
for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W, v being VECTOR of V holds (v |-- (W,L))`1 in W & (v |-- (W,L
))`2 in L;
theorem :: RLSUB_2:52
for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W, v being VECTOR of V holds (v |-- (W,L))`1 = (v |-- (L,W))`2;
theorem :: RLSUB_2:53
for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W, v being VECTOR of V holds (v |-- (W,L))`2 = (v |-- (L,W))`1;
::
:: Introduction of operations on set of subspaces as binary operations.
::
reserve A1,A2,B for Element of Subspaces(V);
definition
let V;
func SubJoin(V) -> BinOp of Subspaces(V) means
:: RLSUB_2:def 7
for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 + W2;
end;
definition
let V;
func SubMeet(V) -> BinOp of Subspaces(V) means
:: RLSUB_2:def 8
for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 /\ W2;
end;
::
:: Definitional theorems of functions SubJoin, SubMeet.
::
theorem :: RLSUB_2:54
LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is Lattice;
registration
let V;
cluster LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) -> Lattice-like;
end;
theorem :: RLSUB_2:55
for V being RealLinearSpace holds LattStr (# Subspaces(V),
SubJoin(V), SubMeet(V) #) is lower-bounded;
theorem :: RLSUB_2:56
for V being RealLinearSpace holds LattStr (# Subspaces(V),
SubJoin(V), SubMeet(V) #) is upper-bounded;
theorem :: RLSUB_2:57
for V being RealLinearSpace holds LattStr (# Subspaces(V),
SubJoin(V), SubMeet(V) #) is 01_Lattice;
theorem :: RLSUB_2:58
for V being RealLinearSpace holds LattStr (# Subspaces(V),
SubJoin(V), SubMeet(V) #) is modular;
reserve l for Lattice;
reserve a,b for Element of l;
theorem :: RLSUB_2:59
for V being RealLinearSpace holds LattStr (# Subspaces(V),
SubJoin(V), SubMeet(V) #) is complemented;
registration
let V;
cluster LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) -> lower-bounded
upper-bounded modular complemented;
end;
::
:: Theorems concerning operations on subspaces (continuation). Proven
:: on the basis that set of subspaces with operations is a lattice.
::
theorem :: RLSUB_2:60
for V being RealLinearSpace, W1,W2,W3 being strict Subspace of V holds
W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3;
::
:: Auxiliary theorems.
::
theorem :: RLSUB_2:61
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v,v1,v2 being Element of V holds v = v1 + v2 iff v1 = v - v2;
theorem :: RLSUB_2:62
for V being RealLinearSpace, W being strict Subspace of V holds (for v
being VECTOR of V holds v in W) implies W = the RLSStruct of V;
theorem :: RLSUB_2:63
ex C st v in C;
theorem :: RLSUB_2:64
(for a holds a "/\" b = b) implies b = Bottom l;
theorem :: RLSUB_2:65
(for a holds a "\/" b = b) implies b = Top l;