Copyright (c) 2002 Association of Mizar Users
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; definitions RLVECT_1, TARSKI, XBOOLE_0; theorems BHSP_1, RLVECT_1, FUNCT_1, TARSKI, FUNCT_2, ZFMISC_1, XBOOLE_0, RELAT_1, RELSET_1, RLSUB_1, XBOOLE_1, XCMPLX_0, XCMPLX_1; schemes XBOOLE_0; begin :: Definition and Axioms of the Subspace of Real Unitary Space definition let V be RealUnitarySpace; mode Subspace of V -> RealUnitarySpace means :Def1: 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:]); existence proof take V; A1:dom(the add of V) = [:the carrier of V, the carrier of V:] by FUNCT_2:def 1; A2:dom(the Mult of V) = [:REAL, the carrier of V:] by FUNCT_2:def 1; dom(the scalar of V) = [:the carrier of V, the carrier of V:] by FUNCT_2:def 1; hence thesis by A1,A2,RELAT_1:98; end; end; theorem 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 proof let V be RealUnitarySpace; let W1,W2 be Subspace of V; let x be set; assume x in W1 & W1 is Subspace of W2; then x in the carrier of W1 & the carrier of W1 c= the carrier of W2 by Def1,RLVECT_1:def 1; hence thesis by RLVECT_1:def 1; end; theorem Th2: for V being RealUnitarySpace, W being Subspace of V, x being set st x in W holds x in V proof let V be RealUnitarySpace; let W be Subspace of V; let x be set; assume x in W; then x in the carrier of W & the carrier of W c= the carrier of V by Def1,RLVECT_1:def 1; hence thesis by RLVECT_1:def 1; end; theorem Th3: for V being RealUnitarySpace, W being Subspace of V, w being VECTOR of W holds w is VECTOR of V proof let V be RealUnitarySpace; let W be Subspace of V; let w be VECTOR of W; w in W by RLVECT_1:3; then w in V by Th2; hence thesis by RLVECT_1:def 1; end; theorem Th4: for V being RealUnitarySpace, W being Subspace of V holds 0.W = 0.V proof let V be RealUnitarySpace; let W be Subspace of V; 0.W = the Zero of W by RLVECT_1:def 2 .= the Zero of V by Def1; hence thesis by RLVECT_1:def 2; end; theorem for V being RealUnitarySpace, W1,W2 being Subspace of V holds 0.W1 = 0.W2 proof let V be RealUnitarySpace; let W1,W2 being Subspace of V; 0.W1 = 0.V by Th4; hence thesis by Th4; end; theorem Th6: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let u,v be VECTOR of V; let w1,w2 be VECTOR of W; assume A1:v = w1 & u = w2; reconsider ww1 = w1, ww2 = w2 as VECTOR of V by Th3; A2:v + u = (the add of V).[ww1,ww2] by A1,RLVECT_1:def 3; w1 + w2 = (the add of W).[w1,w2] by RLVECT_1:def 3 .= ((the add of V) | [:the carrier of W, the carrier of W:]).[w1,w2] by Def1; hence thesis by A2,FUNCT_1:72; end; theorem Th7: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; let w be VECTOR of W; let a be Real; assume A1:w = v; reconsider ww1 = w as VECTOR of V by Th3; A2:a * v = (the Mult of V).[a,ww1] by A1,RLVECT_1:def 4; a * w = (the Mult of W).[a,w] by RLVECT_1:def 4 .= ((the Mult of V) | [:REAL, the carrier of W:]).[a,w] by Def1; hence thesis by A2,FUNCT_1:72; end; theorem 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 proof let V be RealUnitarySpace; let W be Subspace of V; let v1,v2 be VECTOR of V; let w1,w2 be VECTOR of W; assume A1:w1 = v1 & w2 = v2; reconsider ww1 = w1, ww2 = w2 as VECTOR of V by Th3; A2:v1 .|. v2 = (the scalar of V).[ww1,ww2] by A1,BHSP_1:def 1; w1 .|. w2 = (the scalar of W).[w1,w2] by BHSP_1:def 1 .= ((the scalar of V) | [:the carrier of W, the carrier of W:]).[w1,w2] by Def1; hence thesis by A2,FUNCT_1:72; end; theorem Th9: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; let w be VECTOR of W; assume A1:w = v; - v = (- 1) * v & - w = (- 1) * w by RLVECT_1:29; hence thesis by A1,Th7; end; theorem Th10: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let u,v be VECTOR of V; let w1,w2 be VECTOR of W; assume that A1:w1 = v and A2:w2 = u; A3:- w2 = - u by A2,Th9; w1 - w2 = w1 + (- w2) & v - u = v + (- u) by RLVECT_1:def 11; hence thesis by A1,A3,Th6; end; theorem Th11: for V being RealUnitarySpace, W being Subspace of V holds 0.V in W proof let V be RealUnitarySpace; let W be Subspace of V; 0.W in W & 0.V = 0.W by Th4,RLVECT_1:3; hence thesis; end; theorem for V being RealUnitarySpace, W1,W2 being Subspace of V holds 0.W1 in W2 proof let V be RealUnitarySpace; let W1,W2 be Subspace of V; 0.W1 = 0.V by Th4; hence thesis by Th11; end; theorem for V being RealUnitarySpace, W being Subspace of V holds 0.W in V proof let V be RealUnitarySpace; let W be Subspace of V; 0.W in W by RLVECT_1:3; hence thesis by Th2; end; Lm1: for V being RealUnitarySpace, W being Subspace of V, V1,V2 being Subset of V st the carrier of W = V1 holds V1 is lineary-closed proof let V be RealUnitarySpace; let W be Subspace of V; let V1,V2 be Subset of V; assume A1:the carrier of W = V1; set VW = the carrier of W; reconsider WW = W as RealUnitarySpace; A2:for v,u being VECTOR of V st v in V1 & u in V1 holds v + u in V1 proof let v,u be VECTOR of V; assume v in V1 & u in V1; then reconsider vv = v, uu = u as VECTOR of WW by A1; reconsider vw = vv + uu as Element of VW; vw in V1 by A1; hence v + u in V1 by Th6; end; for a being Real, v being VECTOR of V st v in V1 holds a * v in V1 proof let a be Real, v be VECTOR of V; assume v in V1; then reconsider vv = v as VECTOR of WW by A1; reconsider vw = a * vv as Element of VW; vw in V1 by A1; hence a * v in V1 by Th7; end; hence thesis by A2,RLSUB_1:def 1; end; theorem Th14: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let u,v be VECTOR of V; assume u in W & v in W; then A1:u in the carrier of W & v in the carrier of W by RLVECT_1:def 1; reconsider VW = the carrier of W as Subset of V by Def1; VW is lineary-closed by Lm1; then u + v in the carrier of W by A1,RLSUB_1:def 1; hence thesis by RLVECT_1:def 1; end; theorem Th15: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; let a be Real; assume v in W; then A1:v in the carrier of W by RLVECT_1:def 1; reconsider VW = the carrier of W as Subset of V by Def1; VW is lineary-closed by Lm1; then a * v in the carrier of W by A1,RLSUB_1:def 1; hence thesis by RLVECT_1:def 1; end; theorem Th16: for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V st v in W holds - v in W proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; assume v in W; then (- 1) * v in W by Th15; hence thesis by RLVECT_1:29; end; theorem Th17: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let u,v be VECTOR of V; assume that A1:u in W and A2: v in W; - v in W by A2,Th16; then u + (- v) in W by A1,Th14; hence thesis by RLVECT_1:def 11; end; theorem Th18: 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 proof let V be RealUnitarySpace; let V1 be Subset of V; let D be non empty set; let d1 be Element of D; let A be BinOp of D; let M be Function of [:REAL, D:], D; let S be Function of [:D, D:], REAL; assume that A1:V1 = D and A2:d1 = 0.V and A3:A = (the add of V) | [:V1,V1:] and A4:M = (the Mult of V) | [:REAL,V1:] and A5:S = (the scalar of V) | [:V1,V1:]; UNITSTR (# D,d1,A,M,S #) is Subspace of V proof set W = UNITSTR (# D,d1,A,M,S #); A6: the Zero of W = the Zero of V by A2,RLVECT_1:def 2; A7: for x,y being VECTOR of W holds x + y = (the add of V).[x,y] proof let x,y be VECTOR of W; x + y = ((the add of V) | [:the carrier of W, the carrier of W:] ).[x,y] by A1,A3,RLVECT_1:def 3; hence thesis by FUNCT_1:72; end; A8: for a being Real, x being VECTOR of W holds a * x = (the Mult of V).[a,x] proof let a be Real; let x be VECTOR of W; a * x = ((the Mult of V) | [:REAL, the carrier of W:]).[a,x] by A1,A4,RLVECT_1:def 4; hence thesis by FUNCT_1:72; end; A9: d1 = 0.W by RLVECT_1:def 2; A10: for x,y being VECTOR of W holds x .|. y = (the scalar of V).[x,y] proof let x,y be VECTOR of W; x .|. y = ((the scalar of V) | [:the carrier of W, the carrier of W:]).[x,y] by A1,A5,BHSP_1:def 1; hence thesis by FUNCT_1:72; end; W is RealUnitarySpace-like RealLinearSpace-like Abelian add-associative right_zeroed right_complementable proof set AV = the add of V; set MV = the Mult of V; set SV = the scalar of V; A11: for x,y being Element of W holds x + y = y + x proof let x,y be Element of W; reconsider x1 = x, y1 = y as VECTOR of V by A1,TARSKI:def 3; thus x + y = AV.[x1,y1] by A7 .= y1 + x1 by RLVECT_1:def 3 .= AV.[y1,x1] by RLVECT_1:def 3 .= y + x by A7; end; A12: for x,y,z being VECTOR of W holds (x + y) + z = x + (y + z) proof let x,y,z be VECTOR of W; reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1,TARSKI:def 3; thus (x + y) + z = AV.[x + y,z1] by A7 .= AV.[AV.[x1,y1],z1] by A7 .= AV.[x1 + y1,z1] by RLVECT_1:def 3 .= (x1 + y1) + z1 by RLVECT_1:def 3 .= x1 + (y1 + z1) by RLVECT_1:def 6 .= AV.[x1,y1 + z1] by RLVECT_1:def 3 .= AV.[x1,AV.[y1,z1]] by RLVECT_1:def 3 .= AV.[x1,y + z] by A7 .= x + (y + z) by A7; end; A13: for x being VECTOR of W holds x + 0.W = x proof let x be VECTOR of W; reconsider y = x, z = 0.W as VECTOR of V by A1,TARSKI:def 3; thus x + 0.W = AV.[y,z] by A7 .= y + 0.V by A2,A9,RLVECT_1:def 3 .= x by RLVECT_1:10; end; A14: for x being VECTOR of W ex y being VECTOR of W st x + y = 0.W proof let x be VECTOR of W; reconsider x1 = x as VECTOR of V by A1,TARSKI:def 3; consider v being VECTOR of V such that A15: x1 + v = 0.V by RLVECT_1:def 8; v = - x1 by A15,RLVECT_1:def 10 .= (- 1) * x1 by RLVECT_1:29 .= MV.[- 1,x1] by RLVECT_1:def 4 .= (- 1) * x by A8; then reconsider y = v as VECTOR of W; take y; thus x + y = AV.[x1,v] by A7 .= 0.W by A2,A9,A15,RLVECT_1:def 3; end; A16: for a being Real, x,y being VECTOR of W holds a * (x + y) = a * x + a * y proof let a be Real; let x,y be VECTOR of W; reconsider x1 = x, y1 = y as VECTOR of V by A1,TARSKI:def 3; thus a * (x + y) = MV.[a,x + y] by A8 .= MV.[a,AV.[x1,y1]] by A7 .= MV.[a,x1 + y1] by RLVECT_1:def 3 .= a * (x1 + y1) by RLVECT_1:def 4 .= a * x1 + a * y1 by RLVECT_1:def 9 .= AV.[a * x1,a * y1] by RLVECT_1:def 3 .= AV.[MV.[a,x1],a * y1] by RLVECT_1:def 4 .= AV.[MV.[a,x1],MV.[a,y1]] by RLVECT_1:def 4 .= AV.[MV.[a,x1],a * y] by A8 .= AV.[a * x, a * y] by A8 .= a * x + a * y by A7; end; A17: for a,b being Real, x being VECTOR of W holds (a + b) * x = a * x + b * x proof let a,b be Real; let x be VECTOR of W; reconsider y = x as VECTOR of V by A1,TARSKI:def 3; thus (a + b) * x = MV.[a + b,y] by A8 .= (a + b) * y by RLVECT_1:def 4 .= a * y + b * y by RLVECT_1:def 9 .= AV.[a * y,b * y] by RLVECT_1:def 3 .= AV.[MV.[a,y],b * y] by RLVECT_1:def 4 .= AV.[MV.[a,y],MV.[b,y]] by RLVECT_1:def 4 .= AV.[MV.[a,y],b * x] by A8 .= AV.[a * x,b * x] by A8 .= a * x + b * x by A7; end; A18: for a,b being Real, x being VECTOR of W holds (a * b) * x = a * (b * x) proof let a,b be Real; let x be VECTOR of W; reconsider y = x as VECTOR of V by A1,TARSKI:def 3; thus (a * b) * x = MV.[(a * b),y] by A8 .= (a * b) * y by RLVECT_1:def 4 .= a * (b * y) by RLVECT_1:def 9 .= MV.[a,b * y] by RLVECT_1:def 4 .= MV.[a,MV.[b,y]] by RLVECT_1:def 4 .= MV.[a,b * x] by A8 .= a * (b * x) by A8; end; A19: for x being VECTOR of W holds 1 * x = x proof let x be VECTOR of W; reconsider y = x as VECTOR of V by A1,TARSKI:def 3; thus 1 * x = MV.[1,y] by A8 .= 1 * y by RLVECT_1:def 4 .= x by RLVECT_1:def 9; end; for x,y,z being VECTOR of W, a being Real holds (x .|. x = 0 iff x = 0.W) & 0 <= x .|. x & x .|. y = y .|. x & (x+y) .|. z = x .|. z + y .|. z & (a*x) .|. y = a * ( x .|. y ) proof let x,y,z be VECTOR of W; let a be Real; reconsider x1 = x as VECTOR of V by A1,TARSKI:def 3; reconsider y1 = y as VECTOR of V by A1,TARSKI:def 3; reconsider z1 = z as VECTOR of V by A1,TARSKI:def 3; A20: x .|. x = 0 implies x = 0.W proof assume x .|. x = 0; then SV.[x1,x1] = 0 by A10; then x1 .|. x1 = 0 by BHSP_1:def 1; then x1 = 0.V by BHSP_1:def 2; hence thesis by A2,RLVECT_1:def 2; end; x = 0.W implies x .|. x = 0 proof assume x = 0.W; then x1 = 0.V by A2,RLVECT_1:def 2; then x1 .|. x1 = 0 by BHSP_1:def 2; then SV.[x1,x1] = 0 by BHSP_1:def 1; hence thesis by A10; end; hence x .|. x = 0 iff x = 0.W by A20; thus 0 <= x .|. x proof 0 <= x1 .|. x1 by BHSP_1:def 2; then 0 <= SV.[x1,x1] by BHSP_1:def 1; hence thesis by A10; end; thus x .|. y = y .|. x proof SV.[x1,y1] = y1 .|. x1 by BHSP_1:def 1; then SV.[x1,y1] = SV.[y1,x1] by BHSP_1:def 1; then x .|. y = SV.[y1,x1] by A10; hence thesis by A10; end; thus (x+y) .|. z = x .|. z + y .|. z proof A21: SV.[y1,z1] = y1 .|. z1 by BHSP_1:def 1; A22: (x + y) .|. z = SV.[x+y, z] by A10 .= SV.[AV.[x1,y1], z] by A7 .= SV.[x1+y1, z] by RLVECT_1:def 3 .= (x1 + y1) .|. z1 by BHSP_1:def 1 .= x1 .|. z1 + y1 .|. z1 by BHSP_1:def 2; x .|. z + y .|. z = (SV.[x, z]) + (y .|. z) by A10 .= (SV.[x, z]) + (SV.[y, z]) by A10 .= x1 .|. z1 + y1 .|. z1 by A21,BHSP_1:def 1; hence thesis by A22; end; thus thesis proof A23: (a*x) .|. y = SV.[(a*x), y] by A10 .= SV.[MV.[a,x1], y] by A8 .= SV.[(a*x1), y] by RLVECT_1:def 4 .= (a*x1) .|. y1 by BHSP_1:def 1 .= a * ( x1 .|. y1 ) by BHSP_1:def 2; a * ( x .|. y ) = a * SV.[x,y] by A10 .= a * (x1 .|. y1) by BHSP_1:def 1; hence thesis by A23; end; end; hence thesis by A11,A12,A13,A14,A16,A17,A18,A19,BHSP_1:def 2,RLVECT_1: def 5,def 6,def 7,def 8,def 9; end; hence thesis by A1,A3,A4,A5,A6,Def1; end; hence thesis; end; theorem Th19: for V being RealUnitarySpace holds V is Subspace of V proof let V be RealUnitarySpace; thus the carrier of V c= the carrier of V & the Zero of V = the Zero of V; thus thesis by FUNCT_2:40; end; theorem Th20: for V,X being strict RealUnitarySpace holds V is Subspace of X & X is Subspace of V implies V = X proof let V,X be strict RealUnitarySpace; assume A1:V is Subspace of X & X is Subspace of V; set VV = the carrier of V; set VX = the carrier of X; set AV = the add of V; set AX = the add of X; set MV = the Mult of V; set MX = the Mult of X; set SV = the scalar of V; set SX = the scalar of X; VV c= VX & VX c= VV by A1,Def1; then A2:VV = VX by XBOOLE_0:def 10; A3:the Zero of V = the Zero of X by A1,Def1; AV = AX | [:VV,VV:] & AX = AV | [:VX,VX:] by A1,Def1; then A4:AV = AX by A2,RELAT_1:101; MV = MX | [:REAL,VV:] & MX = MV | [:REAL,VX:] by A1,Def1; then A5:MV = MX by A2,RELAT_1:101; SV = SX | [:VV,VV:] & SX = SV | [:VX,VX:] by A1,Def1; hence thesis by A2,A3,A4,A5,RELAT_1:101; end; theorem Th21: for V,X,Y being RealUnitarySpace st V is Subspace of X & X is Subspace of Y holds V is Subspace of Y proof let V,X,Y be RealUnitarySpace; assume A1:V is Subspace of X & X is Subspace of Y; thus the carrier of V c= the carrier of Y proof the carrier of V c= the carrier of X & the carrier of X c= the carrier of Y by A1,Def1; hence thesis by XBOOLE_1:1; end; thus the Zero of V = the Zero of Y proof the Zero of V = the Zero of X & the Zero of X = the Zero of Y by A1,Def1 ; hence thesis; end; thus the add of V = (the add of Y) | [:the carrier of V, the carrier of V:] proof set AV = the add of V; set VV = the carrier of V; set AX = the add of X; set VX = the carrier of X; set AY = the add of Y; AV = AX | [:VV,VV:] & AX = AY | [:VX,VX:] & VV c= VX by A1,Def1; then AV = (AY | [:VX,VX:]) | [:VV,VV:] & [:VV,VV:] c= [:VX,VX:] by ZFMISC_1:119; hence thesis by FUNCT_1:82; end; thus the Mult of V = (the Mult of Y) | [:REAL, the carrier of V:] proof set MV = the Mult of V; set VV = the carrier of V; set MX = the Mult of X; set VX = the carrier of X; set MY = the Mult of Y; MV = MX | [:REAL,VV:] & MX = MY | [:REAL,VX:] & VV c= VX by A1,Def1; then MV = (MY | [:REAL,VX:]) | [:REAL,VV:] & [:REAL,VV:] c= [:REAL,VX:] by ZFMISC_1:118; hence thesis by FUNCT_1:82; end; set SV = the scalar of V; set VV = the carrier of V; set SX = the scalar of X; set VX = the carrier of X; set SY = the scalar of Y; SV = SX | [:VV,VV:] & SX = SY | [:VX,VX:] & VV c= VX by A1,Def1; then SV = (SY | [:VX,VX:]) | [:VV,VV:] & [:VV,VV:] c= [:VX,VX:] by ZFMISC_1:119; hence thesis by FUNCT_1:82; end; theorem Th22: 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 proof let V be RealUnitarySpace; let W1,W2 be Subspace of V; assume A1:the carrier of W1 c= the carrier of W2; set VW1 = the carrier of W1; set VW2 = the carrier of W2; set AV = the add of V; set MV = the Mult of V; set SV = the scalar of V; the Zero of W1 = the Zero of V & the Zero of W2 = the Zero of V by Def1; hence the carrier of W1 c= the carrier of W2 & the Zero of W1 = the Zero of W2 by A1; thus the add of W1 = (the add of W2) | [:the carrier of W1,the carrier of W1:] proof the add of W1 = AV | [:VW1,VW1:] & the add of W2 = AV | [:VW2,VW2:] & [:VW1,VW1:] c= [:VW2,VW2:] by A1,Def1,ZFMISC_1:119; hence thesis by FUNCT_1:82; end; thus the Mult of W1 = (the Mult of W2) | [:REAL, the carrier of W1:] proof the Mult of W1 = MV | [:REAL,VW1:] & the Mult of W2 = MV | [:REAL,VW2:] & [:REAL,VW1:] c= [:REAL,VW2:] by A1,Def1,ZFMISC_1:118; hence thesis by FUNCT_1:82; end; the scalar of W1 = SV | [:VW1,VW1:] & the scalar of W2 = SV | [:VW2,VW2:] & [:VW1,VW1:] c= [:VW2,VW2:] by A1,Def1,ZFMISC_1:119; hence thesis by FUNCT_1:82; end; theorem 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 proof let V be RealUnitarySpace; let W1,W2 be Subspace of V; assume A1:for v being VECTOR of V st v in W1 holds v in W2; the carrier of W1 c= the carrier of W2 proof let x be set; assume A2: x in the carrier of W1; the carrier of W1 c= the carrier of V by Def1; then reconsider v = x as VECTOR of V by A2; v in W1 by A2,RLVECT_1:def 1; then v in W2 by A1; hence thesis by RLVECT_1:def 1; end; hence thesis by Th22; end; definition let V be RealUnitarySpace; cluster strict Subspace of V; existence proof the carrier of V is Subset of V iff the carrier of V c= the carrier of V; then reconsider V1 = the carrier of V as Subset of V; the Zero of V = 0.V & the add of V = (the add of V) | [:V1,V1:] & the Mult of V = (the Mult of V) | [:REAL,V1:] & the scalar of V = (the scalar of V) | [:V1, V1:] by FUNCT_2:40,RLVECT_1:def 2; then UNITSTR(#the carrier of V,the Zero of V,the add of V,the Mult of V, the scalar of V #) is Subspace of V by Th18; hence thesis; end; end; theorem Th24: for V being RealUnitarySpace, W1,W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds W1 = W2 proof let V be RealUnitarySpace; let W1,W2 be strict Subspace of V; assume the carrier of W1 = the carrier of W2; then W1 is Subspace of W2 & W2 is Subspace of W1 by Th22; hence thesis by Th20; end; theorem Th25: 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 proof let V be RealUnitarySpace; let W1,W2 be strict Subspace of V; assume A1:for v being VECTOR of V holds v in W1 iff v in W2; for x being set holds x in the carrier of W1 iff x in the carrier of W2 proof let x be set; thus x in the carrier of W1 implies x in the carrier of W2 proof assume A2: x in the carrier of W1; the carrier of W1 c= the carrier of V by Def1; then reconsider v = x as VECTOR of V by A2; v in W1 by A2,RLVECT_1:def 1; then v in W2 by A1; hence thesis by RLVECT_1:def 1; end; assume A3: x in the carrier of W2; the carrier of W2 c= the carrier of V by Def1; then reconsider v = x as VECTOR of V by A3; v in W2 by A3,RLVECT_1:def 1; then v in W1 by A1; hence thesis by RLVECT_1:def 1; end; then the carrier of W1 = the carrier of W2 by TARSKI:2; hence thesis by Th24; end; theorem for V being strict RealUnitarySpace, W being strict Subspace of V st the carrier of W = the carrier of V holds W = V proof let V be strict RealUnitarySpace; let W be strict Subspace of V; assume A1:the carrier of W = the carrier of V; V is Subspace of V by Th19; hence thesis by A1,Th24; end; theorem 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 proof let V be strict RealUnitarySpace; let W be strict Subspace of V; assume A1:for v being VECTOR of V holds v in W iff v in V; V is Subspace of V by Th19; hence thesis by A1,Th25; end; theorem 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 by Lm1; theorem Th29: 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) proof let V be RealUnitarySpace; let W be Subspace of V; let V1 be Subset of V; assume that A1:V1 <> {} and A2:V1 is lineary-closed; reconsider D = V1 as non empty set by A1; reconsider d1 = 0.V as Element of D by A2,RLSUB_1:4; set A = (the add of V) | [:V1,V1:]; set M = (the Mult of V) | [:REAL,V1:]; set S = (the scalar of V) | [:V1,V1:]; set VV = the carrier of V; dom(the add of V) = [:VV,VV:] by FUNCT_2:def 1; then dom A = [:VV,VV:] /\ [:V1,V1:] & [:V1,V1:] c= [:VV,VV:] by RELAT_1:90; then A3:dom A = [:D,D:] by XBOOLE_1:28; dom(the Mult of V) = [:REAL,VV:] by FUNCT_2:def 1; then dom M = [:REAL,VV:] /\ [:REAL,V1:] & [:REAL,V1:] c= [:REAL,VV:] by RELAT_1:90,ZFMISC_1:118; then A4:dom M = [:REAL,D:] by XBOOLE_1:28; A5:D = rng A proof now let y be set; thus y in D implies ex x being set st x in dom A & y = A.x proof assume A6: y in D; then reconsider v1 = y, v0 = d1 as Element of VV; A7: [d1,y] in [:D,D:] & [d1,y] in [:VV,VV:] by A6,ZFMISC_1:106; then A.[d1,y] = (the add of V).[d1,y] by FUNCT_1:72 .= v0 + v1 by RLVECT_1:def 3 .= y by RLVECT_1:10; hence thesis by A3,A7; end; given x being set such that A8: x in dom A and A9: y = A.x; consider x1,x2 being set such that A10: x1 in D & x2 in D and A11: x = [x1,x2] by A3,A8,ZFMISC_1:def 2; A12: [x1,x2] in [:VV,VV:] & [x1,x2] in [:V1,V1:] by A10,ZFMISC_1:106; reconsider v1 = x1, v2 = x2 as Element of VV by A10; y = (the add of V).[x1,x2] by A9,A11,A12,FUNCT_1:72 .= v1 + v2 by RLVECT_1:def 3; hence y in D by A2,A10,RLSUB_1:def 1; end; hence thesis by FUNCT_1:def 5; end; A13:D = rng M proof now let y be set; thus y in D implies ex x being set st x in dom M & y = M.x proof assume A14: y in D; then reconsider v1 = y as Element of VV; A15: [1,y] in [:REAL,D:] & [1,y] in [:REAL,VV:] by A14,ZFMISC_1:106; then M.[1,y] = (the Mult of V).[1,y] by FUNCT_1:72 .= 1 * v1 by RLVECT_1:def 4 .= y by RLVECT_1:def 9; hence thesis by A4,A15; end; given x being set such that A16: x in dom M and A17: y = M.x; consider x1,x2 being set such that A18: x1 in REAL and A19: x2 in D and A20: x = [x1,x2] by A4,A16,ZFMISC_1:def 2; A21: [x1,x2] in [:REAL,VV:] & [x1,x2] in [:REAL,V1:] by A18,A19,ZFMISC_1:106; reconsider v2 = x2 as Element of VV by A19; reconsider xx1 = x1 as Real by A18; y = (the Mult of V).[x1,x2] by A17,A20,A21,FUNCT_1:72 .= xx1 * v2 by RLVECT_1:def 4; hence y in D by A2,A19,RLSUB_1:def 1; end; hence thesis by FUNCT_1:def 5; end; reconsider A as Function of [:D,D:],D by A3,A5,FUNCT_2:def 1,RELSET_1:11; reconsider M as Function of [:REAL,D:],D by A4,A13,FUNCT_2:def 1,RELSET_1:11; reconsider S as Function of [:D,D:],REAL by FUNCT_2:38; set W = UNITSTR (# D,d1,A,M,S #); W is Subspace of V & the carrier of W = D by Th18; hence thesis; end; 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 :Def2: the carrier of it = {0.V}; correctness proof {0.V} is lineary-closed & {0.V} <> {} by RLSUB_1:7; hence thesis by Th24,Th29; end; end; definition let V being RealUnitarySpace; func (Omega).V -> strict Subspace of V equals :Def3: the UNITSTR of V; coherence proof set W = the UNITSTR of V; W is Abelian add-associative right_zeroed right_complementable RealLinearSpace-like RealUnitarySpace-like proof A1: 0.W = the Zero of W by RLVECT_1:def 2 .= 0.V by RLVECT_1:def 2; A2: now let a be Real; let v,w be VECTOR of W, v',w' be VECTOR of V such that A3: v=v' & w=w'; thus v+w = (the add of W).[v,w] by RLVECT_1:def 3 .= v'+w' by A3,RLVECT_1:def 3; thus a*v = (the Mult of W).[a,v] by RLVECT_1:def 4 .= a*v' by A3,RLVECT_1:def 4; thus v .|. w = (the scalar of W).[v,w] by BHSP_1:def 1 .= v' .|. w' by A3,BHSP_1:def 1; end; thus for v,w being VECTOR of W holds v + w = w + v proof let v,w be VECTOR of W; reconsider v'=v,w'=w as VECTOR of V; thus v + w = w' + v' by A2 .= w + v by A2; end; thus for u,v,w being VECTOR of W holds (u + v) + w = u + (v + w) proof let u,v,w be VECTOR of W; reconsider u'=u,v'=v,w'=w as VECTOR of V; A4: v + w = v' + w' & u + v = u' + v' by A2; hence (u + v) + w = (u' + v') + w' by A2 .= u' + (v' + w') by RLVECT_1:def 6 .= u + (v + w) by A2,A4; end; thus for v being VECTOR of W holds v + 0.W = v proof let v be VECTOR of W; reconsider v'=v as VECTOR of V; thus v + 0.W = v' + 0.V by A1,A2 .= v by RLVECT_1:10; end; thus for v being VECTOR of W ex w being VECTOR of W st v + w = 0.W proof let v be VECTOR of W; reconsider v'=v as VECTOR of V; consider w' being VECTOR of V such that A5: v' + w' = 0.V by RLVECT_1:def 8; reconsider w=w' as VECTOR of W; take w; thus v + w = 0.W by A1,A2,A5; end; thus for a be Real ,v,w being VECTOR of W holds a * (v + w) = a * v + a * w proof let a be Real; let v,w be VECTOR of W; reconsider v'=v,w'=w as VECTOR of V; A6: v + w = v' + w' & a * v = a * v' & a * w = a * w' by A2; hence a * (v + w) = a * (v' + w') by A2 .= a * v' + a * w' by RLVECT_1:def 9 .= a * v + a * w by A2,A6; end; thus for a,b be Real, v being VECTOR of W holds (a + b) * v = a * v + b * v proof let a,b be Real; let v be VECTOR of W; reconsider v'=v as VECTOR of V; A7: a * v = a * v' & b * v = b * v' by A2; thus (a + b) * v = (a + b) * v' by A2 .= a * v' + b * v' by RLVECT_1:def 9 .= a * v + b * v by A2,A7; end; thus for a,b be Real, v being VECTOR of W holds (a * b) * v = a * (b * v) proof let a,b be Real; let v be VECTOR of W; reconsider v'=v as VECTOR of V; A8: b * v = b * v' by A2; thus (a * b) * v = (a * b) * v' by A2 .= a * (b * v') by RLVECT_1:def 9 .= a * (b * v) by A2,A8; end; thus for v being VECTOR of W holds 1 * v = v proof let v be VECTOR of W; reconsider v'=v as VECTOR of V; thus 1 * v = 1 * v' by A2 .= v by RLVECT_1:def 9; end; thus W is RealUnitarySpace-like proof for x , y , z being VECTOR of W , a being Real holds ( x .|. x = 0 iff x = 0.W ) & 0 <= x .|. x & x .|. y = y .|. x & (x+y) .|. z = x .|. z + y .|. z & (a*x) .|. y = a * ( x .|. y ) proof let x,y,z be VECTOR of W; let a be Real; reconsider x' = x as VECTOR of V; reconsider y' = y as VECTOR of V; reconsider z' = z as VECTOR of V; thus x .|. x = 0 iff x = 0.W proof x' .|. x' = x .|. x by A2; hence thesis by A1,BHSP_1:def 2; end; thus 0 <= x .|. x proof x' .|. x' = x .|. x by A2; hence thesis by BHSP_1:def 2; end; thus x .|. y = y .|. x proof x' .|. y' = x .|. y & y' .|. x' = y .|. x by A2; hence thesis; end; thus (x+y) .|. z = x .|. z + y .|. z proof A9: x'+y' = x+y & x' .|. z' = x .|. z & y' .|. z' = y .|. z by A2; then (x+y) .|. z = (x'+y') .|. z' by A2 .= x' .|. z' + y' .|. z' by BHSP_1:def 2; hence thesis by A9; end; thus (a*x) .|. y = a * ( x .|. y ) proof a*x' = a*x & x' .|. y' = x .|. y by A2; then (a*x) .|. y = (a*x') .|. y' by A2 .= a * (x' .|. y') by BHSP_1:def 2; hence thesis by A2; end; end; hence thesis by BHSP_1:def 2; end; end; then reconsider W as RealUnitarySpace; W is Subspace of V proof thus the carrier of W c= the carrier of V & the Zero of W = the Zero of V; thus thesis by FUNCT_2:40; end; hence thesis; end; end; begin :: Theorems of Zero Subspace and Improper Subspace theorem Th30: for V being RealUnitarySpace, W being Subspace of V holds (0).W = (0).V proof let V be RealUnitarySpace; let W be Subspace of V; the carrier of (0).W = {0.W} & the carrier of (0).V = {0.V} by Def2; then the carrier of (0).W = the carrier of (0).V & (0).W is Subspace of V by Th4,Th21; hence thesis by Th24; end; theorem Th31: for V being RealUnitarySpace, W1,W2 being Subspace of V holds (0).W1 = (0).W2 proof let V be RealUnitarySpace; let W1,W2 be Subspace of V; (0).W1 = (0).V & (0).W2 = (0).V by Th30; hence thesis; end; theorem for V being RealUnitarySpace, W being Subspace of V holds (0).W is Subspace of V by Th21; theorem for V being RealUnitarySpace, W being Subspace of V holds (0).V is Subspace of W proof let V be RealUnitarySpace; let W be Subspace of V; the carrier of (0).V = {0.V} by Def2 .= {0.W} by Th4 .= {the Zero of W} by RLVECT_1:def 2; hence thesis by Th22; end; theorem for V being RealUnitarySpace, W1,W2 being Subspace of V holds (0).W1 is Subspace of W2 proof let V be RealUnitarySpace; let W1,W2 be Subspace of V; (0).W1 = (0).W2 & (0).W2 is Subspace of W2 by Th31; hence thesis; end; theorem for V being strict RealUnitarySpace holds V is Subspace of (Omega).V proof let V be strict RealUnitarySpace; V is Subspace of V by Th19; hence thesis by Def3; end; 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 :Def4: {v + u where u is VECTOR of V : u in W}; coherence proof defpred P[set] means ex u being VECTOR of V st $1 = v + u & u in W; consider X being set such that A1:for x being set holds x in X iff x in the carrier of V & P[x] from Separation; X c= the carrier of V proof let x be set; assume x in X; hence x in the carrier of V by A1; end; then reconsider X as Subset of V; set Y = {v + u where u is VECTOR of V : u in W}; X = Y proof thus X c= Y proof let x be set; assume x in X; then ex u being VECTOR of V st x = v + u & u in W by A1; hence thesis; end; thus Y c= X proof let x be set; assume x in Y; then ex u being VECTOR of V st x = v + u & u in W; hence thesis by A1; end; end; hence thesis; end; end; Lm2: for V being RealUnitarySpace, W being Subspace of V holds 0.V + W = the carrier of W proof let V be RealUnitarySpace; let W be Subspace of V; set A = {0.V + u where u is VECTOR of V : u in W}; A1:0.V + W = A by Def4; A2:A c= the carrier of W proof let x be set; assume x in A; then consider u being VECTOR of V such that A3: x = 0.V + u and A4: u in W; x = u by A3,RLVECT_1:10; hence thesis by A4,RLVECT_1:def 1; end; the carrier of W c= A proof let x be set; assume x in the carrier of W; then A5: x in W by RLVECT_1:def 1; then x in V by Th2; then reconsider y = x as Element of V by RLVECT_1:def 1; 0.V + y = x by RLVECT_1:10; hence thesis by A5; end; hence thesis by A1,A2,XBOOLE_0:def 10; end; definition let V be RealUnitarySpace; let W be Subspace of V; mode Coset of W -> Subset of V means :Def5: ex v be VECTOR of V st it = v + W; existence proof reconsider VW = the carrier of W as Subset of V by Def1; take VW; take 0.V; thus thesis by Lm2; end; end; begin :: Theorems of the Cosets theorem Th36: for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds 0.V in v + W iff v in W proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; set A = {v + u where u is VECTOR of V : u in W}; thus 0.V in v + W implies v in W proof assume 0.V in v + W; then 0.V in A by Def4; then consider u being VECTOR of V such that A1: 0.V = v + u and A2: u in W; v = - u by A1,RLVECT_1:def 10; hence thesis by A2,Th16; end; assume v in W; then A3:- v in W by Th16; 0.V = v - v by RLVECT_1:28 .= v + (- v) by RLVECT_1:def 11; then 0.V in A by A3; hence thesis by Def4; end; theorem Th37: for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds v in v + W proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; v + 0.V = v & 0.V in W by Th11,RLVECT_1:10; then v in {v + u where u is VECTOR of V : u in W}; hence thesis by Def4; end; theorem for V being RealUnitarySpace, W being Subspace of V holds 0.V + W = the carrier of W by Lm2; theorem Th39: for V being RealUnitarySpace, v being VECTOR of V holds v + (0).V = {v} proof let V be RealUnitarySpace; let v be VECTOR of V; set A = {v + u where u is VECTOR of V : u in (0).V}; thus v + (0).V c= {v} proof let x be set; assume x in v + (0).V; then x in A by Def4; then consider u being VECTOR of V such that A1: x = v + u and A2: u in (0).V; the carrier of (0).V = {0.V} & u in the carrier of (0).V by A2,Def2,RLVECT_1:def 1; then u = 0.V by TARSKI:def 1; then x = v by A1,RLVECT_1:10; hence thesis by TARSKI:def 1; end; let x be set; assume x in {v}; then A3:x = v by TARSKI:def 1; 0.V in (0).V & v = v + 0.V by Th11,RLVECT_1:10; then x in A by A3; hence thesis by Def4; end; Lm3: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; set A = {v + u where u is VECTOR of V: u in W}; thus v in W implies v + W = the carrier of W proof assume A1: v in W; thus v + W c= the carrier of W proof let x be set; assume x in v + W; then x in A by Def4; then consider u being VECTOR of V such that A2: x = v + u and A3: u in W; v + u in W by A1,A3,Th14; hence thesis by A2,RLVECT_1:def 1; end; let x be set; assume x in the carrier of W; then reconsider y = x, z = v as Element of W by A1,RLVECT_1:def 1; reconsider y1 = y, z1 = z as VECTOR of V by Th3; A4: y - z in W by RLVECT_1:def 1; A5: z + (y - z) = (y + z) - z by RLVECT_1:42 .= y + (z - z) by RLVECT_1:42 .= y + 0.W by RLVECT_1:28 .= x by RLVECT_1:10; A6: y - z = y1 - z1 by Th10; A7: y1 - z1 in W by A4,Th10; z1 + (y1 - z1) = x by A5,A6,Th6; then x in A by A7; hence thesis by Def4; end; assume A8:v + W = the carrier of W; assume A9:not v in W; 0.V in W & v + 0.V = v by Th11,RLVECT_1:10; then v in {v + u where u is VECTOR of V : u in W}; then v in the carrier of W by A8,Def4; hence thesis by A9,RLVECT_1:def 1; end; theorem Th40: for V being RealUnitarySpace, v being VECTOR of V holds v + (Omega).V = the carrier of V proof let V be RealUnitarySpace; let v be VECTOR of V; A1:the carrier of (Omega).V = the carrier of the UNITSTR of V by Def3 .= the carrier of V; then v in (Omega).V by RLVECT_1:def 1; hence thesis by A1,Lm3; end; theorem Th41: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; (0.V in v + W iff v in W) & (v in W iff v + W = the carrier of W) by Lm3,Th36; hence thesis; end; theorem 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 by Lm3; theorem Th43: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; let a be Real; set A = {a * v + u where u is VECTOR of V : u in W}; assume A1:v in W; thus (a * v) + W c= the carrier of W proof let x be set; assume x in (a * v) + W; then x in A by Def4; then consider u being VECTOR of V such that A2: x = a * v + u and A3: u in W; a * v in W by A1,Th15; then a * v + u in W by A3,Th14; hence thesis by A2,RLVECT_1:def 1; end; let x be set; assume A4:x in the carrier of W; the carrier of W c= the carrier of V & v in V by Def1,RLVECT_1:3; then reconsider y = x as Element of V by A4; a * v in W & x in W by A1,A4,Th15,RLVECT_1:def 1; then A5:y - a * v in W by Th17; a * v + (y - a * v) = (y + a * v) - a * v by RLVECT_1:42 .= y + (a * v - a * v) by RLVECT_1:42 .= y + 0.V by RLVECT_1:28 .= x by RLVECT_1:10; then x in A by A5; hence thesis by Def4; end; theorem Th44: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; let a be Real; assume that A1:a <> 0 and A2:(a * v) + W = the carrier of W; assume not v in W; then not 1 * v in W by RLVECT_1:def 9; then not (a" * a) * v in W by A1,XCMPLX_0:def 7; then not a" * (a * v) in W by RLVECT_1:def 9; then A3:not a * v in W by Th15; 0.V in W & a * v + 0.V = a * v by Th11,RLVECT_1:10; then a * v in {a * v + u where u is VECTOR of V : u in W}; then a * v in the carrier of W by A2,Def4; hence contradiction by A3,RLVECT_1:def 1; end; theorem Th45: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; (v in W iff ((- 1) * v) + W = the carrier of W) & (- 1) * v = - v by Th43,Th44,RLVECT_1:29; hence thesis; end; theorem Th46: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let u,v be VECTOR of V; set A = {v + v1 where v1 is VECTOR of V : v1 in W}; set B = {(v + u) + v2 where v2 is VECTOR of V : v2 in W}; thus u in W implies v + W = (v + u) + W proof assume A1: u in W; thus v + W c= (v + u) + W proof let x be set; assume x in v + W; then x in A by Def4; then consider v1 being VECTOR of V such that A2: x = v + v1 and A3: v1 in W; A4: v1 - u in W by A1,A3,Th17; (v + u) + (v1 - u) = v + (u + (v1 - u)) by RLVECT_1:def 6 .= v + ((v1 + u) - u) by RLVECT_1:42 .= v + (v1 + (u - u)) by RLVECT_1:42 .= v + (v1 + 0.V) by RLVECT_1:28 .= x by A2,RLVECT_1:10; then x in B by A4; hence thesis by Def4; end; let x be set; assume x in (v + u) + W; then x in B by Def4; then consider v2 being VECTOR of V such that A5: x = (v + u) + v2 and A6: v2 in W; A7: u + v2 in W by A1,A6,Th14; x = v + (u + v2) by A5,RLVECT_1:def 6; then x in A by A7; hence thesis by Def4; end; assume A8:v + W = (v + u) + W; 0.V in W & v + 0.V = v by Th11,RLVECT_1:10; then v in A; then v in (v + u) + W by A8,Def4; then v in B by Def4; then consider u1 being VECTOR of V such that A9:v = (v + u) + u1 and A10:u1 in W; v = v + 0.V & v = v + (u + u1) by A9,RLVECT_1:10,def 6; then A11:u + u1 = 0.V by RLVECT_1:21; u = - u1 by A11,RLVECT_1:def 10; hence thesis by A10,Th16; end; theorem 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 proof let V be RealUnitarySpace; let W be Subspace of V; let u,v be VECTOR of V; A1:(- u in W iff v + W = (v + (- u)) + W) & v + (- u) = v - u by Th46,RLVECT_1:def 11; - u in W implies u in W proof assume - u in W; then - (- u) in W by Th16; hence thesis by RLVECT_1:30; end; hence thesis by A1,Th16; end; theorem Th48: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let u,v be VECTOR of V; set A = {u + v1 where v1 is VECTOR of V: v1 in W}; set B = {v + v2 where v2 is VECTOR of V: v2 in W}; thus v in u + W implies u + W = v + W proof assume v in u + W; then v in A by Def4; then consider z being VECTOR of V such that A1: v = u + z and A2: z in W; thus u + W c= v + W proof let x be set; assume x in u + W; then x in A by Def4; then consider v1 being VECTOR of V such that A3: x = u + v1 and A4: v1 in W; A5: v1 - z in W by A2,A4,Th17; v - z = u + (z - z) by A1,RLVECT_1:42 .= u + 0.V by RLVECT_1:28 .= u by RLVECT_1:10; then x = (v + (- z)) + v1 by A3,RLVECT_1:def 11 .= v + (v1 + (- z)) by RLVECT_1:def 6 .= v + (v1 - z) by RLVECT_1:def 11; then x in B by A5; hence thesis by Def4; end; let x be set; assume x in v + W; then x in B by Def4; then consider v2 being VECTOR of V such that A6: x = v + v2 and A7: v2 in W; A8: z + v2 in W by A2,A7,Th14; x = u + (z + v2) by A1,A6,RLVECT_1:def 6; then x in A by A8; hence thesis by Def4; end; thus thesis by Th37; end; theorem Th49: for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds v + W = (- v) + W iff v in W proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; thus v + W = (- v) + W implies v in W proof assume v + W = (- v) + W; then v in (- v) + W by Th37; then v in {- v + u where u is VECTOR of V : u in W} by Def4; then consider u being VECTOR of V such that A1: v = - v + u and A2: u in W; 0.V = v - (- v + u) by A1,RLVECT_1:28 .= (v - (- v)) - u by RLVECT_1:41 .= (v + (- (- v))) - u by RLVECT_1:def 11 .= (v + v) - u by RLVECT_1:30 .= (1 * v + v) - u by RLVECT_1:def 9 .= (1 * v + 1 * v) - u by RLVECT_1:def 9 .= ((1 + 1) * v) - u by RLVECT_1:def 9 .= 2 * v - u; then 2" * (2 * v) = 2" * u by RLVECT_1:35; then (2" * 2) * v = 2" * u & 0 <> 2 by RLVECT_1:def 9; then v = 2" * u by RLVECT_1:def 9; hence thesis by A2,Th15; end; assume v in W; then v + W = the carrier of W & (- v) + W = the carrier of W by Lm3,Th45; hence thesis; end; theorem Th50: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let u,v1,v2 be VECTOR of V; assume that A1:u in v1 + W and A2:u in v2 + W; set A = {v1 + u1 where u1 is VECTOR of V : u1 in W}; set B = {v2 + u2 where u2 is VECTOR of V : u2 in W}; u in A by A1,Def4; then consider x1 being VECTOR of V such that A3:u = v1 + x1 and A4:x1 in W; u in B by A2,Def4; then consider x2 being VECTOR of V such that A5:u = v2 + x2 and A6:x2 in W; thus v1 + W c= v2 + W proof let x be set; assume x in v1 + W; then x in A by Def4; then consider u1 being VECTOR of V such that A7: x = v1 + u1 and A8: u1 in W; u - x1 = v1 + (x1 - x1) by A3,RLVECT_1:42 .= v1 + 0.V by RLVECT_1:28 .= v1 by RLVECT_1:10; then A9: x = (v2 + (x2 - x1)) + u1 by A5,A7,RLVECT_1:42 .= v2 + ((x2 - x1) + u1) by RLVECT_1:def 6; x2 - x1 in W by A4,A6,Th17; then (x2 - x1) + u1 in W by A8,Th14; then x in B by A9; hence thesis by Def4; end; let x be set; assume x in v2 + W; then x in B by Def4; then consider u1 being VECTOR of V such that A10:x = v2 + u1 and A11:u1 in W; u - x2 = v2 + (x2 - x2) by A5,RLVECT_1:42 .= v2 + 0.V by RLVECT_1:28 .= v2 by RLVECT_1:10; then A12:x = (v1 + (x1 - x2)) + u1 by A3,A10,RLVECT_1:42 .= v1 + ((x1 - x2) + u1) by RLVECT_1:def 6; x1 - x2 in W by A4,A6,Th17; then (x1 - x2) + u1 in W by A11,Th14; then x in A by A12; hence thesis by Def4; end; theorem 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 proof let V be RealUnitarySpace; let W be Subspace of V; let u,v be VECTOR of V; assume u in v + W & u in (- v) + W; then v + W = (- v) + W by Th50; hence thesis by Th49; end; theorem Th52: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; let a be Real; assume that A1:a <> 1 and A2:a * v in v + W; A3:now assume a - 1 = 0; then (- 1) + a = 0 by XCMPLX_0:def 8; then a = - (- 1) by XCMPLX_0:def 6; hence contradiction by A1; end; a * v in {v + u where u is VECTOR of V : u in W} by A2,Def4; then consider u being VECTOR of V such that A4:a * v = v + u and A5:u in W; u = u + 0.V by RLVECT_1:10 .= u + (v - v) by RLVECT_1:28 .= a * v - v by A4,RLVECT_1:42 .= a * v - 1 * v by RLVECT_1:def 9 .= (a - 1) * v by RLVECT_1:49; then (a - 1)" * u = ((a - 1)" * (a - 1)) * v & a - 1 <> 0 by A3,RLVECT_1:def 9; then 1 * v = (a - 1)" * u by XCMPLX_0:def 7; then v = (a - 1)" * u by RLVECT_1:def 9; hence thesis by A5,Th15; end; theorem Th53: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; let a be Real; assume A1:v in W; A2:a * v = (a - (1 - 1)) * v .= ((a - 1) + 1) * v by XCMPLX_1:37 .= (a - 1) * v + 1 * v by RLVECT_1:def 9 .= v + (a - 1) * v by RLVECT_1:def 9; (a - 1) * v in W by A1,Th15; then a * v in {v + u where u is VECTOR of V : u in W} by A2; hence thesis by Def4; end; theorem for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds - v in v + W iff v in W proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; (v in W implies (- 1) * v in v + W) & (- 1) * v = - v & (-1 <> 1 & (- 1) * v in v + W implies v in W) by Th52,Th53,RLVECT_1:29; hence thesis; end; theorem Th55: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let u,v be VECTOR of V; set A = {v + v1 where v1 is VECTOR of V : v1 in W}; thus u + v in v + W implies u in W proof assume u + v in v + W; then u + v in A by Def4; then consider v1 being VECTOR of V such that A1: u + v = v + v1 and A2: v1 in W; thus thesis by A1,A2,RLVECT_1:21; end; assume u in W; then u + v in A; hence thesis by Def4; end; theorem 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 proof let V be RealUnitarySpace; let W be Subspace of V; let u,v be VECTOR of V; A1:v - u = (- u) + v by RLVECT_1:def 11; A2:u in W implies - u in W by Th16; - u in W implies - (- u) in W by Th16; hence thesis by A1,A2,Th55,RLVECT_1:30; end; theorem Th57: 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) proof let V be RealUnitarySpace; let W be Subspace of V; let u,v be VECTOR of V; set A = {v + v2 where v2 is VECTOR of V : v2 in W}; thus u in v + W implies (ex v1 being VECTOR of V st v1 in W & u = v + v1) proof assume u in v + W; then u in A by Def4; then ex v1 being VECTOR of V st u = v + v1 & v1 in W; hence thesis; end; given v1 being VECTOR of V such that A1:v1 in W & u = v + v1; u in A by A1; hence thesis by Def4; end; theorem 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) proof let V be RealUnitarySpace; let W be Subspace of V; let u,v be VECTOR of V; set A = {v + v2 where v2 is VECTOR of V : v2 in W}; thus u in v + W implies (ex v1 being VECTOR of V st v1 in W & u = v - v1) proof assume u in v + W; then u in A by Def4; then consider v1 being VECTOR of V such that A1: u = v + v1 and A2: v1 in W; take x = - v1; thus x in W by A2,Th16; u = v + (- (- v1)) by A1,RLVECT_1:30 .= v - (- v1) by RLVECT_1:def 11; hence thesis; end; given v1 being VECTOR of V such that A3:v1 in W & u = v - v1; u = v + (- v1) & - v1 in W by A3,Th16,RLVECT_1:def 11; then u in A; hence thesis by Def4; end; theorem Th59: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let v1,v2 be VECTOR of V; thus (ex v being VECTOR of V st v1 in v + W & v2 in v + W) implies v1 - v2 in W proof given v be VECTOR of V such that A1: v1 in v + W and A2: v2 in v + W; consider u1 being VECTOR of V such that A3: u1 in W and A4: v1 = v + u1 by A1,Th57; consider u2 being VECTOR of V such that A5: u2 in W and A6: v2 = v + u2 by A2,Th57; v1 - v2 = (u1 + v) + (- (v + u2)) by A4,A6,RLVECT_1:def 11 .= (u1 + v) + ((- v) - u2) by RLVECT_1:44 .= ((u1 + v) + (- v)) - u2 by RLVECT_1:42 .= (u1 + (v + (- v))) - u2 by RLVECT_1:def 6 .= (u1 + 0.V) - u2 by RLVECT_1:16 .= u1 - u2 by RLVECT_1:10; hence thesis by A3,A5,Th17; end; assume v1 - v2 in W; then A7: - (v1 - v2) in W by Th16; take v1; thus v1 in v1 + W by Th37; v1 + (- (v1 - v2)) = v1 + ((- v1) + v2) by RLVECT_1:47 .= (v1 + (- v1)) + v2 by RLVECT_1:def 6 .= 0.V + v2 by RLVECT_1:16 .= v2 by RLVECT_1:10; hence thesis by A7,Th57; end; theorem Th60: 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) proof let V be RealUnitarySpace; let W be Subspace of V; let u,v be VECTOR of V; assume A1:v + W = u + W; take v1 = u - v; v in u + W by A1,Th37; then v in {u + u2 where u2 is VECTOR of V : u2 in W} by Def4; then consider u1 being VECTOR of V such that A2:v = u + u1 and A3:u1 in W; 0.V = (u + u1) - v by A2,RLVECT_1:28 .= u + (u1 - v) by RLVECT_1:42 .= u + ((- v) + u1) by RLVECT_1:def 11 .= (u + (- v)) + u1 by RLVECT_1:def 6 .= u1 + (u - v) by RLVECT_1:def 11; then v1 = - u1 by RLVECT_1:def 10; hence v1 in W by A3,Th16; thus v + v1 = (u + v) - v by RLVECT_1:42 .= u + (v - v) by RLVECT_1:42 .= u + 0.V by RLVECT_1:28 .= u by RLVECT_1:10; end; theorem Th61: 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) proof let V be RealUnitarySpace; let W be Subspace of V; let u,v be VECTOR of V; assume A1:v + W = u + W; take v1 = v - u; u in v + W by A1,Th37; then u in {v + u2 where u2 is VECTOR of V : u2 in W} by Def4; then consider u1 being VECTOR of V such that A2:u = v + u1 and A3: u1 in W; 0.V = (v + u1) - u by A2,RLVECT_1:28 .= v + (u1 - u) by RLVECT_1:42 .= v + ((- u) + u1) by RLVECT_1:def 11 .= (v + (- u)) + u1 by RLVECT_1:def 6 .= u1 + (v - u) by RLVECT_1:def 11; then v1 = - u1 by RLVECT_1:def 10; hence v1 in W by A3,Th16; thus v - v1 = (v - v) + u by RLVECT_1:43 .= 0.V + u by RLVECT_1:28 .= u by RLVECT_1:10; end; theorem Th62: for V being RealUnitarySpace, W1,W2 being strict Subspace of V, v being VECTOR of V holds v + W1 = v + W2 iff W1 = W2 proof let V be RealUnitarySpace; let W1,W2 be strict Subspace of V; let v be VECTOR of V; thus v + W1 = v + W2 implies W1 = W2 proof assume A1: v + W1 = v + W2; the carrier of W1 = the carrier of W2 proof A2: the carrier of W1 c= the carrier of V by Def1; A3: the carrier of W2 c= the carrier of V by Def1; thus the carrier of W1 c= the carrier of W2 proof let x be set; assume A4: x in the carrier of W1; then reconsider y = x as Element of V by A2; set z = v + y; x in W1 by A4,RLVECT_1:def 1; then z in {v + u where u is VECTOR of V : u in W1}; then z in v + W2 by A1,Def4; then z in {v + u where u is VECTOR of V : u in W2} by Def4; then consider u being VECTOR of V such that A5: z = v + u and A6: u in W2; y = u by A5,RLVECT_1:21; hence thesis by A6,RLVECT_1:def 1; end; let x be set; assume A7: x in the carrier of W2; then reconsider y = x as Element of V by A3; set z = v + y; x in W2 by A7,RLVECT_1:def 1; then z in {v + u where u is VECTOR of V : u in W2}; then z in v + W1 by A1,Def4; then z in {v + u where u is VECTOR of V : u in W1} by Def4; then consider u being VECTOR of V such that A8: z = v + u and A9: u in W1; y = u by A8,RLVECT_1:21; hence thesis by A9,RLVECT_1:def 1; end; hence thesis by Th24; end; thus thesis; end; theorem Th63: 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 proof let V be RealUnitarySpace; let W1,W2 be strict Subspace of V; let u,v be VECTOR of V; assume A1:v + W1 = u + W2; set V1 = the carrier of W1; set V2 = the carrier of W2; assume A2:W1 <> W2; then V1 <> V2 by Th24; then A3:not V1 c= V2 or not V2 c= V1 by XBOOLE_0:def 10; A4:now assume A5: V1 \ V2 <> {}; consider x being Element of V1 \ V2; x in V1 & not x in V2 by A5,XBOOLE_0:def 4; then A6: x in W1 & not x in W2 by RLVECT_1:def 1; then x in V by Th2; then reconsider x as Element of V by RLVECT_1:def 1; set z = v + x; z in {v + u2 where u2 is VECTOR of V : u2 in W1} by A6; then z in u + W2 by A1,Def4; then z in {u + u2 where u2 is VECTOR of V : u2 in W2} by Def4; then consider u1 being VECTOR of V such that A7: z = u + u1 and A8: u1 in W2; x = 0.V + x by RLVECT_1:10 .= v - v + x by RLVECT_1:28 .= (- v + v) + x by RLVECT_1:def 11 .= - v + (u + u1) by A7,RLVECT_1:def 6; then A9: (v + (- v + (u + u1))) + W1 = v + W1 by A6,Th46; v + (- v + (u + u1)) = (v + (- v)) + (u + u1) by RLVECT_1:def 6 .= (v - v) + (u + u1) by RLVECT_1:def 11 .= 0.V + (u + u1) by RLVECT_1:28 .= u + u1 by RLVECT_1:10; then (u + u1) + W2 = (u + u1) + W1 by A1,A8,A9,Th46; hence thesis by A2,Th62; end; now assume A10: V2 \ V1 <> {}; consider x being Element of V2 \ V1; x in V2 & not x in V1 by A10,XBOOLE_0:def 4; then A11: x in W2 & not x in W1 by RLVECT_1:def 1; then x in V by Th2; then reconsider x as Element of V by RLVECT_1:def 1; set z = u + x; z in {u + u2 where u2 is VECTOR of V : u2 in W2} by A11; then z in v + W1 by A1,Def4; then z in {v + u2 where u2 is VECTOR of V : u2 in W1} by Def4; then consider u1 being VECTOR of V such that A12: z = v + u1 and A13: u1 in W1; x = 0.V + x by RLVECT_1:10 .= u - u + x by RLVECT_1:28 .= (- u + u) + x by RLVECT_1:def 11 .= - u + (v + u1) by A12,RLVECT_1:def 6; then A14: (u + (- u + (v + u1))) + W2 = u + W2 by A11,Th46; u + (- u + (v + u1)) = (u + (- u)) + (v + u1) by RLVECT_1:def 6 .= (u - u) + (v + u1) by RLVECT_1:def 11 .= 0.V + (v + u1) by RLVECT_1:28 .= v + u1 by RLVECT_1:10; then (v + u1) + W1 = (v + u1) + W2 by A1,A13,A14,Th46; hence thesis by A2,Th62; end; hence thesis by A3,A4,XBOOLE_1:37; end; theorem 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 proof let V be RealUnitarySpace; let W be Subspace of V; let C be Coset of W; thus C is lineary-closed implies C = the carrier of W proof assume A1: C is lineary-closed; consider v being VECTOR of V such that A2: C = v + W by Def5; C <> {} by A2,Th37; then 0.V in v + W by A1,A2,RLSUB_1:4; hence thesis by A2,Th41; end; thus thesis by Lm1; end; theorem 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 proof let V be RealUnitarySpace; let W1,W2 be strict Subspace of V; let C1 be Coset of W1; let C2 be Coset of W2; A1:ex v1 being VECTOR of V st C1 = v1 + W1 by Def5; ex v2 being VECTOR of V st C2 = v2 + W2 by Def5; hence thesis by A1,Th63; end; theorem 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 proof let V be RealUnitarySpace; let W be Subspace of V; let C be Coset of W; let v be VECTOR of V; v + (0).V = {v} by Th39; hence thesis by Def5; end; theorem 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}) proof let V be RealUnitarySpace; let W be Subspace of V; let V1 be Subset of V; let v be VECTOR of V; assume V1 is Coset of (0).V; then consider v being VECTOR of V such that A1:V1 = v + (0).V by Def5; take v; thus thesis by A1,Th39; end; theorem for V being RealUnitarySpace, W being Subspace of V holds the carrier of W is Coset of W proof let V be RealUnitarySpace; let W be Subspace of V; the carrier of W = 0.V + W by Lm2; hence thesis by Def5; end; theorem for V being RealUnitarySpace holds the carrier of V is Coset of (Omega).V proof let V be RealUnitarySpace; the carrier of V is Subset of V iff the carrier of V c= the carrier of V; then reconsider A = the carrier of V as Subset of V; consider v being VECTOR of V; A = v + (Omega).V by Th40; hence thesis by Def5; end; theorem 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 proof let V be RealUnitarySpace; let W be Subspace of V; let V1 be Subset of V; assume V1 is Coset of (Omega).V; then ex v being VECTOR of V st V1 = v + (Omega).V by Def5; hence thesis by Th40; end; theorem 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 proof let V be RealUnitarySpace; let W be Subspace of V; let C be Coset of W; ex v being VECTOR of V st C = v + W by Def5; hence thesis by Th41; end; theorem Th72: 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 proof let V be RealUnitarySpace; let W be Subspace of V; let C be Coset of W; let u be VECTOR of V; thus u in C implies C = u + W proof assume A1: u in C; ex v being VECTOR of V st C = v + W by Def5; hence thesis by A1,Th48; end; thus thesis by Th37; end; theorem 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) proof let V be RealUnitarySpace; let W be Subspace of V; let C be Coset of W; let u,v be VECTOR of V; assume u in C & v in C; then C = u + W & C = v + W by Th72; hence thesis by Th60; end; theorem 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) proof let V be RealUnitarySpace; let W be Subspace of V; let C be Coset of W; let u,v be VECTOR of V; assume u in C & v in C; then C = u + W & C = v + W by Th72; hence thesis by Th61; end; theorem 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 proof let V be RealUnitarySpace; let W be Subspace of V; let v1,v2 be VECTOR of V; thus (ex C being Coset of W st v1 in C & v2 in C) implies v1 - v2 in W proof given C be Coset of W such that A1: v1 in C & v2 in C; ex v being VECTOR of V st C = v + W by Def5; hence thesis by A1,Th59; end; assume v1 - v2 in W; then consider v being VECTOR of V such that A2:v1 in v + W & v2 in v + W by Th59; reconsider C = v + W as Coset of W by Def5; take C; thus thesis by A2; end; theorem 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 proof let V be RealUnitarySpace; let W be Subspace of V; let u be VECTOR of V; let B,C be Coset of W; assume A1:u in B & u in C; A2:ex v1 being VECTOR of V st B = v1 + W by Def5; ex v2 being VECTOR of V st C = v2 + W by Def5; hence thesis by A1,A2,Th50; end;