### The Mizar article:

### Submodules and Cosets of Submodules in Right Module over Associative Ring

**by****Michal Muzalewski, and****Wojciech Skaba**

- Received October 22, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: RMOD_2
- [ MML identifier index ]

environ vocabulary FUNCSDOM, VECTSP_1, VECTSP_2, RLSUB_1, BOOLE, RLVECT_1, ARYTM_1, LMOD_4, RELAT_1, FUNCT_1, BINOP_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, DOMAIN_1, RLVECT_1, BINOP_1, VECTSP_1, FUNCSDOM, VECTSP_2; constructors DOMAIN_1, BINOP_1, VECTSP_2, PARTFUN1, MEMBERED, XBOOLE_0; clusters FUNCT_1, VECTSP_2, STRUCT_0, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; definitions TARSKI, VECTSP_2, RLVECT_1, XBOOLE_0; theorems BINOP_1, FUNCT_1, FUNCT_2, TARSKI, VECTSP_1, ZFMISC_1, VECTSP_2, MOD_1, RLVECT_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1; schemes XBOOLE_0; begin reserve x,y,y1,y2 for set; reserve R for Ring; reserve a for Scalar of R; reserve V,X,Y for RightMod of R; reserve u,u1,u2,v,v1,v2 for Vector of V; reserve V1,V2,V3 for Subset of V; definition let R, V, V1; attr V1 is lineary-closed means :Def1: (for v,u st v in V1 & u in V1 holds v + u in V1) & (for a,v st v in V1 holds v * a in V1); end; canceled 3; theorem Th4: V1 <> {} & V1 is lineary-closed implies 0.V in V1 proof assume that A1: V1 <> {} and A2: V1 is lineary-closed; consider x being Element of V1; reconsider x as Element of V by A1,TARSKI:def 3; x * 0.R in V1 by A1,A2,Def1; hence thesis by MOD_1:37; end; theorem Th5: V1 is lineary-closed implies (for v st v in V1 holds - v in V1) proof assume A1: V1 is lineary-closed; let v; assume v in V1; then v * (- 1_ R) in V1 by A1,Def1; hence thesis by MOD_1:37; end; theorem V1 is lineary-closed implies (for v,u st v in V1 & u in V1 holds v - u in V1) proof assume A1: V1 is lineary-closed; let v,u; assume that A2: v in V1 and A3: u in V1; v - u = v + (- u) & - u in V1 by A1,A3,Th5,RLVECT_1:def 11; hence thesis by A1,A2,Def1; end; theorem Th7: {0.V} is lineary-closed proof thus for v,u st v in {0.V} & u in {0.V} holds v + u in {0.V} proof let v,u; assume v in {0.V} & u in {0.V}; then v = 0.V & u = 0.V by TARSKI:def 1; then v + u = 0.V & 0.V in {0.V} by TARSKI:def 1,VECTSP_1:7; hence thesis; end; let a,v; assume A1: v in {0.V}; then v = 0.V by TARSKI:def 1; hence thesis by A1,MOD_1:37; end; theorem the carrier of V = V1 implies V1 is lineary-closed proof assume A1: the carrier of V = V1; hence for v,u st v in V1 & u in V1 holds v + u in V1; let a,v; assume v in V1; thus v * a in V1 by A1; end; theorem V1 is lineary-closed & V2 is lineary-closed & V3 = {v + u : v in V1 & u in V2} implies V3 is lineary-closed proof assume that A1: V1 is lineary-closed & V2 is lineary-closed and A2: V3 = {v + u : v in V1 & u in V2}; thus for v,u st v in V3 & u in V3 holds v + u in V3 proof let v,u; assume that A3: v in V3 and A4: u in V3; consider v1,v2 such that A5: v = v1 + v2 and A6: v1 in V1 & v2 in V2 by A2,A3; consider u1,u2 such that A7: u = u1 + u2 and A8: u1 in V1 & u2 in V2 by A2,A4; A9: v1 + u1 in V1 & v2 + u2 in V2 by A1,A6,A8,Def1; v + u = ((v1 + v2) + u1) + u2 by A5,A7,RLVECT_1:def 6 .= ((v1 + u1) + v2) + u2 by RLVECT_1:def 6 .= (v1 + u1) + (v2 + u2) by RLVECT_1:def 6; hence thesis by A2,A9; end; let a,v; assume v in V3; then consider v1,v2 such that A10: v = v1 + v2 and A11: v1 in V1 & v2 in V2 by A2; A12: v1 * a in V1 & v2 * a in V2 by A1,A11,Def1; v * a = v1 * a + v2 * a by A10,VECTSP_2:def 23; hence v * a in V3 by A2,A12; end; theorem V1 is lineary-closed & V2 is lineary-closed implies V1 /\ V2 is lineary-closed proof assume A1: V1 is lineary-closed & V2 is lineary-closed; thus for v,u st v in V1 /\ V2 & u in V1 /\ V2 holds v + u in V1 /\ V2 proof let v,u; assume v in V1 /\ V2 & u in V1 /\ V2; then v in V1 & v in V2 & u in V1 & u in V2 by XBOOLE_0:def 3; then v + u in V1 & v + u in V2 by A1,Def1; hence thesis by XBOOLE_0:def 3; end; let a,v; assume v in V1 /\ V2; then v in V1 & v in V2 by XBOOLE_0:def 3; then v * a in V1 & v * a in V2 by A1,Def1; hence thesis by XBOOLE_0:def 3; end; definition let R; let V; mode Submodule of V -> RightMod of R means :Def2: 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 rmult of it = (the rmult of V) | [:the carrier of it, the carrier of R:]; existence proof take V; 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; end; reserve W,W1,W2 for Submodule of V; reserve w,w1,w2 for Vector of W; canceled 5; theorem x in W1 & W1 is Submodule of W2 implies x in W2 proof assume x in W1 & W1 is Submodule of W2; then x in the carrier of W1 & the carrier of W1 c= the carrier of W2 by Def2,RLVECT_1:def 1; hence thesis by RLVECT_1:def 1; end; theorem Th17: x in W implies x in V proof assume x in W; then x in the carrier of W & the carrier of W c= the carrier of V by Def2,RLVECT_1:def 1; hence thesis by RLVECT_1:def 1; end; theorem Th18: w is Vector of V proof w in W by RLVECT_1:3; then w in V by Th17; hence thesis by RLVECT_1:def 1; end; theorem Th19: 0.W = 0.V proof thus 0.W = the Zero of W by RLVECT_1:def 2 .= the Zero of V by Def2 .= 0.V by RLVECT_1:def 2; end; theorem 0.W1 = 0.W2 proof thus 0.W1 = 0.V by Th19 .= 0.W2 by Th19; end; theorem Th21: w1 = v & w2 = u implies w1 + w2 = v + u proof assume A1: v = w1 & u = w2; set IW = [:the carrier of W, the carrier of W:]; reconsider ww1 = w1, ww2 = w2 as Vector of V by Th18; A2: v + u = (the add of V).(ww1,ww2) by A1,RLVECT_1:5 .= (the add of V).[ww1,ww2] by BINOP_1:def 1; w1 + w2 = (the add of W).(w1,w2) by RLVECT_1:5 .= ((the add of V) | IW).(w1,w2) by Def2 .= ((the add of V) | IW).[w1,w2] by BINOP_1:def 1; hence thesis by A2,FUNCT_1:72; end; theorem Th22: w = v implies w * a = v * a proof assume A1: w = v; reconsider ww1 = w as Vector of V by Th18; A2: v * a = (the rmult of V).(v,a) by VECTSP_2:def 15 .= (the rmult of V).[ww1,a] by A1,BINOP_1:def 1; w * a = (the rmult of W).(w,a) by VECTSP_2:def 15 .= (the rmult of W).[w,a] by BINOP_1:def 1 .= ((the rmult of V) | ([:the carrier of W, the carrier of R:]) ).[w,a] by Def2; hence thesis by A2,FUNCT_1:72; end; theorem Th23: w = v implies - v = - w proof assume A1: w = v; - v = v * (- 1_ R) & - w = w * (- 1_ R) by MOD_1:37; hence thesis by A1,Th22; end; theorem Th24: w1 = v & w2 = u implies w1 - w2 = v - u proof assume that A1: w1 = v and A2: w2 = u; A3: - w2 = - u by A2,Th23; w1 - w2 = w1 + (- w2) & v - u = v + (- u) by RLVECT_1:def 11; hence thesis by A1,A3,Th21; end; Lm1: the carrier of W = V1 implies V1 is lineary-closed proof assume A1: the carrier of W = V1; set VW = the carrier of W; reconsider WW = W as RightMod of R; thus for v,u st v in V1 & u in V1 holds v + u in V1 proof let v,u; 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 Th21; end; let a,v; assume v in V1; then reconsider vv = v as Vector of WW by A1; reconsider vw = vv * a as Element of VW; vw in V1 by A1; hence v * a in V1 by Th22; end; theorem Th25: 0.V in W proof 0.W in W & 0.V = 0.W by Th19,RLVECT_1:3; hence thesis; end; theorem 0.W1 in W2 proof 0.W1 = 0.V by Th19; hence thesis by Th25; end; theorem 0.W in V proof 0.W in W by RLVECT_1:3; hence thesis by Th17; end; theorem Th28: u in W & v in W implies u + v in W proof 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 Def2; VW is lineary-closed by Lm1; then u + v in the carrier of W by A1,Def1; hence thesis by RLVECT_1:def 1; end; theorem Th29: v in W implies v * a in W proof 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 Def2; VW is lineary-closed by Lm1; then v * a in the carrier of W by A1,Def1; hence thesis by RLVECT_1:def 1; end; theorem Th30: v in W implies - v in W proof assume v in W; then v * (- 1_ R) in W by Th29; hence thesis by MOD_1:37; end; theorem Th31: u in W & v in W implies u - v in W proof assume that A1: u in W and A2: v in W; - v in W by A2,Th30; then u + (- v) in W by A1,Th28; hence thesis by RLVECT_1:def 11; end; theorem Th32: V is Submodule of V proof A1: the carrier of V c= the carrier of V & the Zero of V = the Zero of V; the add of V = (the add of V) | [:the carrier of V, the carrier of V:] & the rmult of V = (the rmult of V) | [:the carrier of V, the carrier of R:] by FUNCT_2:40; hence thesis by A1,Def2; end; theorem Th33: for X,V being strict RightMod of R holds V is Submodule of X & X is Submodule of V implies V = X proof let X,V be strict RightMod of R; assume A1: V is Submodule of X & X is Submodule 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 rmult of V; set MX = the rmult of X; VV c= VX & VX c= VV by A1,Def2; then A2: VV = VX by XBOOLE_0:def 10; A3: the Zero of V = the Zero of X by A1,Def2; AV = AX | [:VV,VV:] & AX = AV | [:VX,VX:] by A1,Def2; then A4: AV = AX by A2,RELAT_1:101; MV = MX | [:VV,the carrier of R:] & MX = MV | [:VX,the carrier of R:] by A1,Def2; hence thesis by A2,A3,A4,RELAT_1:101; end; definition let R,V; cluster strict Submodule of V; existence proof set M = the rmult of V; set W = RightModStr (# the carrier of V,the add of V, 0.V,M #); A1: now let a,b be Element of W; let x,y be Vector of V; assume A2: x = a & b = y; thus a + b = (the add of W).(a,b) by RLVECT_1:5 .= x + y by A2,RLVECT_1:5; end; A3: W is Abelian add-associative right_zeroed right_complementable proof thus W is Abelian proof let a,b be Element of W; reconsider x = a, y = b as Vector of V; thus a + b = y + x by A1 .= b + a by A1; end; hereby let a,b,c be Element of W; reconsider x = a, y = b, z = c as Vector of V; A4: a + b = x + y & b + c = y + z by A1; hence a + b + c = x + y + z by A1 .= x + (y + z) by RLVECT_1:def 6 .= a + (b + c) by A1,A4; end; A5: 0.W = 0.V by RLVECT_1:def 2; hereby let a be Element of W; reconsider x = a as Vector of V; thus a + 0.W = x + 0.V by A1,A5 .= a by VECTSP_1:7; end; let a be Element of W; reconsider x = a as Vector of V; reconsider b = (comp V).x as Element of W; take b; thus a + b = x + (comp V).x by A1 .= x + - x by VECTSP_1:def 25 .= 0.W by A5,RLVECT_1:16; end; W is RightMod-like proof let a,b be Scalar of R; let v,w be Vector of W; reconsider x = v, y = w as Vector of V; A6: now let a be Scalar of R; let x be Element of W; let y be Vector of V; assume y = x; hence x * a = M.(y,a) by VECTSP_2:def 15 .= y * a by VECTSP_2:def 15; end; then A7: v * b = x * b & v * a = x * a & w * a = y * a; then v * a + w * a = x * a + y * a & v + w = x + y by A1; hence (v + w) * a = (x + y) * a by A6 .= x * a + y * a by VECTSP_2:def 23 .= v * a + w * a by A1,A7; thus v * (a + b) = x * (a + b) by A6 .= x * a + x * b by VECTSP_2:def 23 .= v * a + v * b by A1,A7; thus v * (b * a) = x * (b * a) by A6 .= x * b * a by VECTSP_2:def 23 .= v * b * a by A6,A7; thus v * 1_ R = x * 1_ R by A6 .= v by VECTSP_2:def 23; end; then reconsider W as RightMod of R by A3; A8: the Zero of W = the Zero of V by RLVECT_1:def 2; the add of W = (the add of V) | [:the carrier of W,the carrier of W:] & the rmult of W = (the rmult of V) | [:the carrier of W, the carrier of R:] by FUNCT_2:40; then reconsider W as Submodule of V by A8,Def2; take W; thus thesis; end; end; theorem Th34: V is Submodule of X & X is Submodule of Y implies V is Submodule of Y proof assume A1: V is Submodule of X & X is Submodule of Y; A2: 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,Def2; hence thesis by XBOOLE_1:1; end; A3: 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,Def2; hence thesis; end; A4: 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,Def2; then AV = (AY | [:VX,VX:]) | [:VV,VV:] & [:VV,VV:] c= [:VX,VX:] by ZFMISC_1:119; hence thesis by FUNCT_1:82; end; set MV = the rmult of V; set VV = the carrier of V; set MX = the rmult of X; set VX = the carrier of X; set MY = the rmult of Y; MV = MX | [:VV,the carrier of R:] & MX = MY | [:VX,the carrier of R:] & VV c= VX by A1,Def2; then MV = (MY | [:VX,the carrier of R:]) | [:VV,the carrier of R:] & [:VV,the carrier of R:] c= [:the carrier of X,the carrier of R:] by ZFMISC_1:118; then MV = MY | [:VV,the carrier of R:] by FUNCT_1:82; hence thesis by A2,A3,A4,Def2; end; theorem Th35: the carrier of W1 c= the carrier of W2 implies W1 is Submodule of W2 proof assume A1: the carrier of W1 c= the carrier of W2; set VW1 = the carrier of W1; set VW2 = the carrier of W2; set MW1 = the rmult of W1; set MW2 = the rmult of W2; set AV = the add of V; set MV = the rmult of V; A2: the Zero of W1 = the Zero of V & the Zero of W2 = the Zero of V by Def2; A3: 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,Def2,ZFMISC_1:119; hence thesis by FUNCT_1:82; end; MW1 = MV | [:VW1,the carrier of R:] & MW2 = MV | [:VW2,the carrier of R:] & [:VW1,the carrier of R:] c= [:VW2,the carrier of R:] by A1,Def2,ZFMISC_1:118; then MW1 = MW2 | [:VW1,the carrier of R:] by FUNCT_1:82; hence thesis by A1,A2,A3,Def2; end; theorem (for v st v in W1 holds v in W2) implies W1 is Submodule of W2 proof assume A1: for 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 Def2; 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 Th35; end; theorem Th37: for W1,W2 being strict Submodule of V holds the carrier of W1 = the carrier of W2 implies W1 = W2 proof let W1,W2 be strict Submodule of V; assume the carrier of W1 = the carrier of W2; then W1 is Submodule of W2 & W2 is Submodule of W1 by Th35; hence thesis by Th33; end; theorem Th38: for W1,W2 being strict Submodule of V holds (for v being Vector of V holds v in W1 iff v in W2) implies W1 = W2 proof let W1,W2 be strict Submodule of V; assume A1: for v being Vector of V holds v in W1 iff v in W2; x in the carrier of W1 iff x in the carrier of W2 proof 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 Def2; 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 Def2; 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 Th37; end; theorem for V being strict RightMod of R, W being strict Submodule of V holds the carrier of W = the carrier of V implies W = V proof let V be strict RightMod of R, W be strict Submodule of V; assume A1: the carrier of W = the carrier of V; V is Submodule of V by Th32; hence thesis by A1,Th37; end; theorem for V being strict RightMod of R, W being strict Submodule of V holds (for v being Vector of V holds v in W) implies W = V proof let V be strict RightMod of R, W be strict Submodule of V; assume for v being Vector of V holds v in W; then A1: for v be Vector of V holds ( v in W iff v in V) by RLVECT_1:3; V is Submodule of V by Th32; hence thesis by A1,Th38; end; theorem the carrier of W = V1 implies V1 is lineary-closed by Lm1; theorem Th42: V1 <> {} & V1 is lineary-closed implies (ex W being strict Submodule of V st V1 = the carrier of W) proof assume that A1: V1 <> {} and A2: V1 is lineary-closed; set VV = the carrier of V; reconsider D = V1 as non empty set by A1; set A = (the add of V) | [:D,D:]; A3: V1 c= the carrier of V & dom(the add of V) = [:VV,VV:] by FUNCT_2:def 1; [:D,D:] c= [:VV,VV:] by ZFMISC_1:119; then A4: dom A = [:D,D:] by A3,RELAT_1:91; rng A c= D proof let x; assume x in rng A; then consider y such that A5: y in dom A and A6: A.y = x by FUNCT_1:def 5; consider y1,y2 such that A7: [y1,y2] = y by A4,A5,ZFMISC_1:102; A8: y1 in D & y2 in D & D c= the carrier of V by A4,A5,A7,ZFMISC_1:106; then reconsider y1,y2 as Vector of V; x = (the add of V).[y1,y2] by A5,A6,A7,FUNCT_1:70 .= (the add of V).(y1,y2) by BINOP_1:def 1 .= y1 + y2 by RLVECT_1:5; hence thesis by A2,A8,Def1; end; then reconsider A as BinOp of D by A4,FUNCT_2:def 1,RELSET_1:11; set C = (comp V) | D; V1 c= the carrier of V & dom(comp V) = VV by FUNCT_2:def 1; then A9: dom C = D by RELAT_1:91; rng C c= D proof let x; assume x in rng C; then consider y such that A10: y in dom C and A11: C.y = x by FUNCT_1: def 5; reconsider y as Vector of V by A9,A10; x = (comp V).y by A10,A11,FUNCT_1:70 .= - y by VECTSP_1:def 25; hence thesis by A2,A9,A10,Th5; end; then reconsider C as UnOp of D by A9,FUNCT_2:def 1,RELSET_1:11; set M = (the rmult of V) | [:D,the carrier of R:]; reconsider d = 0.V as Element of D by A2,Th4; A12: dom(the rmult of V) = [:VV,the carrier of R:] by FUNCT_2:def 1; [:D,the carrier of R:] c= [:VV,the carrier of R:] by ZFMISC_1:119; then A13: dom M = [:D,the carrier of R:] by A12,RELAT_1:91; rng M c= D proof let x; assume x in rng M; then consider y such that A14: y in dom M and A15: M.y = x by FUNCT_1: def 5; consider y2,y1 such that A16: [y2,y1] = y by A13,A14,ZFMISC_1:102; A17: y1 in the carrier of R & y2 in V1 by A13,A14,A16,ZFMISC_1:106; reconsider y1 as Scalar of R by A13,A14,A16,ZFMISC_1:106; reconsider y2 as Vector of V by A17; x = (the rmult of V).[y2,y1] by A14,A15,A16,FUNCT_1:70 .= (the rmult of V).(y2,y1) by BINOP_1:def 1 .= y2 * y1 by VECTSP_2:def 15; hence thesis by A2,A17,Def1; end; then reconsider M as Function of [:D,the carrier of R:], D by A13,FUNCT_2:def 1,RELSET_1:11; set W = RightModStr (# D,A,d,M #); A18: now let a,b be Element of W; let x,y be Vector of V; assume A19: x = a & b = y; thus a + b = (the add of W).(a,b) by RLVECT_1:5 .= A.[a,b] by BINOP_1:def 1 .= (the add of V).[a,b] by A4,FUNCT_1:70 .= (the add of V).(x,y) by A19,BINOP_1:def 1 .= x + y by RLVECT_1:5; end; A20: W is Abelian add-associative right_zeroed right_complementable proof thus W is Abelian proof let a,b be Element of W; reconsider x = a, y = b as Vector of V by TARSKI:def 3; thus a + b = y + x by A18 .= b + a by A18; end; hereby let a,b,c be Element of W; reconsider x = a, y = b, z = c as Vector of V by TARSKI:def 3; A21: a + b = x + y & b + c = y + z by A18; hence a + b + c = x + y + z by A18 .= x + (y + z) by RLVECT_1:def 6 .= a + (b + c) by A18,A21; end; A22: 0.W = 0.V by RLVECT_1:def 2; hereby let a be Element of W; reconsider x = a as Vector of V by TARSKI:def 3; thus a + 0.W = x + 0.V by A18,A22 .= a by VECTSP_1:7; end; let a be Element of W; reconsider x = a as Vector of V by TARSKI:def 3; reconsider b' = (comp V).x as Vector of V; C.x in D by FUNCT_2:7; then reconsider b = ((comp V)|D).x as Element of W; A23: b = b' by FUNCT_1:72; take b; thus a + b = x + b' by A18,A23 .= x + -x by VECTSP_1:def 25 .= 0.W by A22,RLVECT_1:16; end; W is RightMod-like proof let a,b be Scalar of R; let v,w be Vector of W; reconsider x = v, y = w as Vector of V by TARSKI:def 3; A24: now let a be Scalar of R; let x be Element of W; let y be Vector of V; assume A25: y = x; A26: [x,a] in dom M by A13; thus x * a = M.(y,a) by A25,VECTSP_2:def 15 .= M.[y,a] by BINOP_1:def 1 .= (the rmult of V).[y,a] by A25,A26,FUNCT_1:70 .= (the rmult of V).(y,a) by BINOP_1:def 1 .= y * a by VECTSP_2:def 15; end; then A27: v * b = x * b & v * a = x * a & w * a = y * a; then v * a + w * a = x * a + y * a & v + w = x + y by A18; hence (v + w) * a = (x + y) * a by A24 .= x * a + y * a by VECTSP_2:def 23 .= v * a + w * a by A18,A27; thus v * (a + b) = x * (a + b) by A24 .= x * a + x * b by VECTSP_2:def 23 .= v * a + v * b by A18,A27; thus v * (b * a) = x * (b * a) by A24 .= x * b * a by VECTSP_2:def 23 .= v * b * a by A24,A27; thus v * 1_ R = x * 1_ R by A24 .= v by VECTSP_2:def 23; end; then reconsider W as RightMod of R by A20; the Zero of W = the Zero of V by RLVECT_1:def 2; then reconsider W as strict Submodule of V by Def2; take W; thus thesis; end; definition let R; let V; func (0).V -> strict Submodule of V means :Def3: the carrier of it = {0.V}; correctness proof {0.V} is lineary-closed & {0.V} <> {} by Th7; hence thesis by Th37,Th42; end; end; definition let R; let V; func (Omega).V -> strict Submodule of V equals :Def4: the RightModStr of V; coherence proof set W = the RightModStr of V; A1: now let a; let v,w be Vector of W, v',w' be Vector of V such that A2: v=v' & w=w'; thus v+w = (the add of W).(v,w) by RLVECT_1:5 .= v'+w' by A2,RLVECT_1:5; thus v*a = (the rmult of W).(v,a) by VECTSP_2:def 15 .= v'*a by A2,VECTSP_2:def 15; end; A3: W is Abelian add-associative right_zeroed right_complementable proof thus W is Abelian proof let x,y be Element of W; reconsider x' = x, y' = y as Vector of V; thus x+y = y'+x' by A1 .= y+x by A1; end; A4: 0.W = the Zero of W by RLVECT_1:def 2 .= 0.V by RLVECT_1:def 2; hereby let x,y,z be Element of W; reconsider x' = x, y' = y, z' = z as Vector of V; A5: x + y = x' + y' & y + z = y' + z' by A1; hence (x+y)+z = (x'+y')+z' by A1 .= x'+(y'+z') by RLVECT_1:def 6 .= x+(y+z) by A1,A5; end; hereby let x be Element of W; reconsider x' = x as Vector of V; thus x+(0.W) = x'+0.V by A1,A4 .= x by RLVECT_1:10; end; let x be Element of W; reconsider x' = x as Vector of V; consider b being Vector of V such that A6: x' + b = 0.V by RLVECT_1:def 8; reconsider b' = b as Element of W; take b'; thus x+b' = 0.W by A1,A4,A6; end; W is RightMod-like proof let x,y be Element of R, v,w be Element of W; reconsider v' = v, w' = w as Vector of V; A7: v'*x = v*x & v'*y = v*y & w'*x = w*x by A1; v+w = v'+w' by A1; hence (v+w)*x = (v'+w')*x by A1 .= v'*x+w'*x by VECTSP_2:def 23 .= v*x+w*x by A1,A7; thus v*(x+y) = v'*(x+y) by A1 .= v'*x+v'*y by VECTSP_2:def 23 .= v*x +v*y by A1,A7; thus v*(y*x) = v'*(y*x) by A1 .= (v'*y)*x by VECTSP_2:def 23 .= (v*y)*x by A1,A7; thus v*(1_ R) = v'*(1_ R) by A1 .= v by VECTSP_2:def 23; end; then reconsider W as RightMod of R by A3; W is Submodule 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; canceled 3; theorem x in (0).V iff x = 0.V proof thus x in (0).V implies x = 0.V proof assume x in (0).V; then x in the carrier of (0).V by RLVECT_1:def 1; then x in {0.V} by Def3; hence thesis by TARSKI:def 1; end; thus thesis by Th25; end; theorem Th47: (0).W = (0).V proof the carrier of (0).W = {0.W} & the carrier of (0).V = {0.V} by Def3; then the carrier of (0).W = the carrier of (0).V & (0).W is Submodule of V by Th19,Th34; hence thesis by Th37; end; theorem Th48: (0).W1 = (0).W2 proof (0).W1 = (0).V & (0).W2 = (0).V by Th47; hence thesis; end; theorem (0).W is Submodule of V by Th34; theorem (0).V is Submodule of W proof the carrier of (0).V = {0.V} by Def3 .= {0.W} by Th19 .= {the Zero of W} by RLVECT_1:def 2; hence thesis by Th35; end; theorem (0).W1 is Submodule of W2 proof (0).W1 = (0).W2 & (0).W2 is Submodule of W2 by Th48; hence thesis; end; canceled; theorem for V being strict RightMod of R holds V is Submodule of (Omega).V proof let V be strict RightMod of R; V is Submodule of V by Th32; hence thesis by Def4; end; definition let R; let V; let v,W; func v + W -> Subset of V equals :Def5: {v + u : u in W}; coherence proof defpred P[set] means ex u 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 : u in W}; X = Y proof thus X c= Y proof let x be set; assume x in X; then ex u 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 st x = v + u & u in W; hence thesis by A1; end; end; hence thesis; end; end; Lm2: 0.V + W = the carrier of W proof set A = {0.V + u : u in W}; A1: 0.V + W = A by Def5; A2: A c= the carrier of W proof let x be set; assume x in A; then consider u such that A3: x = 0.V + u and A4: u in W; x = u by A3,VECTSP_1:7; 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 Th17; then reconsider y = x as Element of V by RLVECT_1:def 1; 0.V + y = x by VECTSP_1:7; hence thesis by A5; end; hence thesis by A1,A2,XBOOLE_0:def 10; end; definition let R; let V; let W; mode Coset of W -> Subset of V means :Def6: ex v st it = v + W; existence proof reconsider VW = the carrier of W as Subset of V by Def2; take VW; take 0.V; thus thesis by Lm2; end; end; reserve B,C for Coset of W; canceled 3; theorem Th57: x in v + W iff ex u st u in W & x = v + u proof thus x in v + W implies ex u st u in W & x = v + u proof assume x in v + W; then x in {v + u : u in W} by Def5; then consider u such that A1: x = v + u & u in W; take u; thus thesis by A1; end; given u such that A2: u in W & x = v + u; x in {v + v1 : v1 in W} by A2; hence thesis by Def5; end; theorem Th58: 0.V in v + W iff v in W proof set A = {v + u : 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 Def5; then consider u such that A1: 0.V = v + u and A2: u in W; v = - u by A1,VECTSP_1:63; hence thesis by A2,Th30; end; assume v in W; then A3: - v in W by Th30; 0.V = v + (- v) by VECTSP_1:66; then 0.V in A by A3; hence thesis by Def5; end; theorem Th59: v in v + W proof v + 0.V = v & 0.V in W by Th25,VECTSP_1:7; then v in {v + u : u in W}; hence thesis by Def5; end; theorem 0.V + W = the carrier of W by Lm2; theorem Th61: v + (0).V = {v} proof set A = {v + u : 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 Def5; then consider u 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,Def3,RLVECT_1:def 1; then u = 0.V by TARSKI:def 1; then x = v by A1,VECTSP_1:7; 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 Th25,VECTSP_1:7; then x in A by A3; hence thesis by Def5; end; Lm3: v in W iff v + W = the carrier of W proof set A = {v + u : 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 Def5; then consider u such that A2: x = v + u and A3: u in W; v + u in W by A1,A3,Th28; 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 Th18; A4: y - z in W by RLVECT_1:def 1; A5: z + (y - z) = z + (y + (- z)) by RLVECT_1:def 11 .= y + (z + (- z)) by RLVECT_1:def 6 .= y + 0.W by VECTSP_1:66 .= x by VECTSP_1:7; A6: y - z = y1 - z1 by Th24; A7: y1 - z1 in W by A4,Th24; z1 + (y1 - z1) = x by A5,A6,Th21; then x in A by A7; hence thesis by Def5; end; assume A8: v + W = the carrier of W; assume A9: not v in W; 0.V in W & v + 0.V = v by Th25,VECTSP_1:7; then v in {v + u : u in W}; then v in the carrier of W by A8,Def5; hence thesis by A9,RLVECT_1:def 1; end; theorem Th62: v + (Omega).V = the carrier of V proof A1: the carrier of the RightModStr of V = the carrier of V; (Omega).V = the RightModStr of V by Def4; then v in (Omega).V by RLVECT_1:3; then v + (Omega).V = the carrier of (Omega).V by Lm3; hence thesis by A1,Def4; end; theorem Th63: 0.V in v + W iff v + W = the carrier of W proof (0.V in v + W iff v in W) & (v in W iff v + W = the carrier of W) by Lm3,Th58; hence thesis; end; theorem v in W iff v + W = the carrier of W by Lm3; theorem v in W implies (v * a) + W = the carrier of W proof set A = {v * a + u : u in W}; assume A1: v in W; thus (v * a) + W c= the carrier of W proof let x be set; assume x in (v * a) + W; then x in A by Def5; then consider u such that A2: x = v * a + u and A3: u in W; v * a in W by A1,Th29; then v * a + u in W by A3,Th28; 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 Def2,RLVECT_1:3; then reconsider y = x as Element of V by A4; v * a in W & x in W by A1,A4,Th29,RLVECT_1:def 1; then A5: y - v * a in W by Th31; v * a + (y - v * a) = v * a + (y + - (v * a)) by RLVECT_1:def 11 .= y + (v * a + - (v * a)) by RLVECT_1:def 6 .= y + 0.V by VECTSP_1:66 .= x by VECTSP_1:7; then x in A by A5; hence thesis by Def5; end; theorem Th66: u in W iff v + W = (v + u) + W proof set A = {v + v1 : v1 in W}; set B = {(v + u) + v2 : 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 Def5; then consider v1 such that A2: x = v + v1 and A3: v1 in W; A4: v1 - u in W by A1,A3,Th31; (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 VECTSP_1:66 .= x by A2,VECTSP_1:7; then x in B by A4; hence thesis by Def5; end; let x be set; assume x in (v + u) + W; then x in B by Def5; then consider v2 such that A5: x = (v + u) + v2 and A6: v2 in W; A7: u + v2 in W by A1,A6,Th28; x = v + (u + v2) by A5,RLVECT_1:def 6; then x in A by A7; hence thesis by Def5; end; assume A8: v + W = (v + u) + W; 0.V in W & v + 0.V = v by Th25,VECTSP_1:7; then v in A; then v in (v + u) + W by A8,Def5; then v in B by Def5; then consider u1 such that A9: v = (v + u) + u1 and A10: u1 in W; v = v + 0.V & v = v + (u + u1) by A9,VECTSP_1:7; then u + u1 = 0.V by RLVECT_1:22; then u = - u1 by VECTSP_1:63; hence thesis by A10,Th30; end; theorem u in W iff v + W = (v - u) + W proof A1: (- u in W iff v + W = (v + (- u)) + W) & v + (- u) = v - u by Th66,RLVECT_1:def 11; - u in W implies u in W proof assume - u in W; then - (- u) in W by Th30; hence thesis by RLVECT_1:30; end; hence thesis by A1,Th30; end; theorem Th68: v in u + W iff u + W = v + W proof set A = {u + v1 : v1 in W}; set B = {v + v2 : v2 in W}; thus v in u + W implies u + W = v + W proof assume v in u + W; then v in A by Def5; 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 Def5; then consider v1 such that A3: x = u + v1 and A4: v1 in W; A5: v1 - z in W by A2,A4,Th31; v - z = u + (z - z) by A1,RLVECT_1:42 .= u + 0.V by VECTSP_1:66 .= u by VECTSP_1:7; 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 Def5; end; let x be set; assume x in v + W; then x in B by Def5; then consider v2 such that A6: x = v + v2 and A7: v2 in W; A8: z + v2 in W by A2,A7,Th28; x = u + (z + v2) by A1,A6,RLVECT_1:def 6; then x in A by A8; hence thesis by Def5; end; thus thesis by Th59; end; theorem Th69: u in v1 + W & u in v2 + W implies v1 + W = v2 + W proof assume that A1: u in v1 + W and A2: u in v2 + W; set A = {v1 + u1 : u1 in W}; set B = {v2 + u2 : u2 in W}; u in A by A1,Def5; then consider x1 being Vector of V such that A3: u = v1 + x1 and A4: x1 in W; u in B by A2,Def5; 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 Def5; then consider u1 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 VECTSP_1:66 .= v1 by VECTSP_1:7; 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,Th31; then (x2 - x1) + u1 in W by A8,Th28; then x in B by A9; hence thesis by Def5; end; let x be set; assume x in v2 + W; then x in B by Def5; then consider u1 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 VECTSP_1:66 .= v2 by VECTSP_1:7; 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,Th31; then (x1 - x2) + u1 in W by A11,Th28; then x in A by A12; hence thesis by Def5; end; theorem Th70: v in W implies v * a in v + W proof assume A1: v in W; A2: v * a = v * (a - 0.R) by RLVECT_1:26 .= v * (a - (1_ R - 1_ R)) by RLVECT_1:28 .= v * ((a - 1_ R) + 1_ R) by RLVECT_1:43 .= v * (a - 1_ R) + v * 1_ R by VECTSP_2:def 23 .= v + v * (a - 1_ R) by VECTSP_2:def 23; v * (a - 1_ R) in W by A1,Th29; then v * a in {v + u : u in W} by A2; hence thesis by Def5; end; theorem v in W implies - v in v + W proof assume v in W; then v * (- 1_ R) in v + W by Th70; hence thesis by MOD_1:37; end; theorem Th72: u + v in v + W iff u in W proof set A = {v + v1 : 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 Def5; then consider v1 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 Def5; end; theorem v - u in v + W iff u in W proof A1: v - u = (- u) + v by RLVECT_1:def 11; A2: u in W implies - u in W by Th30; - u in W implies - (- u) in W by Th30; hence thesis by A1,A2,Th72,RLVECT_1:30; end; canceled; theorem u in v + W iff (ex v1 st v1 in W & u = v - v1) proof set A = {v + v2 : v2 in W}; thus u in v + W implies (ex v1 st v1 in W & u = v - v1) proof assume u in v + W; then u in A by Def5; then consider v1 such that A1: u = v + v1 and A2: v1 in W; take x = - v1; thus x in W by A2,Th30; u = v + (- (- v1)) by A1,RLVECT_1:30 .= v - (- v1) by RLVECT_1:def 11; hence thesis; end; given v1 such that A3: v1 in W & u = v - v1; u = v + (- v1) & - v1 in W by A3,Th30,RLVECT_1:def 11; then u in A; hence thesis by Def5; end; theorem Th76: (ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W proof thus (ex v st v1 in v + W & v2 in v + W) implies v1 - v2 in W proof given v such that A1: v1 in v + W and A2: v2 in v + W; consider u1 such that A3: u1 in W and A4: v1 = v + u1 by A1,Th57; consider u2 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 VECTSP_1:64 .= ((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 VECTSP_1:7; hence thesis by A3,A5,Th31; end; assume v1 - v2 in W; then A7: - (v1 - v2) in W by Th30; take v1; thus v1 in v1 + W by Th59; v1 + (- (v1 - v2)) = v1 + ((- v1) + v2) by VECTSP_1:64 .= (v1 + (- v1)) + v2 by RLVECT_1:def 6 .= 0.V + v2 by RLVECT_1:16 .= v2 by VECTSP_1:7; hence thesis by A7,Th57; end; theorem Th77: v + W = u + W implies (ex v1 st v1 in W & v + v1 = u) proof assume A1: v + W = u + W; take v1 = u - v; v in u + W by A1,Th59; then v in {u + u2 : u2 in W} by Def5; then consider u1 such that A2: v = u + u1 and A3: u1 in W; 0.V = (u + u1) - v by A2,VECTSP_1:66 .= 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 VECTSP_1:63; hence v1 in W by A3,Th30; thus v + v1 = (u + v) - v by RLVECT_1:42 .= u + (v - v) by RLVECT_1:42 .= u + 0.V by VECTSP_1:66 .= u by VECTSP_1:7; end; theorem Th78: v + W = u + W implies (ex v1 st v1 in W & v - v1 = u) proof assume A1: v + W = u + W; take v1 = v - u; u in v + W by A1,Th59; then u in {v + u2 : u2 in W} by Def5; then consider u1 such that A2: u = v + u1 and A3: u1 in W; 0.V = (v + u1) - u by A2,VECTSP_1:66 .= 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 VECTSP_1:63; hence v1 in W by A3,Th30; thus v - v1 = (v - v) + u by RLVECT_1:43 .= 0.V + u by VECTSP_1:66 .= u by VECTSP_1:7; end; theorem Th79: for W1,W2 being strict Submodule of V holds v + W1 = v + W2 iff W1 = W2 proof let W1,W2 be strict Submodule 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 Def2; A3: the carrier of W2 c= the carrier of V by Def2; 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 : u in W1}; then z in v + W2 by A1,Def5; then z in {v + u : u in W2} by Def5; then consider u 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 : u in W2}; then z in v + W1 by A1,Def5; then z in {v + u : u in W1} by Def5; then consider u 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 Th37; end; thus thesis; end; theorem Th80: for W1,W2 being strict Submodule of V holds v + W1 = u + W2 implies W1 = W2 proof let W1,W2 be strict Submodule 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 Th37; 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 Th17; then reconsider x as Element of V by RLVECT_1:def 1; set z = v + x; z in {v + u2 : u2 in W1} by A6; then z in u + W2 by A1,Def5; then z in {u + u2 : u2 in W2} by Def5; then consider u1 such that A7: z = u + u1 and A8: u1 in W2; x = 0.V + x by VECTSP_1:7 .= (v + (- v)) + x by VECTSP_1:66 .= - v + (u + u1) by A7,RLVECT_1:def 6; then A9: (v + (- v + (u + u1))) + W1 = v + W1 by A6,Th66; v + (- v + (u + u1)) = (v + (- v)) + (u + u1) by RLVECT_1:def 6 .= 0.V + (u + u1) by VECTSP_1:66 .= u + u1 by VECTSP_1:7; then (u + u1) + W2 = (u + u1) + W1 by A1,A8,A9,Th66; hence thesis by A2,Th79; 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 Th17; then reconsider x as Element of V by RLVECT_1:def 1; set z = u + x; z in {u + u2 : u2 in W2} by A11; then z in v + W1 by A1,Def5; then z in {v + u2 : u2 in W1} by Def5; then consider u1 such that A12: z = v + u1 and A13: u1 in W1; x = 0.V + x by VECTSP_1:7 .= (u + (- u)) + x by VECTSP_1:66 .= - u + (v + u1) by A12,RLVECT_1:def 6; then A14: (u + (- u + (v + u1))) + W2 = u + W2 by A11,Th66; u + (- u + (v + u1)) = (u + (- u)) + (v + u1) by RLVECT_1:def 6 .= 0.V + (v + u1) by VECTSP_1:66 .= v + u1 by VECTSP_1:7; then (v + u1) + W1 = (v + u1) + W2 by A1,A13,A14,Th66; hence thesis by A2,Th79; end; hence thesis by A3,A4,XBOOLE_1:37; end; theorem ex C st v in C proof reconsider C = v + W as Coset of W by Def6; take C; thus thesis by Th59; end; theorem C is lineary-closed iff C = the carrier of W proof thus C is lineary-closed implies C = the carrier of W proof assume A1: C is lineary-closed; consider v such that A2: C = v + W by Def6; C <> {} by A2,Th59; then 0.V in v + W by A1,A2,Th4; hence thesis by A2,Th63; end; thus thesis by Lm1; end; theorem for W1,W2 being strict Submodule of V for C1 being Coset of W1, C2 being Coset of W2 holds C1 = C2 implies W1 = W2 proof let W1,W2 be strict Submodule of V; let C1 be Coset of W1, C2 be Coset of W2; A1: ex v1 being Vector of V st C1 = v1 + W1 by Def6; ex v2 being Vector of V st C2 = v2 + W2 by Def6; hence thesis by A1,Th80; end; theorem {v} is Coset of (0).V proof v + (0).V = {v} by Th61; hence thesis by Def6; end; theorem V1 is Coset of (0).V implies (ex v st V1 = {v}) proof assume V1 is Coset of (0).V; then consider v such that A1: V1 = v + (0).V by Def6; take v; thus thesis by A1,Th61; end; theorem the carrier of W is Coset of W proof the carrier of W = 0.V + W by Lm2; hence thesis by Def6; end; theorem the carrier of V is Coset of (Omega).V proof the carrier of V c= the carrier of V; then reconsider A = the carrier of V as Subset of V; consider v; A = v + (Omega).V by Th62; hence thesis by Def6; end; theorem V1 is Coset of (Omega).V implies V1 = the carrier of V proof assume V1 is Coset of (Omega).V; then ex v st V1 = v + (Omega).V by Def6; hence thesis by Th62; end; theorem 0.V in C iff C = the carrier of W proof ex v st C = v + W by Def6; hence thesis by Th63; end; theorem Th90: u in C iff C = u + W proof thus u in C implies C = u + W proof assume A1: u in C; ex v st C = v + W by Def6; hence thesis by A1,Th68; end; thus thesis by Th59; end; theorem u in C & v in C implies (ex v1 st v1 in W & u + v1 = v) proof assume u in C & v in C; then C = u + W & C = v + W by Th90; hence thesis by Th77; end; theorem u in C & v in C implies (ex v1 st v1 in W & u - v1 = v) proof assume u in C & v in C; then C = u + W & C = v + W by Th90; hence thesis by Th78; end; theorem (ex C st v1 in C & v2 in C) iff v1 - v2 in W proof thus (ex C st v1 in C & v2 in C) implies v1 - v2 in W proof given C such that A1: v1 in C & v2 in C; ex v st C = v + W by Def6; hence thesis by A1,Th76; end; assume v1 - v2 in W; then consider v such that A2: v1 in v + W & v2 in v + W by Th76; reconsider C = v + W as Coset of W by Def6; take C; thus thesis by A2; end; theorem u in B & u in C implies B = C proof assume A1: u in B & u in C; A2: ex v1 st B = v1 + W by Def6; ex v2 st C = v2 + W by Def6; hence thesis by A1,A2,Th69; end;

Back to top