:: LMOD_5 semantic presentation begin definition let R be non empty doubleLoopStr ; let V be non empty VectSpStr over R; let IT be Subset of V; attrIT is linearly-independent means :Def1: :: LMOD_5:def 1 for l being Linear_Combination of IT st Sum l = 0. V holds Carrier l = {} ; end; :: deftheorem Def1 defines linearly-independent LMOD_5:def_1_:_ for R being non empty doubleLoopStr for V being non empty VectSpStr over 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 non empty doubleLoopStr ; let V be non empty VectSpStr over R; let IT be Subset of V; antonym linearly-dependent IT for linearly-independent ; end; theorem :: LMOD_5:1 for R being Ring for V being LeftMod 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 LeftMod 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 LeftMod 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 LMOD_5:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} ) reconsider L = l as Linear_Combination of B by A1, VECTSP_6:4; assume Sum l = 0. V ; ::_thesis: Carrier l = {} then Carrier L = {} by A2, Def1; hence Carrier l = {} ; ::_thesis: verum end; theorem Th2: :: LMOD_5:2 for R being Ring for V being LeftMod 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 LeftMod 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 LeftMod 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( set ) -> 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 VECTSP_6:def_1; 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 VECTSP_6:def_4; Sum f = (f . (0. V)) * (0. V) by A6, VECTSP_6:20 .= 0. V by VECTSP_1:14 ; hence contradiction by A2, A6, Def1; ::_thesis: verum end; theorem :: LMOD_5:3 for R being Ring for V being LeftMod of R holds {} the carrier of V is linearly-independent proof let R be Ring; ::_thesis: for V being LeftMod of R holds {} the carrier of V is linearly-independent let V be LeftMod of R; ::_thesis: {} the carrier of V is linearly-independent let l be Linear_Combination of {} the carrier of V; :: according to LMOD_5:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} ) Carrier l c= {} by VECTSP_6:def_4; hence ( Sum l = 0. V implies Carrier l = {} ) ; ::_thesis: verum end; theorem Th4: :: LMOD_5:4 for R being Ring for V being LeftMod 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 LeftMod 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 LeftMod 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, Th2; ::_thesis: verum end; theorem :: LMOD_5:5 for R being Ring for V being LeftMod 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 Th4; theorem Th6: :: LMOD_5:6 for R being domRing for V being LeftMod of R for L being Linear_Combination of V for a being Scalar of R st a <> 0. R holds Carrier (a * L) = Carrier L proof let R be domRing; ::_thesis: for V being LeftMod of R for L being Linear_Combination of V for a being Scalar of R st a <> 0. R holds Carrier (a * L) = Carrier L let V be LeftMod of R; ::_thesis: for L being Linear_Combination of V for a being Scalar of R st a <> 0. R holds Carrier (a * L) = Carrier L let L be Linear_Combination of V; ::_thesis: for a being Scalar of R st a <> 0. R holds Carrier (a * L) = Carrier L let a be Scalar of R; ::_thesis: ( a <> 0. R implies Carrier (a * L) = Carrier L ) set T = { u where u is Vector of V : (a * L) . u <> 0. R } ; set S = { v where v is Vector of V : L . v <> 0. R } ; assume A1: a <> 0. R ; ::_thesis: Carrier (a * L) = Carrier L { u where u is Vector of V : (a * L) . u <> 0. R } = { v where v is Vector of V : L . v <> 0. R } proof thus { u where u is Vector of V : (a * L) . 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 : (a * L) . u <> 0. R } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is Vector of V : (a * L) . 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 : (a * L) . 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 A2: x = u and A3: (a * L) . u <> 0. R ; (a * L) . u = a * (L . u) by VECTSP_6:def_9; then L . u <> 0. R by A3, VECTSP_1:6; hence x in { v where v is Vector of V : L . v <> 0. R } by A2; ::_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 : (a * L) . 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 : (a * L) . u <> 0. R } then consider v being Vector of V such that A4: x = v and A5: L . v <> 0. R ; (a * L) . v = a * (L . v) by VECTSP_6:def_9; then (a * L) . v <> 0. R by A1, A5, VECTSP_2:def_1; hence x in { u where u is Vector of V : (a * L) . u <> 0. R } by A4; ::_thesis: verum end; hence Carrier (a * L) = Carrier L ; ::_thesis: verum end; theorem Th7: :: LMOD_5:7 for R being domRing for V being LeftMod of R for L being Linear_Combination of V for a being Scalar of R holds Sum (a * L) = a * (Sum L) proof let R be domRing; ::_thesis: for V being LeftMod of R for L being Linear_Combination of V for a being Scalar of R holds Sum (a * L) = a * (Sum L) let V be LeftMod of R; ::_thesis: for L being Linear_Combination of V for a being Scalar of R holds Sum (a * L) = a * (Sum L) let L be Linear_Combination of V; ::_thesis: for a being Scalar of R holds Sum (a * L) = a * (Sum L) let a be Scalar of R; ::_thesis: Sum (a * L) = a * (Sum L) percases ( a <> 0. R or a = 0. R ) ; supposeA1: a <> 0. R ; ::_thesis: Sum (a * L) = a * (Sum L) set l = a * L; A2: Carrier (a * L) = Carrier L by A1, Th6; consider G being FinSequence of the carrier of V such that A3: G is one-to-one and A4: rng G = Carrier L and A5: Sum L = Sum (L (#) G) by VECTSP_6:def_6; set g = L (#) G; consider F being FinSequence of the carrier of V such that A6: F is one-to-one and A7: rng F = Carrier (a * L) and A8: Sum (a * L) = Sum ((a * L) (#) F) by VECTSP_6:def_6; A9: len G = len F by A1, A6, A7, A3, A4, Th6, FINSEQ_1:48; set f = (a * L) (#) 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: ( Seg (len F) = dom F & dom P = dom F ) by A10, FINSEQ_1:def_3, FINSEQ_3:29; 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 Element of NAT ; 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 Element of NAT by A17; 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 ) hence x in dom P by A10, A9, FINSEQ_3:29; ::_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 thus x in dom G by A10, A9, A20, FINSEQ_3:29; ::_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 ((a * L) (#) F) = len F by VECTSP_6:def_5; then A28: dom ((a * L) (#) F) = dom F by FINSEQ_3:29; then reconsider P = P as Function of (dom ((a * L) (#) F)),(dom ((a * L) (#) F)) ; reconsider Fp = ((a * L) (#) F) * P as FinSequence of the carrier of V by FINSEQ_2:47; reconsider P = P as Permutation of (dom ((a * L) (#) F)) by A24, A26, A28, FUNCT_2:57; A29: Fp = ((a * L) (#) F) * P ; then A30: len Fp = len ((a * L) (#) F) by FINSEQ_2:44; then A31: len Fp = len (L (#) G) by A9, A27, VECTSP_6:def_5; A32: now__::_thesis:_for_k_being_Element_of_NAT_ for_v_being_Vector_of_V_st_k_in_dom_Fp_&_v_=_(L_(#)_G)_._k_holds_ Fp_._k_=_a_*_v let k be Element of NAT ; ::_thesis: for v being Vector of V st k in dom Fp & v = (L (#) G) . k holds Fp . k = a * v let v be Vector of V; ::_thesis: ( k in dom Fp & v = (L (#) G) . k implies Fp . k = a * v ) assume that A33: k in dom Fp and A34: v = (L (#) G) . k ; ::_thesis: Fp . k = a * v 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 Element of NAT ; 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 ((a * L) (#) F)) by A27, A38, FINSEQ_1:def_3; then A41: i in dom ((a * L) (#) F) by FINSEQ_1:def_3; thus Fp . k = ((a * L) (#) F) . (P . k) by A36, FUNCT_1:13 .= ((a * L) (#) F) . (F <- (G . k)) by A11, A12, A27, A30, A31, A35 .= ((a * L) . (F /. i)) * (F /. i) by A41, VECTSP_6:def_5 .= (a * (L . (F /. i))) * (F /. i) by VECTSP_6:def_9 .= a * ((L . (F /. i)) * (F /. i)) by VECTSP_1:def_16 .= a * v by A34, A40, A39, VECTSP_6:def_5 ; ::_thesis: verum end; Sum Fp = Sum ((a * L) (#) F) by A29, RLVECT_2:7; hence Sum (a * L) = a * (Sum L) by A8, A5, A31, A32, RLVECT_2:66; ::_thesis: verum end; supposeA42: a = 0. R ; ::_thesis: Sum (a * L) = a * (Sum L) hence Sum (a * L) = Sum (ZeroLC V) by VECTSP_6:30 .= 0. V by VECTSP_6:15 .= a * (Sum L) by A42, VECTSP_1:14 ; ::_thesis: verum end; end; end; definition let R be domRing; let V be LeftMod of R; let A be Subset of V; func Lin A -> strict Subspace of V means :Def2: :: LMOD_5:def 2 the carrier of it = { (Sum l) where l is Linear_Combination of A : verum } ; existence ex b1 being strict Subspace 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 } ; { (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 ; reconsider l = ZeroLC V as Linear_Combination of A by VECTSP_6:5; 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 VECTSP_4: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 b1 * b2 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 VECTSP_6:24; v + u = Sum f by A4, A5, VECTSP_6:44; 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 a * b1 in A1 ) let v be Vector of V; ::_thesis: ( not v in A1 or a * v in A1 ) assume v in A1 ; ::_thesis: a * v in A1 then consider l being Linear_Combination of A such that A6: v = Sum l ; reconsider f = a * l as Linear_Combination of A by VECTSP_6:31; a * v = Sum f by A6, Th7; hence a * v in A1 ; ::_thesis: verum end; Sum l = 0. V by VECTSP_6:15; then 0. V in A1 ; hence ex b1 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } by A1, VECTSP_4:34; ::_thesis: verum end; uniqueness for b1, b2 being strict Subspace 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 VECTSP_4:29; end; :: deftheorem Def2 defines Lin LMOD_5:def_2_:_ for R being domRing for V being LeftMod of R for A being Subset of V for b4 being strict Subspace of V holds ( b4 = Lin A iff the carrier of b4 = { (Sum l) where l is Linear_Combination of A : verum } ); theorem Th8: :: LMOD_5:8 for x being set for R being domRing for V being LeftMod 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 LeftMod 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 LeftMod 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 LeftMod 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 Def2; 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 Def2; hence x in Lin A by STRUCT_0:def_5; ::_thesis: verum end; theorem Th9: :: LMOD_5:9 for x being set for R being domRing for V being LeftMod 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 LeftMod 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 LeftMod of R for A being Subset of V st x in A holds x in Lin A let V be LeftMod 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( set ) -> 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 VECTSP_6:def_1; 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 VECTSP_6:def_4; A7: Sum f = (1. R) * v by A2, VECTSP_6:17 .= v by VECTSP_1:def_17 ; {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 VECTSP_6:def_4; Sum f = v by A7; hence x in Lin A by Th8; ::_thesis: verum end; theorem :: LMOD_5:10 for R being domRing for V being LeftMod of R holds Lin ({} the carrier of V) = (0). V proof let R be domRing; ::_thesis: for V being LeftMod of R holds Lin ({} the carrier of V) = (0). V let V be LeftMod 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 Def2; then ex l0 being Linear_Combination of {} the carrier of V st v = Sum l0 by A1; then v = 0. V by VECTSP_6:16; hence v in (0). V by VECTSP_4:35; ::_thesis: verum end; assume v in (0). V ; ::_thesis: v in Lin ({} the carrier of V) then v = 0. V by VECTSP_4:35; hence v in Lin ({} the carrier of V) by VECTSP_4:17; ::_thesis: verum end; hence Lin ({} the carrier of V) = (0). V by VECTSP_4:30; ::_thesis: verum end; theorem :: LMOD_5:11 for R being domRing for V being LeftMod 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 LeftMod of R for A being Subset of V holds ( not Lin A = (0). V or A = {} or A = {(0. V)} ) let V be LeftMod 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 Th9; then x = 0. V by A1, VECTSP_4: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, Th9; hence x in A by A1, A3, VECTSP_4:35; ::_thesis: verum end; theorem Th12: :: LMOD_5:12 for R being domRing for V being LeftMod of R for A being Subset of V for W being strict Subspace 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 LeftMod of R for A being Subset of V for W being strict Subspace of V st 0. R <> 1. R & A = the carrier of W holds Lin A = W let V be LeftMod of R; ::_thesis: for A being Subset of V for W being strict Subspace 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 Subspace of V st 0. R <> 1. R & A = the carrier of W holds Lin A = W let W be strict Subspace 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 Th8; A is linearly-closed by A2, VECTSP_4:33; then v in the carrier of W by A1, A2, A3, VECTSP_6:14; 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, Th9; ::_thesis: verum end; hence Lin A = W by VECTSP_4:30; ::_thesis: verum end; theorem :: LMOD_5:13 for R being domRing for V being strict LeftMod 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 LeftMod 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 LeftMod 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, Th12; ::_thesis: verum end; theorem Th14: :: LMOD_5:14 for R being domRing for V being LeftMod of R for A, B being Subset of V st A c= B holds Lin A is Subspace of Lin B proof let R be domRing; ::_thesis: for V being LeftMod of R for A, B being Subset of V st A c= B holds Lin A is Subspace of Lin B let V be LeftMod of R; ::_thesis: for A, B being Subset of V st A c= B holds Lin A is Subspace of Lin B let A, B be Subset of V; ::_thesis: ( A c= B implies Lin A is Subspace of Lin B ) assume A1: A c= B ; ::_thesis: Lin A is Subspace 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 Th8; reconsider l = l as Linear_Combination of B by A1, VECTSP_6:4; Sum l = v by A2; hence v in Lin B by Th8; ::_thesis: verum end; hence Lin A is Subspace of Lin B by VECTSP_4:28; ::_thesis: verum end; theorem :: LMOD_5:15 for R being domRing for V being strict LeftMod 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 LeftMod of R for A, B being Subset of V st Lin A = V & A c= B holds Lin B = V let V be strict LeftMod 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 Subspace of Lin B by Th14; hence Lin B = V by VECTSP_4:25; ::_thesis: verum end; theorem :: LMOD_5:16 for R being domRing for V being LeftMod 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 LeftMod of R for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B) let V be LeftMod 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 Th8; 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; A2: now__::_thesis:_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_)_) let x be set ; ::_thesis: ( x in the carrier of V implies ( ( S1[x] implies H2(x) in the carrier of R ) & ( not S1[x] implies H1(x) in the carrier of R ) ) ) assume x in the carrier of V ; ::_thesis: ( ( S1[x] implies H2(x) in the carrier of R ) & ( not S1[x] implies H1(x) 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 ( S1[x] implies H2(x) in the carrier of R ) ; ::_thesis: ( not S1[x] implies H1(x) in the carrier of R ) assume not S1[x] ; ::_thesis: H1(x) in the carrier of R thus H1(x) in the carrier of R ; ::_thesis: verum end; A3: (Carrier l) \ A c= B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Carrier l) \ A or x in B ) assume x in (Carrier l) \ A ; ::_thesis: x in B then A4: ( x in Carrier l & not x in A ) by XBOOLE_0:def_5; Carrier l c= A \/ B by VECTSP_6:def_4; hence x in B by A4, XBOOLE_0:def_3; ::_thesis: verum end; consider f being Function of the carrier of V, the carrier of R such that A5: 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 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 (Carrier l) /\ A holds f . u = 0. R by A5; then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1; A6: Carrier f c= (Carrier l) /\ A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in (Carrier l) /\ A ) assume x in Carrier f ; ::_thesis: x in (Carrier l) /\ A then A7: ex u being Vector of V st ( x = u & f . u <> 0. R ) ; assume not x in (Carrier l) /\ A ; ::_thesis: contradiction hence contradiction by A5, A7; ::_thesis: verum end; (Carrier l) /\ A c= A by XBOOLE_1:17; then Carrier f c= A by A6, XBOOLE_1:1; then reconsider f = f as Linear_Combination of A by VECTSP_6:def_4; defpred S2[ set ] means \$1 in (Carrier l) \ A; A8: now__::_thesis:_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_)_) let x be set ; ::_thesis: ( x in the carrier of V implies ( ( S2[x] implies H2(x) in the carrier of R ) & ( not S2[x] implies H1(x) in the carrier of R ) ) ) assume x in the carrier of V ; ::_thesis: ( ( S2[x] implies H2(x) in the carrier of R ) & ( not S2[x] implies H1(x) 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 ( S2[x] implies H2(x) in the carrier of R ) ; ::_thesis: ( not S2[x] implies H1(x) in the carrier of R ) assume not S2[x] ; ::_thesis: H1(x) in the carrier of R thus H1(x) in the carrier of R ; ::_thesis: verum end; consider g being Function of the carrier of V, the carrier of R such that A9: 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(A8); 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 (Carrier l) \ A holds g . u = 0. R by A9; then reconsider g = g as Linear_Combination of V by VECTSP_6:def_1; Carrier g c= (Carrier l) \ A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in (Carrier l) \ A ) assume x in Carrier g ; ::_thesis: x in (Carrier l) \ A then A10: ex u being Vector of V st ( x = u & g . u <> 0. R ) ; assume not x in (Carrier l) \ A ; ::_thesis: contradiction hence contradiction by A9, A10; ::_thesis: verum end; then Carrier g c= B by A3, XBOOLE_1:1; then reconsider g = g as Linear_Combination of B by VECTSP_6:def_4; l = f + g proof let v be Vector of V; :: according to VECTSP_6:def_7 ::_thesis: l . v = (f + g) . v now__::_thesis:_(f_+_g)_._v_=_l_._v percases ( v in (Carrier l) /\ A or not v in (Carrier l) /\ A ) ; supposeA11: v in (Carrier l) /\ A ; ::_thesis: (f + g) . v = l . v A12: now__::_thesis:_not_v_in_(Carrier_l)_\_A assume v in (Carrier l) \ A ; ::_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 VECTSP_6:22 .= (l . v) + (g . v) by A5, A11 .= (l . v) + (0. R) by A9, A12 .= l . v by RLVECT_1:4 ; ::_thesis: verum end; supposeA13: not v in (Carrier l) /\ A ; ::_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_(Carrier_l)_\_A assume not v in (Carrier l) \ A ; ::_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 VECTSP_6:22 .= (0. R) + (g . v) by A5, A13 .= g . v by RLVECT_1:4 .= l . v by A9, A15 ; ::_thesis: verum end; supposeA16: not v in Carrier l ; ::_thesis: (f + g) . v = l . v then A17: not v in (Carrier l) \ A by XBOOLE_0:def_5; A18: not v in (Carrier l) /\ A by A16, XBOOLE_0:def_4; thus (f + g) . v = (f . v) + (g . v) by VECTSP_6:22 .= (0. R) + (g . v) by A5, A18 .= (0. R) + (0. R) by A9, 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, VECTSP_6:44; ( Sum f in Lin A & Sum g in Lin B ) by Th8; hence v in (Lin A) + (Lin B) by A19, VECTSP_5:1; ::_thesis: verum end; then A20: Lin (A \/ B) is Subspace of (Lin A) + (Lin B) by VECTSP_4:28; ( Lin A is Subspace of Lin (A \/ B) & Lin B is Subspace of Lin (A \/ B) ) by Th14, XBOOLE_1:7; then (Lin A) + (Lin B) is Subspace of Lin (A \/ B) by VECTSP_5:34; hence Lin (A \/ B) = (Lin A) + (Lin B) by A20, VECTSP_4:25; ::_thesis: verum end; theorem :: LMOD_5:17 for R being domRing for V being LeftMod of R for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) proof let R be domRing; ::_thesis: for V being LeftMod of R for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) let V be LeftMod of R; ::_thesis: for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) let A, B be Subset of V; ::_thesis: Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) ( Lin (A /\ B) is Subspace of Lin A & Lin (A /\ B) is Subspace of Lin B ) by Th14, XBOOLE_1:17; hence Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) by VECTSP_5:19; ::_thesis: verum end;