Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Operations on Subspaces in Vector Space

**by****Wojciech A. Trybulec**- Received July 27, 1990
- MML identifier: VECTSP_5

- [ Mizar article, MML identifier index ]

environ vocabulary RLVECT_1, BINOP_1, VECTSP_1, LATTICES, RLSUB_1, BOOLE, ARYTM_1, RLSUB_2, FUNCT_1, RELAT_1, TARSKI, MCART_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, RELAT_1, FUNCT_1, STRUCT_0, LATTICES, RELSET_1, RLVECT_1, VECTSP_1, DOMAIN_1, VECTSP_4; constructors BINOP_1, LATTICES, DOMAIN_1, VECTSP_4, MEMBERED, XBOOLE_0; clusters LATTICES, VECTSP_1, VECTSP_4, STRUCT_0, RLSUB_2, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin reserve GF for add-associative right_zeroed right_complementable Abelian associative left_unital distributive (non empty doubleLoopStr); reserve M for Abelian add-associative right_zeroed right_complementable VectSp-like (non empty VectSpStr 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,x,y,y1,y2 for set; 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; canceled 4; theorem :: VECTSP_5:5 x in W1 + W2 iff (ex v1,v2 st v1 in W1 & v2 in W2 & x = v1 + v2); theorem :: VECTSP_5:6 v in W1 or v in W2 implies v in W1 + W2; theorem :: VECTSP_5:7 x in W1 /\ W2 iff x in W1 & x in W2; theorem :: VECTSP_5:8 for W being strict Subspace of M holds W + W = W; theorem :: VECTSP_5:9 W1 + W2 = W2 + W1; theorem :: VECTSP_5:10 W1 + (W2 + W3) = (W1 + W2) + W3; theorem :: VECTSP_5:11 W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2; theorem :: VECTSP_5:12 for W2 being strict Subspace of M holds W1 is Subspace of W2 iff W1 + W2 = W2; theorem :: VECTSP_5:13 for W being strict Subspace of M holds (0).M + W = W & W + (0).M = W; theorem :: VECTSP_5:14 (0).M + (Omega).M = the VectSpStr of M & (Omega). M + (0).M = the VectSpStr of M; theorem :: VECTSP_5:15 (Omega).M + W = the VectSpStr of M & W + (Omega).M = the VectSpStr of M; theorem :: VECTSP_5:16 for M being strict Abelian add-associative right_zeroed right_complementable VectSp-like (non empty VectSpStr over GF) holds (Omega).M + (Omega).M = M; theorem :: VECTSP_5:17 for W being strict Subspace of M holds W /\ W = W; theorem :: VECTSP_5:18 W1 /\ W2 = W2 /\ W1; theorem :: VECTSP_5:19 W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3; theorem :: VECTSP_5:20 W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2; theorem :: VECTSP_5:21 (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:22 W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3; theorem :: VECTSP_5:23 W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3; theorem :: VECTSP_5:24 W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of W2 /\ W3; theorem :: VECTSP_5:25 (0).M /\ W = (0).M & W /\ (0).M = (0).M; canceled; theorem :: VECTSP_5:27 for W being strict Subspace of M holds (Omega).M /\ W = W & W /\ (Omega).M = W; theorem :: VECTSP_5:28 for M being strict Abelian add-associative right_zeroed right_complementable VectSp-like (non empty VectSpStr over GF) holds (Omega).M /\ (Omega).M = M; theorem :: VECTSP_5:29 W1 /\ W2 is Subspace of W1 + W2; theorem :: VECTSP_5:30 for W2 being strict Subspace of M holds (W1 /\ W2) + W2 = W2; theorem :: VECTSP_5:31 for W1 being strict Subspace of M holds W1 /\ (W1 + W2) = W1; theorem :: VECTSP_5:32 (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3); theorem :: VECTSP_5:33 W1 is Subspace of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3); theorem :: VECTSP_5:34 W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3); theorem :: VECTSP_5:35 W1 is Subspace of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3); theorem :: VECTSP_5:36 for W1 being strict Subspace of M holds W1 is Subspace of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3; theorem :: VECTSP_5:37 for W1,W2 being strict Subspace of M holds W1 + W2 = W2 iff W1 /\ W2 = W1; theorem :: VECTSP_5:38 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:39 W1 is Subspace of W2 implies W1 is Subspace of W2 + W3; theorem :: VECTSP_5:40 W1 is Subspace of W3 & W2 is Subspace of W3 implies W1 + W2 is Subspace of W3; theorem :: VECTSP_5:41 (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 holds x in it iff ex W being strict Subspace of M st W = x; end; definition let GF; let M; cluster Subspaces(M) -> non empty; end; canceled 2; theorem :: VECTSP_5:44 for M being strict Abelian add-associative right_zeroed right_complementable VectSp-like (non empty VectSpStr 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 VectSpStr 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; canceled 2; theorem :: VECTSP_5:47 V is_the_direct_sum_of W1,W2 implies W2 is Linear_Compl of W1; theorem :: VECTSP_5:48 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:49 for L being Linear_Compl of W holds W + L = the VectSpStr of V & L + W = the VectSpStr of V; theorem :: VECTSP_5:50 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:51 M is_the_direct_sum_of W1,W2 implies M is_the_direct_sum_of W2,W1; theorem :: VECTSP_5:52 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:53 for L being Linear_Compl of W holds W is Linear_Compl of L; theorem :: VECTSP_5:54 (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:55 C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2; theorem :: VECTSP_5:56 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:57 for M being strict Abelian add-associative right_zeroed right_complementable VectSp-like (non empty VectSpStr 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:58 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:59 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; canceled 4; theorem :: VECTSP_5:64 M is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`1 = (v |-- (W2,W1))`2; theorem :: VECTSP_5:65 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:66 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:67 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:68 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:69 for L being Linear_Compl of W, v being Element of V holds (v |-- (W,L))`1 = (v |-- (L,W))`2; theorem :: VECTSP_5:70 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; canceled 4; theorem :: VECTSP_5:75 LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is Lattice; theorem :: VECTSP_5:76 LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is 0_Lattice; theorem :: VECTSP_5:77 LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is 1_Lattice; theorem :: VECTSP_5:78 LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is 01_Lattice; theorem :: VECTSP_5:79 LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is M_Lattice; theorem :: VECTSP_5:80 for F being Field, V being VectSp of F holds LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is C_Lattice;

Back to top