Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Subspaces and Cosets of Subspaces in Real Linear Space

**by****Wojciech A. Trybulec**- Received July 24, 1989
- MML identifier: RLSUB_1

- [ Mizar article, MML identifier index ]

environ vocabulary RLVECT_1, BOOLE, ARYTM_1, RELAT_1, FUNCT_1, BINOP_1, RLSUB_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, REAL_1, MCART_1, FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1, BINOP_1, STRUCT_0, RLVECT_1; constructors REAL_1, DOMAIN_1, RLVECT_1, PARTFUN1, MEMBERED, XBOOLE_0; clusters FUNCT_1, RLVECT_1, STRUCT_0, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve V,X,Y for RealLinearSpace; reserve u,u1,u2,v,v1,v2 for VECTOR of V; reserve a,b for Real; reserve V1,V2,V3 for Subset of V; reserve x for set; :: :: Introduction of predicate lineary closed subsets of the carrier. :: definition let V; let V1; attr V1 is lineary-closed means :: RLSUB_1:def 1 (for v,u st v in V1 & u in V1 holds v + u in V1) & (for a,v st v in V1 holds a * v in V1); end; canceled 3; theorem :: RLSUB_1:4 V1 <> {} & V1 is lineary-closed implies 0.V in V1; theorem :: RLSUB_1:5 V1 is lineary-closed implies (for v st v in V1 holds - v in V1); theorem :: RLSUB_1:6 V1 is lineary-closed implies (for v,u st v in V1 & u in V1 holds v - u in V1); theorem :: RLSUB_1:7 {0.V} is lineary-closed; theorem :: RLSUB_1:8 the carrier of V = V1 implies V1 is lineary-closed; theorem :: RLSUB_1:9 V1 is lineary-closed & V2 is lineary-closed & V3 = {v + u : v in V1 & u in V2} implies V3 is lineary-closed; theorem :: RLSUB_1:10 V1 is lineary-closed & V2 is lineary-closed implies V1 /\ V2 is lineary-closed; definition let V; mode Subspace of V -> RealLinearSpace means :: RLSUB_1:def 2 the carrier of it c= the carrier of V & the Zero of it = the Zero of V & the add of it = (the add of V) | [:the carrier of it,the carrier of it:] & the Mult of it = (the Mult of V) | [:REAL, the carrier of it:]; end; reserve W,W1,W2 for Subspace of V; reserve w,w1,w2 for VECTOR of W; :: :: Axioms of the subspaces of real linear spaces. :: canceled 5; theorem :: RLSUB_1:16 x in W1 & W1 is Subspace of W2 implies x in W2; theorem :: RLSUB_1:17 x in W implies x in V; theorem :: RLSUB_1:18 w is VECTOR of V; theorem :: RLSUB_1:19 0.W = 0.V; theorem :: RLSUB_1:20 0.W1 = 0.W2; theorem :: RLSUB_1:21 w1 = v & w2 = u implies w1 + w2 = v + u; theorem :: RLSUB_1:22 w = v implies a * w = a * v; theorem :: RLSUB_1:23 w = v implies - v = - w; theorem :: RLSUB_1:24 w1 = v & w2 = u implies w1 - w2 = v - u; theorem :: RLSUB_1:25 0.V in W; theorem :: RLSUB_1:26 0.W1 in W2; theorem :: RLSUB_1:27 0.W in V; theorem :: RLSUB_1:28 u in W & v in W implies u + v in W; theorem :: RLSUB_1:29 v in W implies a * v in W; theorem :: RLSUB_1:30 v in W implies - v in W; theorem :: RLSUB_1:31 u in W & v in W implies u - v in W; reserve D for non empty set; reserve d1 for Element of D; reserve A for BinOp of D; reserve M for Function of [:REAL,D:],D; theorem :: RLSUB_1:32 V1 = D & d1 = 0.V & A = (the add of V) | [:V1,V1:] & M = (the Mult of V) | [:REAL,V1:] implies RLSStruct (# D,d1,A,M #) is Subspace of V; theorem :: RLSUB_1:33 V is Subspace of V; theorem :: RLSUB_1:34 for V,X being strict RealLinearSpace holds V is Subspace of X & X is Subspace of V implies V = X; theorem :: RLSUB_1:35 V is Subspace of X & X is Subspace of Y implies V is Subspace of Y; theorem :: RLSUB_1:36 the carrier of W1 c= the carrier of W2 implies W1 is Subspace of W2; theorem :: RLSUB_1:37 (for v st v in W1 holds v in W2) implies W1 is Subspace of W2; definition let V; cluster strict Subspace of V; end; theorem :: RLSUB_1:38 for W1,W2 being strict Subspace of V holds the carrier of W1 = the carrier of W2 implies W1 = W2; theorem :: RLSUB_1:39 for W1,W2 being strict Subspace of V holds (for v holds v in W1 iff v in W2) implies W1 = W2; theorem :: RLSUB_1:40 for V being strict RealLinearSpace, W being strict Subspace of V holds the carrier of W = the carrier of V implies W = V; theorem :: RLSUB_1:41 for V being strict RealLinearSpace, W being strict Subspace of V holds (for v being VECTOR of V holds v in W iff v in V) implies W = V; theorem :: RLSUB_1:42 the carrier of W = V1 implies V1 is lineary-closed; theorem :: RLSUB_1:43 V1 <> {} & V1 is lineary-closed implies (ex W being strict Subspace of V st V1 = the carrier of W); :: :: Definition of zero subspace and improper subspace of real linear space. :: definition let V; func (0).V -> strict Subspace of V means :: RLSUB_1:def 3 the carrier of it = {0.V}; end; definition let V; func (Omega).V -> strict Subspace of V equals :: RLSUB_1:def 4 the RLSStruct of V; end; :: :: Definitional theorems of zero subspace and improper subspace. :: canceled 4; theorem :: RLSUB_1:48 (0).W = (0).V; theorem :: RLSUB_1:49 (0).W1 = (0).W2; theorem :: RLSUB_1:50 (0).W is Subspace of V; theorem :: RLSUB_1:51 (0).V is Subspace of W; theorem :: RLSUB_1:52 (0).W1 is Subspace of W2; canceled; theorem :: RLSUB_1:54 for V being strict RealLinearSpace holds V is Subspace of (Omega).V; :: :: Introduction of the cosets of subspace. :: definition let V; let v,W; func v + W -> Subset of V equals :: RLSUB_1:def 5 {v + u : u in W}; end; definition let V; let W; mode Coset of W -> Subset of V means :: RLSUB_1:def 6 ex v st it = v + W; end; reserve B,C for Coset of W; :: :: Definitional theorems of the cosets. :: canceled 3; theorem :: RLSUB_1:58 0.V in v + W iff v in W; theorem :: RLSUB_1:59 v in v + W; theorem :: RLSUB_1:60 0.V + W = the carrier of W; theorem :: RLSUB_1:61 v + (0).V = {v}; theorem :: RLSUB_1:62 v + (Omega).V = the carrier of V; theorem :: RLSUB_1:63 0.V in v + W iff v + W = the carrier of W; theorem :: RLSUB_1:64 v in W iff v + W = the carrier of W; theorem :: RLSUB_1:65 v in W implies (a * v) + W = the carrier of W; theorem :: RLSUB_1:66 a <> 0 & (a * v) + W = the carrier of W implies v in W; theorem :: RLSUB_1:67 v in W iff - v + W = the carrier of W; theorem :: RLSUB_1:68 u in W iff v + W = (v + u) + W; theorem :: RLSUB_1:69 u in W iff v + W = (v - u) + W; theorem :: RLSUB_1:70 v in u + W iff u + W = v + W; theorem :: RLSUB_1:71 v + W = (- v) + W iff v in W; theorem :: RLSUB_1:72 u in v1 + W & u in v2 + W implies v1 + W = v2 + W; theorem :: RLSUB_1:73 u in v + W & u in (- v) + W implies v in W; theorem :: RLSUB_1:74 a <> 1 & a * v in v + W implies v in W; theorem :: RLSUB_1:75 v in W implies a * v in v + W; theorem :: RLSUB_1:76 - v in v + W iff v in W; theorem :: RLSUB_1:77 u + v in v + W iff u in W; theorem :: RLSUB_1:78 v - u in v + W iff u in W; theorem :: RLSUB_1:79 u in v + W iff (ex v1 st v1 in W & u = v + v1); theorem :: RLSUB_1:80 u in v + W iff (ex v1 st v1 in W & u = v - v1); theorem :: RLSUB_1:81 (ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W; theorem :: RLSUB_1:82 v + W = u + W implies (ex v1 st v1 in W & v + v1 = u); theorem :: RLSUB_1:83 v + W = u + W implies (ex v1 st v1 in W & v - v1 = u); theorem :: RLSUB_1:84 for W1,W2 being strict Subspace of V holds v + W1 = v + W2 iff W1 = W2; theorem :: RLSUB_1:85 for W1,W2 being strict Subspace of V holds v + W1 = u + W2 implies W1 = W2; :: :: Theorems concerning cosets of subspace :: regarded as subsets of the carrier. :: theorem :: RLSUB_1:86 C is lineary-closed iff C = the carrier of W; theorem :: RLSUB_1:87 for W1,W2 being strict Subspace of V, C1 being Coset of W1, C2 being Coset of W2 holds C1 = C2 implies W1 = W2; theorem :: RLSUB_1:88 {v} is Coset of (0).V; theorem :: RLSUB_1:89 V1 is Coset of (0).V implies (ex v st V1 = {v}); theorem :: RLSUB_1:90 the carrier of W is Coset of W; theorem :: RLSUB_1:91 the carrier of V is Coset of (Omega).V; theorem :: RLSUB_1:92 V1 is Coset of (Omega).V implies V1 = the carrier of V; theorem :: RLSUB_1:93 0.V in C iff C = the carrier of W; theorem :: RLSUB_1:94 u in C iff C = u + W; theorem :: RLSUB_1:95 u in C & v in C implies (ex v1 st v1 in W & u + v1 = v); theorem :: RLSUB_1:96 u in C & v in C implies (ex v1 st v1 in W & u - v1 = v); theorem :: RLSUB_1:97 (ex C st v1 in C & v2 in C) iff v1 - v2 in W; theorem :: RLSUB_1:98 u in B & u in C implies B = C;

Back to top