environ vocabulary RLVECT_1, BINOP_1, FUNCT_1, PROB_2, ARYTM_1, RELAT_1, BHSP_1, BOOLE, RLSUB_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, NUMBERS, XCMPLX_0, XREAL_0, MCART_1, FUNCT_1, RELSET_1, REAL_1, FUNCT_2, DOMAIN_1, BINOP_1, RLVECT_1, RLSUB_1, BHSP_1; constructors REAL_1, DOMAIN_1, RLSUB_1, PARTFUN1, SEQ_1, BHSP_1, MEMBERED; clusters SUBSET_1, STRUCT_0, RELSET_1, BHSP_1, SEQ_1, FUNCT_1, MEMBERED; requirements NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Definition and Axioms of the Subspace of Real Unitary Space definition let V be RealUnitarySpace; mode Subspace of V -> RealUnitarySpace means :: RUSUB_1:def 1 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:]) & the scalar of it = (the scalar of V)|([:the carrier of it, the carrier of it:]); end; theorem :: RUSUB_1:1 for V being RealUnitarySpace, W1,W2 being Subspace of V, x being set st x in W1 & W1 is Subspace of W2 holds x in W2; theorem :: RUSUB_1:2 for V being RealUnitarySpace, W being Subspace of V, x being set st x in W holds x in V; theorem :: RUSUB_1:3 for V being RealUnitarySpace, W being Subspace of V, w being VECTOR of W holds w is VECTOR of V; theorem :: RUSUB_1:4 for V being RealUnitarySpace, W being Subspace of V holds 0.W = 0.V; theorem :: RUSUB_1:5 for V being RealUnitarySpace, W1,W2 being Subspace of V holds 0.W1 = 0.W2; theorem :: RUSUB_1:6 for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V, w1,w2 being VECTOR of W st w1 = v & w2 = u holds w1 + w2 = v + u; theorem :: RUSUB_1:7 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V, w being VECTOR of W, a being Real st w = v holds a * w = a * v; theorem :: RUSUB_1:8 for V being RealUnitarySpace, W being Subspace of V, v1,v2 being VECTOR of V, w1,w2 being VECTOR of W st w1 = v1 & w2 = v2 holds w1 .|. w2 = v1 .|. v2; theorem :: RUSUB_1:9 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V, w being VECTOR of W st w = v holds - v = - w; theorem :: RUSUB_1:10 for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V, w1,w2 being VECTOR of W st w1 = v & w2 = u holds w1 - w2 = v - u; theorem :: RUSUB_1:11 for V being RealUnitarySpace, W being Subspace of V holds 0.V in W; theorem :: RUSUB_1:12 for V being RealUnitarySpace, W1,W2 being Subspace of V holds 0.W1 in W2; theorem :: RUSUB_1:13 for V being RealUnitarySpace, W being Subspace of V holds 0.W in V; theorem :: RUSUB_1:14 for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V st u in W & v in W holds u + v in W; theorem :: RUSUB_1:15 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V, a being Real st v in W holds a * v in W; theorem :: RUSUB_1:16 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V st v in W holds - v in W; theorem :: RUSUB_1:17 for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V st u in W & v in W holds u - v in W; theorem :: RUSUB_1:18 for V being RealUnitarySpace, V1 being Subset of V, D being non empty set, d1 being Element of D, A being BinOp of D, M being Function of [:REAL, D:], D, S being Function of [:D,D:],REAL st V1 = D & d1 = 0.V & A = (the add of V) | [:V1,V1:] & M = (the Mult of V) | [:REAL,V1:] & S = (the scalar of V) | [:V1,V1:] holds UNITSTR (# D,d1,A,M,S #) is Subspace of V; theorem :: RUSUB_1:19 for V being RealUnitarySpace holds V is Subspace of V; theorem :: RUSUB_1:20 for V,X being strict RealUnitarySpace holds V is Subspace of X & X is Subspace of V implies V = X; theorem :: RUSUB_1:21 for V,X,Y being RealUnitarySpace st V is Subspace of X & X is Subspace of Y holds V is Subspace of Y; theorem :: RUSUB_1:22 for V being RealUnitarySpace, W1,W2 being Subspace of V st the carrier of W1 c= the carrier of W2 holds W1 is Subspace of W2; theorem :: RUSUB_1:23 for V being RealUnitarySpace, W1,W2 being Subspace of V st (for v being VECTOR of V st v in W1 holds v in W2) holds W1 is Subspace of W2; definition let V be RealUnitarySpace; cluster strict Subspace of V; end; theorem :: RUSUB_1:24 for V being RealUnitarySpace, W1,W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds W1 = W2; theorem :: RUSUB_1:25 for V being RealUnitarySpace, W1,W2 being strict Subspace of V st (for v being VECTOR of V holds v in W1 iff v in W2) holds W1 = W2; theorem :: RUSUB_1:26 for V being strict RealUnitarySpace, W being strict Subspace of V st the carrier of W = the carrier of V holds W = V; theorem :: RUSUB_1:27 for V being strict RealUnitarySpace, W being strict Subspace of V st (for v being VECTOR of V holds v in W iff v in V) holds W = V; theorem :: RUSUB_1:28 for V being RealUnitarySpace, W being Subspace of V, V1 being Subset of V st the carrier of W = V1 holds V1 is lineary-closed; theorem :: RUSUB_1:29 for V being RealUnitarySpace, W being Subspace of V, V1 being Subset of V st V1 <> {} & V1 is lineary-closed holds (ex W being strict Subspace of V st V1 = the carrier of W); begin :: Definition of Zero Subspace and Improper Subspace of Real Unitary Space definition let V being RealUnitarySpace; func (0).V -> strict Subspace of V means :: RUSUB_1:def 2 the carrier of it = {0.V}; end; definition let V being RealUnitarySpace; func (Omega).V -> strict Subspace of V equals :: RUSUB_1:def 3 the UNITSTR of V; end; begin :: Theorems of Zero Subspace and Improper Subspace theorem :: RUSUB_1:30 for V being RealUnitarySpace, W being Subspace of V holds (0).W = (0).V; theorem :: RUSUB_1:31 for V being RealUnitarySpace, W1,W2 being Subspace of V holds (0).W1 = (0).W2; theorem :: RUSUB_1:32 for V being RealUnitarySpace, W being Subspace of V holds (0).W is Subspace of V; theorem :: RUSUB_1:33 for V being RealUnitarySpace, W being Subspace of V holds (0).V is Subspace of W; theorem :: RUSUB_1:34 for V being RealUnitarySpace, W1,W2 being Subspace of V holds (0).W1 is Subspace of W2; theorem :: RUSUB_1:35 for V being strict RealUnitarySpace holds V is Subspace of (Omega).V; begin :: The Cosets of Subspace of Real Unitary Space definition let V be RealUnitarySpace, v be VECTOR of V, W be Subspace of V; func v + W -> Subset of V equals :: RUSUB_1:def 4 {v + u where u is VECTOR of V : u in W}; end; definition let V be RealUnitarySpace; let W be Subspace of V; mode Coset of W -> Subset of V means :: RUSUB_1:def 5 ex v be VECTOR of V st it = v + W; end; begin :: Theorems of the Cosets theorem :: RUSUB_1:36 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds 0.V in v + W iff v in W; theorem :: RUSUB_1:37 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds v in v + W; theorem :: RUSUB_1:38 for V being RealUnitarySpace, W being Subspace of V holds 0.V + W = the carrier of W; theorem :: RUSUB_1:39 for V being RealUnitarySpace, v being VECTOR of V holds v + (0).V = {v}; theorem :: RUSUB_1:40 for V being RealUnitarySpace, v being VECTOR of V holds v + (Omega).V = the carrier of V; theorem :: RUSUB_1:41 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds 0.V in v + W iff v + W = the carrier of W; theorem :: RUSUB_1:42 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds v in W iff v + W = the carrier of W; theorem :: RUSUB_1:43 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V, a being Real st v in W holds (a * v) + W = the carrier of W; theorem :: RUSUB_1:44 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V, a being Real st a <> 0 & (a * v) + W = the carrier of W holds v in W; theorem :: RUSUB_1:45 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds v in W iff - v + W = the carrier of W; theorem :: RUSUB_1:46 for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V holds u in W iff v + W = (v + u) + W; theorem :: RUSUB_1:47 for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V holds u in W iff v + W = (v - u) + W; theorem :: RUSUB_1:48 for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V holds v in u + W iff u + W = v + W; theorem :: RUSUB_1:49 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds v + W = (- v) + W iff v in W; theorem :: RUSUB_1:50 for V being RealUnitarySpace, W being Subspace of V, u,v1,v2 being VECTOR of V st u in v1 + W & u in v2 + W holds v1 + W = v2 + W; theorem :: RUSUB_1:51 for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V st u in v + W & u in (- v) + W holds v in W; theorem :: RUSUB_1:52 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V, a being Real st a <> 1 & a * v in v + W holds v in W; theorem :: RUSUB_1:53 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V, a being Real st v in W holds a * v in v + W; theorem :: RUSUB_1:54 for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds - v in v + W iff v in W; theorem :: RUSUB_1:55 for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V holds u + v in v + W iff u in W; theorem :: RUSUB_1:56 for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V holds v - u in v + W iff u in W; theorem :: RUSUB_1:57 for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V holds u in v + W iff (ex v1 being VECTOR of V st v1 in W & u = v + v1); theorem :: RUSUB_1:58 for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V holds u in v + W iff (ex v1 being VECTOR of V st v1 in W & u = v - v1); theorem :: RUSUB_1:59 for V being RealUnitarySpace, W being Subspace of V, v1,v2 being VECTOR of V holds (ex v being VECTOR of V st v1 in v + W & v2 in v + W) iff v1 - v2 in W; theorem :: RUSUB_1:60 for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V st v + W = u + W holds (ex v1 being VECTOR of V st v1 in W & v + v1 = u); theorem :: RUSUB_1:61 for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V st v + W = u + W holds (ex v1 being VECTOR of V st v1 in W & v - v1 = u); theorem :: RUSUB_1:62 for V being RealUnitarySpace, W1,W2 being strict Subspace of V, v being VECTOR of V holds v + W1 = v + W2 iff W1 = W2; theorem :: RUSUB_1:63 for V being RealUnitarySpace, W1,W2 being strict Subspace of V, u,v being VECTOR of V st v + W1 = u + W2 holds W1 = W2; theorem :: RUSUB_1:64 for V being RealUnitarySpace, W being Subspace of V, C being Coset of W holds C is lineary-closed iff C = the carrier of W; theorem :: RUSUB_1:65 for V being RealUnitarySpace, W1,W2 being strict Subspace of V, C1 being Coset of W1, C2 being Coset of W2 holds C1 = C2 implies W1 = W2; theorem :: RUSUB_1:66 for V being RealUnitarySpace, W being Subspace of V, C being Coset of W, v being VECTOR of V holds {v} is Coset of (0).V; theorem :: RUSUB_1:67 for V being RealUnitarySpace, W being Subspace of V, V1 being Subset of V, v being VECTOR of V holds V1 is Coset of (0).V implies (ex v being VECTOR of V st V1 = {v}); theorem :: RUSUB_1:68 for V being RealUnitarySpace, W being Subspace of V holds the carrier of W is Coset of W; theorem :: RUSUB_1:69 for V being RealUnitarySpace holds the carrier of V is Coset of (Omega).V; theorem :: RUSUB_1:70 for V being RealUnitarySpace, W being Subspace of V, V1 being Subset of V st V1 is Coset of (Omega).V holds V1 = the carrier of V; theorem :: RUSUB_1:71 for V being RealUnitarySpace, W being Subspace of V, C being Coset of W holds 0.V in C iff C = the carrier of W; theorem :: RUSUB_1:72 for V being RealUnitarySpace, W being Subspace of V, C being Coset of W, u being VECTOR of V holds u in C iff C = u + W; theorem :: RUSUB_1:73 for V being RealUnitarySpace, W being Subspace of V, C being Coset of W, u,v being VECTOR of V st u in C & v in C holds (ex v1 being VECTOR of V st v1 in W & u + v1 = v); theorem :: RUSUB_1:74 for V being RealUnitarySpace, W being Subspace of V, C being Coset of W, u,v being VECTOR of V st u in C & v in C holds (ex v1 being VECTOR of V st v1 in W & u - v1 = v); theorem :: RUSUB_1:75 for V being RealUnitarySpace, W being Subspace of V, v1,v2 being VECTOR of V holds (ex C being Coset of W st v1 in C & v2 in C) iff v1 - v2 in W; theorem :: RUSUB_1:76 for V being RealUnitarySpace, W being Subspace of V, u being VECTOR of V, B,C being Coset of W st u in B & u in C holds B = C;