Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Operations on Subspaces in Real Linear Space

**by****Wojciech A. Trybulec**- Received September 20, 1989
- MML identifier: RLSUB_2

- [ Mizar article, MML identifier index ]

environ vocabulary RLVECT_1, RLSUB_1, BOOLE, ARYTM_1, FUNCT_1, RELAT_1, TARSKI, MCART_1, BINOP_1, LATTICES, RLSUB_2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, RELAT_1, FUNCT_1, LATTICES, REAL_1, RELSET_1, STRUCT_0, RLVECT_1, RLSUB_1, DOMAIN_1; constructors BINOP_1, LATTICES, REAL_1, RLSUB_1, DOMAIN_1, MEMBERED, XBOOLE_0; clusters LATTICES, RLVECT_1, RLSUB_1, STRUCT_0, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_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 for set; reserve 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. :: canceled 4; theorem :: RLSUB_2:5 x in W1 + W2 iff (ex v1,v2 st v1 in W1 & v2 in W2 & x = v1 + v2); theorem :: RLSUB_2:6 v in W1 or v in W2 implies v in W1 + W2; theorem :: RLSUB_2:7 x in W1 /\ W2 iff x in W1 & x in W2; theorem :: RLSUB_2:8 for W being strict Subspace of V holds W + W = W; theorem :: RLSUB_2:9 W1 + W2 = W2 + W1; theorem :: RLSUB_2:10 W1 + (W2 + W3) = (W1 + W2) + W3; theorem :: RLSUB_2:11 W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2; theorem :: RLSUB_2:12 for W2 being strict Subspace of V holds W1 is Subspace of W2 iff W1 + W2 = W2; theorem :: RLSUB_2:13 for W being strict Subspace of V holds (0).V + W = W & W + (0).V = W; theorem :: RLSUB_2:14 (0).V + (Omega).V = the RLSStruct of V & (Omega). V + (0).V = the RLSStruct of V; theorem :: RLSUB_2:15 (Omega).V + W = the RLSStruct of V & W + (Omega).V = the RLSStruct of V; theorem :: RLSUB_2:16 for V being strict RealLinearSpace holds (Omega).V + (Omega).V = V; theorem :: RLSUB_2:17 for W being strict Subspace of V holds W /\ W = W; theorem :: RLSUB_2:18 W1 /\ W2 = W2 /\ W1; theorem :: RLSUB_2:19 W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3; theorem :: RLSUB_2:20 W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2; theorem :: RLSUB_2:21 for W1 being strict Subspace of V holds W1 is Subspace of W2 iff W1 /\ W2 = W1; theorem :: RLSUB_2:22 (0).V /\ W = (0).V & W /\ (0).V = (0).V; theorem :: RLSUB_2:23 (0).V /\ (Omega).V = (0).V & (Omega).V /\ (0).V = (0).V; theorem :: RLSUB_2:24 for W being strict Subspace of V holds (Omega).V /\ W = W & W /\ (Omega).V = W; theorem :: RLSUB_2:25 for V being strict RealLinearSpace holds (Omega).V /\ (Omega).V = V; theorem :: RLSUB_2:26 W1 /\ W2 is Subspace of W1 + W2; theorem :: RLSUB_2:27 for W2 being strict Subspace of V holds (W1 /\ W2) + W2 = W2; theorem :: RLSUB_2:28 for W1 being strict Subspace of V holds W1 /\ (W1 + W2) = W1; theorem :: RLSUB_2:29 (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3); theorem :: RLSUB_2:30 W1 is Subspace of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3); theorem :: RLSUB_2:31 W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3); theorem :: RLSUB_2:32 W1 is Subspace of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3); theorem :: RLSUB_2:33 W1 is strict Subspace of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3; theorem :: RLSUB_2:34 for W1,W2 being strict Subspace of V holds W1 + W2 = W2 iff W1 /\ W2 = W1; theorem :: RLSUB_2:35 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:36 (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 holds x in it iff x is strict Subspace of V; end; definition let V; cluster Subspaces(V) -> non empty; end; canceled 2; theorem :: RLSUB_2:39 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; definition let V be RealLinearSpace; let W be Subspace of V; cluster strict Linear_Compl of W; end; canceled 2; theorem :: RLSUB_2:42 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:43 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:44 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:45 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:46 V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2,W1; theorem :: RLSUB_2:47 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:48 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:49 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:50 C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2; theorem :: RLSUB_2:51 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:52 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:53 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:54 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; canceled 4; theorem :: RLSUB_2:59 V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`1 = (v |-- (W2,W1))`2; theorem :: RLSUB_2:60 V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`2 = (v |-- (W2,W1))`1; theorem :: RLSUB_2:61 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:62 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:63 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:64 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:65 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. :: definition let X be non empty set, m,u be BinOp of X; cluster LattStr(#X,m,u#) -> non empty; end; canceled 4; theorem :: RLSUB_2:70 LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is Lattice; definition let V; cluster LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) -> Lattice-like; end; theorem :: RLSUB_2:71 for V being RealLinearSpace holds LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is lower-bounded; theorem :: RLSUB_2:72 for V being RealLinearSpace holds LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is upper-bounded; theorem :: RLSUB_2:73 for V being RealLinearSpace holds LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is 01_Lattice; theorem :: RLSUB_2:74 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:75 for V being RealLinearSpace holds LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is complemented; definition 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:76 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:77 X c< Y implies ex x st x in Y & not x in X; theorem :: RLSUB_2:78 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v,v1,v2 being Element of V holds v = v1 + v2 iff v1 = v - v2; theorem :: RLSUB_2:79 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:80 ex C st v in C; canceled 3; theorem :: RLSUB_2:84 (for a holds a "/\" b = b) implies b = Bottom l; theorem :: RLSUB_2:85 (for a holds a "\/" b = b) implies b = Top l;

Back to top