:: RMOD_4 semantic presentation begin Lm1: for R being Ring for V being RightMod of R for v being Vector of V for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds Sum F = (Sum G) + v proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds Sum F = (Sum G) + v let V be RightMod of R; ::_thesis: for v being Vector of V for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds Sum F = (Sum G) + v let v be Vector of V; ::_thesis: for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds Sum F = (Sum G) + v let F, G be FinSequence of V; ::_thesis: ( len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) implies Sum F = (Sum G) + v ) ( len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) implies Sum F = (Sum G) + v ) by RLVECT_1:38; hence ( len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) implies Sum F = (Sum G) + v ) by FINSEQ_1:def_3; ::_thesis: verum end; theorem Th1: :: RMOD_4:1 for R being Ring for V being RightMod of R for a being Scalar of R for F, G being FinSequence of V st len F = len G & ( for k being Nat for v being Vector of V st k in dom F & v = G . k holds F . k = v * a ) holds Sum F = (Sum G) * a proof let R be Ring; ::_thesis: for V being RightMod of R for a being Scalar of R for F, G being FinSequence of V st len F = len G & ( for k being Nat for v being Vector of V st k in dom F & v = G . k holds F . k = v * a ) holds Sum F = (Sum G) * a let V be RightMod of R; ::_thesis: for a being Scalar of R for F, G being FinSequence of V st len F = len G & ( for k being Nat for v being Vector of V st k in dom F & v = G . k holds F . k = v * a ) holds Sum F = (Sum G) * a let a be Scalar of R; ::_thesis: for F, G being FinSequence of V st len F = len G & ( for k being Nat for v being Vector of V st k in dom F & v = G . k holds F . k = v * a ) holds Sum F = (Sum G) * a let F, G be FinSequence of V; ::_thesis: ( len F = len G & ( for k being Nat for v being Vector of V st k in dom F & v = G . k holds F . k = v * a ) implies Sum F = (Sum G) * a ) defpred S1[ Nat] means for H, I being FinSequence of V st len H = len I & len H = $1 & ( for k being Nat for v being Vector of V st k in dom H & v = I . k holds H . k = v * a ) holds Sum H = (Sum I) * a; now__::_thesis:_for_n_being_Element_of_NAT_st_(_for_H,_I_being_FinSequence_of_V_st_len_H_=_len_I_&_len_H_=_n_&_(_for_k_being_Nat for_v_being_Vector_of_V_st_k_in_dom_H_&_v_=_I_._k_holds_ H_._k_=_v_*_a_)_holds_ Sum_H_=_(Sum_I)_*_a_)_holds_ for_H,_I_being_FinSequence_of_V_st_len_H_=_len_I_&_len_H_=_n_+_1_&_(_for_k_being_Nat for_v_being_Vector_of_V_st_k_in_dom_H_&_v_=_I_._k_holds_ H_._k_=_v_*_a_)_holds_ Sum_H_=_(Sum_I)_*_a let n be Element of NAT ; ::_thesis: ( ( for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Nat for v being Vector of V st k in dom H & v = I . k holds H . k = v * a ) holds Sum H = (Sum I) * a ) implies for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Nat for v being Vector of V st k in dom H & v = I . k holds H . k = v * a ) holds Sum H = (Sum I) * a ) assume A1: for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Nat for v being Vector of V st k in dom H & v = I . k holds H . k = v * a ) holds Sum H = (Sum I) * a ; ::_thesis: for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Nat for v being Vector of V st k in dom H & v = I . k holds H . k = v * a ) holds Sum H = (Sum I) * a let H, I be FinSequence of V; ::_thesis: ( len H = len I & len H = n + 1 & ( for k being Nat for v being Vector of V st k in dom H & v = I . k holds H . k = v * a ) implies Sum H = (Sum I) * a ) assume that A2: len H = len I and A3: len H = n + 1 and A4: for k being Nat for v being Vector of V st k in dom H & v = I . k holds H . k = v * a ; ::_thesis: Sum H = (Sum I) * a reconsider p = H | (Seg n), q = I | (Seg n) as FinSequence of V by FINSEQ_1:18; A5: n <= n + 1 by NAT_1:12; then A6: len p = n by A3, FINSEQ_1:17; A7: len q = n by A2, A3, A5, FINSEQ_1:17; A8: now__::_thesis:_for_k_being_Nat for_v_being_Vector_of_V_st_k_in_dom_p_&_v_=_q_._k_holds_ p_._k_=_v_*_a len p <= len H by A3, A5, FINSEQ_1:17; then A9: dom p c= dom H by FINSEQ_3:30; let k be Nat; ::_thesis: for v being Vector of V st k in dom p & v = q . k holds p . k = v * a let v be Vector of V; ::_thesis: ( k in dom p & v = q . k implies p . k = v * a ) assume that A10: k in dom p and A11: v = q . k ; ::_thesis: p . k = v * a dom p = dom q by A6, A7, FINSEQ_3:29; then I . k = q . k by A10, FUNCT_1:47; then H . k = v * a by A4, A10, A11, A9; hence p . k = v * a by A10, FUNCT_1:47; ::_thesis: verum end; A12: n + 1 in Seg (n + 1) by FINSEQ_1:4; then ( n + 1 in dom H & n + 1 in dom I ) by A2, A3, FINSEQ_1:def_3; then reconsider v1 = H . (n + 1), v2 = I . (n + 1) as Vector of V by FINSEQ_2:11; n + 1 in dom H by A3, A12, FINSEQ_1:def_3; then A13: v1 = v2 * a by A4; thus Sum H = (Sum p) + v1 by A3, A6, Lm1 .= ((Sum q) * a) + (v2 * a) by A1, A6, A7, A8, A13 .= ((Sum q) + v2) * a by VECTSP_2:def_9 .= (Sum I) * a by A2, A3, A7, Lm1 ; ::_thesis: verum end; then A14: for i being Element of NAT st S1[i] holds S1[i + 1] ; now__::_thesis:_for_H,_I_being_FinSequence_of_V_st_len_H_=_len_I_&_len_H_=_0_&_(_for_k_being_Nat for_v_being_Vector_of_V_st_k_in_dom_H_&_v_=_I_._k_holds_ H_._k_=_v_*_a_)_holds_ Sum_H_=_(Sum_I)_*_a let H, I be FinSequence of V; ::_thesis: ( len H = len I & len H = 0 & ( for k being Nat for v being Vector of V st k in dom H & v = I . k holds H . k = v * a ) implies Sum H = (Sum I) * a ) assume that A15: len H = len I and A16: len H = 0 and for k being Nat for v being Vector of V st k in dom H & v = I . k holds H . k = v * a ; ::_thesis: Sum H = (Sum I) * a H = <*> the carrier of V by A16; then A17: Sum H = 0. V by RLVECT_1:43; I = <*> the carrier of V by A15, A16; then Sum I = 0. V by RLVECT_1:43; hence Sum H = (Sum I) * a by A17, VECTSP_2:32; ::_thesis: verum end; then A18: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A18, A14); hence ( len F = len G & ( for k being Nat for v being Vector of V st k in dom F & v = G . k holds F . k = v * a ) implies Sum F = (Sum G) * a ) ; ::_thesis: verum end; Lm2: for R being Ring for V being RightMod of R for a being Scalar of R for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds G . k = (F /. k) * a ) holds Sum G = (Sum F) * a proof let R be Ring; ::_thesis: for V being RightMod of R for a being Scalar of R for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds G . k = (F /. k) * a ) holds Sum G = (Sum F) * a let V be RightMod of R; ::_thesis: for a being Scalar of R for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds G . k = (F /. k) * a ) holds Sum G = (Sum F) * a let a be Scalar of R; ::_thesis: for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds G . k = (F /. k) * a ) holds Sum G = (Sum F) * a let F, G be FinSequence of V; ::_thesis: ( len F = len G & ( for k being Nat st k in dom F holds G . k = (F /. k) * a ) implies Sum G = (Sum F) * a ) assume that A1: len F = len G and A2: for k being Nat st k in dom F holds G . k = (F /. k) * a ; ::_thesis: Sum G = (Sum F) * a now__::_thesis:_for_k_being_Nat for_v_being_Vector_of_V_st_k_in_dom_G_&_v_=_F_._k_holds_ G_._k_=_v_*_a let k be Nat; ::_thesis: for v being Vector of V st k in dom G & v = F . k holds G . k = v * a let v be Vector of V; ::_thesis: ( k in dom G & v = F . k implies G . k = v * a ) assume that A3: k in dom G and A4: v = F . k ; ::_thesis: G . k = v * a A5: k in dom F by A1, A3, FINSEQ_3:29; then v = F /. k by A4, PARTFUN1:def_6; hence G . k = v * a by A2, A5; ::_thesis: verum end; hence Sum G = (Sum F) * a by A1, Th1; ::_thesis: verum end; theorem :: RMOD_4:2 for R being Ring for V being RightMod of R for a being Scalar of R holds (Sum (<*> the carrier of V)) * a = 0. V proof let R be Ring; ::_thesis: for V being RightMod of R for a being Scalar of R holds (Sum (<*> the carrier of V)) * a = 0. V let V be RightMod of R; ::_thesis: for a being Scalar of R holds (Sum (<*> the carrier of V)) * a = 0. V let a be Scalar of R; ::_thesis: (Sum (<*> the carrier of V)) * a = 0. V thus (Sum (<*> the carrier of V)) * a = (0. V) * a by RLVECT_1:43 .= 0. V by VECTSP_2:32 ; ::_thesis: verum end; theorem :: RMOD_4:3 for R being Ring for V being RightMod of R for a being Scalar of R for v, u being Vector of V holds (Sum <*v,u*>) * a = (v * a) + (u * a) proof let R be Ring; ::_thesis: for V being RightMod of R for a being Scalar of R for v, u being Vector of V holds (Sum <*v,u*>) * a = (v * a) + (u * a) let V be RightMod of R; ::_thesis: for a being Scalar of R for v, u being Vector of V holds (Sum <*v,u*>) * a = (v * a) + (u * a) let a be Scalar of R; ::_thesis: for v, u being Vector of V holds (Sum <*v,u*>) * a = (v * a) + (u * a) let v, u be Vector of V; ::_thesis: (Sum <*v,u*>) * a = (v * a) + (u * a) thus (Sum <*v,u*>) * a = (v + u) * a by RLVECT_1:45 .= (v * a) + (u * a) by VECTSP_2:def_9 ; ::_thesis: verum end; theorem :: RMOD_4:4 for R being Ring for V being RightMod of R for a being Scalar of R for v, u, w being Vector of V holds (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a) proof let R be Ring; ::_thesis: for V being RightMod of R for a being Scalar of R for v, u, w being Vector of V holds (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a) let V be RightMod of R; ::_thesis: for a being Scalar of R for v, u, w being Vector of V holds (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a) let a be Scalar of R; ::_thesis: for v, u, w being Vector of V holds (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a) let v, u, w be Vector of V; ::_thesis: (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a) thus (Sum <*v,u,w*>) * a = ((v + u) + w) * a by RLVECT_1:46 .= ((v + u) * a) + (w * a) by VECTSP_2:def_9 .= ((v * a) + (u * a)) + (w * a) by VECTSP_2:def_9 ; ::_thesis: verum end; definition let R be Ring; let V be RightMod of R; let T be finite Subset of V; func Sum T -> Vector of V means :Def1: :: RMOD_4:def 1 ex F being FinSequence of V st ( rng F = T & F is one-to-one & it = Sum F ); existence ex b1 being Vector of V ex F being FinSequence of V st ( rng F = T & F is one-to-one & b1 = Sum F ) proof consider p being FinSequence such that A1: rng p = T and A2: p is one-to-one by FINSEQ_4:58; reconsider p = p as FinSequence of V by A1, FINSEQ_1:def_4; take Sum p ; ::_thesis: ex F being FinSequence of V st ( rng F = T & F is one-to-one & Sum p = Sum F ) take p ; ::_thesis: ( rng p = T & p is one-to-one & Sum p = Sum p ) thus ( rng p = T & p is one-to-one & Sum p = Sum p ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being Vector of V st ex F being FinSequence of V st ( rng F = T & F is one-to-one & b1 = Sum F ) & ex F being FinSequence of V st ( rng F = T & F is one-to-one & b2 = Sum F ) holds b1 = b2 by RLVECT_1:42; end; :: deftheorem Def1 defines Sum RMOD_4:def_1_:_ for R being Ring for V being RightMod of R for T being finite Subset of V for b4 being Vector of V holds ( b4 = Sum T iff ex F being FinSequence of V st ( rng F = T & F is one-to-one & b4 = Sum F ) ); theorem Th5: :: RMOD_4:5 for R being Ring for V being RightMod of R holds Sum ({} V) = 0. V proof let R be Ring; ::_thesis: for V being RightMod of R holds Sum ({} V) = 0. V let V be RightMod of R; ::_thesis: Sum ({} V) = 0. V Sum (<*> the carrier of V) = 0. V by RLVECT_1:43; hence Sum ({} V) = 0. V by Def1, RELAT_1:38; ::_thesis: verum end; theorem :: RMOD_4:6 for R being Ring for V being RightMod of R for v being Vector of V holds Sum {v} = v proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V holds Sum {v} = v let V be RightMod of R; ::_thesis: for v being Vector of V holds Sum {v} = v let v be Vector of V; ::_thesis: Sum {v} = v A1: Sum <*v*> = v by RLVECT_1:44; ( rng <*v*> = {v} & <*v*> is one-to-one ) by FINSEQ_1:39, FINSEQ_3:93; hence Sum {v} = v by A1, Def1; ::_thesis: verum end; theorem :: RMOD_4:7 for R being Ring for V being RightMod of R for v1, v2 being Vector of V st v1 <> v2 holds Sum {v1,v2} = v1 + v2 proof let R be Ring; ::_thesis: for V being RightMod of R for v1, v2 being Vector of V st v1 <> v2 holds Sum {v1,v2} = v1 + v2 let V be RightMod of R; ::_thesis: for v1, v2 being Vector of V st v1 <> v2 holds Sum {v1,v2} = v1 + v2 let v1, v2 be Vector of V; ::_thesis: ( v1 <> v2 implies Sum {v1,v2} = v1 + v2 ) assume v1 <> v2 ; ::_thesis: Sum {v1,v2} = v1 + v2 then A1: <*v1,v2*> is one-to-one by FINSEQ_3:94; ( rng <*v1,v2*> = {v1,v2} & Sum <*v1,v2*> = v1 + v2 ) by FINSEQ_2:127, RLVECT_1:45; hence Sum {v1,v2} = v1 + v2 by A1, Def1; ::_thesis: verum end; theorem :: RMOD_4:8 for R being Ring for V being RightMod of R for v1, v2, v3 being Vector of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds Sum {v1,v2,v3} = (v1 + v2) + v3 proof let R be Ring; ::_thesis: for V being RightMod of R for v1, v2, v3 being Vector of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds Sum {v1,v2,v3} = (v1 + v2) + v3 let V be RightMod of R; ::_thesis: for v1, v2, v3 being Vector of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds Sum {v1,v2,v3} = (v1 + v2) + v3 let v1, v2, v3 be Vector of V; ::_thesis: ( v1 <> v2 & v2 <> v3 & v1 <> v3 implies Sum {v1,v2,v3} = (v1 + v2) + v3 ) assume ( v1 <> v2 & v2 <> v3 & v1 <> v3 ) ; ::_thesis: Sum {v1,v2,v3} = (v1 + v2) + v3 then A1: <*v1,v2,v3*> is one-to-one by FINSEQ_3:95; ( rng <*v1,v2,v3*> = {v1,v2,v3} & Sum <*v1,v2,v3*> = (v1 + v2) + v3 ) by FINSEQ_2:128, RLVECT_1:46; hence Sum {v1,v2,v3} = (v1 + v2) + v3 by A1, Def1; ::_thesis: verum end; theorem Th9: :: RMOD_4:9 for R being Ring for V being RightMod of R for T, S being finite Subset of V st T misses S holds Sum (T \/ S) = (Sum T) + (Sum S) proof let R be Ring; ::_thesis: for V being RightMod of R for T, S being finite Subset of V st T misses S holds Sum (T \/ S) = (Sum T) + (Sum S) let V be RightMod of R; ::_thesis: for T, S being finite Subset of V st T misses S holds Sum (T \/ S) = (Sum T) + (Sum S) let T, S be finite Subset of V; ::_thesis: ( T misses S implies Sum (T \/ S) = (Sum T) + (Sum S) ) consider F being FinSequence of V such that A1: rng F = T \/ S and A2: ( F is one-to-one & Sum (T \/ S) = Sum F ) by Def1; consider G being FinSequence of V such that A3: rng G = T and A4: G is one-to-one and A5: Sum T = Sum G by Def1; consider H being FinSequence of V such that A6: rng H = S and A7: H is one-to-one and A8: Sum S = Sum H by Def1; set I = G ^ H; assume T misses S ; ::_thesis: Sum (T \/ S) = (Sum T) + (Sum S) then A9: G ^ H is one-to-one by A3, A4, A6, A7, FINSEQ_3:91; rng (G ^ H) = rng F by A1, A3, A6, FINSEQ_1:31; hence Sum (T \/ S) = Sum (G ^ H) by A2, A9, RLVECT_1:42 .= (Sum T) + (Sum S) by A5, A8, RLVECT_1:41 ; ::_thesis: verum end; theorem Th10: :: RMOD_4:10 for R being Ring for V being RightMod of R for T, S being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) proof let R be Ring; ::_thesis: for V being RightMod of R for T, S being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) let V be RightMod of R; ::_thesis: for T, S being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) let T, S be finite Subset of V; ::_thesis: Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) set A = S \ T; set B = T \ S; set Z = (S \ T) \/ (T \ S); set I = T /\ S; A1: (S \ T) \/ (T /\ S) = S by XBOOLE_1:51; A2: (T \ S) \/ (T /\ S) = T by XBOOLE_1:51; A3: (S \ T) \/ (T \ S) = T \+\ S ; then ((S \ T) \/ (T \ S)) \/ (T /\ S) = T \/ S by XBOOLE_1:93; then (Sum (T \/ S)) + (Sum (T /\ S)) = ((Sum ((S \ T) \/ (T \ S))) + (Sum (T /\ S))) + (Sum (T /\ S)) by A3, Th9, XBOOLE_1:103 .= (((Sum (S \ T)) + (Sum (T \ S))) + (Sum (T /\ S))) + (Sum (T /\ S)) by Th9, XBOOLE_1:82 .= ((Sum (S \ T)) + ((Sum (T /\ S)) + (Sum (T \ S)))) + (Sum (T /\ S)) by RLVECT_1:def_3 .= ((Sum (S \ T)) + (Sum (T /\ S))) + ((Sum (T \ S)) + (Sum (T /\ S))) by RLVECT_1:def_3 .= (Sum S) + ((Sum (T \ S)) + (Sum (T /\ S))) by A1, Th9, XBOOLE_1:89 .= (Sum T) + (Sum S) by A2, Th9, XBOOLE_1:89 ; hence Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) by RLSUB_2:61; ::_thesis: verum end; theorem :: RMOD_4:11 for R being Ring for V being RightMod of R for T, S being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S)) proof let R be Ring; ::_thesis: for V being RightMod of R for T, S being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S)) let V be RightMod of R; ::_thesis: for T, S being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S)) let T, S be finite Subset of V; ::_thesis: Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S)) Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) by Th10; then (Sum T) + (Sum S) = (Sum (T /\ S)) + (Sum (T \/ S)) by RLSUB_2:61; hence Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S)) by RLSUB_2:61; ::_thesis: verum end; theorem Th12: :: RMOD_4:12 for R being Ring for V being RightMod of R for T, S being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S) proof let R be Ring; ::_thesis: for V being RightMod of R for T, S being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S) let V be RightMod of R; ::_thesis: for T, S being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S) let T, S be finite Subset of V; ::_thesis: Sum (T \ S) = (Sum (T \/ S)) - (Sum S) T \ S misses S by XBOOLE_1:79; then A1: (T \ S) /\ S = {} V by XBOOLE_0:def_7; (T \ S) \/ S = T \/ S by XBOOLE_1:39; then Sum (T \/ S) = ((Sum (T \ S)) + (Sum S)) - (Sum ((T \ S) /\ S)) by Th10; then Sum (T \/ S) = ((Sum (T \ S)) + (Sum S)) - (0. V) by A1, Th5 .= (Sum (T \ S)) + (Sum S) by VECTSP_1:18 ; hence Sum (T \ S) = (Sum (T \/ S)) - (Sum S) by RLSUB_2:61; ::_thesis: verum end; theorem Th13: :: RMOD_4:13 for R being Ring for V being RightMod of R for T, S being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S)) proof let R be Ring; ::_thesis: for V being RightMod of R for T, S being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S)) let V be RightMod of R; ::_thesis: for T, S being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S)) let T, S be finite Subset of V; ::_thesis: Sum (T \ S) = (Sum T) - (Sum (T /\ S)) T \ (T /\ S) = T \ S by XBOOLE_1:47; then Sum (T \ S) = (Sum (T \/ (T /\ S))) - (Sum (T /\ S)) by Th12; hence Sum (T \ S) = (Sum T) - (Sum (T /\ S)) by XBOOLE_1:22; ::_thesis: verum end; theorem :: RMOD_4:14 for R being Ring for V being RightMod of R for T, S being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S)) proof let R be Ring; ::_thesis: for V being RightMod of R for T, S being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S)) let V be RightMod of R; ::_thesis: for T, S being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S)) let T, S be finite Subset of V; ::_thesis: Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S)) T \+\ S = (T \/ S) \ (T /\ S) by XBOOLE_1:101; hence Sum (T \+\ S) = (Sum (T \/ S)) - (Sum ((T \/ S) /\ (T /\ S))) by Th13 .= (Sum (T \/ S)) - (Sum (((T \/ S) /\ T) /\ S)) by XBOOLE_1:16 .= (Sum (T \/ S)) - (Sum (T /\ S)) by XBOOLE_1:21 ; ::_thesis: verum end; theorem :: RMOD_4:15 for R being Ring for V being RightMod of R for T, S being finite Subset of V holds Sum (T \+\ S) = (Sum (T \ S)) + (Sum (S \ T)) by Th9, XBOOLE_1:82; definition let R be Ring; let V be RightMod of R; mode Linear_Combination of V -> Element of Funcs ( the carrier of V, the carrier of R) means :Def2: :: RMOD_4:def 2 ex T being finite Subset of V st for v being Vector of V st not v in T holds it . v = 0. R; existence ex b1 being Element of Funcs ( the carrier of V, the carrier of R) ex T being finite Subset of V st for v being Vector of V st not v in T holds b1 . v = 0. R proof {} V = {} ; then reconsider P = {} as finite Subset of V ; reconsider f = the carrier of V --> (0. R) as Function of V,R ; reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8; take f ; ::_thesis: ex T being finite Subset of V st for v being Vector of V st not v in T holds f . v = 0. R take P ; ::_thesis: for v being Vector of V st not v in P holds f . v = 0. R thus for v being Vector of V st not v in P holds f . v = 0. R by FUNCOP_1:7; ::_thesis: verum end; end; :: deftheorem Def2 defines Linear_Combination RMOD_4:def_2_:_ for R being Ring for V being RightMod of R for b3 being Element of Funcs ( the carrier of V, the carrier of R) holds ( b3 is Linear_Combination of V iff ex T being finite Subset of V st for v being Vector of V st not v in T holds b3 . v = 0. R ); definition let R be Ring; let V be RightMod of R; let L be Linear_Combination of V; func Carrier L -> finite Subset of V equals :: RMOD_4:def 3 { v where v is Vector of V : L . v <> 0. R } ; coherence { v where v is Vector of V : L . v <> 0. R } is finite Subset of V proof set A = { v where v is Vector of V : L . v <> 0. R } ; consider T being finite Subset of V such that A1: for v being Vector of V st not v in T holds L . v = 0. R by Def2; { v where v is Vector of V : L . v <> 0. R } c= T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Vector of V : L . v <> 0. R } or x in T ) assume x in { v where v is Vector of V : L . v <> 0. R } ; ::_thesis: x in T then ex v being Vector of V st ( x = v & L . v <> 0. R ) ; hence x in T by A1; ::_thesis: verum end; hence { v where v is Vector of V : L . v <> 0. R } is finite Subset of V by XBOOLE_1:1; ::_thesis: verum end; end; :: deftheorem defines Carrier RMOD_4:def_3_:_ for R being Ring for V being RightMod of R for L being Linear_Combination of V holds Carrier L = { v where v is Vector of V : L . v <> 0. R } ; theorem :: RMOD_4:16 for R being Ring for V being RightMod of R for x being set for L being Linear_Combination of V holds ( x in Carrier L iff ex v being Vector of V st ( x = v & L . v <> 0. R ) ) ; theorem :: RMOD_4:17 for R being Ring for V being RightMod of R for v being Vector of V for L being Linear_Combination of V holds ( L . v = 0. R iff not v in Carrier L ) proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for L being Linear_Combination of V holds ( L . v = 0. R iff not v in Carrier L ) let V be RightMod of R; ::_thesis: for v being Vector of V for L being Linear_Combination of V holds ( L . v = 0. R iff not v in Carrier L ) let v be Vector of V; ::_thesis: for L being Linear_Combination of V holds ( L . v = 0. R iff not v in Carrier L ) let L be Linear_Combination of V; ::_thesis: ( L . v = 0. R iff not v in Carrier L ) thus ( L . v = 0. R implies not v in Carrier L ) ::_thesis: ( not v in Carrier L implies L . v = 0. R ) proof assume A1: L . v = 0. R ; ::_thesis: not v in Carrier L assume v in Carrier L ; ::_thesis: contradiction then ex u being Vector of V st ( u = v & L . u <> 0. R ) ; hence contradiction by A1; ::_thesis: verum end; assume not v in Carrier L ; ::_thesis: L . v = 0. R hence L . v = 0. R ; ::_thesis: verum end; definition let R be Ring; let V be RightMod of R; func ZeroLC V -> Linear_Combination of V means :Def4: :: RMOD_4:def 4 Carrier it = {} ; existence ex b1 being Linear_Combination of V st Carrier b1 = {} proof reconsider f = the carrier of V --> (0. R) as Function of V,R ; reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8; f is Linear_Combination of V proof reconsider T = {} V as empty finite Subset of V ; take T ; :: according to RMOD_4:def_2 ::_thesis: for v being Vector of V st not v in T holds f . v = 0. R thus for v being Vector of V st not v in T holds f . v = 0. R by FUNCOP_1:7; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V ; take f ; ::_thesis: Carrier f = {} set C = { v where v is Vector of V : f . v <> 0. R } ; now__::_thesis:_not__{__v_where_v_is_Vector_of_V_:_f_._v_<>_0._R__}__<>_{} set x = the Element of { v where v is Vector of V : f . v <> 0. R } ; assume { v where v is Vector of V : f . v <> 0. R } <> {} ; ::_thesis: contradiction then the Element of { v where v is Vector of V : f . v <> 0. R } in { v where v is Vector of V : f . v <> 0. R } ; then ex v being Vector of V st ( the Element of { v where v is Vector of V : f . v <> 0. R } = v & f . v <> 0. R ) ; hence contradiction by FUNCOP_1:7; ::_thesis: verum end; hence Carrier f = {} ; ::_thesis: verum end; uniqueness for b1, b2 being Linear_Combination of V st Carrier b1 = {} & Carrier b2 = {} holds b1 = b2 proof let L, L9 be Linear_Combination of V; ::_thesis: ( Carrier L = {} & Carrier L9 = {} implies L = L9 ) assume that A1: Carrier L = {} and A2: Carrier L9 = {} ; ::_thesis: L = L9 now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_ L_._x_=_L9_._x let x be set ; ::_thesis: ( x in the carrier of V implies L . x = L9 . x ) assume x in the carrier of V ; ::_thesis: L . x = L9 . x then reconsider v = x as Element of V ; A3: now__::_thesis:_not_L9_._v_<>_0._R assume L9 . v <> 0. R ; ::_thesis: contradiction then v in { u where u is Vector of V : L9 . u <> 0. R } ; hence contradiction by A2; ::_thesis: verum end; now__::_thesis:_not_L_._v_<>_0._R assume L . v <> 0. R ; ::_thesis: contradiction then v in { u where u is Vector of V : L . u <> 0. R } ; hence contradiction by A1; ::_thesis: verum end; hence L . x = L9 . x by A3; ::_thesis: verum end; hence L = L9 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def4 defines ZeroLC RMOD_4:def_4_:_ for R being Ring for V being RightMod of R for b3 being Linear_Combination of V holds ( b3 = ZeroLC V iff Carrier b3 = {} ); theorem Th18: :: RMOD_4:18 for R being Ring for V being RightMod of R for v being Vector of V holds (ZeroLC V) . v = 0. R proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V holds (ZeroLC V) . v = 0. R let V be RightMod of R; ::_thesis: for v being Vector of V holds (ZeroLC V) . v = 0. R let v be Vector of V; ::_thesis: (ZeroLC V) . v = 0. R ( Carrier (ZeroLC V) = {} & not v in {} ) by Def4; hence (ZeroLC V) . v = 0. R ; ::_thesis: verum end; definition let R be Ring; let V be RightMod of R; let A be Subset of V; mode Linear_Combination of A -> Linear_Combination of V means :Def5: :: RMOD_4:def 5 Carrier it c= A; existence ex b1 being Linear_Combination of V st Carrier b1 c= A proof take L = ZeroLC V; ::_thesis: Carrier L c= A Carrier L = {} by Def4; hence Carrier L c= A by XBOOLE_1:2; ::_thesis: verum end; end; :: deftheorem Def5 defines Linear_Combination RMOD_4:def_5_:_ for R being Ring for V being RightMod of R for A being Subset of V for b4 being Linear_Combination of V holds ( b4 is Linear_Combination of A iff Carrier b4 c= A ); theorem Th19: :: RMOD_4:19 for R being Ring for V being RightMod of R for A, B being Subset of V for l being Linear_Combination of A st A c= B holds l is Linear_Combination of B proof let R be Ring; ::_thesis: for V being RightMod of R for A, B being Subset of V for l being Linear_Combination of A st A c= B holds l is Linear_Combination of B let V be RightMod of R; ::_thesis: for A, B being Subset of V for l being Linear_Combination of A st A c= B holds l is Linear_Combination of B let A, B be Subset of V; ::_thesis: for l being Linear_Combination of A st A c= B holds l is Linear_Combination of B let l be Linear_Combination of A; ::_thesis: ( A c= B implies l is Linear_Combination of B ) assume A1: A c= B ; ::_thesis: l is Linear_Combination of B Carrier l c= A by Def5; then Carrier l c= B by A1, XBOOLE_1:1; hence l is Linear_Combination of B by Def5; ::_thesis: verum end; theorem Th20: :: RMOD_4:20 for R being Ring for V being RightMod of R for A being Subset of V holds ZeroLC V is Linear_Combination of A proof let R be Ring; ::_thesis: for V being RightMod of R for A being Subset of V holds ZeroLC V is Linear_Combination of A let V be RightMod of R; ::_thesis: for A being Subset of V holds ZeroLC V is Linear_Combination of A let A be Subset of V; ::_thesis: ZeroLC V is Linear_Combination of A ( Carrier (ZeroLC V) = {} & {} c= A ) by Def4, XBOOLE_1:2; hence ZeroLC V is Linear_Combination of A by Def5; ::_thesis: verum end; theorem Th21: :: RMOD_4:21 for R being Ring for V being RightMod of R for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V proof let R be Ring; ::_thesis: for V being RightMod of R for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V let V be RightMod of R; ::_thesis: for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V let l be Linear_Combination of {} the carrier of V; ::_thesis: l = ZeroLC V Carrier l c= {} by Def5; then Carrier l = {} ; hence l = ZeroLC V by Def4; ::_thesis: verum end; theorem :: RMOD_4:22 for R being Ring for V being RightMod of R for L being Linear_Combination of V holds L is Linear_Combination of Carrier L by Def5; definition let R be Ring; let V be RightMod of R; let F be FinSequence of V; let f be Function of V,R; funcf (#) F -> FinSequence of V means :Def6: :: RMOD_4:def 6 ( len it = len F & ( for i being Nat st i in dom it holds it . i = (F /. i) * (f . (F /. i)) ) ); existence ex b1 being FinSequence of V st ( len b1 = len F & ( for i being Nat st i in dom b1 holds b1 . i = (F /. i) * (f . (F /. i)) ) ) proof deffunc H1( Nat) -> Element of the carrier of V = (F /. $1) * (f . (F /. $1)); consider G being FinSequence such that A1: len G = len F and A2: for n being Nat st n in dom G holds G . n = H1(n) from FINSEQ_1:sch_2(); rng G c= the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng G or x in the carrier of V ) assume x in rng G ; ::_thesis: x in the carrier of V then consider y being set such that A3: y in dom G and A4: G . y = x by FUNCT_1:def_3; y in Seg (len F) by A1, A3, FINSEQ_1:def_3; then reconsider y = y as Element of NAT ; G . y = (F /. y) * (f . (F /. y)) by A2, A3; hence x in the carrier of V by A4; ::_thesis: verum end; then reconsider G = G as FinSequence of V by FINSEQ_1:def_4; take G ; ::_thesis: ( len G = len F & ( for i being Nat st i in dom G holds G . i = (F /. i) * (f . (F /. i)) ) ) thus ( len G = len F & ( for i being Nat st i in dom G holds G . i = (F /. i) * (f . (F /. i)) ) ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of V st len b1 = len F & ( for i being Nat st i in dom b1 holds b1 . i = (F /. i) * (f . (F /. i)) ) & len b2 = len F & ( for i being Nat st i in dom b2 holds b2 . i = (F /. i) * (f . (F /. i)) ) holds b1 = b2 proof let H1, H2 be FinSequence of V; ::_thesis: ( len H1 = len F & ( for i being Nat st i in dom H1 holds H1 . i = (F /. i) * (f . (F /. i)) ) & len H2 = len F & ( for i being Nat st i in dom H2 holds H2 . i = (F /. i) * (f . (F /. i)) ) implies H1 = H2 ) assume that A5: len H1 = len F and A6: for i being Nat st i in dom H1 holds H1 . i = (F /. i) * (f . (F /. i)) and A7: len H2 = len F and A8: for i being Nat st i in dom H2 holds H2 . i = (F /. i) * (f . (F /. i)) ; ::_thesis: H1 = H2 now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_H1_holds_ H1_._k_=_H2_._k let k be Nat; ::_thesis: ( 1 <= k & k <= len H1 implies H1 . k = H2 . k ) assume ( 1 <= k & k <= len H1 ) ; ::_thesis: H1 . k = H2 . k then A9: k in Seg (len H1) by FINSEQ_1:1; then k in dom H1 by FINSEQ_1:def_3; then A10: H1 . k = (F /. k) * (f . (F /. k)) by A6; k in dom H2 by A5, A7, A9, FINSEQ_1:def_3; hence H1 . k = H2 . k by A8, A10; ::_thesis: verum end; hence H1 = H2 by A5, A7, FINSEQ_1:14; ::_thesis: verum end; end; :: deftheorem Def6 defines (#) RMOD_4:def_6_:_ for R being Ring for V being RightMod of R for F being FinSequence of V for f being Function of V,R for b5 being FinSequence of V holds ( b5 = f (#) F iff ( len b5 = len F & ( for i being Nat st i in dom b5 holds b5 . i = (F /. i) * (f . (F /. i)) ) ) ); theorem Th23: :: RMOD_4:23 for R being Ring for V being RightMod of R for i being Nat for v being Vector of V for F being FinSequence of V for f being Function of V,R st i in dom F & v = F . i holds (f (#) F) . i = v * (f . v) proof let R be Ring; ::_thesis: for V being RightMod of R for i being Nat for v being Vector of V for F being FinSequence of V for f being Function of V,R st i in dom F & v = F . i holds (f (#) F) . i = v * (f . v) let V be RightMod of R; ::_thesis: for i being Nat for v being Vector of V for F being FinSequence of V for f being Function of V,R st i in dom F & v = F . i holds (f (#) F) . i = v * (f . v) let i be Nat; ::_thesis: for v being Vector of V for F being FinSequence of V for f being Function of V,R st i in dom F & v = F . i holds (f (#) F) . i = v * (f . v) let v be Vector of V; ::_thesis: for F being FinSequence of V for f being Function of V,R st i in dom F & v = F . i holds (f (#) F) . i = v * (f . v) let F be FinSequence of V; ::_thesis: for f being Function of V,R st i in dom F & v = F . i holds (f (#) F) . i = v * (f . v) let f be Function of V,R; ::_thesis: ( i in dom F & v = F . i implies (f (#) F) . i = v * (f . v) ) assume that A1: i in dom F and A2: v = F . i ; ::_thesis: (f (#) F) . i = v * (f . v) A3: F /. i = F . i by A1, PARTFUN1:def_6; len (f (#) F) = len F by Def6; then i in dom (f (#) F) by A1, FINSEQ_3:29; hence (f (#) F) . i = v * (f . v) by A2, A3, Def6; ::_thesis: verum end; theorem :: RMOD_4:24 for R being Ring for V being RightMod of R for f being Function of V,R holds f (#) (<*> the carrier of V) = <*> the carrier of V proof let R be Ring; ::_thesis: for V being RightMod of R for f being Function of V,R holds f (#) (<*> the carrier of V) = <*> the carrier of V let V be RightMod of R; ::_thesis: for f being Function of V,R holds f (#) (<*> the carrier of V) = <*> the carrier of V let f be Function of V,R; ::_thesis: f (#) (<*> the carrier of V) = <*> the carrier of V len (f (#) (<*> the carrier of V)) = len (<*> the carrier of V) by Def6 .= 0 ; hence f (#) (<*> the carrier of V) = <*> the carrier of V ; ::_thesis: verum end; theorem Th25: :: RMOD_4:25 for R being Ring for V being RightMod of R for v being Vector of V for f being Function of V,R holds f (#) <*v*> = <*(v * (f . v))*> proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for f being Function of V,R holds f (#) <*v*> = <*(v * (f . v))*> let V be RightMod of R; ::_thesis: for v being Vector of V for f being Function of V,R holds f (#) <*v*> = <*(v * (f . v))*> let v be Vector of V; ::_thesis: for f being Function of V,R holds f (#) <*v*> = <*(v * (f . v))*> let f be Function of V,R; ::_thesis: f (#) <*v*> = <*(v * (f . v))*> A1: 1 in {1} by TARSKI:def_1; A2: len (f (#) <*v*>) = len <*v*> by Def6 .= 1 by FINSEQ_1:40 ; then dom (f (#) <*v*>) = {1} by FINSEQ_1:2, FINSEQ_1:def_3; then (f (#) <*v*>) . 1 = (<*v*> /. 1) * (f . (<*v*> /. 1)) by A1, Def6 .= v * (f . (<*v*> /. 1)) by FINSEQ_4:16 .= v * (f . v) by FINSEQ_4:16 ; hence f (#) <*v*> = <*(v * (f . v))*> by A2, FINSEQ_1:40; ::_thesis: verum end; theorem Th26: :: RMOD_4:26 for R being Ring for V being RightMod of R for v1, v2 being Vector of V for f being Function of V,R holds f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*> proof let R be Ring; ::_thesis: for V being RightMod of R for v1, v2 being Vector of V for f being Function of V,R holds f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*> let V be RightMod of R; ::_thesis: for v1, v2 being Vector of V for f being Function of V,R holds f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*> let v1, v2 be Vector of V; ::_thesis: for f being Function of V,R holds f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*> let f be Function of V,R; ::_thesis: f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*> A1: len (f (#) <*v1,v2*>) = len <*v1,v2*> by Def6 .= 2 by FINSEQ_1:44 ; then A2: dom (f (#) <*v1,v2*>) = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3; 2 in {1,2} by TARSKI:def_2; then A3: (f (#) <*v1,v2*>) . 2 = (<*v1,v2*> /. 2) * (f . (<*v1,v2*> /. 2)) by A2, Def6 .= v2 * (f . (<*v1,v2*> /. 2)) by FINSEQ_4:17 .= v2 * (f . v2) by FINSEQ_4:17 ; 1 in {1,2} by TARSKI:def_2; then (f (#) <*v1,v2*>) . 1 = (<*v1,v2*> /. 1) * (f . (<*v1,v2*> /. 1)) by A2, Def6 .= v1 * (f . (<*v1,v2*> /. 1)) by FINSEQ_4:17 .= v1 * (f . v1) by FINSEQ_4:17 ; hence f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*> by A1, A3, FINSEQ_1:44; ::_thesis: verum end; theorem :: RMOD_4:27 for R being Ring for V being RightMod of R for v1, v2, v3 being Vector of V for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*> proof let R be Ring; ::_thesis: for V being RightMod of R for v1, v2, v3 being Vector of V for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*> let V be RightMod of R; ::_thesis: for v1, v2, v3 being Vector of V for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*> let v1, v2, v3 be Vector of V; ::_thesis: for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*> let f be Function of V,R; ::_thesis: f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*> A1: len (f (#) <*v1,v2,v3*>) = len <*v1,v2,v3*> by Def6 .= 3 by FINSEQ_1:45 ; then A2: dom (f (#) <*v1,v2,v3*>) = {1,2,3} by FINSEQ_1:def_3, FINSEQ_3:1; 3 in {1,2,3} by ENUMSET1:def_1; then A3: (f (#) <*v1,v2,v3*>) . 3 = (<*v1,v2,v3*> /. 3) * (f . (<*v1,v2,v3*> /. 3)) by A2, Def6 .= v3 * (f . (<*v1,v2,v3*> /. 3)) by FINSEQ_4:18 .= v3 * (f . v3) by FINSEQ_4:18 ; 2 in {1,2,3} by ENUMSET1:def_1; then A4: (f (#) <*v1,v2,v3*>) . 2 = (<*v1,v2,v3*> /. 2) * (f . (<*v1,v2,v3*> /. 2)) by A2, Def6 .= v2 * (f . (<*v1,v2,v3*> /. 2)) by FINSEQ_4:18 .= v2 * (f . v2) by FINSEQ_4:18 ; 1 in {1,2,3} by ENUMSET1:def_1; then (f (#) <*v1,v2,v3*>) . 1 = (<*v1,v2,v3*> /. 1) * (f . (<*v1,v2,v3*> /. 1)) by A2, Def6 .= v1 * (f . (<*v1,v2,v3*> /. 1)) by FINSEQ_4:18 .= v1 * (f . v1) by FINSEQ_4:18 ; hence f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*> by A1, A4, A3, FINSEQ_1:45; ::_thesis: verum end; theorem Th28: :: RMOD_4:28 for R being Ring for V being RightMod of R for F, G being FinSequence of V for f being Function of V,R holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G) proof let R be Ring; ::_thesis: for V being RightMod of R for F, G being FinSequence of V for f being Function of V,R holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G) let V be RightMod of R; ::_thesis: for F, G being FinSequence of V for f being Function of V,R holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G) let F, G be FinSequence of V; ::_thesis: for f being Function of V,R holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G) let f be Function of V,R; ::_thesis: f (#) (F ^ G) = (f (#) F) ^ (f (#) G) set H = (f (#) F) ^ (f (#) G); set I = F ^ G; A1: len F = len (f (#) F) by Def6; A2: len ((f (#) F) ^ (f (#) G)) = (len (f (#) F)) + (len (f (#) G)) by FINSEQ_1:22 .= (len F) + (len (f (#) G)) by Def6 .= (len F) + (len G) by Def6 .= len (F ^ G) by FINSEQ_1:22 ; A3: len G = len (f (#) G) by Def6; now__::_thesis:_for_k_being_Nat_st_k_in_dom_((f_(#)_F)_^_(f_(#)_G))_holds_ ((f_(#)_F)_^_(f_(#)_G))_._k_=_((F_^_G)_/._k)_*_(f_._((F_^_G)_/._k)) let k be Nat; ::_thesis: ( k in dom ((f (#) F) ^ (f (#) G)) implies ((f (#) F) ^ (f (#) G)) . k = ((F ^ G) /. k) * (f . ((F ^ G) /. k)) ) assume A4: k in dom ((f (#) F) ^ (f (#) G)) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = ((F ^ G) /. k) * (f . ((F ^ G) /. k)) now__::_thesis:_((f_(#)_F)_^_(f_(#)_G))_._k_=_((F_^_G)_/._k)_*_(f_._((F_^_G)_/._k)) percases ( k in dom (f (#) F) or ex n being Nat st ( n in dom (f (#) G) & k = (len (f (#) F)) + n ) ) by A4, FINSEQ_1:25; supposeA5: k in dom (f (#) F) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = ((F ^ G) /. k) * (f . ((F ^ G) /. k)) then A6: k in dom F by A1, FINSEQ_3:29; then A7: k in dom (F ^ G) by FINSEQ_3:22; A8: F /. k = F . k by A6, PARTFUN1:def_6 .= (F ^ G) . k by A6, FINSEQ_1:def_7 .= (F ^ G) /. k by A7, PARTFUN1:def_6 ; thus ((f (#) F) ^ (f (#) G)) . k = (f (#) F) . k by A5, FINSEQ_1:def_7 .= ((F ^ G) /. k) * (f . ((F ^ G) /. k)) by A5, A8, Def6 ; ::_thesis: verum end; supposeA9: ex n being Nat st ( n in dom (f (#) G) & k = (len (f (#) F)) + n ) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = ((F ^ G) /. k) * (f . ((F ^ G) /. k)) A10: k in dom (F ^ G) by A2, A4, FINSEQ_3:29; consider n being Nat such that A11: n in dom (f (#) G) and A12: k = (len (f (#) F)) + n by A9; A13: n in dom G by A3, A11, FINSEQ_3:29; then A14: G /. n = G . n by PARTFUN1:def_6 .= (F ^ G) . k by A1, A12, A13, FINSEQ_1:def_7 .= (F ^ G) /. k by A10, PARTFUN1:def_6 ; thus ((f (#) F) ^ (f (#) G)) . k = (f (#) G) . n by A11, A12, FINSEQ_1:def_7 .= ((F ^ G) /. k) * (f . ((F ^ G) /. k)) by A11, A14, Def6 ; ::_thesis: verum end; end; end; hence ((f (#) F) ^ (f (#) G)) . k = ((F ^ G) /. k) * (f . ((F ^ G) /. k)) ; ::_thesis: verum end; hence f (#) (F ^ G) = (f (#) F) ^ (f (#) G) by A2, Def6; ::_thesis: verum end; definition let R be Ring; let V be RightMod of R; let L be Linear_Combination of V; func Sum L -> Vector of V means :Def7: :: RMOD_4:def 7 ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) ); existence ex b1 being Vector of V ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & b1 = Sum (L (#) F) ) proof consider F being FinSequence such that A1: rng F = Carrier L and A2: F is one-to-one by FINSEQ_4:58; reconsider F = F as FinSequence of V by A1, FINSEQ_1:def_4; take Sum (L (#) F) ; ::_thesis: ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) ) take F ; ::_thesis: ( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) ) thus ( F is one-to-one & rng F = Carrier L ) by A1, A2; ::_thesis: Sum (L (#) F) = Sum (L (#) F) thus Sum (L (#) F) = Sum (L (#) F) ; ::_thesis: verum end; uniqueness for b1, b2 being Vector of V st ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & b1 = Sum (L (#) F) ) & ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & b2 = Sum (L (#) F) ) holds b1 = b2 proof let v1, v2 be Vector of V; ::_thesis: ( ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & v1 = Sum (L (#) F) ) & ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & v2 = Sum (L (#) F) ) implies v1 = v2 ) given F1 being FinSequence of V such that A3: F1 is one-to-one and A4: rng F1 = Carrier L and A5: v1 = Sum (L (#) F1) ; ::_thesis: ( for F being FinSequence of V holds ( not F is one-to-one or not rng F = Carrier L or not v2 = Sum (L (#) F) ) or v1 = v2 ) given F2 being FinSequence of V such that A6: F2 is one-to-one and A7: rng F2 = Carrier L and A8: v2 = Sum (L (#) F2) ; ::_thesis: v1 = v2 defpred S1[ set , set ] means {$2} = F1 " {(F2 . $1)}; A9: len F1 = len F2 by A3, A4, A6, A7, FINSEQ_1:48; A10: dom F1 = Seg (len F1) by FINSEQ_1:def_3; A11: dom F2 = Seg (len F2) by FINSEQ_1:def_3; A12: for x being set st x in dom F1 holds ex y being set st ( y in dom F1 & S1[x,y] ) proof let x be set ; ::_thesis: ( x in dom F1 implies ex y being set st ( y in dom F1 & S1[x,y] ) ) assume x in dom F1 ; ::_thesis: ex y being set st ( y in dom F1 & S1[x,y] ) then F2 . x in rng F1 by A4, A7, A9, A10, A11, FUNCT_1:def_3; then consider y being set such that A13: F1 " {(F2 . x)} = {y} by A3, FUNCT_1:74; take y ; ::_thesis: ( y in dom F1 & S1[x,y] ) y in F1 " {(F2 . x)} by A13, TARSKI:def_1; hence y in dom F1 by FUNCT_1:def_7; ::_thesis: S1[x,y] thus S1[x,y] by A13; ::_thesis: verum end; consider f being Function of (dom F1),(dom F1) such that A14: for x being set st x in dom F1 holds S1[x,f . x] from FUNCT_2:sch_1(A12); A15: rng f = dom F1 proof thus rng f c= dom F1 by RELAT_1:def_19; :: according to XBOOLE_0:def_10 ::_thesis: dom F1 c= rng f let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom F1 or y in rng f ) assume A16: y in dom F1 ; ::_thesis: y in rng f then F1 . y in rng F2 by A4, A7, FUNCT_1:def_3; then consider x being set such that A17: x in dom F2 and A18: F2 . x = F1 . y by FUNCT_1:def_3; F1 " {(F2 . x)} = F1 " (Im (F1,y)) by A16, A18, FUNCT_1:59; then F1 " {(F2 . x)} c= {y} by A3, FUNCT_1:82; then {(f . x)} c= {y} by A9, A10, A11, A14, A17; then A19: f . x = y by ZFMISC_1:18; x in dom f by A9, A10, A11, A17, FUNCT_2:def_1; hence y in rng f by A19, FUNCT_1:def_3; ::_thesis: verum end; set G1 = L (#) F1; A20: len (L (#) F1) = len F1 by Def6; A21: ( dom F1 = {} implies dom F1 = {} ) ; A22: f is one-to-one proof let y1, y2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not y1 in dom f or not y2 in dom f or not f . y1 = f . y2 or y1 = y2 ) assume that A23: y1 in dom f and A24: y2 in dom f and A25: f . y1 = f . y2 ; ::_thesis: y1 = y2 A26: y2 in dom F1 by A21, A24, FUNCT_2:def_1; then A27: F1 " {(F2 . y2)} = {(f . y2)} by A14; A28: y1 in dom F1 by A21, A23, FUNCT_2:def_1; then F2 . y1 in rng F1 by A4, A7, A9, A10, A11, FUNCT_1:def_3; then A29: {(F2 . y1)} c= rng F1 by ZFMISC_1:31; F2 . y2 in rng F1 by A4, A7, A9, A10, A11, A26, FUNCT_1:def_3; then A30: {(F2 . y2)} c= rng F1 by ZFMISC_1:31; F1 " {(F2 . y1)} = {(f . y1)} by A14, A28; then {(F2 . y1)} = {(F2 . y2)} by A25, A27, A29, A30, FUNCT_1:91; then A31: F2 . y1 = F2 . y2 by ZFMISC_1:3; ( y1 in dom F2 & y2 in dom F2 ) by A9, A10, A11, A21, A23, A24, FUNCT_2:def_1; hence y1 = y2 by A6, A31, FUNCT_1:def_4; ::_thesis: verum end; set G2 = L (#) F2; A32: dom (L (#) F2) = Seg (len (L (#) F2)) by FINSEQ_1:def_3; reconsider f = f as Permutation of (dom F1) by A15, A22, FUNCT_2:57; ( dom F1 = Seg (len F1) & dom (L (#) F1) = Seg (len (L (#) F1)) ) by FINSEQ_1:def_3; then reconsider f = f as Permutation of (dom (L (#) F1)) by A20; A33: len (L (#) F2) = len F2 by Def6; A34: dom (L (#) F1) = Seg (len (L (#) F1)) by FINSEQ_1:def_3; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(L_(#)_F2)_holds_ (L_(#)_F2)_._i_=_(L_(#)_F1)_._(f_._i) let i be Element of NAT ; ::_thesis: ( i in dom (L (#) F2) implies (L (#) F2) . i = (L (#) F1) . (f . i) ) assume A35: i in dom (L (#) F2) ; ::_thesis: (L (#) F2) . i = (L (#) F1) . (f . i) then A36: ( (L (#) F2) . i = (F2 /. i) * (L . (F2 /. i)) & F2 . i = F2 /. i ) by A33, A11, A32, Def6, PARTFUN1:def_6; i in dom F2 by A33, A35, FINSEQ_3:29; then reconsider u = F2 . i as Vector of V by FINSEQ_2:11; i in dom f by A9, A20, A33, A34, A32, A35, FUNCT_2:def_1; then A37: f . i in dom F1 by A15, FUNCT_1:def_3; then reconsider m = f . i as Element of NAT by A10; reconsider v = F1 . m as Vector of V by A37, FINSEQ_2:11; {(F1 . (f . i))} = Im (F1,(f . i)) by A37, FUNCT_1:59 .= F1 .: (F1 " {(F2 . i)}) by A9, A33, A10, A32, A14, A35 ; then A38: u = v by FUNCT_1:75, ZFMISC_1:18; F1 . m = F1 /. m by A37, PARTFUN1:def_6; hence (L (#) F2) . i = (L (#) F1) . (f . i) by A20, A10, A34, A37, A38, A36, Def6; ::_thesis: verum end; hence v1 = v2 by A3, A4, A5, A6, A7, A8, A20, A33, FINSEQ_1:48, RLVECT_2:6; ::_thesis: verum end; end; :: deftheorem Def7 defines Sum RMOD_4:def_7_:_ for R being Ring for V being RightMod of R for L being Linear_Combination of V for b4 being Vector of V holds ( b4 = Sum L iff ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & b4 = Sum (L (#) F) ) ); Lm3: for R being Ring for V being RightMod of R holds Sum (ZeroLC V) = 0. V proof let R be Ring; ::_thesis: for V being RightMod of R holds Sum (ZeroLC V) = 0. V let V be RightMod of R; ::_thesis: Sum (ZeroLC V) = 0. V consider F being FinSequence of V such that F is one-to-one and A1: rng F = Carrier (ZeroLC V) and A2: Sum (ZeroLC V) = Sum ((ZeroLC V) (#) F) by Def7; Carrier (ZeroLC V) = {} by Def4; then F = {} by A1, RELAT_1:41; then len F = 0 ; then len ((ZeroLC V) (#) F) = 0 by Def6; hence Sum (ZeroLC V) = 0. V by A2, RLVECT_1:75; ::_thesis: verum end; theorem Th29: :: RMOD_4:29 for R being Ring for V being RightMod of R for A being Subset of V st 0. R <> 1_ R holds ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) proof let R be Ring; ::_thesis: for V being RightMod of R for A being Subset of V st 0. R <> 1_ R holds ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) let V be RightMod of R; ::_thesis: for A being Subset of V st 0. R <> 1_ R holds ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) let A be Subset of V; ::_thesis: ( 0. R <> 1_ R implies ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) ) assume A1: 0. R <> 1_ R ; ::_thesis: ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) thus ( A <> {} & A is linearly-closed implies for l being Linear_Combination of A holds Sum l in A ) ::_thesis: ( ( for l being Linear_Combination of A holds Sum l in A ) implies ( A <> {} & A is linearly-closed ) ) proof defpred S1[ Nat] means for l being Linear_Combination of A st card (Carrier l) = $1 holds Sum l in A; assume that A2: A <> {} and A3: A is linearly-closed ; ::_thesis: for l being Linear_Combination of A holds Sum l in A now__::_thesis:_for_l_being_Linear_Combination_of_A_st_card_(Carrier_l)_=_0_holds_ Sum_l_in_A let l be Linear_Combination of A; ::_thesis: ( card (Carrier l) = 0 implies Sum l in A ) assume card (Carrier l) = 0 ; ::_thesis: Sum l in A then Carrier l = {} ; then l = ZeroLC V by Def4; then Sum l = 0. V by Lm3; hence Sum l in A by A2, A3, RMOD_2:1; ::_thesis: verum end; then A4: S1[ 0 ] ; now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_l_being_Linear_Combination_of_A_st_card_(Carrier_l)_=_k_holds_ Sum_l_in_A_)_holds_ for_l_being_Linear_Combination_of_A_st_card_(Carrier_l)_=_k_+_1_holds_ Sum_l_in_A let k be Element of NAT ; ::_thesis: ( ( for l being Linear_Combination of A st card (Carrier l) = k holds Sum l in A ) implies for l being Linear_Combination of A st card (Carrier l) = k + 1 holds Sum l in A ) assume A5: for l being Linear_Combination of A st card (Carrier l) = k holds Sum l in A ; ::_thesis: for l being Linear_Combination of A st card (Carrier l) = k + 1 holds Sum l in A let l be Linear_Combination of A; ::_thesis: ( card (Carrier l) = k + 1 implies Sum l in A ) deffunc H1( Element of V) -> Element of the carrier of R = l . $1; consider F being FinSequence of V such that A6: F is one-to-one and A7: rng F = Carrier l and A8: Sum l = Sum (l (#) F) by Def7; reconsider G = F | (Seg k) as FinSequence of V by FINSEQ_1:18; assume A9: card (Carrier l) = k + 1 ; ::_thesis: Sum l in A then A10: len F = k + 1 by A6, A7, FINSEQ_4:62; then A11: len (l (#) F) = k + 1 by Def6; A12: k + 1 in Seg (k + 1) by FINSEQ_1:4; then A13: k + 1 in dom F by A10, FINSEQ_1:def_3; k + 1 in dom F by A10, A12, FINSEQ_1:def_3; then reconsider v = F . (k + 1) as Vector of V by FINSEQ_2:11; consider f being Function of V,R such that A14: f . v = 0. R and A15: for u being Element of V st u <> v holds f . u = H1(u) from FUNCT_2:sch_6(); reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8; A16: v in Carrier l by A7, A13, FUNCT_1:def_3; now__::_thesis:_for_u_being_Vector_of_V_st_not_u_in_Carrier_l_holds_ f_._u_=_0._R let u be Vector of V; ::_thesis: ( not u in Carrier l implies f . u = 0. R ) assume A17: not u in Carrier l ; ::_thesis: f . u = 0. R hence f . u = l . u by A16, A15 .= 0. R by A17 ; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def2; A18: A \ {v} c= A by XBOOLE_1:36; A19: Carrier l c= A by Def5; then A20: v * (l . v) in A by A3, A16, RMOD_2:def_1; A21: Carrier f = (Carrier l) \ {v} proof thus Carrier f c= (Carrier l) \ {v} :: according to XBOOLE_0:def_10 ::_thesis: (Carrier l) \ {v} c= Carrier f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in (Carrier l) \ {v} ) assume x in Carrier f ; ::_thesis: x in (Carrier l) \ {v} then consider u being Vector of V such that A22: u = x and A23: f . u <> 0. R ; f . u = l . u by A14, A15, A23; then A24: x in Carrier l by A22, A23; not x in {v} by A14, A22, A23, TARSKI:def_1; hence x in (Carrier l) \ {v} by A24, XBOOLE_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Carrier l) \ {v} or x in Carrier f ) assume A25: x in (Carrier l) \ {v} ; ::_thesis: x in Carrier f then x in Carrier l by XBOOLE_0:def_5; then consider u being Vector of V such that A26: x = u and A27: l . u <> 0. R ; not x in {v} by A25, XBOOLE_0:def_5; then x <> v by TARSKI:def_1; then l . u = f . u by A15, A26; hence x in Carrier f by A26, A27; ::_thesis: verum end; then Carrier f c= A \ {v} by A19, XBOOLE_1:33; then Carrier f c= A by A18, XBOOLE_1:1; then reconsider f = f as Linear_Combination of A by Def5; A28: len G = k by A10, FINSEQ_3:53; then A29: len (f (#) G) = k by Def6; A30: rng G = Carrier f proof thus rng G c= Carrier f :: according to XBOOLE_0:def_10 ::_thesis: Carrier f c= rng G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng G or x in Carrier f ) assume x in rng G ; ::_thesis: x in Carrier f then consider y being set such that A31: y in dom G and A32: G . y = x by FUNCT_1:def_3; reconsider y = y as Nat by A31, FINSEQ_3:23; A33: ( dom G c= dom F & G . y = F . y ) by A31, FUNCT_1:47, RELAT_1:60; now__::_thesis:_not_x_=_v assume x = v ; ::_thesis: contradiction then A34: k + 1 = y by A6, A13, A31, A32, A33, FUNCT_1:def_4; y <= k by A28, A31, FINSEQ_3:25; hence contradiction by A34, XREAL_1:29; ::_thesis: verum end; then A35: not x in {v} by TARSKI:def_1; x in rng F by A31, A32, A33, FUNCT_1:def_3; hence x in Carrier f by A7, A21, A35, XBOOLE_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in rng G ) assume A36: x in Carrier f ; ::_thesis: x in rng G then x in rng F by A7, A21, XBOOLE_0:def_5; then consider y being set such that A37: y in dom F and A38: F . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A37, FINSEQ_3:23; now__::_thesis:_y_in_Seg_k assume not y in Seg k ; ::_thesis: contradiction then y in (dom F) \ (Seg k) by A37, XBOOLE_0:def_5; then y in (Seg (k + 1)) \ (Seg k) by A10, FINSEQ_1:def_3; then y in {(k + 1)} by FINSEQ_3:15; then y = k + 1 by TARSKI:def_1; then not v in {v} by A21, A36, A38, XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; then y in (dom F) /\ (Seg k) by A37, XBOOLE_0:def_4; then A39: y in dom G by RELAT_1:61; then G . y = F . y by FUNCT_1:47; hence x in rng G by A38, A39, FUNCT_1:def_3; ::_thesis: verum end; (Seg (k + 1)) /\ (Seg k) = Seg k by FINSEQ_1:7, NAT_1:12 .= dom (f (#) G) by A29, FINSEQ_1:def_3 ; then A40: dom (f (#) G) = (dom (l (#) F)) /\ (Seg k) by A11, FINSEQ_1:def_3; now__::_thesis:_for_x_being_set_st_x_in_dom_(f_(#)_G)_holds_ (f_(#)_G)_._x_=_(l_(#)_F)_._x let x be set ; ::_thesis: ( x in dom (f (#) G) implies (f (#) G) . x = (l (#) F) . x ) A41: rng F c= the carrier of V by FINSEQ_1:def_4; assume A42: x in dom (f (#) G) ; ::_thesis: (f (#) G) . x = (l (#) F) . x then reconsider n = x as Nat by FINSEQ_3:23; n in dom (l (#) F) by A40, A42, XBOOLE_0:def_4; then A43: n in dom F by A10, A11, FINSEQ_3:29; then F . n in rng F by FUNCT_1:def_3; then reconsider w = F . n as Vector of V by A41; A44: n in dom G by A28, A29, A42, FINSEQ_3:29; then A45: G . n in rng G by FUNCT_1:def_3; rng G c= the carrier of V by FINSEQ_1:def_4; then reconsider u = G . n as Vector of V by A45; not u in {v} by A21, A30, A45, XBOOLE_0:def_5; then A46: u <> v by TARSKI:def_1; A47: (f (#) G) . n = u * (f . u) by A44, Th23 .= u * (l . u) by A15, A46 ; w = u by A44, FUNCT_1:47; hence (f (#) G) . x = (l (#) F) . x by A47, A43, Th23; ::_thesis: verum end; then f (#) G = (l (#) F) | (Seg k) by A40, FUNCT_1:46; then A48: f (#) G = (l (#) F) | (dom (f (#) G)) by A29, FINSEQ_1:def_3; v in rng F by A13, FUNCT_1:def_3; then {v} c= Carrier l by A7, ZFMISC_1:31; then card (Carrier f) = (k + 1) - (card {v}) by A9, A21, CARD_2:44 .= (k + 1) - 1 by CARD_1:30 .= k by XCMPLX_1:26 ; then A49: Sum f in A by A5; G is one-to-one by A6, FUNCT_1:52; then A50: Sum (f (#) G) = Sum f by A30, Def7; (l (#) F) . (len F) = v * (l . v) by A10, A13, Th23; then Sum (l (#) F) = (Sum (f (#) G)) + (v * (l . v)) by A10, A11, A29, A48, RLVECT_1:38; hence Sum l in A by A3, A8, A20, A50, A49, RMOD_2:def_1; ::_thesis: verum end; then A51: for k being Element of NAT st S1[k] holds S1[k + 1] ; let l be Linear_Combination of A; ::_thesis: Sum l in A A52: card (Carrier l) = card (Carrier l) ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A51); hence Sum l in A by A52; ::_thesis: verum end; assume A53: for l being Linear_Combination of A holds Sum l in A ; ::_thesis: ( A <> {} & A is linearly-closed ) hence A <> {} ; ::_thesis: A is linearly-closed ( ZeroLC V is Linear_Combination of A & Sum (ZeroLC V) = 0. V ) by Lm3, Th20; then A54: 0. V in A by A53; A55: for a being Scalar of R for v being Vector of V st v in A holds v * a in A proof let a be Scalar of R; ::_thesis: for v being Vector of V st v in A holds v * a in A let v be Vector of V; ::_thesis: ( v in A implies v * a in A ) assume A56: v in A ; ::_thesis: v * a in A now__::_thesis:_v_*_a_in_A percases ( a = 0. R or a <> 0. R ) ; suppose a = 0. R ; ::_thesis: v * a in A hence v * a in A by A54, VECTSP_2:32; ::_thesis: verum end; supposeA57: a <> 0. R ; ::_thesis: v * a in A deffunc H1( Element of V) -> Element of the carrier of R = 0. R; consider f being Function of V,R such that A58: f . v = a and A59: for u being Element of V st u <> v holds f . u = H1(u) from FUNCT_2:sch_6(); reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8; now__::_thesis:_for_u_being_Vector_of_V_st_not_u_in_{v}_holds_ f_._u_=_0._R let u be Vector of V; ::_thesis: ( not u in {v} implies f . u = 0. R ) assume not u in {v} ; ::_thesis: f . u = 0. R then u <> v by TARSKI:def_1; hence f . u = 0. R by A59; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def2; A60: Carrier f = {v} proof thus Carrier f c= {v} :: according to XBOOLE_0:def_10 ::_thesis: {v} c= Carrier f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} ) assume x in Carrier f ; ::_thesis: x in {v} then consider u being Vector of V such that A61: x = u and A62: f . u <> 0. R ; u = v by A59, A62; hence x in {v} by A61, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in Carrier f ) assume x in {v} ; ::_thesis: x in Carrier f then x = v by TARSKI:def_1; hence x in Carrier f by A57, A58; ::_thesis: verum end; {v} c= A by A56, ZFMISC_1:31; then reconsider f = f as Linear_Combination of A by A60, Def5; consider F being FinSequence of V such that A63: ( F is one-to-one & rng F = Carrier f ) and A64: Sum (f (#) F) = Sum f by Def7; F = <*v*> by A60, A63, FINSEQ_3:97; then f (#) F = <*(v * (f . v))*> by Th25; then Sum f = v * a by A58, A64, RLVECT_1:44; hence v * a in A by A53; ::_thesis: verum end; end; end; hence v * a in A ; ::_thesis: verum end; thus for v, u being Vector of V st v in A & u in A holds v + u in A :: according to RMOD_2:def_1 ::_thesis: for b1 being Element of the carrier of R for b2 being Element of the carrier of V holds ( not b2 in A or b2 * b1 in A ) proof let v, u be Vector of V; ::_thesis: ( v in A & u in A implies v + u in A ) assume that A65: v in A and A66: u in A ; ::_thesis: v + u in A now__::_thesis:_v_+_u_in_A percases ( u = v or v <> u ) ; suppose u = v ; ::_thesis: v + u in A then v + u = (v * (1_ R)) + v by VECTSP_2:def_9 .= (v * (1_ R)) + (v * (1_ R)) by VECTSP_2:def_9 .= v * ((1_ R) + (1_ R)) by VECTSP_2:def_9 ; hence v + u in A by A55, A65; ::_thesis: verum end; supposeA67: v <> u ; ::_thesis: v + u in A deffunc H1( Element of V) -> Element of the carrier of R = 0. R; consider f being Function of V,R such that A68: ( f . v = 1_ R & f . u = 1_ R ) and A69: for w being Element of V st w <> v & w <> u holds f . w = H1(w) from FUNCT_2:sch_7(A67); reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8; now__::_thesis:_for_w_being_Vector_of_V_st_not_w_in_{v,u}_holds_ f_._w_=_0._R let w be Vector of V; ::_thesis: ( not w in {v,u} implies f . w = 0. R ) assume not w in {v,u} ; ::_thesis: f . w = 0. R then ( w <> v & w <> u ) by TARSKI:def_2; hence f . w = 0. R by A69; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def2; A70: Carrier f = {v,u} proof thus Carrier f c= {v,u} :: according to XBOOLE_0:def_10 ::_thesis: {v,u} c= Carrier f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v,u} ) assume x in Carrier f ; ::_thesis: x in {v,u} then ex w being Vector of V st ( x = w & f . w <> 0. R ) ; then ( x = v or x = u ) by A69; hence x in {v,u} by TARSKI:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v,u} or x in Carrier f ) assume x in {v,u} ; ::_thesis: x in Carrier f then ( x = v or x = u ) by TARSKI:def_2; hence x in Carrier f by A1, A68; ::_thesis: verum end; then A71: Carrier f c= A by A65, A66, ZFMISC_1:32; A72: ( u * (1_ R) = u & v * (1_ R) = v ) by VECTSP_2:def_9; reconsider f = f as Linear_Combination of A by A71, Def5; consider F being FinSequence of V such that A73: ( F is one-to-one & rng F = Carrier f ) and A74: Sum (f (#) F) = Sum f by Def7; ( F = <*v,u*> or F = <*u,v*> ) by A67, A70, A73, FINSEQ_3:99; then ( f (#) F = <*(v * (1_ R)),(u * (1_ R))*> or f (#) F = <*(u * (1_ R)),(v * (1_ R))*> ) by A68, Th26; then Sum f = v + u by A74, A72, RLVECT_1:45; hence v + u in A by A53; ::_thesis: verum end; end; end; hence v + u in A ; ::_thesis: verum end; thus for b1 being Element of the carrier of R for b2 being Element of the carrier of V holds ( not b2 in A or b2 * b1 in A ) by A55; ::_thesis: verum end; theorem :: RMOD_4:30 for R being Ring for V being RightMod of R holds Sum (ZeroLC V) = 0. V by Lm3; theorem Th31: :: RMOD_4:31 for R being Ring for V being RightMod of R for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V proof let R be Ring; ::_thesis: for V being RightMod of R for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V let V be RightMod of R; ::_thesis: for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V let l be Linear_Combination of {} the carrier of V; ::_thesis: Sum l = 0. V l = ZeroLC V by Th21; hence Sum l = 0. V by Lm3; ::_thesis: verum end; theorem Th32: :: RMOD_4:32 for R being Ring for V being RightMod of R for v being Vector of V for l being Linear_Combination of {v} holds Sum l = v * (l . v) proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for l being Linear_Combination of {v} holds Sum l = v * (l . v) let V be RightMod of R; ::_thesis: for v being Vector of V for l being Linear_Combination of {v} holds Sum l = v * (l . v) let v be Vector of V; ::_thesis: for l being Linear_Combination of {v} holds Sum l = v * (l . v) let l be Linear_Combination of {v}; ::_thesis: Sum l = v * (l . v) A1: Carrier l c= {v} by Def5; now__::_thesis:_Sum_l_=_v_*_(l_._v) percases ( Carrier l = {} or Carrier l = {v} ) by A1, ZFMISC_1:33; suppose Carrier l = {} ; ::_thesis: Sum l = v * (l . v) then A2: l = ZeroLC V by Def4; hence Sum l = 0. V by Lm3 .= v * (0. R) by VECTSP_2:32 .= v * (l . v) by A2, Th18 ; ::_thesis: verum end; suppose Carrier l = {v} ; ::_thesis: Sum l = v * (l . v) then consider F being FinSequence of V such that A3: ( F is one-to-one & rng F = {v} ) and A4: Sum l = Sum (l (#) F) by Def7; F = <*v*> by A3, FINSEQ_3:97; then l (#) F = <*(v * (l . v))*> by Th25; hence Sum l = v * (l . v) by A4, RLVECT_1:44; ::_thesis: verum end; end; end; hence Sum l = v * (l . v) ; ::_thesis: verum end; theorem Th33: :: RMOD_4:33 for R being Ring for V being RightMod of R for v1, v2 being Vector of V st v1 <> v2 holds for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) proof let R be Ring; ::_thesis: for V being RightMod of R for v1, v2 being Vector of V st v1 <> v2 holds for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) let V be RightMod of R; ::_thesis: for v1, v2 being Vector of V st v1 <> v2 holds for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) let v1, v2 be Vector of V; ::_thesis: ( v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) ) assume A1: v1 <> v2 ; ::_thesis: for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) let l be Linear_Combination of {v1,v2}; ::_thesis: Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) A2: Carrier l c= {v1,v2} by Def5; now__::_thesis:_Sum_l_=_(v1_*_(l_._v1))_+_(v2_*_(l_._v2)) percases ( Carrier l = {} or Carrier l = {v1} or Carrier l = {v2} or Carrier l = {v1,v2} ) by A2, ZFMISC_1:36; suppose Carrier l = {} ; ::_thesis: Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) then A3: l = ZeroLC V by Def4; hence Sum l = 0. V by Lm3 .= (0. V) + (0. V) by RLVECT_1:def_4 .= (v1 * (0. R)) + (0. V) by VECTSP_2:32 .= (v1 * (0. R)) + (v2 * (0. R)) by VECTSP_2:32 .= (v1 * (l . v1)) + (v2 * (0. R)) by A3, Th18 .= (v1 * (l . v1)) + (v2 * (l . v2)) by A3, Th18 ; ::_thesis: verum end; supposeA4: Carrier l = {v1} ; ::_thesis: Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) then reconsider L = l as Linear_Combination of {v1} by Def5; A5: not v2 in Carrier l by A1, A4, TARSKI:def_1; thus Sum l = Sum L .= v1 * (l . v1) by Th32 .= (v1 * (l . v1)) + (0. V) by RLVECT_1:def_4 .= (v1 * (l . v1)) + (v2 * (0. R)) by VECTSP_2:32 .= (v1 * (l . v1)) + (v2 * (l . v2)) by A5 ; ::_thesis: verum end; supposeA6: Carrier l = {v2} ; ::_thesis: Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) then reconsider L = l as Linear_Combination of {v2} by Def5; A7: not v1 in Carrier l by A1, A6, TARSKI:def_1; thus Sum l = Sum L .= v2 * (l . v2) by Th32 .= (0. V) + (v2 * (l . v2)) by RLVECT_1:def_4 .= (v1 * (0. R)) + (v2 * (l . v2)) by VECTSP_2:32 .= (v1 * (l . v1)) + (v2 * (l . v2)) by A7 ; ::_thesis: verum end; suppose Carrier l = {v1,v2} ; ::_thesis: Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) then consider F being FinSequence of V such that A8: ( F is one-to-one & rng F = {v1,v2} ) and A9: Sum l = Sum (l (#) F) by Def7; ( F = <*v1,v2*> or F = <*v2,v1*> ) by A1, A8, FINSEQ_3:99; then ( l (#) F = <*(v1 * (l . v1)),(v2 * (l . v2))*> or l (#) F = <*(v2 * (l . v2)),(v1 * (l . v1))*> ) by Th26; hence Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) by A9, RLVECT_1:45; ::_thesis: verum end; end; end; hence Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) ; ::_thesis: verum end; theorem :: RMOD_4:34 for R being Ring for V being RightMod of R for L being Linear_Combination of V st Carrier L = {} holds Sum L = 0. V proof let R be Ring; ::_thesis: for V being RightMod of R for L being Linear_Combination of V st Carrier L = {} holds Sum L = 0. V let V be RightMod of R; ::_thesis: for L being Linear_Combination of V st Carrier L = {} holds Sum L = 0. V let L be Linear_Combination of V; ::_thesis: ( Carrier L = {} implies Sum L = 0. V ) assume Carrier L = {} ; ::_thesis: Sum L = 0. V then L = ZeroLC V by Def4; hence Sum L = 0. V by Lm3; ::_thesis: verum end; theorem Th35: :: RMOD_4:35 for R being Ring for V being RightMod of R for v being Vector of V for L being Linear_Combination of V st Carrier L = {v} holds Sum L = v * (L . v) proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for L being Linear_Combination of V st Carrier L = {v} holds Sum L = v * (L . v) let V be RightMod of R; ::_thesis: for v being Vector of V for L being Linear_Combination of V st Carrier L = {v} holds Sum L = v * (L . v) let v be Vector of V; ::_thesis: for L being Linear_Combination of V st Carrier L = {v} holds Sum L = v * (L . v) let L be Linear_Combination of V; ::_thesis: ( Carrier L = {v} implies Sum L = v * (L . v) ) assume Carrier L = {v} ; ::_thesis: Sum L = v * (L . v) then L is Linear_Combination of {v} by Def5; hence Sum L = v * (L . v) by Th32; ::_thesis: verum end; theorem :: RMOD_4:36 for R being Ring for V being RightMod of R for v1, v2 being Vector of V for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds Sum L = (v1 * (L . v1)) + (v2 * (L . v2)) proof let R be Ring; ::_thesis: for V being RightMod of R for v1, v2 being Vector of V for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds Sum L = (v1 * (L . v1)) + (v2 * (L . v2)) let V be RightMod of R; ::_thesis: for v1, v2 being Vector of V for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds Sum L = (v1 * (L . v1)) + (v2 * (L . v2)) let v1, v2 be Vector of V; ::_thesis: for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds Sum L = (v1 * (L . v1)) + (v2 * (L . v2)) let L be Linear_Combination of V; ::_thesis: ( Carrier L = {v1,v2} & v1 <> v2 implies Sum L = (v1 * (L . v1)) + (v2 * (L . v2)) ) assume that A1: Carrier L = {v1,v2} and A2: v1 <> v2 ; ::_thesis: Sum L = (v1 * (L . v1)) + (v2 * (L . v2)) L is Linear_Combination of {v1,v2} by A1, Def5; hence Sum L = (v1 * (L . v1)) + (v2 * (L . v2)) by A2, Th33; ::_thesis: verum end; definition let R be Ring; let V be RightMod of R; let L1, L2 be Linear_Combination of V; :: original: = redefine predL1 = L2 means :: RMOD_4:def 8 for v being Vector of V holds L1 . v = L2 . v; compatibility ( L1 = L2 iff for v being Vector of V holds L1 . v = L2 . v ) by FUNCT_2:63; end; :: deftheorem defines = RMOD_4:def_8_:_ for R being Ring for V being RightMod of R for L1, L2 being Linear_Combination of V holds ( L1 = L2 iff for v being Vector of V holds L1 . v = L2 . v ); definition let R be Ring; let V be RightMod of R; let L1, L2 be Linear_Combination of V; funcL1 + L2 -> Linear_Combination of V means :Def9: :: RMOD_4:def 9 for v being Vector of V holds it . v = (L1 . v) + (L2 . v); existence ex b1 being Linear_Combination of V st for v being Vector of V holds b1 . v = (L1 . v) + (L2 . v) proof deffunc H1( Element of V) -> Element of the carrier of R = (L1 . $1) + (L2 . $1); consider f being Function of V,R such that A1: for v being Element of V holds f . v = H1(v) from FUNCT_2:sch_4(); reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8; now__::_thesis:_for_v_being_Vector_of_V_st_not_v_in_(Carrier_L1)_\/_(Carrier_L2)_holds_ f_._v_=_0._R let v be Vector of V; ::_thesis: ( not v in (Carrier L1) \/ (Carrier L2) implies f . v = 0. R ) assume A2: not v in (Carrier L1) \/ (Carrier L2) ; ::_thesis: f . v = 0. R then not v in Carrier L2 by XBOOLE_0:def_3; then A3: L2 . v = 0. R ; not v in Carrier L1 by A2, XBOOLE_0:def_3; then L1 . v = 0. R ; hence f . v = (0. R) + (0. R) by A1, A3 .= 0. R by RLVECT_1:4 ; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def2; take f ; ::_thesis: for v being Vector of V holds f . v = (L1 . v) + (L2 . v) let v be Vector of V; ::_thesis: f . v = (L1 . v) + (L2 . v) thus f . v = (L1 . v) + (L2 . v) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Linear_Combination of V st ( for v being Vector of V holds b1 . v = (L1 . v) + (L2 . v) ) & ( for v being Vector of V holds b2 . v = (L1 . v) + (L2 . v) ) holds b1 = b2 proof let M, N be Linear_Combination of V; ::_thesis: ( ( for v being Vector of V holds M . v = (L1 . v) + (L2 . v) ) & ( for v being Vector of V holds N . v = (L1 . v) + (L2 . v) ) implies M = N ) assume A4: for v being Vector of V holds M . v = (L1 . v) + (L2 . v) ; ::_thesis: ( ex v being Vector of V st not N . v = (L1 . v) + (L2 . v) or M = N ) assume A5: for v being Vector of V holds N . v = (L1 . v) + (L2 . v) ; ::_thesis: M = N let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: M . v = N . v thus M . v = (L1 . v) + (L2 . v) by A4 .= N . v by A5 ; ::_thesis: verum end; end; :: deftheorem Def9 defines + RMOD_4:def_9_:_ for R being Ring for V being RightMod of R for L1, L2, b5 being Linear_Combination of V holds ( b5 = L1 + L2 iff for v being Vector of V holds b5 . v = (L1 . v) + (L2 . v) ); theorem Th37: :: RMOD_4:37 for R being Ring for V being RightMod of R for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) proof let R be Ring; ::_thesis: for V being RightMod of R for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) let V be RightMod of R; ::_thesis: for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) let L1, L2 be Linear_Combination of V; ::_thesis: Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier (L1 + L2) or x in (Carrier L1) \/ (Carrier L2) ) assume x in Carrier (L1 + L2) ; ::_thesis: x in (Carrier L1) \/ (Carrier L2) then consider u being Vector of V such that A1: x = u and A2: (L1 + L2) . u <> 0. R ; (L1 + L2) . u = (L1 . u) + (L2 . u) by Def9; then ( L1 . u <> 0. R or L2 . u <> 0. R ) by A2, RLVECT_1:4; then ( x in { v1 where v1 is Vector of V : L1 . v1 <> 0. R } or x in { v2 where v2 is Vector of V : L2 . v2 <> 0. R } ) by A1; hence x in (Carrier L1) \/ (Carrier L2) by XBOOLE_0:def_3; ::_thesis: verum end; theorem Th38: :: RMOD_4:38 for R being Ring for V being RightMod of R for A being Subset of V for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds L1 + L2 is Linear_Combination of A proof let R be Ring; ::_thesis: for V being RightMod of R for A being Subset of V for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds L1 + L2 is Linear_Combination of A let V be RightMod of R; ::_thesis: for A being Subset of V for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds L1 + L2 is Linear_Combination of A let A be Subset of V; ::_thesis: for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds L1 + L2 is Linear_Combination of A let L1, L2 be Linear_Combination of V; ::_thesis: ( L1 is Linear_Combination of A & L2 is Linear_Combination of A implies L1 + L2 is Linear_Combination of A ) assume ( L1 is Linear_Combination of A & L2 is Linear_Combination of A ) ; ::_thesis: L1 + L2 is Linear_Combination of A then ( Carrier L1 c= A & Carrier L2 c= A ) by Def5; then A1: (Carrier L1) \/ (Carrier L2) c= A by XBOOLE_1:8; Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) by Th37; hence Carrier (L1 + L2) c= A by A1, XBOOLE_1:1; :: according to RMOD_4:def_5 ::_thesis: verum end; theorem Th39: :: RMOD_4:39 for R being comRing for V being RightMod of R for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1 proof let R be comRing; ::_thesis: for V being RightMod of R for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1 let V be RightMod of R; ::_thesis: for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1 let L1, L2 be Linear_Combination of V; ::_thesis: L1 + L2 = L2 + L1 let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: (L1 + L2) . v = (L2 + L1) . v thus (L1 + L2) . v = (L2 . v) + (L1 . v) by Def9 .= (L2 + L1) . v by Def9 ; ::_thesis: verum end; theorem :: RMOD_4:40 for R being Ring for V being RightMod of R for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3 proof let R be Ring; ::_thesis: for V being RightMod of R for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3 let V be RightMod of R; ::_thesis: for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3 let L1, L2, L3 be Linear_Combination of V; ::_thesis: L1 + (L2 + L3) = (L1 + L2) + L3 let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: (L1 + (L2 + L3)) . v = ((L1 + L2) + L3) . v thus (L1 + (L2 + L3)) . v = (L1 . v) + ((L2 + L3) . v) by Def9 .= (L1 . v) + ((L2 . v) + (L3 . v)) by Def9 .= ((L1 . v) + (L2 . v)) + (L3 . v) by RLVECT_1:def_3 .= ((L1 + L2) . v) + (L3 . v) by Def9 .= ((L1 + L2) + L3) . v by Def9 ; ::_thesis: verum end; theorem :: RMOD_4:41 for R being comRing for V being RightMod of R for L being Linear_Combination of V holds ( L + (ZeroLC V) = L & (ZeroLC V) + L = L ) proof let R be comRing; ::_thesis: for V being RightMod of R for L being Linear_Combination of V holds ( L + (ZeroLC V) = L & (ZeroLC V) + L = L ) let V be RightMod of R; ::_thesis: for L being Linear_Combination of V holds ( L + (ZeroLC V) = L & (ZeroLC V) + L = L ) let L be Linear_Combination of V; ::_thesis: ( L + (ZeroLC V) = L & (ZeroLC V) + L = L ) thus L + (ZeroLC V) = L ::_thesis: (ZeroLC V) + L = L proof let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: (L + (ZeroLC V)) . v = L . v thus (L + (ZeroLC V)) . v = (L . v) + ((ZeroLC V) . v) by Def9 .= (L . v) + (0. R) by Th18 .= L . v by RLVECT_1:4 ; ::_thesis: verum end; hence (ZeroLC V) + L = L by Th39; ::_thesis: verum end; definition let R be Ring; let V be RightMod of R; let a be Scalar of R; let L be Linear_Combination of V; funcL * a -> Linear_Combination of V means :Def10: :: RMOD_4:def 10 for v being Vector of V holds it . v = (L . v) * a; existence ex b1 being Linear_Combination of V st for v being Vector of V holds b1 . v = (L . v) * a proof deffunc H1( Element of V) -> Element of the carrier of R = (L . $1) * a; consider f being Function of V,R such that A1: for v being Element of V holds f . v = H1(v) from FUNCT_2:sch_4(); reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8; now__::_thesis:_for_v_being_Vector_of_V_st_not_v_in_Carrier_L_holds_ f_._v_=_0._R let v be Vector of V; ::_thesis: ( not v in Carrier L implies f . v = 0. R ) assume not v in Carrier L ; ::_thesis: f . v = 0. R then L . v = 0. R ; hence f . v = (0. R) * a by A1 .= 0. R by VECTSP_1:7 ; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def2; take f ; ::_thesis: for v being Vector of V holds f . v = (L . v) * a let v be Vector of V; ::_thesis: f . v = (L . v) * a thus f . v = (L . v) * a by A1; ::_thesis: verum end; uniqueness for b1, b2 being Linear_Combination of V st ( for v being Vector of V holds b1 . v = (L . v) * a ) & ( for v being Vector of V holds b2 . v = (L . v) * a ) holds b1 = b2 proof let L1, L2 be Linear_Combination of V; ::_thesis: ( ( for v being Vector of V holds L1 . v = (L . v) * a ) & ( for v being Vector of V holds L2 . v = (L . v) * a ) implies L1 = L2 ) assume A2: for v being Vector of V holds L1 . v = (L . v) * a ; ::_thesis: ( ex v being Vector of V st not L2 . v = (L . v) * a or L1 = L2 ) assume A3: for v being Vector of V holds L2 . v = (L . v) * a ; ::_thesis: L1 = L2 let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: L1 . v = L2 . v thus L1 . v = (L . v) * a by A2 .= L2 . v by A3 ; ::_thesis: verum end; end; :: deftheorem Def10 defines * RMOD_4:def_10_:_ for R being Ring for V being RightMod of R for a being Scalar of R for L, b5 being Linear_Combination of V holds ( b5 = L * a iff for v being Vector of V holds b5 . v = (L . v) * a ); theorem Th42: :: RMOD_4:42 for R being Ring for V being RightMod of R for a being Scalar of R for L being Linear_Combination of V holds Carrier (L * a) c= Carrier L proof let R be Ring; ::_thesis: for V being RightMod of R for a being Scalar of R for L being Linear_Combination of V holds Carrier (L * a) c= Carrier L let V be RightMod of R; ::_thesis: for a being Scalar of R for L being Linear_Combination of V holds Carrier (L * a) c= Carrier L let a be Scalar of R; ::_thesis: for L being Linear_Combination of V holds Carrier (L * a) c= Carrier L let L be Linear_Combination of V; ::_thesis: Carrier (L * a) c= Carrier L set T = { u where u is Vector of V : (L * a) . u <> 0. R } ; set S = { v where v is Vector of V : L . v <> 0. R } ; { u where u is Vector of V : (L * a) . u <> 0. R } c= { v where v is Vector of V : L . v <> 0. R } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is Vector of V : (L * a) . u <> 0. R } or x in { v where v is Vector of V : L . v <> 0. R } ) assume x in { u where u is Vector of V : (L * a) . u <> 0. R } ; ::_thesis: x in { v where v is Vector of V : L . v <> 0. R } then consider u being Vector of V such that A1: x = u and A2: (L * a) . u <> 0. R ; (L * a) . u = (L . u) * a by Def10; then L . u <> 0. R by A2, VECTSP_1:7; hence x in { v where v is Vector of V : L . v <> 0. R } by A1; ::_thesis: verum end; hence Carrier (L * a) c= Carrier L ; ::_thesis: verum end; theorem Th43: :: RMOD_4:43 for RR being domRing for VV being RightMod of RR for LL being Linear_Combination of VV for aa being Scalar of RR st aa <> 0. RR holds Carrier (LL * aa) = Carrier LL proof let RR be domRing; ::_thesis: for VV being RightMod of RR for LL being Linear_Combination of VV for aa being Scalar of RR st aa <> 0. RR holds Carrier (LL * aa) = Carrier LL let VV be RightMod of RR; ::_thesis: for LL being Linear_Combination of VV for aa being Scalar of RR st aa <> 0. RR holds Carrier (LL * aa) = Carrier LL let LL be Linear_Combination of VV; ::_thesis: for aa being Scalar of RR st aa <> 0. RR holds Carrier (LL * aa) = Carrier LL let aa be Scalar of RR; ::_thesis: ( aa <> 0. RR implies Carrier (LL * aa) = Carrier LL ) set T = { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } ; set S = { vv where vv is Vector of VV : LL . vv <> 0. RR } ; assume A1: aa <> 0. RR ; ::_thesis: Carrier (LL * aa) = Carrier LL { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } = { vv where vv is Vector of VV : LL . vv <> 0. RR } proof thus { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } c= { vv where vv is Vector of VV : LL . vv <> 0. RR } :: according to XBOOLE_0:def_10 ::_thesis: { vv where vv is Vector of VV : LL . vv <> 0. RR } c= { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } or x in { vv where vv is Vector of VV : LL . vv <> 0. RR } ) assume x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } ; ::_thesis: x in { vv where vv is Vector of VV : LL . vv <> 0. RR } then consider uu being Vector of VV such that A2: x = uu and A3: (LL * aa) . uu <> 0. RR ; (LL * aa) . uu = (LL . uu) * aa by Def10; then LL . uu <> 0. RR by A3, VECTSP_1:6; hence x in { vv where vv is Vector of VV : LL . vv <> 0. RR } by A2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { vv where vv is Vector of VV : LL . vv <> 0. RR } or x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } ) assume x in { vv where vv is Vector of VV : LL . vv <> 0. RR } ; ::_thesis: x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } then consider vv being Vector of VV such that A4: x = vv and A5: LL . vv <> 0. RR ; (LL * aa) . vv = (LL . vv) * aa by Def10; then (LL * aa) . vv <> 0. RR by A1, A5, VECTSP_2:def_1; hence x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } by A4; ::_thesis: verum end; hence Carrier (LL * aa) = Carrier LL ; ::_thesis: verum end; theorem Th44: :: RMOD_4:44 for R being Ring for V being RightMod of R for L being Linear_Combination of V holds L * (0. R) = ZeroLC V proof let R be Ring; ::_thesis: for V being RightMod of R for L being Linear_Combination of V holds L * (0. R) = ZeroLC V let V be RightMod of R; ::_thesis: for L being Linear_Combination of V holds L * (0. R) = ZeroLC V let L be Linear_Combination of V; ::_thesis: L * (0. R) = ZeroLC V let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: (L * (0. R)) . v = (ZeroLC V) . v thus (L * (0. R)) . v = (L . v) * (0. R) by Def10 .= 0. R by VECTSP_1:6 .= (ZeroLC V) . v by Th18 ; ::_thesis: verum end; theorem Th45: :: RMOD_4:45 for R being Ring for V being RightMod of R for a being Scalar of R for A being Subset of V for L being Linear_Combination of V st L is Linear_Combination of A holds L * a is Linear_Combination of A proof let R be Ring; ::_thesis: for V being RightMod of R for a being Scalar of R for A being Subset of V for L being Linear_Combination of V st L is Linear_Combination of A holds L * a is Linear_Combination of A let V be RightMod of R; ::_thesis: for a being Scalar of R for A being Subset of V for L being Linear_Combination of V st L is Linear_Combination of A holds L * a is Linear_Combination of A let a be Scalar of R; ::_thesis: for A being Subset of V for L being Linear_Combination of V st L is Linear_Combination of A holds L * a is Linear_Combination of A let A be Subset of V; ::_thesis: for L being Linear_Combination of V st L is Linear_Combination of A holds L * a is Linear_Combination of A let L be Linear_Combination of V; ::_thesis: ( L is Linear_Combination of A implies L * a is Linear_Combination of A ) assume L is Linear_Combination of A ; ::_thesis: L * a is Linear_Combination of A then A1: Carrier L c= A by Def5; Carrier (L * a) c= Carrier L by Th42; then Carrier (L * a) c= A by A1, XBOOLE_1:1; hence L * a is Linear_Combination of A by Def5; ::_thesis: verum end; theorem :: RMOD_4:46 for R being Ring for V being RightMod of R for a, b being Scalar of R for L being Linear_Combination of V holds L * (a + b) = (L * a) + (L * b) proof let R be Ring; ::_thesis: for V being RightMod of R for a, b being Scalar of R for L being Linear_Combination of V holds L * (a + b) = (L * a) + (L * b) let V be RightMod of R; ::_thesis: for a, b being Scalar of R for L being Linear_Combination of V holds L * (a + b) = (L * a) + (L * b) let a, b be Scalar of R; ::_thesis: for L being Linear_Combination of V holds L * (a + b) = (L * a) + (L * b) let L be Linear_Combination of V; ::_thesis: L * (a + b) = (L * a) + (L * b) let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: (L * (a + b)) . v = ((L * a) + (L * b)) . v thus (L * (a + b)) . v = (L . v) * (a + b) by Def10 .= ((L . v) * a) + ((L . v) * b) by VECTSP_1:def_7 .= ((L * a) . v) + ((L . v) * b) by Def10 .= ((L * a) . v) + ((L * b) . v) by Def10 .= ((L * a) + (L * b)) . v by Def9 ; ::_thesis: verum end; theorem :: RMOD_4:47 for R being Ring for V being RightMod of R for a being Scalar of R for L1, L2 being Linear_Combination of V holds (L1 + L2) * a = (L1 * a) + (L2 * a) proof let R be Ring; ::_thesis: for V being RightMod of R for a being Scalar of R for L1, L2 being Linear_Combination of V holds (L1 + L2) * a = (L1 * a) + (L2 * a) let V be RightMod of R; ::_thesis: for a being Scalar of R for L1, L2 being Linear_Combination of V holds (L1 + L2) * a = (L1 * a) + (L2 * a) let a be Scalar of R; ::_thesis: for L1, L2 being Linear_Combination of V holds (L1 + L2) * a = (L1 * a) + (L2 * a) let L1, L2 be Linear_Combination of V; ::_thesis: (L1 + L2) * a = (L1 * a) + (L2 * a) let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: ((L1 + L2) * a) . v = ((L1 * a) + (L2 * a)) . v thus ((L1 + L2) * a) . v = ((L1 + L2) . v) * a by Def10 .= ((L1 . v) + (L2 . v)) * a by Def9 .= ((L1 . v) * a) + ((L2 . v) * a) by VECTSP_1:def_7 .= ((L1 * a) . v) + ((L2 . v) * a) by Def10 .= ((L1 * a) . v) + ((L2 * a) . v) by Def10 .= ((L1 * a) + (L2 * a)) . v by Def9 ; ::_thesis: verum end; theorem Th48: :: RMOD_4:48 for R being Ring for V being RightMod of R for b, a being Scalar of R for L being Linear_Combination of V holds (L * b) * a = L * (b * a) proof let R be Ring; ::_thesis: for V being RightMod of R for b, a being Scalar of R for L being Linear_Combination of V holds (L * b) * a = L * (b * a) let V be RightMod of R; ::_thesis: for b, a being Scalar of R for L being Linear_Combination of V holds (L * b) * a = L * (b * a) let b, a be Scalar of R; ::_thesis: for L being Linear_Combination of V holds (L * b) * a = L * (b * a) let L be Linear_Combination of V; ::_thesis: (L * b) * a = L * (b * a) let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: ((L * b) * a) . v = (L * (b * a)) . v thus ((L * b) * a) . v = ((L * b) . v) * a by Def10 .= ((L . v) * b) * a by Def10 .= (L . v) * (b * a) by GROUP_1:def_3 .= (L * (b * a)) . v by Def10 ; ::_thesis: verum end; theorem :: RMOD_4:49 for R being Ring for V being RightMod of R for L being Linear_Combination of V holds L * (1_ R) = L proof let R be Ring; ::_thesis: for V being RightMod of R for L being Linear_Combination of V holds L * (1_ R) = L let V be RightMod of R; ::_thesis: for L being Linear_Combination of V holds L * (1_ R) = L let L be Linear_Combination of V; ::_thesis: L * (1_ R) = L let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: (L * (1_ R)) . v = L . v thus (L * (1_ R)) . v = (L . v) * (1_ R) by Def10 .= L . v by VECTSP_1:def_4 ; ::_thesis: verum end; definition let R be Ring; let V be RightMod of R; let L be Linear_Combination of V; func - L -> Linear_Combination of V equals :: RMOD_4:def 11 L * (- (1_ R)); correctness coherence L * (- (1_ R)) is Linear_Combination of V; ; involutiveness for b1, b2 being Linear_Combination of V st b1 = b2 * (- (1_ R)) holds b2 = b1 * (- (1_ R)) proof let L, L9 be Linear_Combination of V; ::_thesis: ( L = L9 * (- (1_ R)) implies L9 = L * (- (1_ R)) ) assume A1: L = L9 * (- (1_ R)) ; ::_thesis: L9 = L * (- (1_ R)) let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: L9 . v = (L * (- (1_ R))) . v thus L9 . v = (L9 . v) * (1_ R) by VECTSP_1:def_4 .= (L9 . v) * ((1_ R) * (1_ R)) by VECTSP_1:def_4 .= (L9 . v) * ((- (1_ R)) * (- (1_ R))) by VECTSP_1:10 .= (L9 * ((- (1_ R)) * (- (1_ R)))) . v by Def10 .= (L * (- (1_ R))) . v by A1, Th48 ; ::_thesis: verum end; end; :: deftheorem defines - RMOD_4:def_11_:_ for R being Ring for V being RightMod of R for L being Linear_Combination of V holds - L = L * (- (1_ R)); theorem Th50: :: RMOD_4:50 for R being Ring for V being RightMod of R for v being Vector of V for L being Linear_Combination of V holds (- L) . v = - (L . v) proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for L being Linear_Combination of V holds (- L) . v = - (L . v) let V be RightMod of R; ::_thesis: for v being Vector of V for L being Linear_Combination of V holds (- L) . v = - (L . v) let v be Vector of V; ::_thesis: for L being Linear_Combination of V holds (- L) . v = - (L . v) let L be Linear_Combination of V; ::_thesis: (- L) . v = - (L . v) thus (- L) . v = (L . v) * (- (1_ R)) by Def10 .= - (L . v) by VECTSP_2:28 ; ::_thesis: verum end; theorem :: RMOD_4:51 for R being Ring for V being RightMod of R for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds L2 = - L1 proof let R be Ring; ::_thesis: for V being RightMod of R for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds L2 = - L1 let V be RightMod of R; ::_thesis: for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds L2 = - L1 let L1, L2 be Linear_Combination of V; ::_thesis: ( L1 + L2 = ZeroLC V implies L2 = - L1 ) assume A1: L1 + L2 = ZeroLC V ; ::_thesis: L2 = - L1 let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: L2 . v = (- L1) . v (L1 . v) + (L2 . v) = (ZeroLC V) . v by A1, Def9 .= 0. R by Th18 ; hence L2 . v = - (L1 . v) by RLVECT_1:6 .= (- L1) . v by Th50 ; ::_thesis: verum end; theorem Th52: :: RMOD_4:52 for R being Ring for V being RightMod of R for L being Linear_Combination of V holds Carrier (- L) = Carrier L proof let R be Ring; ::_thesis: for V being RightMod of R for L being Linear_Combination of V holds Carrier (- L) = Carrier L let V be RightMod of R; ::_thesis: for L being Linear_Combination of V holds Carrier (- L) = Carrier L let L be Linear_Combination of V; ::_thesis: Carrier (- L) = Carrier L set a = - (1_ R); Carrier (L * (- (1_ R))) = Carrier L proof set S = { v where v is Vector of V : L . v <> 0. R } ; set T = { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } ; { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } = { v where v is Vector of V : L . v <> 0. R } proof thus { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } c= { v where v is Vector of V : L . v <> 0. R } :: according to XBOOLE_0:def_10 ::_thesis: { v where v is Vector of V : L . v <> 0. R } c= { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } or x in { v where v is Vector of V : L . v <> 0. R } ) assume x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } ; ::_thesis: x in { v where v is Vector of V : L . v <> 0. R } then consider u being Vector of V such that A1: x = u and A2: (L * (- (1_ R))) . u <> 0. R ; (L * (- (1_ R))) . u = (L . u) * (- (1_ R)) by Def10; then L . u <> 0. R by A2, VECTSP_1:7; hence x in { v where v is Vector of V : L . v <> 0. R } by A1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Vector of V : L . v <> 0. R } or x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } ) assume x in { v where v is Vector of V : L . v <> 0. R } ; ::_thesis: x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } then consider v being Vector of V such that A3: x = v and A4: L . v <> 0. R ; (L * (- (1_ R))) . v = (L . v) * (- (1_ R)) by Def10 .= - (L . v) by VECTSP_2:28 ; then (L * (- (1_ R))) . v <> 0. R by A4, VECTSP_2:3; hence x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } by A3; ::_thesis: verum end; hence Carrier (L * (- (1_ R))) = Carrier L ; ::_thesis: verum end; hence Carrier (- L) = Carrier L ; ::_thesis: verum end; theorem :: RMOD_4:53 for R being Ring for V being RightMod of R for A being Subset of V for L being Linear_Combination of V st L is Linear_Combination of A holds - L is Linear_Combination of A by Th45; definition let R be Ring; let V be RightMod of R; let L1, L2 be Linear_Combination of V; funcL1 - L2 -> Linear_Combination of V equals :: RMOD_4:def 12 L1 + (- L2); correctness coherence L1 + (- L2) is Linear_Combination of V; ; end; :: deftheorem defines - RMOD_4:def_12_:_ for R being Ring for V being RightMod of R for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2); theorem Th54: :: RMOD_4:54 for R being Ring for V being RightMod of R for v being Vector of V for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) let V be RightMod of R; ::_thesis: for v being Vector of V for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) let v be Vector of V; ::_thesis: for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) let L1, L2 be Linear_Combination of V; ::_thesis: (L1 - L2) . v = (L1 . v) - (L2 . v) thus (L1 - L2) . v = (L1 . v) + ((- L2) . v) by Def9 .= (L1 . v) + (- (L2 . v)) by Th50 .= (L1 . v) - (L2 . v) by RLVECT_1:def_11 ; ::_thesis: verum end; theorem :: RMOD_4:55 for R being Ring for V being RightMod of R for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) proof let R be Ring; ::_thesis: for V being RightMod of R for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) let V be RightMod of R; ::_thesis: for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) let L1, L2 be Linear_Combination of V; ::_thesis: Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier (- L2)) by Th37; hence Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) by Th52; ::_thesis: verum end; theorem :: RMOD_4:56 for R being Ring for V being RightMod of R for A being Subset of V for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds L1 - L2 is Linear_Combination of A proof let R be Ring; ::_thesis: for V being RightMod of R for A being Subset of V for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds L1 - L2 is Linear_Combination of A let V be RightMod of R; ::_thesis: for A being Subset of V for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds L1 - L2 is Linear_Combination of A let A be Subset of V; ::_thesis: for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds L1 - L2 is Linear_Combination of A let L1, L2 be Linear_Combination of V; ::_thesis: ( L1 is Linear_Combination of A & L2 is Linear_Combination of A implies L1 - L2 is Linear_Combination of A ) assume that A1: L1 is Linear_Combination of A and A2: L2 is Linear_Combination of A ; ::_thesis: L1 - L2 is Linear_Combination of A - L2 is Linear_Combination of A by A2, Th45; hence L1 - L2 is Linear_Combination of A by A1, Th38; ::_thesis: verum end; theorem :: RMOD_4:57 for R being Ring for V being RightMod of R for L being Linear_Combination of V holds L - L = ZeroLC V proof let R be Ring; ::_thesis: for V being RightMod of R for L being Linear_Combination of V holds L - L = ZeroLC V let V be RightMod of R; ::_thesis: for L being Linear_Combination of V holds L - L = ZeroLC V let L be Linear_Combination of V; ::_thesis: L - L = ZeroLC V let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: (L - L) . v = (ZeroLC V) . v thus (L - L) . v = (L . v) - (L . v) by Th54 .= 0. R by RLVECT_1:15 .= (ZeroLC V) . v by Th18 ; ::_thesis: verum end; theorem Th58: :: RMOD_4:58 for R being Ring for V being RightMod of R for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2) proof let R be Ring; ::_thesis: for V being RightMod of R for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2) let V be RightMod of R; ::_thesis: for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2) let L1, L2 be Linear_Combination of V; ::_thesis: Sum (L1 + L2) = (Sum L1) + (Sum L2) set A = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2); set C1 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1); consider p being FinSequence such that A1: rng p = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) and A2: p is one-to-one by FINSEQ_4:58; reconsider p = p as FinSequence of V by A1, FINSEQ_1:def_4; A3: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier L1) \/ ((Carrier (L1 + L2)) \/ (Carrier L2)) by XBOOLE_1:4; set C3 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)); consider r being FinSequence such that A4: rng r = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) and A5: r is one-to-one by FINSEQ_4:58; reconsider r = r as FinSequence of V by A4, FINSEQ_1:def_4; A6: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier (L1 + L2)) \/ ((Carrier L1) \/ (Carrier L2)) by XBOOLE_1:4; set C2 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2); consider q being FinSequence such that A7: rng q = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) and A8: q is one-to-one by FINSEQ_4:58; reconsider q = q as FinSequence of V by A7, FINSEQ_1:def_4; consider F being FinSequence of V such that A9: F is one-to-one and A10: rng F = Carrier (L1 + L2) and A11: Sum ((L1 + L2) (#) F) = Sum (L1 + L2) by Def7; set FF = F ^ r; consider G being FinSequence of V such that A12: G is one-to-one and A13: rng G = Carrier L1 and A14: Sum (L1 (#) G) = Sum L1 by Def7; rng (F ^ r) = (rng F) \/ (rng r) by FINSEQ_1:31; then rng (F ^ r) = (Carrier (L1 + L2)) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A10, A4, XBOOLE_1:39; then A15: rng (F ^ r) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by A6, XBOOLE_1:7, XBOOLE_1:12; set GG = G ^ p; rng (G ^ p) = (rng G) \/ (rng p) by FINSEQ_1:31; then rng (G ^ p) = (Carrier L1) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A13, A1, XBOOLE_1:39; then A16: rng (G ^ p) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by A3, XBOOLE_1:7, XBOOLE_1:12; rng F misses rng r proof set x = the Element of (rng F) /\ (rng r); assume not rng F misses rng r ; ::_thesis: contradiction then (rng F) /\ (rng r) <> {} by XBOOLE_0:def_7; then ( the Element of (rng F) /\ (rng r) in Carrier (L1 + L2) & the Element of (rng F) /\ (rng r) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) ) by A10, A4, XBOOLE_0:def_4; hence contradiction by XBOOLE_0:def_5; ::_thesis: verum end; then A17: F ^ r is one-to-one by A9, A5, FINSEQ_3:91; rng G misses rng p proof set x = the Element of (rng G) /\ (rng p); assume not rng G misses rng p ; ::_thesis: contradiction then (rng G) /\ (rng p) <> {} by XBOOLE_0:def_7; then ( the Element of (rng G) /\ (rng p) in Carrier L1 & the Element of (rng G) /\ (rng p) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) ) by A13, A1, XBOOLE_0:def_4; hence contradiction by XBOOLE_0:def_5; ::_thesis: verum end; then A18: G ^ p is one-to-one by A12, A2, FINSEQ_3:91; then A19: len (G ^ p) = len (F ^ r) by A17, A16, A15, FINSEQ_1:48; deffunc H1( Nat) -> set = (F ^ r) <- ((G ^ p) . $1); consider P being FinSequence such that A20: len P = len (F ^ r) and A21: for k being Nat st k in dom P holds P . k = H1(k) from FINSEQ_1:sch_2(); A22: dom P = Seg (len (F ^ r)) by A20, FINSEQ_1:def_3; A23: now__::_thesis:_for_x_being_set_st_x_in_dom_(G_^_p)_holds_ (G_^_p)_._x_=_(F_^_r)_._(P_._x) let x be set ; ::_thesis: ( x in dom (G ^ p) implies (G ^ p) . x = (F ^ r) . (P . x) ) assume A24: x in dom (G ^ p) ; ::_thesis: (G ^ p) . x = (F ^ r) . (P . x) then reconsider n = x as Nat by FINSEQ_3:23; (G ^ p) . n in rng (F ^ r) by A16, A15, A24, FUNCT_1:def_3; then A25: F ^ r just_once_values (G ^ p) . n by A17, FINSEQ_4:8; n in Seg (len (F ^ r)) by A19, A24, FINSEQ_1:def_3; then (F ^ r) . (P . n) = (F ^ r) . ((F ^ r) <- ((G ^ p) . n)) by A21, A22 .= (G ^ p) . n by A25, FINSEQ_4:def_3 ; hence (G ^ p) . x = (F ^ r) . (P . x) ; ::_thesis: verum end; A26: dom (G ^ p) = dom (F ^ r) by A19, FINSEQ_3:29; A27: rng P c= dom (F ^ r) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng P or x in dom (F ^ r) ) assume x in rng P ; ::_thesis: x in dom (F ^ r) then consider y being set such that A28: y in dom P and A29: P . y = x by FUNCT_1:def_3; reconsider y = y as Nat by A28, FINSEQ_3:23; y in dom (F ^ r) by A20, A28, FINSEQ_3:29; then (G ^ p) . y in rng (F ^ r) by A16, A15, A26, FUNCT_1:def_3; then A30: F ^ r just_once_values (G ^ p) . y by A17, FINSEQ_4:8; P . y = (F ^ r) <- ((G ^ p) . y) by A21, A28; hence x in dom (F ^ r) by A29, A30, FINSEQ_4:def_3; ::_thesis: verum end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_(G_^_p)_implies_(_x_in_dom_P_&_P_._x_in_dom_(F_^_r)_)_)_&_(_x_in_dom_P_&_P_._x_in_dom_(F_^_r)_implies_x_in_dom_(G_^_p)_)_) let x be set ; ::_thesis: ( ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) & ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) ) ) thus ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) ::_thesis: ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) ) proof assume x in dom (G ^ p) ; ::_thesis: ( x in dom P & P . x in dom (F ^ r) ) hence x in dom P by A19, A20, FINSEQ_3:29; ::_thesis: P . x in dom (F ^ r) then P . x in rng P by FUNCT_1:def_3; hence P . x in dom (F ^ r) by A27; ::_thesis: verum end; assume that A31: x in dom P and P . x in dom (F ^ r) ; ::_thesis: x in dom (G ^ p) x in Seg (len P) by A31, FINSEQ_1:def_3; hence x in dom (G ^ p) by A19, A20, FINSEQ_1:def_3; ::_thesis: verum end; then A32: G ^ p = (F ^ r) * P by A23, FUNCT_1:10; dom (F ^ r) c= rng P proof set f = ((F ^ r) ") * (G ^ p); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (F ^ r) or x in rng P ) assume A33: x in dom (F ^ r) ; ::_thesis: x in rng P dom ((F ^ r) ") = rng (G ^ p) by A17, A16, A15, FUNCT_1:33; then A34: rng (((F ^ r) ") * (G ^ p)) = rng ((F ^ r) ") by RELAT_1:28 .= dom (F ^ r) by A17, FUNCT_1:33 ; ((F ^ r) ") * (G ^ p) = (((F ^ r) ") * (F ^ r)) * P by A32, RELAT_1:36 .= (id (dom (F ^ r))) * P by A17, FUNCT_1:39 .= P by A27, RELAT_1:53 ; hence x in rng P by A33, A34; ::_thesis: verum end; then A35: dom (F ^ r) = rng P by A27, XBOOLE_0:def_10; A36: len r = len ((L1 + L2) (#) r) by Def6; now__::_thesis:_for_k_being_Nat_st_k_in_dom_r_holds_ ((L1_+_L2)_(#)_r)_._k_=_(r_/._k)_*_(0._R) let k be Nat; ::_thesis: ( k in dom r implies ((L1 + L2) (#) r) . k = (r /. k) * (0. R) ) assume A37: k in dom r ; ::_thesis: ((L1 + L2) (#) r) . k = (r /. k) * (0. R) then r /. k = r . k by PARTFUN1:def_6; then r /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) by A4, A37, FUNCT_1:def_3; then A38: not r /. k in Carrier (L1 + L2) by XBOOLE_0:def_5; k in dom ((L1 + L2) (#) r) by A36, A37, FINSEQ_3:29; then ((L1 + L2) (#) r) . k = (r /. k) * ((L1 + L2) . (r /. k)) by Def6; hence ((L1 + L2) (#) r) . k = (r /. k) * (0. R) by A38; ::_thesis: verum end; then A39: Sum ((L1 + L2) (#) r) = (Sum r) * (0. R) by A36, Lm2 .= 0. V by VECTSP_2:32 ; A40: len p = len (L1 (#) p) by Def6; now__::_thesis:_for_k_being_Nat_st_k_in_dom_p_holds_ (L1_(#)_p)_._k_=_(p_/._k)_*_(0._R) let k be Nat; ::_thesis: ( k in dom p implies (L1 (#) p) . k = (p /. k) * (0. R) ) assume A41: k in dom p ; ::_thesis: (L1 (#) p) . k = (p /. k) * (0. R) then p /. k = p . k by PARTFUN1:def_6; then p /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) by A1, A41, FUNCT_1:def_3; then A42: not p /. k in Carrier L1 by XBOOLE_0:def_5; k in dom (L1 (#) p) by A40, A41, FINSEQ_3:29; then (L1 (#) p) . k = (p /. k) * (L1 . (p /. k)) by Def6; hence (L1 (#) p) . k = (p /. k) * (0. R) by A42; ::_thesis: verum end; then A43: Sum (L1 (#) p) = (Sum p) * (0. R) by A40, Lm2 .= 0. V by VECTSP_2:32 ; set f = (L1 + L2) (#) (F ^ r); consider H being FinSequence of V such that A44: H is one-to-one and A45: rng H = Carrier L2 and A46: Sum (L2 (#) H) = Sum L2 by Def7; set HH = H ^ q; rng H misses rng q proof set x = the Element of (rng H) /\ (rng q); assume not rng H misses rng q ; ::_thesis: contradiction then (rng H) /\ (rng q) <> {} by XBOOLE_0:def_7; then ( the Element of (rng H) /\ (rng q) in Carrier L2 & the Element of (rng H) /\ (rng q) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) ) by A45, A7, XBOOLE_0:def_4; hence contradiction by XBOOLE_0:def_5; ::_thesis: verum end; then A47: H ^ q is one-to-one by A44, A8, FINSEQ_3:91; A48: len q = len (L2 (#) q) by Def6; now__::_thesis:_for_k_being_Nat_st_k_in_dom_q_holds_ (L2_(#)_q)_._k_=_(q_/._k)_*_(0._R) let k be Nat; ::_thesis: ( k in dom q implies (L2 (#) q) . k = (q /. k) * (0. R) ) assume A49: k in dom q ; ::_thesis: (L2 (#) q) . k = (q /. k) * (0. R) then q /. k = q . k by PARTFUN1:def_6; then q /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) by A7, A49, FUNCT_1:def_3; then A50: not q /. k in Carrier L2 by XBOOLE_0:def_5; k in dom (L2 (#) q) by A48, A49, FINSEQ_3:29; then (L2 (#) q) . k = (q /. k) * (L2 . (q /. k)) by Def6; hence (L2 (#) q) . k = (q /. k) * (0. R) by A50; ::_thesis: verum end; then A51: Sum (L2 (#) q) = (Sum q) * (0. R) by A48, Lm2 .= 0. V by VECTSP_2:32 ; set g = L1 (#) (G ^ p); A52: len (L1 (#) (G ^ p)) = len (G ^ p) by Def6; then A53: Seg (len (G ^ p)) = dom (L1 (#) (G ^ p)) by FINSEQ_1:def_3; rng (H ^ q) = (rng H) \/ (rng q) by FINSEQ_1:31; then rng (H ^ q) = (Carrier L2) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A45, A7, XBOOLE_1:39; then A54: rng (H ^ q) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by XBOOLE_1:7, XBOOLE_1:12; then A55: len (G ^ p) = len (H ^ q) by A47, A18, A16, FINSEQ_1:48; deffunc H2( Nat) -> set = (H ^ q) <- ((G ^ p) . $1); consider R being FinSequence such that A56: len R = len (H ^ q) and A57: for k being Nat st k in dom R holds R . k = H2(k) from FINSEQ_1:sch_2(); A58: dom R = Seg (len (H ^ q)) by A56, FINSEQ_1:def_3; A59: now__::_thesis:_for_x_being_set_st_x_in_dom_(G_^_p)_holds_ (G_^_p)_._x_=_(H_^_q)_._(R_._x) let x be set ; ::_thesis: ( x in dom (G ^ p) implies (G ^ p) . x = (H ^ q) . (R . x) ) assume A60: x in dom (G ^ p) ; ::_thesis: (G ^ p) . x = (H ^ q) . (R . x) then reconsider n = x as Nat by FINSEQ_3:23; (G ^ p) . n in rng (H ^ q) by A16, A54, A60, FUNCT_1:def_3; then A61: H ^ q just_once_values (G ^ p) . n by A47, FINSEQ_4:8; n in Seg (len (H ^ q)) by A55, A60, FINSEQ_1:def_3; then (H ^ q) . (R . n) = (H ^ q) . ((H ^ q) <- ((G ^ p) . n)) by A57, A58 .= (G ^ p) . n by A61, FINSEQ_4:def_3 ; hence (G ^ p) . x = (H ^ q) . (R . x) ; ::_thesis: verum end; A62: dom (G ^ p) = dom (H ^ q) by A55, FINSEQ_3:29; A63: rng R c= dom (H ^ q) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng R or x in dom (H ^ q) ) assume x in rng R ; ::_thesis: x in dom (H ^ q) then consider y being set such that A64: y in dom R and A65: R . y = x by FUNCT_1:def_3; reconsider y = y as Nat by A64, FINSEQ_3:23; y in dom (H ^ q) by A56, A64, FINSEQ_3:29; then (G ^ p) . y in rng (H ^ q) by A16, A54, A62, FUNCT_1:def_3; then A66: H ^ q just_once_values (G ^ p) . y by A47, FINSEQ_4:8; R . y = (H ^ q) <- ((G ^ p) . y) by A57, A64; hence x in dom (H ^ q) by A65, A66, FINSEQ_4:def_3; ::_thesis: verum end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_(G_^_p)_implies_(_x_in_dom_R_&_R_._x_in_dom_(H_^_q)_)_)_&_(_x_in_dom_R_&_R_._x_in_dom_(H_^_q)_implies_x_in_dom_(G_^_p)_)_) let x be set ; ::_thesis: ( ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) & ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) ) ) thus ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) ::_thesis: ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) ) proof assume x in dom (G ^ p) ; ::_thesis: ( x in dom R & R . x in dom (H ^ q) ) then x in Seg (len R) by A55, A56, FINSEQ_1:def_3; hence x in dom R by FINSEQ_1:def_3; ::_thesis: R . x in dom (H ^ q) then R . x in rng R by FUNCT_1:def_3; hence R . x in dom (H ^ q) by A63; ::_thesis: verum end; assume that A67: x in dom R and R . x in dom (H ^ q) ; ::_thesis: x in dom (G ^ p) x in Seg (len R) by A67, FINSEQ_1:def_3; hence x in dom (G ^ p) by A55, A56, FINSEQ_1:def_3; ::_thesis: verum end; then A68: G ^ p = (H ^ q) * R by A59, FUNCT_1:10; dom (H ^ q) c= rng R proof set f = ((H ^ q) ") * (G ^ p); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (H ^ q) or x in rng R ) assume A69: x in dom (H ^ q) ; ::_thesis: x in rng R dom ((H ^ q) ") = rng (G ^ p) by A47, A16, A54, FUNCT_1:33; then A70: rng (((H ^ q) ") * (G ^ p)) = rng ((H ^ q) ") by RELAT_1:28 .= dom (H ^ q) by A47, FUNCT_1:33 ; ((H ^ q) ") * (G ^ p) = (((H ^ q) ") * (H ^ q)) * R by A68, RELAT_1:36 .= (id (dom (H ^ q))) * R by A47, FUNCT_1:39 .= R by A63, RELAT_1:53 ; hence x in rng R by A69, A70; ::_thesis: verum end; then A71: dom (H ^ q) = rng R by A63, XBOOLE_0:def_10; A72: Sum (L1 (#) (G ^ p)) = Sum ((L1 (#) G) ^ (L1 (#) p)) by Th28 .= (Sum (L1 (#) G)) + (0. V) by A43, RLVECT_1:41 .= Sum (L1 (#) G) by RLVECT_1:def_4 ; set h = L2 (#) (H ^ q); A73: Sum (L2 (#) (H ^ q)) = Sum ((L2 (#) H) ^ (L2 (#) q)) by Th28 .= (Sum (L2 (#) H)) + (0. V) by A51, RLVECT_1:41 .= Sum (L2 (#) H) by RLVECT_1:def_4 ; A74: Sum ((L1 + L2) (#) (F ^ r)) = Sum (((L1 + L2) (#) F) ^ ((L1 + L2) (#) r)) by Th28 .= (Sum ((L1 + L2) (#) F)) + (0. V) by A39, RLVECT_1:41 .= Sum ((L1 + L2) (#) F) by RLVECT_1:def_4 ; A75: dom P = dom (F ^ r) by A20, FINSEQ_3:29; then A76: P is one-to-one by A35, FINSEQ_4:60; A77: dom R = dom (H ^ q) by A56, FINSEQ_3:29; then A78: R is one-to-one by A71, FINSEQ_4:60; reconsider R = R as Function of (dom (H ^ q)),(dom (H ^ q)) by A63, A77, FUNCT_2:2; A79: len (L2 (#) (H ^ q)) = len (H ^ q) by Def6; then A80: dom (L2 (#) (H ^ q)) = dom (H ^ q) by FINSEQ_3:29; then reconsider R = R as Function of (dom (L2 (#) (H ^ q))),(dom (L2 (#) (H ^ q))) ; reconsider Hp = (L2 (#) (H ^ q)) * R as FinSequence of V by FINSEQ_2:47; reconsider R = R as Permutation of (dom (L2 (#) (H ^ q))) by A71, A78, A80, FUNCT_2:57; A81: Hp = (L2 (#) (H ^ q)) * R ; then A82: len Hp = len (G ^ p) by A55, A79, FINSEQ_2:44; reconsider P = P as Function of (dom (F ^ r)),(dom (F ^ r)) by A27, A75, FUNCT_2:2; A83: len ((L1 + L2) (#) (F ^ r)) = len (F ^ r) by Def6; then A84: dom ((L1 + L2) (#) (F ^ r)) = dom (F ^ r) by FINSEQ_3:29; then reconsider P = P as Function of (dom ((L1 + L2) (#) (F ^ r))),(dom ((L1 + L2) (#) (F ^ r))) ; reconsider Fp = ((L1 + L2) (#) (F ^ r)) * P as FinSequence of V by FINSEQ_2:47; reconsider P = P as Permutation of (dom ((L1 + L2) (#) (F ^ r))) by A35, A76, A84, FUNCT_2:57; A85: Fp = ((L1 + L2) (#) (F ^ r)) * P ; then A86: Sum Fp = Sum ((L1 + L2) (#) (F ^ r)) by RLVECT_2:7; deffunc H3( Nat) -> Element of the carrier of V = ((L1 (#) (G ^ p)) /. $1) + (Hp /. $1); consider I being FinSequence such that A87: len I = len (G ^ p) and A88: for k being Nat st k in dom I holds I . k = H3(k) from FINSEQ_1:sch_2(); A89: dom I = Seg (len (G ^ p)) by A87, FINSEQ_1:def_3; then A90: for k being Element of NAT st k in Seg (len (G ^ p)) holds I . k = H3(k) by A88; rng I c= the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng I or x in the carrier of V ) assume x in rng I ; ::_thesis: x in the carrier of V then consider y being set such that A91: y in dom I and A92: I . y = x by FUNCT_1:def_3; reconsider y = y as Nat by A91, FINSEQ_3:23; I . y = ((L1 (#) (G ^ p)) /. y) + (Hp /. y) by A88, A91; hence x in the carrier of V by A92; ::_thesis: verum end; then reconsider I = I as FinSequence of V by FINSEQ_1:def_4; A93: len Fp = len I by A19, A83, A85, A87, FINSEQ_2:44; A94: now__::_thesis:_for_x_being_set_st_x_in_Seg_(len_I)_holds_ I_._x_=_Fp_._x let x be set ; ::_thesis: ( x in Seg (len I) implies I . x = Fp . x ) assume A95: x in Seg (len I) ; ::_thesis: I . x = Fp . x then reconsider k = x as Element of NAT ; A96: x in dom (H ^ q) by A55, A87, A95, FINSEQ_1:def_3; then R . k in dom R by A71, A77, FUNCT_1:def_3; then reconsider j = R . k as Nat by FINSEQ_3:23; A97: x in dom (G ^ p) by A87, A95, FINSEQ_1:def_3; then A98: (H ^ q) . j = (G ^ p) . k by A59 .= (G ^ p) /. k by A97, PARTFUN1:def_6 ; P . k in dom P by A26, A62, A35, A75, A96, FUNCT_1:def_3; then reconsider l = P . k as Nat by FINSEQ_3:23; set v = (G ^ p) /. k; A99: x in dom Fp by A93, A95, FINSEQ_1:def_3; A100: (F ^ r) . l = (G ^ p) . k by A23, A97 .= (G ^ p) /. k by A97, PARTFUN1:def_6 ; P . k in dom (F ^ r) by A26, A62, A35, A75, A96, FUNCT_1:def_3; then A101: ((L1 + L2) (#) (F ^ r)) . l = ((G ^ p) /. k) * ((L1 + L2) . ((G ^ p) /. k)) by A100, Th23 .= ((G ^ p) /. k) * ((L1 . ((G ^ p) /. k)) + (L2 . ((G ^ p) /. k))) by Def9 .= (((G ^ p) /. k) * (L1 . ((G ^ p) /. k))) + (((G ^ p) /. k) * (L2 . ((G ^ p) /. k))) by VECTSP_2:def_9 ; A102: x in dom Hp by A87, A82, A95, FINSEQ_1:def_3; then A103: Hp /. k = ((L2 (#) (H ^ q)) * R) . k by PARTFUN1:def_6 .= (L2 (#) (H ^ q)) . (R . k) by A102, FUNCT_1:12 ; R . k in dom (H ^ q) by A71, A77, A96, FUNCT_1:def_3; then A104: (L2 (#) (H ^ q)) . j = ((G ^ p) /. k) * (L2 . ((G ^ p) /. k)) by A98, Th23; A105: x in dom (L1 (#) (G ^ p)) by A87, A52, A95, FINSEQ_1:def_3; then (L1 (#) (G ^ p)) /. k = (L1 (#) (G ^ p)) . k by PARTFUN1:def_6 .= ((G ^ p) /. k) * (L1 . ((G ^ p) /. k)) by A105, Def6 ; hence I . x = (((G ^ p) /. k) * (L1 . ((G ^ p) /. k))) + (((G ^ p) /. k) * (L2 . ((G ^ p) /. k))) by A87, A88, A89, A95, A103, A104 .= Fp . x by A99, A101, FUNCT_1:12 ; ::_thesis: verum end; ( dom I = Seg (len I) & dom Fp = Seg (len I) ) by A93, FINSEQ_1:def_3; then A106: I = Fp by A94, FUNCT_1:2; Sum Hp = Sum (L2 (#) (H ^ q)) by A81, RLVECT_2:7; hence Sum (L1 + L2) = (Sum L1) + (Sum L2) by A11, A14, A46, A72, A73, A74, A86, A87, A90, A82, A52, A106, A53, RLVECT_2:2; ::_thesis: verum end; theorem Th59: :: RMOD_4:59 for R being domRing for V being RightMod of R for L being Linear_Combination of V for a being Scalar of R holds Sum (L * a) = (Sum L) * a proof let R be domRing; ::_thesis: for V being RightMod of R for L being Linear_Combination of V for a being Scalar of R holds Sum (L * a) = (Sum L) * a let V be RightMod of R; ::_thesis: for L being Linear_Combination of V for a being Scalar of R holds Sum (L * a) = (Sum L) * a let L be Linear_Combination of V; ::_thesis: for a being Scalar of R holds Sum (L * a) = (Sum L) * a let a be Scalar of R; ::_thesis: Sum (L * a) = (Sum L) * a percases ( a <> 0. R or a = 0. R ) ; supposeA1: a <> 0. R ; ::_thesis: Sum (L * a) = (Sum L) * a set l = L * a; A2: Carrier (L * a) = Carrier L by A1, Th43; consider G being FinSequence of V such that A3: G is one-to-one and A4: rng G = Carrier L and A5: Sum L = Sum (L (#) G) by Def7; set g = L (#) G; consider F being FinSequence of V such that A6: F is one-to-one and A7: rng F = Carrier (L * a) and A8: Sum (L * a) = Sum ((L * a) (#) F) by Def7; A9: len G = len F by A1, A6, A7, A3, A4, Th43, FINSEQ_1:48; set f = (L * a) (#) F; deffunc H1( Nat) -> set = F <- (G . $1); consider P being FinSequence such that A10: len P = len F and A11: for k being Nat st k in dom P holds P . k = H1(k) from FINSEQ_1:sch_2(); A12: dom P = Seg (len F) by A10, FINSEQ_1:def_3; A13: now__::_thesis:_for_x_being_set_st_x_in_dom_G_holds_ G_._x_=_F_._(P_._x) let x be set ; ::_thesis: ( x in dom G implies G . x = F . (P . x) ) assume A14: x in dom G ; ::_thesis: G . x = F . (P . x) then reconsider n = x as Nat by FINSEQ_3:23; G . n in rng F by A7, A4, A2, A14, FUNCT_1:def_3; then A15: F just_once_values G . n by A6, FINSEQ_4:8; n in Seg (len F) by A9, A14, FINSEQ_1:def_3; then F . (P . n) = F . (F <- (G . n)) by A11, A12 .= G . n by A15, FINSEQ_4:def_3 ; hence G . x = F . (P . x) ; ::_thesis: verum end; A16: rng P c= dom F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng P or x in dom F ) assume x in rng P ; ::_thesis: x in dom F then consider y being set such that A17: y in dom P and A18: P . y = x by FUNCT_1:def_3; reconsider y = y as Nat by A17, FINSEQ_3:23; y in dom G by A10, A9, A17, FINSEQ_3:29; then G . y in rng F by A7, A4, A2, FUNCT_1:def_3; then A19: F just_once_values G . y by A6, FINSEQ_4:8; P . y = F <- (G . y) by A11, A17; hence x in dom F by A18, A19, FINSEQ_4:def_3; ::_thesis: verum end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_G_implies_(_x_in_dom_P_&_P_._x_in_dom_F_)_)_&_(_x_in_dom_P_&_P_._x_in_dom_F_implies_x_in_dom_G_)_) let x be set ; ::_thesis: ( ( x in dom G implies ( x in dom P & P . x in dom F ) ) & ( x in dom P & P . x in dom F implies x in dom G ) ) thus ( x in dom G implies ( x in dom P & P . x in dom F ) ) ::_thesis: ( x in dom P & P . x in dom F implies x in dom G ) proof assume x in dom G ; ::_thesis: ( x in dom P & P . x in dom F ) then x in Seg (len P) by A10, A9, FINSEQ_1:def_3; hence x in dom P by FINSEQ_1:def_3; ::_thesis: P . x in dom F then P . x in rng P by FUNCT_1:def_3; hence P . x in dom F by A16; ::_thesis: verum end; assume that A20: x in dom P and P . x in dom F ; ::_thesis: x in dom G x in Seg (len P) by A20, FINSEQ_1:def_3; hence x in dom G by A10, A9, FINSEQ_1:def_3; ::_thesis: verum end; then A21: G = F * P by A13, FUNCT_1:10; dom F c= rng P proof set f = (F ") * G; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom F or x in rng P ) assume A22: x in dom F ; ::_thesis: x in rng P dom (F ") = rng G by A6, A7, A4, A2, FUNCT_1:33; then A23: rng ((F ") * G) = rng (F ") by RELAT_1:28 .= dom F by A6, FUNCT_1:33 ; (F ") * G = ((F ") * F) * P by A21, RELAT_1:36 .= (id (dom F)) * P by A6, FUNCT_1:39 .= P by A16, RELAT_1:53 ; hence x in rng P by A22, A23; ::_thesis: verum end; then A24: dom F = rng P by A16, XBOOLE_0:def_10; A25: dom P = dom F by A10, FINSEQ_3:29; then A26: P is one-to-one by A24, FINSEQ_4:60; reconsider P = P as Function of (dom F),(dom F) by A16, A25, FUNCT_2:2; A27: len ((L * a) (#) F) = len F by Def6; then A28: dom ((L * a) (#) F) = dom F by FINSEQ_3:29; then reconsider P = P as Function of (dom ((L * a) (#) F)),(dom ((L * a) (#) F)) ; reconsider Fp = ((L * a) (#) F) * P as FinSequence of V by FINSEQ_2:47; reconsider P = P as Permutation of (dom ((L * a) (#) F)) by A24, A26, A28, FUNCT_2:57; A29: Fp = ((L * a) (#) F) * P ; then A30: len Fp = len ((L * a) (#) F) by FINSEQ_2:44; then A31: len Fp = len (L (#) G) by A9, A27, Def6; A32: now__::_thesis:_for_k_being_Nat for_v_being_Vector_of_V_st_k_in_dom_Fp_&_v_=_(L_(#)_G)_._k_holds_ Fp_._k_=_v_*_a let k be Nat; ::_thesis: for v being Vector of V st k in dom Fp & v = (L (#) G) . k holds Fp . k = v * a let v be Vector of V; ::_thesis: ( k in dom Fp & v = (L (#) G) . k implies Fp . k = v * a ) assume that A33: k in dom Fp and A34: v = (L (#) G) . k ; ::_thesis: Fp . k = v * a A35: k in Seg (len (L (#) G)) by A31, A33, FINSEQ_1:def_3; then A36: k in dom P by A10, A27, A30, A31, FINSEQ_1:def_3; A37: k in dom G by A9, A27, A30, A31, A35, FINSEQ_1:def_3; then G . k in rng G by FUNCT_1:def_3; then F just_once_values G . k by A6, A7, A4, A2, FINSEQ_4:8; then A38: F <- (G . k) in dom F by FINSEQ_4:def_3; then reconsider i = F <- (G . k) as Nat by FINSEQ_3:23; A39: G /. k = G . k by A37, PARTFUN1:def_6 .= F . (P . k) by A21, A36, FUNCT_1:13 .= F . i by A11, A12, A27, A30, A31, A35 .= F /. i by A38, PARTFUN1:def_6 ; A40: k in dom (L (#) G) by A35, FINSEQ_1:def_3; i in Seg (len ((L * a) (#) F)) by A27, A38, FINSEQ_1:def_3; then A41: i in dom ((L * a) (#) F) by FINSEQ_1:def_3; thus Fp . k = ((L * a) (#) F) . (P . k) by A36, FUNCT_1:13 .= ((L * a) (#) F) . (F <- (G . k)) by A11, A12, A27, A30, A31, A35 .= (F /. i) * ((L * a) . (F /. i)) by A41, Def6 .= (F /. i) * ((L . (F /. i)) * a) by Def10 .= ((F /. i) * (L . (F /. i))) * a by VECTSP_2:def_9 .= v * a by A34, A40, A39, Def6 ; ::_thesis: verum end; Sum Fp = Sum ((L * a) (#) F) by A29, RLVECT_2:7; hence Sum (L * a) = (Sum L) * a by A8, A5, A31, A32, Th1; ::_thesis: verum end; supposeA42: a = 0. R ; ::_thesis: Sum (L * a) = (Sum L) * a hence Sum (L * a) = Sum (ZeroLC V) by Th44 .= 0. V by Lm3 .= (Sum L) * a by A42, VECTSP_2:32 ; ::_thesis: verum end; end; end; theorem Th60: :: RMOD_4:60 for R being domRing for V being RightMod of R for L being Linear_Combination of V holds Sum (- L) = - (Sum L) proof let R be domRing; ::_thesis: for V being RightMod of R for L being Linear_Combination of V holds Sum (- L) = - (Sum L) let V be RightMod of R; ::_thesis: for L being Linear_Combination of V holds Sum (- L) = - (Sum L) let L be Linear_Combination of V; ::_thesis: Sum (- L) = - (Sum L) thus Sum (- L) = (Sum L) * (- (1_ R)) by Th59 .= - (Sum L) by VECTSP_2:32 ; ::_thesis: verum end; theorem :: RMOD_4:61 for R being domRing for V being RightMod of R for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2) proof let R be domRing; ::_thesis: for V being RightMod of R for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2) let V be RightMod of R; ::_thesis: for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2) let L1, L2 be Linear_Combination of V; ::_thesis: Sum (L1 - L2) = (Sum L1) - (Sum L2) thus Sum (L1 - L2) = (Sum L1) + (Sum (- L2)) by Th58 .= (Sum L1) + (- (Sum L2)) by Th60 .= (Sum L1) - (Sum L2) by RLVECT_1:def_11 ; ::_thesis: verum end; begin definition let R be Ring; let V be RightMod of R; let IT be Subset of V; attrIT is linearly-independent means :Def13: :: RMOD_4:def 13 for l being Linear_Combination of IT st Sum l = 0. V holds Carrier l = {} ; end; :: deftheorem Def13 defines linearly-independent RMOD_4:def_13_:_ for R being Ring for V being RightMod of R for IT being Subset of V holds ( IT is linearly-independent iff for l being Linear_Combination of IT st Sum l = 0. V holds Carrier l = {} ); notation let R be Ring; let V be RightMod of R; let IT be Subset of V; antonym linearly-dependent IT for linearly-independent ; end; theorem :: RMOD_4:62 for R being Ring for V being RightMod of R for A, B being Subset of V st A c= B & B is linearly-independent holds A is linearly-independent proof let R be Ring; ::_thesis: for V being RightMod of R for A, B being Subset of V st A c= B & B is linearly-independent holds A is linearly-independent let V be RightMod of R; ::_thesis: for A, B being Subset of V st A c= B & B is linearly-independent holds A is linearly-independent let A, B be Subset of V; ::_thesis: ( A c= B & B is linearly-independent implies A is linearly-independent ) assume that A1: A c= B and A2: B is linearly-independent ; ::_thesis: A is linearly-independent let l be Linear_Combination of A; :: according to RMOD_4:def_13 ::_thesis: ( Sum l = 0. V implies Carrier l = {} ) reconsider L = l as Linear_Combination of B by A1, Th19; assume Sum l = 0. V ; ::_thesis: Carrier l = {} then Carrier L = {} by A2, Def13; hence Carrier l = {} ; ::_thesis: verum end; theorem Th63: :: RMOD_4:63 for R being Ring for V being RightMod of R for A being Subset of V st 0. R <> 1_ R & A is linearly-independent holds not 0. V in A proof let R be Ring; ::_thesis: for V being RightMod of R for A being Subset of V st 0. R <> 1_ R & A is linearly-independent holds not 0. V in A let V be RightMod of R; ::_thesis: for A being Subset of V st 0. R <> 1_ R & A is linearly-independent holds not 0. V in A let A be Subset of V; ::_thesis: ( 0. R <> 1_ R & A is linearly-independent implies not 0. V in A ) assume that A1: 0. R <> 1_ R and A2: A is linearly-independent and A3: 0. V in A ; ::_thesis: contradiction deffunc H1( Element of V) -> Element of the carrier of R = 0. R; consider f being Function of the carrier of V, the carrier of R such that A4: f . (0. V) = 1_ R and A5: for v being Element of V st v <> 0. V holds f . v = H1(v) from FUNCT_2:sch_6(); reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8; ex T being finite Subset of V st for v being Vector of V st not v in T holds f . v = 0. R proof take T = {(0. V)}; ::_thesis: for v being Vector of V st not v in T holds f . v = 0. R let v be Vector of V; ::_thesis: ( not v in T implies f . v = 0. R ) assume not v in T ; ::_thesis: f . v = 0. R then v <> 0. V by TARSKI:def_1; hence f . v = 0. R by A5; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def2; A6: Carrier f = {(0. V)} proof thus Carrier f c= {(0. V)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. V)} c= Carrier f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {(0. V)} ) assume x in Carrier f ; ::_thesis: x in {(0. V)} then consider v being Vector of V such that A7: v = x and A8: f . v <> 0. R ; v = 0. V by A5, A8; hence x in {(0. V)} by A7, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. V)} or x in Carrier f ) assume x in {(0. V)} ; ::_thesis: x in Carrier f then x = 0. V by TARSKI:def_1; hence x in Carrier f by A1, A4; ::_thesis: verum end; then Carrier f c= A by A3, ZFMISC_1:31; then reconsider f = f as Linear_Combination of A by Def5; Sum f = (0. V) * (f . (0. V)) by A6, Th35 .= 0. V by VECTSP_2:32 ; hence contradiction by A2, A6, Def13; ::_thesis: verum end; theorem :: RMOD_4:64 for R being Ring for V being RightMod of R holds {} the carrier of V is linearly-independent proof let R be Ring; ::_thesis: for V being RightMod of R holds {} the carrier of V is linearly-independent let V be RightMod of R; ::_thesis: {} the carrier of V is linearly-independent let l be Linear_Combination of {} the carrier of V; :: according to RMOD_4:def_13 ::_thesis: ( Sum l = 0. V implies Carrier l = {} ) Carrier l c= {} by Def5; hence ( Sum l = 0. V implies Carrier l = {} ) ; ::_thesis: verum end; theorem Th65: :: RMOD_4:65 for R being Ring for V being RightMod of R for v1, v2 being Vector of V st 0. R <> 1_ R & {v1,v2} is linearly-independent holds ( v1 <> 0. V & v2 <> 0. V ) proof let R be Ring; ::_thesis: for V being RightMod of R for v1, v2 being Vector of V st 0. R <> 1_ R & {v1,v2} is linearly-independent holds ( v1 <> 0. V & v2 <> 0. V ) let V be RightMod of R; ::_thesis: for v1, v2 being Vector of V st 0. R <> 1_ R & {v1,v2} is linearly-independent holds ( v1 <> 0. V & v2 <> 0. V ) let v1, v2 be Vector of V; ::_thesis: ( 0. R <> 1_ R & {v1,v2} is linearly-independent implies ( v1 <> 0. V & v2 <> 0. V ) ) A1: ( v1 in {v1,v2} & v2 in {v1,v2} ) by TARSKI:def_2; assume ( 0. R <> 1_ R & {v1,v2} is linearly-independent ) ; ::_thesis: ( v1 <> 0. V & v2 <> 0. V ) hence ( v1 <> 0. V & v2 <> 0. V ) by A1, Th63; ::_thesis: verum end; theorem :: RMOD_4:66 for R being Ring for V being RightMod of R for v being Vector of V st 0. R <> 1_ R holds ( {v,(0. V)} is linearly-dependent & {(0. V),v} is linearly-dependent ) by Th65; definition let R be domRing; let V be RightMod of R; let A be Subset of V; func Lin A -> strict Submodule of V means :Def14: :: RMOD_4:def 14 the carrier of it = { (Sum l) where l is Linear_Combination of A : verum } ; existence ex b1 being strict Submodule of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } proof set A1 = { (Sum l) where l is Linear_Combination of A : verum } ; reconsider l = ZeroLC V as Linear_Combination of A by Th20; { (Sum l) where l is Linear_Combination of A : verum } c= the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Sum l) where l is Linear_Combination of A : verum } or x in the carrier of V ) assume x in { (Sum l) where l is Linear_Combination of A : verum } ; ::_thesis: x in the carrier of V then ex l being Linear_Combination of A st x = Sum l ; hence x in the carrier of V ; ::_thesis: verum end; then reconsider A1 = { (Sum l) where l is Linear_Combination of A : verum } as Subset of V ; A1: A1 is linearly-closed proof thus for v, u being Vector of V st v in A1 & u in A1 holds v + u in A1 :: according to RMOD_2:def_1 ::_thesis: for b1 being Element of the carrier of R for b2 being Element of the carrier of V holds ( not b2 in A1 or b2 * b1 in A1 ) proof let v, u be Vector of V; ::_thesis: ( v in A1 & u in A1 implies v + u in A1 ) assume that A2: v in A1 and A3: u in A1 ; ::_thesis: v + u in A1 consider l1 being Linear_Combination of A such that A4: v = Sum l1 by A2; consider l2 being Linear_Combination of A such that A5: u = Sum l2 by A3; reconsider f = l1 + l2 as Linear_Combination of A by Th38; v + u = Sum f by A4, A5, Th58; hence v + u in A1 ; ::_thesis: verum end; let a be Scalar of R; ::_thesis: for b1 being Element of the carrier of V holds ( not b1 in A1 or b1 * a in A1 ) let v be Vector of V; ::_thesis: ( not v in A1 or v * a in A1 ) assume v in A1 ; ::_thesis: v * a in A1 then consider l being Linear_Combination of A such that A6: v = Sum l ; reconsider f = l * a as Linear_Combination of A by Th45; v * a = Sum f by A6, Th59; hence v * a in A1 ; ::_thesis: verum end; Sum l = 0. V by Lm3; then 0. V in A1 ; hence ex b1 being strict Submodule of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } by A1, RMOD_2:34; ::_thesis: verum end; uniqueness for b1, b2 being strict Submodule of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } & the carrier of b2 = { (Sum l) where l is Linear_Combination of A : verum } holds b1 = b2 by RMOD_2:29; end; :: deftheorem Def14 defines Lin RMOD_4:def_14_:_ for R being domRing for V being RightMod of R for A being Subset of V for b4 being strict Submodule of V holds ( b4 = Lin A iff the carrier of b4 = { (Sum l) where l is Linear_Combination of A : verum } ); theorem Th67: :: RMOD_4:67 for x being set for R being domRing for V being RightMod of R for A being Subset of V holds ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l ) proof let x be set ; ::_thesis: for R being domRing for V being RightMod of R for A being Subset of V holds ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l ) let R be domRing; ::_thesis: for V being RightMod of R for A being Subset of V holds ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l ) let V be RightMod of R; ::_thesis: for A being Subset of V holds ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l ) let A be Subset of V; ::_thesis: ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l ) thus ( x in Lin A implies ex l being Linear_Combination of A st x = Sum l ) ::_thesis: ( ex l being Linear_Combination of A st x = Sum l implies x in Lin A ) proof assume x in Lin A ; ::_thesis: ex l being Linear_Combination of A st x = Sum l then x in the carrier of (Lin A) by STRUCT_0:def_5; then x in { (Sum l) where l is Linear_Combination of A : verum } by Def14; hence ex l being Linear_Combination of A st x = Sum l ; ::_thesis: verum end; given k being Linear_Combination of A such that A1: x = Sum k ; ::_thesis: x in Lin A x in { (Sum l) where l is Linear_Combination of A : verum } by A1; then x in the carrier of (Lin A) by Def14; hence x in Lin A by STRUCT_0:def_5; ::_thesis: verum end; theorem Th68: :: RMOD_4:68 for x being set for R being domRing for V being RightMod of R for A being Subset of V st x in A holds x in Lin A proof let x be set ; ::_thesis: for R being domRing for V being RightMod of R for A being Subset of V st x in A holds x in Lin A let R be domRing; ::_thesis: for V being RightMod of R for A being Subset of V st x in A holds x in Lin A let V be RightMod of R; ::_thesis: for A being Subset of V st x in A holds x in Lin A let A be Subset of V; ::_thesis: ( x in A implies x in Lin A ) deffunc H1( Element of V) -> Element of the carrier of R = 0. R; assume A1: x in A ; ::_thesis: x in Lin A then reconsider v = x as Vector of V ; consider f being Function of the carrier of V, the carrier of R such that A2: f . v = 1_ R and A3: for u being Vector of V st u <> v holds f . u = H1(u) from FUNCT_2:sch_6(); reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8; ex T being finite Subset of V st for u being Vector of V st not u in T holds f . u = 0. R proof take T = {v}; ::_thesis: for u being Vector of V st not u in T holds f . u = 0. R let u be Vector of V; ::_thesis: ( not u in T implies f . u = 0. R ) assume not u in T ; ::_thesis: f . u = 0. R then u <> v by TARSKI:def_1; hence f . u = 0. R by A3; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def2; A4: Carrier f c= {v} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} ) assume x in Carrier f ; ::_thesis: x in {v} then consider u being Vector of V such that A5: x = u and A6: f . u <> 0. R ; u = v by A3, A6; hence x in {v} by A5, TARSKI:def_1; ::_thesis: verum end; then reconsider f = f as Linear_Combination of {v} by Def5; A7: Sum f = v * (1_ R) by A2, Th32 .= v by VECTSP_2:def_9 ; {v} c= A by A1, ZFMISC_1:31; then Carrier f c= A by A4, XBOOLE_1:1; then reconsider f = f as Linear_Combination of A by Def5; Sum f = v by A7; hence x in Lin A by Th67; ::_thesis: verum end; theorem :: RMOD_4:69 for R being domRing for V being RightMod of R holds Lin ({} the carrier of V) = (0). V proof let R be domRing; ::_thesis: for V being RightMod of R holds Lin ({} the carrier of V) = (0). V let V be RightMod of R; ::_thesis: Lin ({} the carrier of V) = (0). V set A = Lin ({} the carrier of V); now__::_thesis:_for_v_being_Vector_of_V_holds_ (_(_v_in_Lin_({}_the_carrier_of_V)_implies_v_in_(0)._V_)_&_(_v_in_(0)._V_implies_v_in_Lin_({}_the_carrier_of_V)_)_) let v be Vector of V; ::_thesis: ( ( v in Lin ({} the carrier of V) implies v in (0). V ) & ( v in (0). V implies v in Lin ({} the carrier of V) ) ) thus ( v in Lin ({} the carrier of V) implies v in (0). V ) ::_thesis: ( v in (0). V implies v in Lin ({} the carrier of V) ) proof assume v in Lin ({} the carrier of V) ; ::_thesis: v in (0). V then A1: v in the carrier of (Lin ({} the carrier of V)) by STRUCT_0:def_5; the carrier of (Lin ({} the carrier of V)) = { (Sum l0) where l0 is Linear_Combination of {} the carrier of V : verum } by Def14; then ex l0 being Linear_Combination of {} the carrier of V st v = Sum l0 by A1; then v = 0. V by Th31; hence v in (0). V by RMOD_2:35; ::_thesis: verum end; assume v in (0). V ; ::_thesis: v in Lin ({} the carrier of V) then v = 0. V by RMOD_2:35; hence v in Lin ({} the carrier of V) by RMOD_2:17; ::_thesis: verum end; hence Lin ({} the carrier of V) = (0). V by RMOD_2:30; ::_thesis: verum end; theorem :: RMOD_4:70 for R being domRing for V being RightMod of R for A being Subset of V holds ( not Lin A = (0). V or A = {} or A = {(0. V)} ) proof let R be domRing; ::_thesis: for V being RightMod of R for A being Subset of V holds ( not Lin A = (0). V or A = {} or A = {(0. V)} ) let V be RightMod of R; ::_thesis: for A being Subset of V holds ( not Lin A = (0). V or A = {} or A = {(0. V)} ) let A be Subset of V; ::_thesis: ( not Lin A = (0). V or A = {} or A = {(0. V)} ) assume that A1: Lin A = (0). V and A2: A <> {} ; ::_thesis: A = {(0. V)} thus A c= {(0. V)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. V)} c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in {(0. V)} ) assume x in A ; ::_thesis: x in {(0. V)} then x in Lin A by Th68; then x = 0. V by A1, RMOD_2:35; hence x in {(0. V)} by TARSKI:def_1; ::_thesis: verum end; set y = the Element of A; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. V)} or x in A ) assume x in {(0. V)} ; ::_thesis: x in A then A3: x = 0. V by TARSKI:def_1; ( the Element of A in A & the Element of A in Lin A ) by A2, Th68; hence x in A by A1, A3, RMOD_2:35; ::_thesis: verum end; theorem Th71: :: RMOD_4:71 for R being domRing for V being RightMod of R for A being Subset of V for W being strict Submodule of V st 0. R <> 1_ R & A = the carrier of W holds Lin A = W proof let R be domRing; ::_thesis: for V being RightMod of R for A being Subset of V for W being strict Submodule of V st 0. R <> 1_ R & A = the carrier of W holds Lin A = W let V be RightMod of R; ::_thesis: for A being Subset of V for W being strict Submodule of V st 0. R <> 1_ R & A = the carrier of W holds Lin A = W let A be Subset of V; ::_thesis: for W being strict Submodule of V st 0. R <> 1_ R & A = the carrier of W holds Lin A = W let W be strict Submodule of V; ::_thesis: ( 0. R <> 1_ R & A = the carrier of W implies Lin A = W ) assume that A1: 0. R <> 1_ R and A2: A = the carrier of W ; ::_thesis: Lin A = W now__::_thesis:_for_v_being_Vector_of_V_holds_ (_(_v_in_Lin_A_implies_v_in_W_)_&_(_v_in_W_implies_v_in_Lin_A_)_) let v be Vector of V; ::_thesis: ( ( v in Lin A implies v in W ) & ( v in W implies v in Lin A ) ) thus ( v in Lin A implies v in W ) ::_thesis: ( v in W implies v in Lin A ) proof assume v in Lin A ; ::_thesis: v in W then A3: ex l being Linear_Combination of A st v = Sum l by Th67; A is linearly-closed by A2, RMOD_2:33; then v in the carrier of W by A1, A2, A3, Th29; hence v in W by STRUCT_0:def_5; ::_thesis: verum end; ( v in W iff v in the carrier of W ) by STRUCT_0:def_5; hence ( v in W implies v in Lin A ) by A2, Th68; ::_thesis: verum end; hence Lin A = W by RMOD_2:30; ::_thesis: verum end; theorem :: RMOD_4:72 for R being domRing for V being strict RightMod of R for A being Subset of V st 0. R <> 1_ R & A = the carrier of V holds Lin A = V proof let R be domRing; ::_thesis: for V being strict RightMod of R for A being Subset of V st 0. R <> 1_ R & A = the carrier of V holds Lin A = V let V be strict RightMod of R; ::_thesis: for A being Subset of V st 0. R <> 1_ R & A = the carrier of V holds Lin A = V let A be Subset of V; ::_thesis: ( 0. R <> 1_ R & A = the carrier of V implies Lin A = V ) assume A1: 0. R <> 1_ R ; ::_thesis: ( not A = the carrier of V or Lin A = V ) assume A2: A = the carrier of V ; ::_thesis: Lin A = V (Omega). V = V ; hence Lin A = V by A1, A2, Th71; ::_thesis: verum end; theorem Th73: :: RMOD_4:73 for R being domRing for V being RightMod of R for A, B being Subset of V st A c= B holds Lin A is Submodule of Lin B proof let R be domRing; ::_thesis: for V being RightMod of R for A, B being Subset of V st A c= B holds Lin A is Submodule of Lin B let V be RightMod of R; ::_thesis: for A, B being Subset of V st A c= B holds Lin A is Submodule of Lin B let A, B be Subset of V; ::_thesis: ( A c= B implies Lin A is Submodule of Lin B ) assume A1: A c= B ; ::_thesis: Lin A is Submodule of Lin B now__::_thesis:_for_v_being_Vector_of_V_st_v_in_Lin_A_holds_ v_in_Lin_B let v be Vector of V; ::_thesis: ( v in Lin A implies v in Lin B ) assume v in Lin A ; ::_thesis: v in Lin B then consider l being Linear_Combination of A such that A2: v = Sum l by Th67; reconsider l = l as Linear_Combination of B by A1, Th19; Sum l = v by A2; hence v in Lin B by Th67; ::_thesis: verum end; hence Lin A is Submodule of Lin B by RMOD_2:28; ::_thesis: verum end; theorem :: RMOD_4:74 for R being domRing for V being strict RightMod of R for A, B being Subset of V st Lin A = V & A c= B holds Lin B = V proof let R be domRing; ::_thesis: for V being strict RightMod of R for A, B being Subset of V st Lin A = V & A c= B holds Lin B = V let V be strict RightMod of R; ::_thesis: for A, B being Subset of V st Lin A = V & A c= B holds Lin B = V let A, B be Subset of V; ::_thesis: ( Lin A = V & A c= B implies Lin B = V ) assume ( Lin A = V & A c= B ) ; ::_thesis: Lin B = V then V is Submodule of Lin B by Th73; hence Lin B = V by RMOD_2:25; ::_thesis: verum end; theorem :: RMOD_4:75 for R being domRing for V being RightMod of R for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B) proof let R be domRing; ::_thesis: for V being RightMod of R for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B) let V be RightMod of R; ::_thesis: for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B) let A, B be Subset of V; ::_thesis: Lin (A \/ B) = (Lin A) + (Lin B) now__::_thesis:_for_v_being_Vector_of_V_st_v_in_Lin_(A_\/_B)_holds_ v_in_(Lin_A)_+_(Lin_B) deffunc H1( set ) -> Element of the carrier of R = 0. R; let v be Vector of V; ::_thesis: ( v in Lin (A \/ B) implies v in (Lin A) + (Lin B) ) assume v in Lin (A \/ B) ; ::_thesis: v in (Lin A) + (Lin B) then consider l being Linear_Combination of A \/ B such that A1: v = Sum l by Th67; deffunc H2( set ) -> set = l . $1; set D = (Carrier l) \ A; set C = (Carrier l) /\ A; defpred S1[ set ] means $1 in (Carrier l) /\ A; defpred S2[ set ] means $1 in (Carrier l) \ A; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_ (_(_x_in_(Carrier_l)_/\_A_implies_l_._x_in_the_carrier_of_R_)_&_(_not_x_in_(Carrier_l)_/\_A_implies_0._R_in_the_carrier_of_R_)_) let x be set ; ::_thesis: ( x in the carrier of V implies ( ( x in (Carrier l) /\ A implies l . x in the carrier of R ) & ( not x in (Carrier l) /\ A implies 0. R in the carrier of R ) ) ) assume x in the carrier of V ; ::_thesis: ( ( x in (Carrier l) /\ A implies l . x in the carrier of R ) & ( not x in (Carrier l) /\ A implies 0. R in the carrier of R ) ) then reconsider v = x as Vector of V ; for f being Function of the carrier of V, the carrier of R holds f . v in the carrier of R ; hence ( x in (Carrier l) /\ A implies l . x in the carrier of R ) ; ::_thesis: ( not x in (Carrier l) /\ A implies 0. R in the carrier of R ) assume not x in (Carrier l) /\ A ; ::_thesis: 0. R in the carrier of R thus 0. R in the carrier of R ; ::_thesis: verum end; then A2: for x being set st x in the carrier of V holds ( ( S1[x] implies H2(x) in the carrier of R ) & ( not S1[x] implies H1(x) in the carrier of R ) ) ; consider f being Function of the carrier of V, the carrier of R such that A3: for x being set st x in the carrier of V holds ( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from FUNCT_2:sch_5(A2); reconsider C = (Carrier l) /\ A as finite Subset of V ; reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8; for u being Vector of V st not u in C holds f . u = 0. R by A3; then reconsider f = f as Linear_Combination of V by Def2; A4: Carrier f c= C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in C ) assume x in Carrier f ; ::_thesis: x in C then A5: ex u being Vector of V st ( x = u & f . u <> 0. R ) ; assume not x in C ; ::_thesis: contradiction hence contradiction by A3, A5; ::_thesis: verum end; C c= A by XBOOLE_1:17; then Carrier f c= A by A4, XBOOLE_1:1; then reconsider f = f as Linear_Combination of A by Def5; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_ (_(_x_in_(Carrier_l)_\_A_implies_l_._x_in_the_carrier_of_R_)_&_(_not_x_in_(Carrier_l)_\_A_implies_0._R_in_the_carrier_of_R_)_) let x be set ; ::_thesis: ( x in the carrier of V implies ( ( x in (Carrier l) \ A implies l . x in the carrier of R ) & ( not x in (Carrier l) \ A implies 0. R in the carrier of R ) ) ) assume x in the carrier of V ; ::_thesis: ( ( x in (Carrier l) \ A implies l . x in the carrier of R ) & ( not x in (Carrier l) \ A implies 0. R in the carrier of R ) ) then reconsider v = x as Vector of V ; for g being Function of the carrier of V, the carrier of R holds g . v in the carrier of R ; hence ( x in (Carrier l) \ A implies l . x in the carrier of R ) ; ::_thesis: ( not x in (Carrier l) \ A implies 0. R in the carrier of R ) assume not x in (Carrier l) \ A ; ::_thesis: 0. R in the carrier of R thus 0. R in the carrier of R ; ::_thesis: verum end; then A6: for x being set st x in the carrier of V holds ( ( S2[x] implies H2(x) in the carrier of R ) & ( not S2[x] implies H1(x) in the carrier of R ) ) ; consider g being Function of the carrier of V, the carrier of R such that A7: for x being set st x in the carrier of V holds ( ( S2[x] implies g . x = H2(x) ) & ( not S2[x] implies g . x = H1(x) ) ) from FUNCT_2:sch_5(A6); reconsider D = (Carrier l) \ A as finite Subset of V ; reconsider g = g as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8; for u being Vector of V st not u in D holds g . u = 0. R by A7; then reconsider g = g as Linear_Combination of V by Def2; A8: D c= B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in B ) assume x in D ; ::_thesis: x in B then A9: ( x in Carrier l & not x in A ) by XBOOLE_0:def_5; Carrier l c= A \/ B by Def5; hence x in B by A9, XBOOLE_0:def_3; ::_thesis: verum end; Carrier g c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in D ) assume x in Carrier g ; ::_thesis: x in D then A10: ex u being Vector of V st ( x = u & g . u <> 0. R ) ; assume not x in D ; ::_thesis: contradiction hence contradiction by A7, A10; ::_thesis: verum end; then Carrier g c= B by A8, XBOOLE_1:1; then reconsider g = g as Linear_Combination of B by Def5; l = f + g proof let v be Vector of V; :: according to RMOD_4:def_8 ::_thesis: l . v = (f + g) . v now__::_thesis:_(f_+_g)_._v_=_l_._v percases ( v in C or not v in C ) ; supposeA11: v in C ; ::_thesis: (f + g) . v = l . v A12: now__::_thesis:_not_v_in_D assume v in D ; ::_thesis: contradiction then not v in A by XBOOLE_0:def_5; hence contradiction by A11, XBOOLE_0:def_4; ::_thesis: verum end; thus (f + g) . v = (f . v) + (g . v) by Def9 .= (l . v) + (g . v) by A3, A11 .= (l . v) + (0. R) by A7, A12 .= l . v by RLVECT_1:4 ; ::_thesis: verum end; supposeA13: not v in C ; ::_thesis: l . v = (f + g) . v now__::_thesis:_(f_+_g)_._v_=_l_._v percases ( v in Carrier l or not v in Carrier l ) ; supposeA14: v in Carrier l ; ::_thesis: (f + g) . v = l . v A15: now__::_thesis:_v_in_D assume not v in D ; ::_thesis: contradiction then ( not v in Carrier l or v in A ) by XBOOLE_0:def_5; hence contradiction by A13, A14, XBOOLE_0:def_4; ::_thesis: verum end; thus (f + g) . v = (f . v) + (g . v) by Def9 .= (0. R) + (g . v) by A3, A13 .= g . v by RLVECT_1:4 .= l . v by A7, A15 ; ::_thesis: verum end; supposeA16: not v in Carrier l ; ::_thesis: (f + g) . v = l . v then A17: not v in D by XBOOLE_0:def_5; A18: not v in C by A16, XBOOLE_0:def_4; thus (f + g) . v = (f . v) + (g . v) by Def9 .= (0. R) + (g . v) by A3, A18 .= (0. R) + (0. R) by A7, A17 .= 0. R by RLVECT_1:4 .= l . v by A16 ; ::_thesis: verum end; end; end; hence l . v = (f + g) . v ; ::_thesis: verum end; end; end; hence l . v = (f + g) . v ; ::_thesis: verum end; then A19: v = (Sum f) + (Sum g) by A1, Th58; ( Sum f in Lin A & Sum g in Lin B ) by Th67; hence v in (Lin A) + (Lin B) by A19, RMOD_3:1; ::_thesis: verum end; then A20: Lin (A \/ B) is Submodule of (Lin A) + (Lin B) by RMOD_2:28; ( Lin A is Submodule of Lin (A \/ B) & Lin B is Submodule of Lin (A \/ B) ) by Th73, XBOOLE_1:7; then (Lin A) + (Lin B) is Submodule of Lin (A \/ B) by RMOD_3:35; hence Lin (A \/ B) = (Lin A) + (Lin B) by A20, RMOD_2:25; ::_thesis: verum end; theorem :: RMOD_4:76 for R being domRing for V being RightMod of R for A, B being Subset of V holds Lin (A /\ B) is Submodule of (Lin A) /\ (Lin B) proof let R be domRing; ::_thesis: for V being RightMod of R for A, B being Subset of V holds Lin (A /\ B) is Submodule of (Lin A) /\ (Lin B) let V be RightMod of R; ::_thesis: for A, B being Subset of V holds Lin (A /\ B) is Submodule of (Lin A) /\ (Lin B) let A, B be Subset of V; ::_thesis: Lin (A /\ B) is Submodule of (Lin A) /\ (Lin B) ( Lin (A /\ B) is Submodule of Lin A & Lin (A /\ B) is Submodule of Lin B ) by Th73, XBOOLE_1:17; hence Lin (A /\ B) is Submodule of (Lin A) /\ (Lin B) by RMOD_3:20; ::_thesis: verum end;