:: RLVECT_X semantic presentation begin reconsider z0 = 0 as Real ; deffunc H1( set ) -> Element of NAT = 0 ; theorem :: RLVECT_X:1 for X being RealLinearSpace for R1, R2 being FinSequence of X st len R1 = len R2 holds Sum (R1 + R2) = (Sum R1) + (Sum R2) proof let X be RealLinearSpace; ::_thesis: for R1, R2 being FinSequence of X st len R1 = len R2 holds Sum (R1 + R2) = (Sum R1) + (Sum R2) let R1, R2 be FinSequence of X; ::_thesis: ( len R1 = len R2 implies Sum (R1 + R2) = (Sum R1) + (Sum R2) ) assume len R1 = len R2 ; ::_thesis: Sum (R1 + R2) = (Sum R1) + (Sum R2) then dom R1 = dom R2 by FINSEQ_3:29; hence Sum (R1 + R2) = (Sum R1) + (Sum R2) by BINOM:7; ::_thesis: verum end; theorem :: RLVECT_X:2 for X being RealLinearSpace for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 - R2 holds Sum R3 = (Sum R1) - (Sum R2) proof let X be RealLinearSpace; ::_thesis: for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 - R2 holds Sum R3 = (Sum R1) - (Sum R2) let R1, R2, R3 be FinSequence of X; ::_thesis: ( len R1 = len R2 & R3 = R1 - R2 implies Sum R3 = (Sum R1) - (Sum R2) ) assume A1: ( len R1 = len R2 & R3 = R1 - R2 ) ; ::_thesis: Sum R3 = (Sum R1) - (Sum R2) then A2: dom R1 = dom R2 by FINSEQ_3:29; A3: dom R3 = (dom R1) /\ (dom R2) by A1, VFUNCT_1:def_2 .= dom R1 by A2 ; then A4: len R3 = len R1 by FINSEQ_3:29; for k being Element of NAT st k in dom R1 holds R3 . k = (R1 /. k) - (R2 /. k) proof let k be Element of NAT ; ::_thesis: ( k in dom R1 implies R3 . k = (R1 /. k) - (R2 /. k) ) assume A5: k in dom R1 ; ::_thesis: R3 . k = (R1 /. k) - (R2 /. k) hence R3 . k = R3 /. k by A3, PARTFUN1:def_6 .= (R1 /. k) - (R2 /. k) by A1, A5, A3, VFUNCT_1:def_2 ; ::_thesis: verum end; hence Sum R3 = (Sum R1) - (Sum R2) by A1, A4, RLVECT_2:5; ::_thesis: verum end; theorem Th3: :: RLVECT_X:3 for X being RealLinearSpace for R1, R2 being FinSequence of X for a being Element of REAL st R2 = a (#) R1 holds Sum R2 = a * (Sum R1) proof let X be RealLinearSpace; ::_thesis: for R1, R2 being FinSequence of X for a being Element of REAL st R2 = a (#) R1 holds Sum R2 = a * (Sum R1) let R1, R2 be FinSequence of X; ::_thesis: for a being Element of REAL st R2 = a (#) R1 holds Sum R2 = a * (Sum R1) let a be Element of REAL ; ::_thesis: ( R2 = a (#) R1 implies Sum R2 = a * (Sum R1) ) assume A1: R2 = a (#) R1 ; ::_thesis: Sum R2 = a * (Sum R1) dom R2 = dom R1 by A1, VFUNCT_1:def_4; then A2: len R2 = len R1 by FINSEQ_3:29; for k being Element of NAT st k in dom R1 holds R2 . k = a * (R1 /. k) proof let k be Element of NAT ; ::_thesis: ( k in dom R1 implies R2 . k = a * (R1 /. k) ) assume k in dom R1 ; ::_thesis: R2 . k = a * (R1 /. k) then A3: k in dom R2 by A1, VFUNCT_1:def_4; hence R2 . k = R2 /. k by PARTFUN1:def_6 .= a * (R1 /. k) by A3, A1, VFUNCT_1:def_4 ; ::_thesis: verum end; hence Sum R2 = a * (Sum R1) by A2, RLVECT_2:3; ::_thesis: verum end; begin definition let V be RealLinearSpace; let i be Integer; let L be Linear_Combination of V; funci * L -> Linear_Combination of V means :Def1: :: RLVECT_X:def 1 for v being VECTOR of V holds it . v = i * (L . v); existence ex b1 being Linear_Combination of V st for v being VECTOR of V holds b1 . v = i * (L . v) proof deffunc H2( Element of V) -> Element of REAL = i * (L . \$1); consider f being Function of the carrier of V,REAL such that A1: for v being Element of V holds f . v = H2(v) from FUNCT_2:sch_4(); reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; now__::_thesis:_for_v_being_Element_of_V_st_not_v_in_Carrier_L_holds_ f_._v_=_0 let v be Element of V; ::_thesis: ( not v in Carrier L implies f . v = 0 ) assume not v in Carrier L ; ::_thesis: f . v = 0 then L . v = 0 ; hence f . v = i * 0 by A1 .= 0 ; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3; take f ; ::_thesis: for v being VECTOR of V holds f . v = i * (L . v) let v be VECTOR of V; ::_thesis: f . v = i * (L . v) thus f . v = i * (L . 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 = i * (L . v) ) & ( for v being VECTOR of V holds b2 . v = i * (L . v) ) holds b1 = b2 proof let L1, L2 be Linear_Combination of V; ::_thesis: ( ( for v being VECTOR of V holds L1 . v = i * (L . v) ) & ( for v being VECTOR of V holds L2 . v = i * (L . v) ) implies L1 = L2 ) assume that A2: for v being VECTOR of V holds L1 . v = i * (L . v) and A3: for v being VECTOR of V holds L2 . v = i * (L . v) ; ::_thesis: L1 = L2 let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: L1 . v = L2 . v thus L1 . v = i * (L . v) by A2 .= L2 . v by A3 ; ::_thesis: verum end; end; :: deftheorem Def1 defines * RLVECT_X:def_1_:_ for V being RealLinearSpace for i being Integer for L, b4 being Linear_Combination of V holds ( b4 = i * L iff for v being VECTOR of V holds b4 . v = i * (L . v) ); definition let V be RealLinearSpace; let A be Subset of V; func Z_Lin A -> Subset of V equals :: RLVECT_X:def 2 { (Sum l) where l is Linear_Combination of A : rng l c= INT } ; correctness coherence { (Sum l) where l is Linear_Combination of A : rng l c= INT } is Subset of V; proof set A1 = { (Sum l) where l is Linear_Combination of A : rng l c= INT } ; { (Sum l) where l is Linear_Combination of A : rng l c= INT } 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 : rng l c= INT } or x in the carrier of V ) assume x in { (Sum l) where l is Linear_Combination of A : rng l c= INT } ; ::_thesis: x in the carrier of V then ex l being Linear_Combination of A st ( x = Sum l & rng l c= INT ) ; hence x in the carrier of V ; ::_thesis: verum end; hence { (Sum l) where l is Linear_Combination of A : rng l c= INT } is Subset of V ; ::_thesis: verum end; end; :: deftheorem defines Z_Lin RLVECT_X:def_2_:_ for V being RealLinearSpace for A being Subset of V holds Z_Lin A = { (Sum l) where l is Linear_Combination of A : rng l c= INT } ; theorem Th4: :: RLVECT_X:4 for a being Real for i being Integer for V being RealLinearSpace for A being Subset of V for l being Linear_Combination of A st a = i holds a * l = i * l proof let a be Real; ::_thesis: for i being Integer for V being RealLinearSpace for A being Subset of V for l being Linear_Combination of A st a = i holds a * l = i * l let i be Integer; ::_thesis: for V being RealLinearSpace for A being Subset of V for l being Linear_Combination of A st a = i holds a * l = i * l let V be RealLinearSpace; ::_thesis: for A being Subset of V for l being Linear_Combination of A st a = i holds a * l = i * l let A be Subset of V; ::_thesis: for l being Linear_Combination of A st a = i holds a * l = i * l let l be Linear_Combination of A; ::_thesis: ( a = i implies a * l = i * l ) assume A1: a = i ; ::_thesis: a * l = i * l for v being VECTOR of V holds (i * l) . v = a * (l . v) by A1, Def1; hence a * l = i * l by RLVECT_2:def_11; ::_thesis: verum end; theorem Th5: :: RLVECT_X:5 for V being RealLinearSpace for A being Subset of V for l1, l2 being Linear_Combination of A st rng l1 c= INT & rng l2 c= INT holds rng (l1 + l2) c= INT proof let V be RealLinearSpace; ::_thesis: for A being Subset of V for l1, l2 being Linear_Combination of A st rng l1 c= INT & rng l2 c= INT holds rng (l1 + l2) c= INT let A be Subset of V; ::_thesis: for l1, l2 being Linear_Combination of A st rng l1 c= INT & rng l2 c= INT holds rng (l1 + l2) c= INT let l1, l2 be Linear_Combination of A; ::_thesis: ( rng l1 c= INT & rng l2 c= INT implies rng (l1 + l2) c= INT ) assume A1: ( rng l1 c= INT & rng l2 c= INT ) ; ::_thesis: rng (l1 + l2) c= INT let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (l1 + l2) or y in INT ) assume A2: y in rng (l1 + l2) ; ::_thesis: y in INT consider x being set such that A3: ( x in the carrier of V & y = (l1 + l2) . x ) by A2, FUNCT_2:11; reconsider z = x as VECTOR of V by A3; l1 . z in rng l1 by FUNCT_2:4; then reconsider z1 = l1 . z as Integer by A1; l2 . z in rng l2 by FUNCT_2:4; then reconsider z2 = l2 . z as Integer by A1; (l1 + l2) . z = z1 + z2 by RLVECT_2:def_10; hence y in INT by A3; ::_thesis: verum end; theorem Th6: :: RLVECT_X:6 for i being Integer for V being RealLinearSpace for A being Subset of V for l being Linear_Combination of A st rng l c= INT holds rng (i * l) c= INT proof let i be Integer; ::_thesis: for V being RealLinearSpace for A being Subset of V for l being Linear_Combination of A st rng l c= INT holds rng (i * l) c= INT let V be RealLinearSpace; ::_thesis: for A being Subset of V for l being Linear_Combination of A st rng l c= INT holds rng (i * l) c= INT let A be Subset of V; ::_thesis: for l being Linear_Combination of A st rng l c= INT holds rng (i * l) c= INT let l be Linear_Combination of A; ::_thesis: ( rng l c= INT implies rng (i * l) c= INT ) assume A1: rng l c= INT ; ::_thesis: rng (i * l) c= INT let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (i * l) or y in INT ) assume A2: y in rng (i * l) ; ::_thesis: y in INT consider x being set such that A3: ( x in the carrier of V & y = (i * l) . x ) by A2, FUNCT_2:11; reconsider z = x as VECTOR of V by A3; reconsider ii = i as Real by XREAL_0:def_1; l . z in rng l by FUNCT_2:4; then reconsider z1 = l . z as Integer by A1; (i * l) . z = (ii * l) . z by Th4 .= i * z1 by RLVECT_2:def_11 ; hence y in INT by A3; ::_thesis: verum end; theorem Th7: :: RLVECT_X:7 for V being RealLinearSpace holds rng (ZeroLC V) c= INT proof let V be RealLinearSpace; ::_thesis: rng (ZeroLC V) c= INT let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (ZeroLC V) or y in INT ) assume A1: y in rng (ZeroLC V) ; ::_thesis: y in INT consider x being set such that A2: ( x in the carrier of V & y = (ZeroLC V) . x ) by A1, FUNCT_2:11; reconsider z = x as VECTOR of V by A2; (ZeroLC V) . z = 0 by RLVECT_2:20; hence y in INT by A2, NUMBERS:17, TARSKI:def_3; ::_thesis: verum end; theorem Th8: :: RLVECT_X:8 for V being RealLinearSpace for A being Subset of V holds Z_Lin A c= the carrier of (Lin A) proof let V be RealLinearSpace; ::_thesis: for A being Subset of V holds Z_Lin A c= the carrier of (Lin A) let A be Subset of V; ::_thesis: Z_Lin A c= the carrier of (Lin A) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z_Lin A or x in the carrier of (Lin A) ) assume x in Z_Lin A ; ::_thesis: x in the carrier of (Lin A) then consider l1 being Linear_Combination of A such that A1: ( x = Sum l1 & rng l1 c= INT ) ; x in Lin A by A1, RLVECT_3:14; hence x in the carrier of (Lin A) by STRUCT_0:def_5; ::_thesis: verum end; theorem Th9: :: RLVECT_X:9 for V being RealLinearSpace for v, u being VECTOR of V for A being Subset of V st v in Z_Lin A & u in Z_Lin A holds v + u in Z_Lin A proof let V be RealLinearSpace; ::_thesis: for v, u being VECTOR of V for A being Subset of V st v in Z_Lin A & u in Z_Lin A holds v + u in Z_Lin A let v, u be VECTOR of V; ::_thesis: for A being Subset of V st v in Z_Lin A & u in Z_Lin A holds v + u in Z_Lin A let A be Subset of V; ::_thesis: ( v in Z_Lin A & u in Z_Lin A implies v + u in Z_Lin A ) assume that A1: v in Z_Lin A and A2: u in Z_Lin A ; ::_thesis: v + u in Z_Lin A consider l1 being Linear_Combination of A such that A3: ( v = Sum l1 & rng l1 c= INT ) by A1; consider l2 being Linear_Combination of A such that A4: ( u = Sum l2 & rng l2 c= INT ) by A2; reconsider f = l1 + l2 as Linear_Combination of A by RLVECT_2:38; A5: rng f c= INT by A3, A4, Th5; v + u = Sum f by A3, A4, RLVECT_3:1; hence v + u in Z_Lin A by A5; ::_thesis: verum end; theorem Th10: :: RLVECT_X:10 for i being Integer for V being RealLinearSpace for v being VECTOR of V for A being Subset of V st v in Z_Lin A holds i * v in Z_Lin A proof let i be Integer; ::_thesis: for V being RealLinearSpace for v being VECTOR of V for A being Subset of V st v in Z_Lin A holds i * v in Z_Lin A let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for A being Subset of V st v in Z_Lin A holds i * v in Z_Lin A let v be VECTOR of V; ::_thesis: for A being Subset of V st v in Z_Lin A holds i * v in Z_Lin A let A be Subset of V; ::_thesis: ( v in Z_Lin A implies i * v in Z_Lin A ) assume v in Z_Lin A ; ::_thesis: i * v in Z_Lin A then consider l being Linear_Combination of A such that A1: ( v = Sum l & rng l c= INT ) ; reconsider a = i as Real by XREAL_0:def_1; A2: a * l = i * l by Th4; then reconsider f = i * l as Linear_Combination of A by RLVECT_2:44; A3: i * v = Sum f by A1, A2, RLVECT_3:2; rng (i * l) c= INT by Th6, A1; hence i * v in Z_Lin A by A3; ::_thesis: verum end; theorem Th11: :: RLVECT_X:11 for V being RealLinearSpace for A being Subset of V holds 0. V in Z_Lin A proof let V be RealLinearSpace; ::_thesis: for A being Subset of V holds 0. V in Z_Lin A let A be Subset of V; ::_thesis: 0. V in Z_Lin A reconsider l = ZeroLC V as Linear_Combination of A by RLVECT_2:22; A1: Sum l = 0. V by RLVECT_2:30; rng l c= INT by Th7; hence 0. V in Z_Lin A by A1; ::_thesis: verum end; theorem Th12: :: RLVECT_X:12 for x being set for V being RealLinearSpace for A being Subset of V st x in A holds x in Z_Lin A proof let x be set ; ::_thesis: for V being RealLinearSpace for A being Subset of V st x in A holds x in Z_Lin A let V be RealLinearSpace; ::_thesis: for A being Subset of V st x in A holds x in Z_Lin A let A be Subset of V; ::_thesis: ( x in A implies x in Z_Lin A ) assume A1: x in A ; ::_thesis: x in Z_Lin A then reconsider v = x as VECTOR of V ; consider f being Function of the carrier of V,REAL such that A2: f . v = 1 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,REAL) 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 proof take T = {v}; ::_thesis: for u being VECTOR of V st not u in T holds f . u = 0 let u be VECTOR of V; ::_thesis: ( not u in T implies f . u = 0 ) assume not u in T ; ::_thesis: f . u = 0 then u <> v by TARSKI:def_1; hence f . u = 0 by A3; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3; 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 ; 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 RLVECT_2:def_6; A7: Sum f = (f . v) * v by RLVECT_2:32 .= v by A2, RLVECT_1:def_8 ; {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 RLVECT_2:def_6; rng f c= INT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in INT ) assume A8: y in rng f ; ::_thesis: y in INT consider x being set such that A9: ( x in the carrier of V & y = f . x ) by A8, FUNCT_2:11; reconsider z = x as VECTOR of V by A9; percases ( z <> v or z = v ) ; suppose z <> v ; ::_thesis: y in INT then f . z = 0 by A3; hence y in INT by A9, NUMBERS:17, TARSKI:def_3; ::_thesis: verum end; suppose z = v ; ::_thesis: y in INT hence y in INT by A9, A2, NUMBERS:17, TARSKI:def_3; ::_thesis: verum end; end; end; hence x in Z_Lin A by A7; ::_thesis: verum end; theorem Th13: :: RLVECT_X:13 for V being RealLinearSpace for A, B being Subset of V st A c= B holds Z_Lin A c= Z_Lin B proof let V be RealLinearSpace; ::_thesis: for A, B being Subset of V st A c= B holds Z_Lin A c= Z_Lin B let A, B be Subset of V; ::_thesis: ( A c= B implies Z_Lin A c= Z_Lin B ) assume A1: A c= B ; ::_thesis: Z_Lin A c= Z_Lin B let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in Z_Lin A or v in Z_Lin B ) assume v in Z_Lin A ; ::_thesis: v in Z_Lin B then consider l being Linear_Combination of A such that A2: ( v = Sum l & rng l c= INT ) ; reconsider l = l as Linear_Combination of B by A1, RLVECT_2:21; Sum l = v by A2; hence v in Z_Lin B by A2; ::_thesis: verum end; theorem :: RLVECT_X:14 for V being RealLinearSpace for A, B being Subset of V holds Z_Lin (A \/ B) = (Z_Lin A) + (Z_Lin B) proof let V be RealLinearSpace; ::_thesis: for A, B being Subset of V holds Z_Lin (A \/ B) = (Z_Lin A) + (Z_Lin B) let A, B be Subset of V; ::_thesis: Z_Lin (A \/ B) = (Z_Lin A) + (Z_Lin B) now__::_thesis:_for_v_being_set_st_v_in_Z_Lin_(A_\/_B)_holds_ v_in_(Z_Lin_A)_+_(Z_Lin_B) let v be set ; ::_thesis: ( v in Z_Lin (A \/ B) implies v in (Z_Lin A) + (Z_Lin B) ) assume v in Z_Lin (A \/ B) ; ::_thesis: v in (Z_Lin A) + (Z_Lin B) then consider l being Linear_Combination of A \/ B such that A1: ( v = Sum l & rng l c= INT ) ; deffunc H2( set ) -> Element of REAL = 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; A2: for x being set st x in the carrier of V holds ( ( S1[x] implies H2(x) in REAL ) & ( not S1[x] implies H1(x) in REAL ) ) ; consider f being Function of the carrier of V,REAL 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,REAL) by FUNCT_2:8; for u being VECTOR of V st not u in C holds f . u = 0 by A3; then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3; A4: rng f c= INT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in INT ) assume A5: y in rng f ; ::_thesis: y in INT consider x being set such that A6: ( x in the carrier of V & y = f . x ) by A5, FUNCT_2:11; reconsider z = x as VECTOR of V by A6; percases ( not z in C or z in C ) ; suppose not z in C ; ::_thesis: y in INT then f . z = 0 by A3; hence y in INT by A6, NUMBERS:17, TARSKI:def_3; ::_thesis: verum end; suppose z in C ; ::_thesis: y in INT then f . z = l . z by A3; then f . z in rng l by FUNCT_2:4; hence y in INT by A6, A1; ::_thesis: verum end; end; end; A7: 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 A8: ex u being VECTOR of V st ( x = u & f . u <> 0 ) ; assume not x in C ; ::_thesis: contradiction hence contradiction by A3, A8; ::_thesis: verum end; C c= A by XBOOLE_1:17; then Carrier f c= A by A7, XBOOLE_1:1; then reconsider f = f as Linear_Combination of A by RLVECT_2:def_6; A9: for x being set st x in the carrier of V holds ( ( S2[x] implies H2(x) in REAL ) & ( not S2[x] implies H1(x) in REAL ) ) ; consider g being Function of the carrier of V,REAL such that A10: 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(A9); reconsider D = (Carrier l) \ A as finite Subset of V ; reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; for u being VECTOR of V st not u in D holds g . u = 0 by A10; then reconsider g = g as Linear_Combination of V by RLVECT_2:def_3; A11: rng g c= INT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in INT ) assume A12: y in rng g ; ::_thesis: y in INT consider x being set such that A13: ( x in the carrier of V & y = g . x ) by A12, FUNCT_2:11; reconsider z = x as VECTOR of V by A13; percases ( not z in D or z in D ) ; suppose not z in D ; ::_thesis: y in INT then g . z = 0 by A10; hence y in INT by A13, NUMBERS:17, TARSKI:def_3; ::_thesis: verum end; suppose z in D ; ::_thesis: y in INT then g . z = l . z by A10; then g . z in rng l by FUNCT_2:4; hence y in INT by A13, A1; ::_thesis: verum end; end; end; A14: 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 A15: ( x in Carrier l & not x in A ) by XBOOLE_0:def_5; Carrier l c= A \/ B by RLVECT_2:def_6; hence x in B by A15, 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 A16: ex u being VECTOR of V st ( x = u & g . u <> 0 ) ; assume not x in D ; ::_thesis: contradiction hence contradiction by A10, A16; ::_thesis: verum end; then Carrier g c= B by A14, XBOOLE_1:1; then reconsider g = g as Linear_Combination of B by RLVECT_2:def_6; l = f + g proof let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: l . v = (f + g) . v now__::_thesis:_(f_+_g)_._v_=_l_._v percases ( v in C or not v in C ) ; supposeA17: v in C ; ::_thesis: (f + g) . v = l . v A18: 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 A17, XBOOLE_0:def_4; ::_thesis: verum end; thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def_10 .= (l . v) + (g . v) by A3, A17 .= (l . v) + z0 by A10, A18 .= l . v ; ::_thesis: verum end; supposeA19: 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 ) ; supposeA20: v in Carrier l ; ::_thesis: (f + g) . v = l . v A21: 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 A19, A20, XBOOLE_0:def_4; ::_thesis: verum end; thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def_10 .= z0 + (g . v) by A3, A19 .= l . v by A10, A21 ; ::_thesis: verum end; supposeA22: not v in Carrier l ; ::_thesis: (f + g) . v = l . v then A23: not v in D by XBOOLE_0:def_5; A24: not v in C by A22, XBOOLE_0:def_4; thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def_10 .= z0 + (g . v) by A3, A24 .= z0 + z0 by A10, A23 .= l . v by A22 ; ::_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 A25: v = (Sum f) + (Sum g) by A1, RLVECT_3:1; ( Sum f in Z_Lin A & Sum g in Z_Lin B ) by A4, A11; hence v in (Z_Lin A) + (Z_Lin B) by A25; ::_thesis: verum end; then A26: Z_Lin (A \/ B) c= (Z_Lin A) + (Z_Lin B) by TARSKI:def_3; A27: ( Z_Lin A c= Z_Lin (A \/ B) & Z_Lin B c= Z_Lin (A \/ B) ) by Th13, XBOOLE_1:7; now__::_thesis:_for_x_being_set_st_x_in_(Z_Lin_A)_+_(Z_Lin_B)_holds_ x_in_Z_Lin_(A_\/_B) let x be set ; ::_thesis: ( x in (Z_Lin A) + (Z_Lin B) implies x in Z_Lin (A \/ B) ) assume x in (Z_Lin A) + (Z_Lin B) ; ::_thesis: x in Z_Lin (A \/ B) then consider u, v being Element of V such that A28: ( x = u + v & u in Z_Lin A & v in Z_Lin B ) ; thus x in Z_Lin (A \/ B) by A28, A27, Th9; ::_thesis: verum end; then (Z_Lin A) + (Z_Lin B) c= Z_Lin (A \/ B) by TARSKI:def_3; hence Z_Lin (A \/ B) = (Z_Lin A) + (Z_Lin B) by A26, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: RLVECT_X:15 for V being RealLinearSpace for A, B being Subset of V holds Z_Lin (A /\ B) c= (Z_Lin A) /\ (Z_Lin B) proof let V be RealLinearSpace; ::_thesis: for A, B being Subset of V holds Z_Lin (A /\ B) c= (Z_Lin A) /\ (Z_Lin B) let A, B be Subset of V; ::_thesis: Z_Lin (A /\ B) c= (Z_Lin A) /\ (Z_Lin B) ( Z_Lin (A /\ B) c= Z_Lin A & Z_Lin (A /\ B) c= Z_Lin B ) by Th13, XBOOLE_1:17; hence Z_Lin (A /\ B) c= (Z_Lin A) /\ (Z_Lin B) by XBOOLE_1:19; ::_thesis: verum end; theorem Th16: :: RLVECT_X:16 for x being set for V being RealLinearSpace for v being VECTOR of V holds ( x in Z_Lin {v} iff ex a being Integer st x = a * v ) proof let x be set ; ::_thesis: for V being RealLinearSpace for v being VECTOR of V holds ( x in Z_Lin {v} iff ex a being Integer st x = a * v ) let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds ( x in Z_Lin {v} iff ex a being Integer st x = a * v ) let v be VECTOR of V; ::_thesis: ( x in Z_Lin {v} iff ex a being Integer st x = a * v ) thus ( x in Z_Lin {v} implies ex a being Integer st x = a * v ) ::_thesis: ( ex a being Integer st x = a * v implies x in Z_Lin {v} ) proof assume x in Z_Lin {v} ; ::_thesis: ex a being Integer st x = a * v then consider l being Linear_Combination of {v} such that A1: ( x = Sum l & rng l c= INT ) ; A2: Sum l = (l . v) * v by RLVECT_2:32; ex f being Function st ( l = f & dom f = the carrier of V & rng f c= REAL ) by FUNCT_2:def_2; then l . v in rng l by FUNCT_1:3; hence ex a being Integer st x = a * v by A1, A2; ::_thesis: verum end; given a0 being Integer such that A3: x = a0 * v ; ::_thesis: x in Z_Lin {v} reconsider a = a0 as Real by XREAL_0:def_1; consider f being Function of the carrier of V,REAL such that A4: f . v = a and A5: for z being VECTOR of V st z <> v holds f . z = H1(z) from FUNCT_2:sch_6(); reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; A6: now__::_thesis:_for_z_being_VECTOR_of_V_st_not_z_in_{v}_holds_ f_._z_=_0 let z be VECTOR of V; ::_thesis: ( not z in {v} implies f . z = 0 ) assume not z in {v} ; ::_thesis: f . z = 0 then z <> v by TARSKI:def_1; hence f . z = 0 by A5; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3; 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 A7: x in Carrier f ; ::_thesis: x in {v} then f . x <> 0 by RLVECT_2:19; then x = v by A5, A7; hence x in {v} by TARSKI:def_1; ::_thesis: verum end; then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def_6; A8: Sum f = x by A3, A4, RLVECT_2:32; rng f c= INT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in INT ) assume A9: y in rng f ; ::_thesis: y in INT consider x being set such that A10: ( x in the carrier of V & y = f . x ) by A9, FUNCT_2:11; reconsider z = x as VECTOR of V by A10; percases ( not z in {v} or z in {v} ) ; suppose not z in {v} ; ::_thesis: y in INT then f . z = 0 by A6; hence y in INT by A10, NUMBERS:17, TARSKI:def_3; ::_thesis: verum end; suppose z in {v} ; ::_thesis: y in INT then f . z = a0 by A4, TARSKI:def_1; hence y in INT by A10, INT_1:def_2; ::_thesis: verum end; end; end; hence x in Z_Lin {v} by A8; ::_thesis: verum end; theorem :: RLVECT_X:17 for V being RealLinearSpace for v being VECTOR of V holds v in Z_Lin {v} proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds v in Z_Lin {v} let v be VECTOR of V; ::_thesis: v in Z_Lin {v} v in {v} by TARSKI:def_1; hence v in Z_Lin {v} by Th12; ::_thesis: verum end; theorem :: RLVECT_X:18 for x being set for V being RealLinearSpace for v, w being VECTOR of V holds ( x in v + (Z_Lin {w}) iff ex a being Integer st x = v + (a * w) ) proof let x be set ; ::_thesis: for V being RealLinearSpace for v, w being VECTOR of V holds ( x in v + (Z_Lin {w}) iff ex a being Integer st x = v + (a * w) ) let V be RealLinearSpace; ::_thesis: for v, w being VECTOR of V holds ( x in v + (Z_Lin {w}) iff ex a being Integer st x = v + (a * w) ) let v, w be VECTOR of V; ::_thesis: ( x in v + (Z_Lin {w}) iff ex a being Integer st x = v + (a * w) ) thus ( x in v + (Z_Lin {w}) implies ex a being Integer st x = v + (a * w) ) ::_thesis: ( ex a being Integer st x = v + (a * w) implies x in v + (Z_Lin {w}) ) proof assume x in v + (Z_Lin {w}) ; ::_thesis: ex a being Integer st x = v + (a * w) then consider u being VECTOR of V such that A1: x = v + u and A2: u in Z_Lin {w} ; ex a being Integer st u = a * w by A2, Th16; hence ex a being Integer st x = v + (a * w) by A1; ::_thesis: verum end; given a0 being Integer such that A3: x = v + (a0 * w) ; ::_thesis: x in v + (Z_Lin {w}) a0 * w in Z_Lin {w} by Th16; hence x in v + (Z_Lin {w}) by A3; ::_thesis: verum end; theorem Th19: :: RLVECT_X:19 for x being set for V being RealLinearSpace for w1, w2 being VECTOR of V holds ( x in Z_Lin {w1,w2} iff ex a, b being Integer st x = (a * w1) + (b * w2) ) proof let x be set ; ::_thesis: for V being RealLinearSpace for w1, w2 being VECTOR of V holds ( x in Z_Lin {w1,w2} iff ex a, b being Integer st x = (a * w1) + (b * w2) ) let V be RealLinearSpace; ::_thesis: for w1, w2 being VECTOR of V holds ( x in Z_Lin {w1,w2} iff ex a, b being Integer st x = (a * w1) + (b * w2) ) let w1, w2 be VECTOR of V; ::_thesis: ( x in Z_Lin {w1,w2} iff ex a, b being Integer st x = (a * w1) + (b * w2) ) thus ( x in Z_Lin {w1,w2} implies ex a, b being Integer st x = (a * w1) + (b * w2) ) ::_thesis: ( ex a, b being Integer st x = (a * w1) + (b * w2) implies x in Z_Lin {w1,w2} ) proof assume A1: x in Z_Lin {w1,w2} ; ::_thesis: ex a, b being Integer st x = (a * w1) + (b * w2) now__::_thesis:_ex_a,_b_being_Integer_st_x_=_(a_*_w1)_+_(b_*_w2) percases ( w1 = w2 or w1 <> w2 ) ; suppose w1 = w2 ; ::_thesis: ex a, b being Integer st x = (a * w1) + (b * w2) then {w1,w2} = {w1} by ENUMSET1:29; then consider a being Integer such that A2: x = a * w1 by A1, Th16; consider b being Integer such that A3: b = 0 ; x = (a * w1) + (0. V) by A2, RLVECT_1:4; then x = (a * w1) + (b * w2) by A3, RLVECT_1:10; hence ex a, b being Integer st x = (a * w1) + (b * w2) ; ::_thesis: verum end; supposeA4: w1 <> w2 ; ::_thesis: ex a, b being Integer st x = (a * w1) + (b * w2) consider l being Linear_Combination of {w1,w2} such that A5: ( x = Sum l & rng l c= INT ) by A1; A6: x = ((l . w1) * w1) + ((l . w2) * w2) by A4, A5, RLVECT_2:33; ex f being Function st ( l = f & dom f = the carrier of V & rng f c= REAL ) by FUNCT_2:def_2; then ( l . w1 in rng l & l . w2 in rng l ) by FUNCT_1:3; hence ex a, b being Integer st x = (a * w1) + (b * w2) by A5, A6; ::_thesis: verum end; end; end; hence ex a, b being Integer st x = (a * w1) + (b * w2) ; ::_thesis: verum end; given a0, b0 being Integer such that A7: x = (a0 * w1) + (b0 * w2) ; ::_thesis: x in Z_Lin {w1,w2} reconsider a = a0, b = b0 as Real by XREAL_0:def_1; now__::_thesis:_x_in_Z_Lin_{w1,w2} percases ( w1 = w2 or w1 <> w2 ) ; supposeA8: w1 = w2 ; ::_thesis: x in Z_Lin {w1,w2} then x = (a + b) * w1 by A7, RLVECT_1:def_6; then x in Z_Lin {w1} by Th16; hence x in Z_Lin {w1,w2} by A8, ENUMSET1:29; ::_thesis: verum end; supposeA9: w1 <> w2 ; ::_thesis: x in Z_Lin {w1,w2} consider f being Function of the carrier of V,REAL such that A10: ( f . w1 = a & f . w2 = b ) and A11: for u being VECTOR of V st u <> w1 & u <> w2 holds f . u = H1(u) from FUNCT_2:sch_7(A9); reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; A12: now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{w1,w2}_holds_ f_._u_=_0 let u be VECTOR of V; ::_thesis: ( not u in {w1,w2} implies f . u = 0 ) assume not u in {w1,w2} ; ::_thesis: f . u = 0 then ( u <> w1 & u <> w2 ) by TARSKI:def_2; hence f . u = 0 by A11; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3; Carrier f c= {w1,w2} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {w1,w2} ) assume that A13: x in Carrier f and A14: not x in {w1,w2} ; ::_thesis: contradiction ( x <> w1 & x <> w2 ) by A14, TARSKI:def_2; then f . x = 0 by A11, A13; hence contradiction by A13, RLVECT_2:19; ::_thesis: verum end; then reconsider f = f as Linear_Combination of {w1,w2} by RLVECT_2:def_6; A15: x = Sum f by A7, A9, A10, RLVECT_2:33; rng f c= INT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in INT ) assume A16: y in rng f ; ::_thesis: y in INT consider x being set such that A17: ( x in the carrier of V & y = f . x ) by A16, FUNCT_2:11; reconsider v = x as VECTOR of V by A17; percases ( not v in {w1,w2} or v in {w1,w2} ) ; suppose not v in {w1,w2} ; ::_thesis: y in INT then f . v = 0 by A12; hence y in INT by A17, NUMBERS:17, TARSKI:def_3; ::_thesis: verum end; suppose v in {w1,w2} ; ::_thesis: y in INT then ( f . v = a0 or f . v = b0 ) by A10, TARSKI:def_2; hence y in INT by A17, INT_1:def_2; ::_thesis: verum end; end; end; hence x in Z_Lin {w1,w2} by A15; ::_thesis: verum end; end; end; hence x in Z_Lin {w1,w2} ; ::_thesis: verum end; theorem :: RLVECT_X:20 for V being RealLinearSpace for w1, w2 being VECTOR of V holds w1 in Z_Lin {w1,w2} proof let V be RealLinearSpace; ::_thesis: for w1, w2 being VECTOR of V holds w1 in Z_Lin {w1,w2} let w1, w2 be VECTOR of V; ::_thesis: w1 in Z_Lin {w1,w2} w1 in {w1,w2} by TARSKI:def_2; hence w1 in Z_Lin {w1,w2} by Th12; ::_thesis: verum end; theorem :: RLVECT_X:21 for x being set for V being RealLinearSpace for v, w1, w2 being VECTOR of V holds ( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) ) proof let x be set ; ::_thesis: for V being RealLinearSpace for v, w1, w2 being VECTOR of V holds ( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) ) let V be RealLinearSpace; ::_thesis: for v, w1, w2 being VECTOR of V holds ( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) ) let v, w1, w2 be VECTOR of V; ::_thesis: ( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) ) thus ( x in v + (Z_Lin {w1,w2}) implies ex a, b being Integer st x = (v + (a * w1)) + (b * w2) ) ::_thesis: ( ex a, b being Integer st x = (v + (a * w1)) + (b * w2) implies x in v + (Z_Lin {w1,w2}) ) proof assume x in v + (Z_Lin {w1,w2}) ; ::_thesis: ex a, b being Integer st x = (v + (a * w1)) + (b * w2) then consider u being VECTOR of V such that A1: x = v + u and A2: u in Z_Lin {w1,w2} ; consider a, b being Integer such that A3: u = (a * w1) + (b * w2) by A2, Th19; take a ; ::_thesis: ex b being Integer st x = (v + (a * w1)) + (b * w2) take b ; ::_thesis: x = (v + (a * w1)) + (b * w2) thus x = (v + (a * w1)) + (b * w2) by A1, A3, RLVECT_1:def_3; ::_thesis: verum end; given a, b being Integer such that A4: x = (v + (a * w1)) + (b * w2) ; ::_thesis: x in v + (Z_Lin {w1,w2}) (a * w1) + (b * w2) in Z_Lin {w1,w2} by Th19; then v + ((a * w1) + (b * w2)) in v + (Z_Lin {w1,w2}) ; hence x in v + (Z_Lin {w1,w2}) by A4, RLVECT_1:def_3; ::_thesis: verum end; theorem Th22: :: RLVECT_X:22 for x being set for V being RealLinearSpace for v1, v2, v3 being VECTOR of V holds ( x in Z_Lin {v1,v2,v3} iff ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) ) proof let x be set ; ::_thesis: for V being RealLinearSpace for v1, v2, v3 being VECTOR of V holds ( x in Z_Lin {v1,v2,v3} iff ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) ) let V be RealLinearSpace; ::_thesis: for v1, v2, v3 being VECTOR of V holds ( x in Z_Lin {v1,v2,v3} iff ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) ) let v1, v2, v3 be VECTOR of V; ::_thesis: ( x in Z_Lin {v1,v2,v3} iff ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) ) thus ( x in Z_Lin {v1,v2,v3} implies ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) ) ::_thesis: ( ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) implies x in Z_Lin {v1,v2,v3} ) proof assume A1: x in Z_Lin {v1,v2,v3} ; ::_thesis: ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) now__::_thesis:_ex_a,_b,_c_being_Integer_st_x_=_((a_*_v1)_+_(b_*_v2))_+_(c_*_v3) percases ( ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) or v1 = v2 or v1 = v3 or v2 = v3 ) ; supposeA2: ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ; ::_thesis: ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) consider l being Linear_Combination of {v1,v2,v3} such that A3: ( x = Sum l & rng l c= INT ) by A1; A4: x = (((l . v1) * v1) + ((l . v2) * v2)) + ((l . v3) * v3) by A2, A3, RLVECT_4:6; ex f being Function st ( l = f & dom f = the carrier of V & rng f c= REAL ) by FUNCT_2:def_2; then ( l . v1 in rng l & l . v2 in rng l & l . v3 in rng l ) by FUNCT_1:3; hence ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) by A3, A4; ::_thesis: verum end; suppose ( v1 = v2 or v1 = v3 or v2 = v3 ) ; ::_thesis: ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) then A5: ( {v1,v2,v3} = {v1,v3} or {v1,v2,v3} = {v1,v1,v2} or {v1,v2,v3} = {v3,v3,v1} ) by ENUMSET1:30, ENUMSET1:59; now__::_thesis:_ex_a,_b,_c_being_Integer_st_x_=_((a_*_v1)_+_(b_*_v2))_+_(c_*_v3) percases ( {v1,v2,v3} = {v1,v2} or {v1,v2,v3} = {v1,v3} ) by A5, ENUMSET1:30; suppose {v1,v2,v3} = {v1,v2} ; ::_thesis: ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) then consider a, b being Integer such that A6: x = (a * v1) + (b * v2) by A1, Th19; consider c being Integer such that A7: c = 0 ; x = ((a * v1) + (b * v2)) + (0. V) by A6, RLVECT_1:4 .= ((a * v1) + (b * v2)) + (c * v3) by A7, RLVECT_1:10 ; hence ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum end; suppose {v1,v2,v3} = {v1,v3} ; ::_thesis: ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) then consider a, b being Integer such that A8: x = (a * v1) + (b * v3) by A1, Th19; consider c being Integer such that A9: c = 0 ; x = ((a * v1) + (0. V)) + (b * v3) by A8, RLVECT_1:4 .= ((a * v1) + (c * v2)) + (b * v3) by A9, RLVECT_1:10 ; hence ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum end; end; end; hence ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum end; end; end; hence ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum end; given a0, b0, c0 being Integer such that A10: x = ((a0 * v1) + (b0 * v2)) + (c0 * v3) ; ::_thesis: x in Z_Lin {v1,v2,v3} reconsider a = a0, b = b0, c = c0 as Real by XREAL_0:def_1; now__::_thesis:_x_in_Z_Lin_{v1,v2,v3} percases ( v1 = v2 or v1 = v3 or v2 = v3 or ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ) ; supposeA11: ( v1 = v2 or v1 = v3 or v2 = v3 ) ; ::_thesis: x in Z_Lin {v1,v2,v3} now__::_thesis:_x_in_Z_Lin_{v1,v2,v3} percases ( v1 = v2 or v1 = v3 or v2 = v3 ) by A11; suppose v1 = v2 ; ::_thesis: x in Z_Lin {v1,v2,v3} then ( {v1,v2,v3} = {v1,v3} & x = ((a + b) * v1) + (c * v3) ) by A10, ENUMSET1:30, RLVECT_1:def_6; hence x in Z_Lin {v1,v2,v3} by Th19; ::_thesis: verum end; supposeA12: v1 = v3 ; ::_thesis: x in Z_Lin {v1,v2,v3} then A13: {v1,v2,v3} = {v1,v1,v2} by ENUMSET1:57 .= {v2,v1} by ENUMSET1:30 ; x = (b * v2) + ((a * v1) + (c * v1)) by A10, A12, RLVECT_1:def_3 .= (b * v2) + ((a + c) * v1) by RLVECT_1:def_6 ; hence x in Z_Lin {v1,v2,v3} by A13, Th19; ::_thesis: verum end; supposeA14: v2 = v3 ; ::_thesis: x in Z_Lin {v1,v2,v3} then A15: {v1,v2,v3} = {v2,v2,v1} by ENUMSET1:59 .= {v1,v2} by ENUMSET1:30 ; x = (a * v1) + ((b * v2) + (c * v2)) by A10, A14, RLVECT_1:def_3 .= (a * v1) + ((b + c) * v2) by RLVECT_1:def_6 ; hence x in Z_Lin {v1,v2,v3} by A15, Th19; ::_thesis: verum end; end; end; hence x in Z_Lin {v1,v2,v3} ; ::_thesis: verum end; supposeA16: ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ; ::_thesis: x in Z_Lin {v1,v2,v3} A17: v1 <> v3 by A16; A18: v2 <> v3 by A16; A19: v1 <> v2 by A16; consider f being Function of the carrier of V,REAL such that A20: ( f . v1 = a & f . v2 = b & f . v3 = c ) and A21: for v being VECTOR of V st v <> v1 & v <> v2 & v <> v3 holds f . v = H1(v) from RLVECT_4:sch_1(A19, A17, A18); reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; A22: now__::_thesis:_for_v_being_VECTOR_of_V_st_not_v_in_{v1,v2,v3}_holds_ f_._v_=_0 let v be VECTOR of V; ::_thesis: ( not v in {v1,v2,v3} implies f . v = 0 ) assume A23: not v in {v1,v2,v3} ; ::_thesis: f . v = 0 then A24: v <> v3 by ENUMSET1:def_1; ( v <> v1 & v <> v2 ) by A23, ENUMSET1:def_1; hence f . v = 0 by A21, A24; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3; Carrier f c= {v1,v2,v3} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v1,v2,v3} ) assume that A25: x in Carrier f and A26: not x in {v1,v2,v3} ; ::_thesis: contradiction A27: x <> v3 by A26, ENUMSET1:def_1; ( x <> v1 & x <> v2 ) by A26, ENUMSET1:def_1; then f . x = 0 by A21, A25, A27; hence contradiction by A25, RLVECT_2:19; ::_thesis: verum end; then reconsider f = f as Linear_Combination of {v1,v2,v3} by RLVECT_2:def_6; A28: x = Sum f by A10, A16, A20, RLVECT_4:6; rng f c= INT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in INT ) assume A29: y in rng f ; ::_thesis: y in INT consider x being set such that A30: ( x in the carrier of V & y = f . x ) by A29, FUNCT_2:11; reconsider v = x as VECTOR of V by A30; percases ( not v in {v1,v2,v3} or v in {v1,v2,v3} ) ; suppose not v in {v1,v2,v3} ; ::_thesis: y in INT then f . v = 0 by A22; hence y in INT by A30, NUMBERS:17, TARSKI:def_3; ::_thesis: verum end; suppose v in {v1,v2,v3} ; ::_thesis: y in INT then ( f . v = a0 or f . v = b0 or f . v = c0 ) by A20, ENUMSET1:def_1; hence y in INT by A30, INT_1:def_2; ::_thesis: verum end; end; end; hence x in Z_Lin {v1,v2,v3} by A28; ::_thesis: verum end; end; end; hence x in Z_Lin {v1,v2,v3} ; ::_thesis: verum end; theorem :: RLVECT_X:23 for V being RealLinearSpace for w1, w2, w3 being VECTOR of V holds ( w1 in Z_Lin {w1,w2,w3} & w2 in Z_Lin {w1,w2,w3} & w3 in Z_Lin {w1,w2,w3} ) proof let V be RealLinearSpace; ::_thesis: for w1, w2, w3 being VECTOR of V holds ( w1 in Z_Lin {w1,w2,w3} & w2 in Z_Lin {w1,w2,w3} & w3 in Z_Lin {w1,w2,w3} ) let w1, w2, w3 be VECTOR of V; ::_thesis: ( w1 in Z_Lin {w1,w2,w3} & w2 in Z_Lin {w1,w2,w3} & w3 in Z_Lin {w1,w2,w3} ) A1: w3 in {w1,w2,w3} by ENUMSET1:def_1; ( w1 in {w1,w2,w3} & w2 in {w1,w2,w3} ) by ENUMSET1:def_1; hence ( w1 in Z_Lin {w1,w2,w3} & w2 in Z_Lin {w1,w2,w3} & w3 in Z_Lin {w1,w2,w3} ) by A1, Th12; ::_thesis: verum end; theorem :: RLVECT_X:24 for x being set for V being RealLinearSpace for v, w1, w2, w3 being VECTOR of V holds ( x in v + (Z_Lin {w1,w2,w3}) iff ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) proof let x be set ; ::_thesis: for V being RealLinearSpace for v, w1, w2, w3 being VECTOR of V holds ( x in v + (Z_Lin {w1,w2,w3}) iff ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) let V be RealLinearSpace; ::_thesis: for v, w1, w2, w3 being VECTOR of V holds ( x in v + (Z_Lin {w1,w2,w3}) iff ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) let v, w1, w2, w3 be VECTOR of V; ::_thesis: ( x in v + (Z_Lin {w1,w2,w3}) iff ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) thus ( x in v + (Z_Lin {w1,w2,w3}) implies ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) ::_thesis: ( ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) implies x in v + (Z_Lin {w1,w2,w3}) ) proof assume x in v + (Z_Lin {w1,w2,w3}) ; ::_thesis: ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) then consider u being VECTOR of V such that A1: x = v + u and A2: u in Z_Lin {w1,w2,w3} ; consider a, b, c being Integer such that A3: u = ((a * w1) + (b * w2)) + (c * w3) by A2, Th22; take a ; ::_thesis: ex b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) take b ; ::_thesis: ex c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) take c ; ::_thesis: x = ((v + (a * w1)) + (b * w2)) + (c * w3) x = (v + ((a * w1) + (b * w2))) + (c * w3) by A1, A3, RLVECT_1:def_3; hence x = ((v + (a * w1)) + (b * w2)) + (c * w3) by RLVECT_1:def_3; ::_thesis: verum end; given a, b, c being Integer such that A4: x = ((v + (a * w1)) + (b * w2)) + (c * w3) ; ::_thesis: x in v + (Z_Lin {w1,w2,w3}) ((a * w1) + (b * w2)) + (c * w3) in Z_Lin {w1,w2,w3} by Th22; then v + (((a * w1) + (b * w2)) + (c * w3)) in v + (Z_Lin {w1,w2,w3}) ; then (v + ((a * w1) + (b * w2))) + (c * w3) in v + (Z_Lin {w1,w2,w3}) by RLVECT_1:def_3; hence x in v + (Z_Lin {w1,w2,w3}) by A4, RLVECT_1:def_3; ::_thesis: verum end; Lm1: for RS being RealLinearSpace for X being Subset of RS for g1, h1 being FinSequence of RS for a1 being INT -valued FinSequence st rng g1 c= X & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) holds Sum h1 in Z_Lin X proof let RS be RealLinearSpace; ::_thesis: for X being Subset of RS for g1, h1 being FinSequence of RS for a1 being INT -valued FinSequence st rng g1 c= X & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) holds Sum h1 in Z_Lin X let X be Subset of RS; ::_thesis: for g1, h1 being FinSequence of RS for a1 being INT -valued FinSequence st rng g1 c= X & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) holds Sum h1 in Z_Lin X defpred S1[ Nat] means for g, h being FinSequence of RS for s being INT -valued FinSequence st rng g c= X & len g = \$1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) holds Sum h in Z_Lin X; A1: S1[ 0 ] proof let g, h be FinSequence of RS; ::_thesis: for s being INT -valued FinSequence st rng g c= X & len g = 0 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) holds Sum h in Z_Lin X let s be INT -valued FinSequence; ::_thesis: ( rng g c= X & len g = 0 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) implies Sum h in Z_Lin X ) set x = Sum h; assume A2: ( rng g c= X & len g = 0 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) ) ; ::_thesis: Sum h in Z_Lin X Sum h = Sum (<*> the carrier of RS) by A2, FINSEQ_1:20 .= 0. RS by RLVECT_1:43 ; hence Sum h in Z_Lin X by Th11; ::_thesis: verum end; A3: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A4: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_for_g,_h_being_FinSequence_of_RS for_s_being_INT_-valued_FinSequence for_x_being_set_st_x_=_Sum_h_&_rng_g_c=_X_&_len_g_=_n_+_1_&_len_g_=_len_h_&_len_g_=_len_s_&_(_for_i_being_Nat_st_i_in_Seg_(len_g)_holds_ h_/._i_=_(s_._i)_*_(g_/._i)_)_holds_ x_in_Z_Lin_X let g, h be FinSequence of RS; ::_thesis: for s being INT -valued FinSequence for x being set st x = Sum h & rng g c= X & len g = n + 1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) holds x in Z_Lin X let s be INT -valued FinSequence; ::_thesis: for x being set st x = Sum h & rng g c= X & len g = n + 1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) holds x in Z_Lin X let x be set ; ::_thesis: ( x = Sum h & rng g c= X & len g = n + 1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) implies x in Z_Lin X ) assume A5: ( x = Sum h & rng g c= X & len g = n + 1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) ) ; ::_thesis: x in Z_Lin X reconsider gn = g | n as FinSequence of RS ; reconsider hn = h | n as FinSequence of RS ; reconsider sn = s | n as real-valued FinSequence ; ( rng gn c= X & len gn = n & len gn = len hn & len gn = len sn & ( for i being Nat st i in Seg (len gn) holds hn /. i = (sn . i) * (gn /. i) ) ) proof rng gn c= rng g by RELAT_1:70; then A6: rng gn c= X by A5, XBOOLE_1:1; A7: n <= len g by A5, NAT_1:11; A8: n <= len h by A5, NAT_1:11; A9: len hn = n by A5, FINSEQ_1:59, NAT_1:11; A10: len sn = n by A5, FINSEQ_1:59, NAT_1:11; for i being Nat st i in Seg (len gn) holds hn /. i = (sn . i) * (gn /. i) proof percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: for i being Nat st i in Seg (len gn) holds hn /. i = (sn . i) * (gn /. i) hence for i being Nat st i in Seg (len gn) holds hn /. i = (sn . i) * (gn /. i) ; ::_thesis: verum end; suppose n <> 0 ; ::_thesis: for i being Nat st i in Seg (len gn) holds hn /. i = (sn . i) * (gn /. i) then A11: n >= 1 by NAT_1:14; let i be Nat; ::_thesis: ( i in Seg (len gn) implies hn /. i = (sn . i) * (gn /. i) ) assume i in Seg (len gn) ; ::_thesis: hn /. i = (sn . i) * (gn /. i) then A12: i in Seg n by A5, FINSEQ_1:59, NAT_1:11; n in Seg (len g) by A7, A11, FINSEQ_1:1; then n in dom g by FINSEQ_1:def_3; then A13: gn /. i = g /. i by A12, FINSEQ_4:71; n in Seg (len h) by A8, A11, FINSEQ_1:1; then n in dom h by FINSEQ_1:def_3; then A14: hn /. i = h /. i by A12, FINSEQ_4:71; i <= n by A12, FINSEQ_1:1; then sn . i = s . i by FINSEQ_3:112; hence hn /. i = (sn . i) * (gn /. i) by A5, A12, A13, A14, FINSEQ_2:8; ::_thesis: verum end; end; end; hence ( rng gn c= X & len gn = n & len gn = len hn & len gn = len sn & ( for i being Nat st i in Seg (len gn) holds hn /. i = (sn . i) * (gn /. i) ) ) by A6, A9, A10, A5, FINSEQ_1:59, NAT_1:11; ::_thesis: verum end; then A15: Sum hn in Z_Lin X by A4; A16: n + 1 in Seg (len g) by A5, FINSEQ_1:4; A17: h /. (n + 1) = (s . (n + 1)) * (g /. (n + 1)) by A5, FINSEQ_1:4; A18: h = hn ^ <*((s . (n + 1)) * (g /. (n + 1)))*> by A5, A17, FINSEQ_5:21; A19: n + 1 in dom g by A16, FINSEQ_1:def_3; then g /. (n + 1) = g . (n + 1) by PARTFUN1:def_6; then g /. (n + 1) in rng g by A19, FUNCT_1:3; then g /. (n + 1) in Z_Lin X by A5, Th12; then A20: (s . (n + 1)) * (g /. (n + 1)) in Z_Lin X by Th10; Sum h = (Sum hn) + (Sum <*((s . (n + 1)) * (g /. (n + 1)))*>) by A18, RLVECT_1:41 .= (Sum hn) + ((s . (n + 1)) * (g /. (n + 1))) by RLVECT_1:44 ; hence x in Z_Lin X by A5, A15, A20, Th9; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A3); hence for g1, h1 being FinSequence of RS for a1 being INT -valued FinSequence st rng g1 c= X & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) holds Sum h1 in Z_Lin X ; ::_thesis: verum end; Lm2: for V being RealLinearSpace for A being Subset of V for x being set st x in Z_Lin A holds ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st ( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) ) proof let V be RealLinearSpace; ::_thesis: for A being Subset of V for x being set st x in Z_Lin A holds ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st ( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) ) let A be Subset of V; ::_thesis: for x being set st x in Z_Lin A holds ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st ( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) ) let x be set ; ::_thesis: ( x in Z_Lin A implies ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st ( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) ) ) assume x in Z_Lin A ; ::_thesis: ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st ( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) ) then consider z being Linear_Combination of A such that A1: ( x = Sum z & rng z c= INT ) ; consider F being FinSequence of V such that A2: ( F is one-to-one & rng F = Carrier z & Sum z = Sum (z (#) F) ) by RLVECT_2:def_8; A3: ( len (z (#) F) = len F & ( for i being Nat st i in dom (z (#) F) holds (z (#) F) . i = (z . (F /. i)) * (F /. i) ) ) by RLVECT_2:def_7; defpred S1[ Nat, set ] means \$2 = z . (F /. \$1); A4: now__::_thesis:_for_k_being_Nat_st_k_in_Seg_(len_F)_holds_ ex_x_being_Element_of_INT_st_S1[k,x] let k be Nat; ::_thesis: ( k in Seg (len F) implies ex x being Element of INT st S1[k,x] ) assume k in Seg (len F) ; ::_thesis: ex x being Element of INT st S1[k,x] z . (F /. k) in rng z by FUNCT_2:4; hence ex x being Element of INT st S1[k,x] by A1; ::_thesis: verum end; consider u being FinSequence of INT such that A5: ( dom u = Seg (len F) & ( for i being Nat st i in Seg (len F) holds S1[i,u . i] ) ) from FINSEQ_1:sch_5(A4); A6: rng F c= A by A2, RLVECT_2:def_6; A7: len F = len (z (#) F) by RLVECT_2:def_7; A8: len F = len u by A5, FINSEQ_1:def_3; now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_F)_holds_ (z_(#)_F)_/._i_=_(u_._i)_*_(F_/._i) let i be Nat; ::_thesis: ( i in Seg (len F) implies (z (#) F) /. i = (u . i) * (F /. i) ) assume A9: i in Seg (len F) ; ::_thesis: (z (#) F) /. i = (u . i) * (F /. i) then A10: i in dom (z (#) F) by A3, FINSEQ_1:def_3; hence (z (#) F) /. i = (z (#) F) . i by PARTFUN1:def_6 .= (z . (F /. i)) * (F /. i) by A10, RLVECT_2:def_7 .= (u . i) * (F /. i) by A5, A9 ; ::_thesis: verum end; hence ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st ( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) ) by A6, A7, A8, A1, A2; ::_thesis: verum end; theorem :: RLVECT_X:25 for V being RealLinearSpace for A being Subset of V for x being set holds ( x in Z_Lin A iff ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st ( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) ) ) by Lm1, Lm2; registration let D be non empty set ; let n be Nat; cluster Relation-like NAT -defined D -valued Function-like finite n -element FinSequence-like FinSubsequence-like for set ; existence ex b1 being FinSequence st ( b1 is n -element & b1 is D -valued ) proof take n |-> the Element of D ; ::_thesis: ( n |-> the Element of D is n -element & n |-> the Element of D is D -valued ) thus ( n |-> the Element of D is n -element & n |-> the Element of D is D -valued ) ; ::_thesis: verum end; end; definition let RS be RealLinearSpace; let f be FinSequence of RS; func Z_Lin f -> Subset of RS equals :: RLVECT_X:def 3 { (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st for i being Nat st i in Seg (len f) holds g /. i = (a . i) * (f /. i) } ; correctness coherence { (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st for i being Nat st i in Seg (len f) holds g /. i = (a . i) * (f /. i) } is Subset of RS; proof now__::_thesis:_for_x_being_set_st_x_in__{__(Sum_g)_where_g_is_len_f_-element_FinSequence_of_RS_:_ex_a_being_INT_-valued_len_f_-element_FinSequence_st_ for_i_being_Nat_st_i_in_Seg_(len_f)_holds_ g_/._i_=_(a_._i)_*_(f_/._i)__}__holds_ x_in_the_carrier_of_RS let x be set ; ::_thesis: ( x in { (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st for i being Nat st i in Seg (len f) holds g /. i = (a . i) * (f /. i) } implies x in the carrier of RS ) assume x in { (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st for i being Nat st i in Seg (len f) holds g /. i = (a . i) * (f /. i) } ; ::_thesis: x in the carrier of RS then ex g being len f -element FinSequence of RS st ( x = Sum g & ex a being INT -valued len f -element FinSequence st for i being Nat st i in Seg (len f) holds g /. i = (a . i) * (f /. i) ) ; hence x in the carrier of RS ; ::_thesis: verum end; hence { (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st for i being Nat st i in Seg (len f) holds g /. i = (a . i) * (f /. i) } is Subset of RS by TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines Z_Lin RLVECT_X:def_3_:_ for RS being RealLinearSpace for f being FinSequence of RS holds Z_Lin f = { (Sum g) where g is len b2 -element FinSequence of RS : ex a being INT -valued len b2 -element FinSequence st for i being Nat st i in Seg (len f) holds g /. i = (a . i) * (f /. i) } ; theorem Th26: :: RLVECT_X:26 for RS being RealLinearSpace for f being FinSequence of RS for x being set holds ( x in Z_Lin f iff ex g being len b2 -element FinSequence of RS ex a being INT -valued len b2 -element FinSequence st ( x = Sum g & ( for i being Nat st i in Seg (len f) holds g /. i = (a . i) * (f /. i) ) ) ) proof let RS be RealLinearSpace; ::_thesis: for f being FinSequence of RS for x being set holds ( x in Z_Lin f iff ex g being len b1 -element FinSequence of RS ex a being INT -valued len b1 -element FinSequence st ( x = Sum g & ( for i being Nat st i in Seg (len f) holds g /. i = (a . i) * (f /. i) ) ) ) let f be FinSequence of RS; ::_thesis: for x being set holds ( x in Z_Lin f iff ex g being len f -element FinSequence of RS ex a being INT -valued len f -element FinSequence st ( x = Sum g & ( for i being Nat st i in Seg (len f) holds g /. i = (a . i) * (f /. i) ) ) ) let x be set ; ::_thesis: ( x in Z_Lin f iff ex g being len f -element FinSequence of RS ex a being INT -valued len f -element FinSequence st ( x = Sum g & ( for i being Nat st i in Seg (len f) holds g /. i = (a . i) * (f /. i) ) ) ) hereby ::_thesis: ( ex g being len f -element FinSequence of RS ex a being INT -valued len f -element FinSequence st ( x = Sum g & ( for i being Nat st i in Seg (len f) holds g /. i = (a . i) * (f /. i) ) ) implies x in Z_Lin f ) assume x in Z_Lin f ; ::_thesis: ex g being len f -element FinSequence of RS ex s being INT -valued len f -element FinSequence st ( x = Sum g & ( for i being Nat st i in Seg (len f) holds g /. i = (s . i) * (f /. i) ) ) then consider g being len f -element FinSequence of RS such that A1: ( x = Sum g & ex s being INT -valued len f -element FinSequence st for i being Nat st i in Seg (len f) holds g /. i = (s . i) * (f /. i) ) ; consider s being INT -valued len f -element FinSequence such that A2: for i being Nat st i in Seg (len f) holds g /. i = (s . i) * (f /. i) by A1; take g = g; ::_thesis: ex s being INT -valued len f -element FinSequence st ( x = Sum g & ( for i being Nat st i in Seg (len f) holds g /. i = (s . i) * (f /. i) ) ) take s = s; ::_thesis: ( x = Sum g & ( for i being Nat st i in Seg (len f) holds g /. i = (s . i) * (f /. i) ) ) thus ( x = Sum g & ( for i being Nat st i in Seg (len f) holds g /. i = (s . i) * (f /. i) ) ) by A1, A2; ::_thesis: verum end; assume ex g being len f -element FinSequence of RS ex a being INT -valued len f -element FinSequence st ( x = Sum g & ( for i being Nat st i in Seg (len f) holds g /. i = (a . i) * (f /. i) ) ) ; ::_thesis: x in Z_Lin f hence x in Z_Lin f ; ::_thesis: verum end; theorem Th27: :: RLVECT_X:27 for RS being RealLinearSpace for f being FinSequence of RS for x, y being Element of RS for a, b being Element of INT st x in Z_Lin f & y in Z_Lin f holds (a * x) + (b * y) in Z_Lin f proof let RS be RealLinearSpace; ::_thesis: for f being FinSequence of RS for x, y being Element of RS for a, b being Element of INT st x in Z_Lin f & y in Z_Lin f holds (a * x) + (b * y) in Z_Lin f let f be FinSequence of RS; ::_thesis: for x, y being Element of RS for a, b being Element of INT st x in Z_Lin f & y in Z_Lin f holds (a * x) + (b * y) in Z_Lin f let x, y be Element of RS; ::_thesis: for a, b being Element of INT st x in Z_Lin f & y in Z_Lin f holds (a * x) + (b * y) in Z_Lin f let a, b be Element of INT ; ::_thesis: ( x in Z_Lin f & y in Z_Lin f implies (a * x) + (b * y) in Z_Lin f ) assume A1: ( x in Z_Lin f & y in Z_Lin f ) ; ::_thesis: (a * x) + (b * y) in Z_Lin f consider g being len f -element FinSequence of RS, s being INT -valued len f -element FinSequence such that A2: ( x = Sum g & ( for i being Nat st i in Seg (len f) holds g /. i = (s . i) * (f /. i) ) ) by A1, Th26; consider h being len f -element FinSequence of RS, t being INT -valued len f -element FinSequence such that A3: ( y = Sum h & ( for i being Nat st i in Seg (len f) holds h /. i = (t . i) * (f /. i) ) ) by A1, Th26; defpred S1[ Nat, set ] means \$2 = (a * (s . \$1)) + (b * (t . \$1)); A4: for k being Nat st k in Seg (len f) holds ex x being Element of INT st S1[k,x] ; consider u being FinSequence of INT such that A5: ( dom u = Seg (len f) & ( for i being Nat st i in Seg (len f) holds S1[i,u . i] ) ) from FINSEQ_1:sch_5(A4); len u = len f by A5, FINSEQ_1:def_3; then reconsider u = u as INT -valued len f -element FinSequence by CARD_1:def_7; defpred S2[ Nat, set ] means \$2 = (a * (g /. \$1)) + (b * (h /. \$1)); A6: for k being Nat st k in Seg (len f) holds ex x being Element of RS st S2[k,x] ; consider w being FinSequence of RS such that A7: ( dom w = Seg (len f) & ( for i being Nat st i in Seg (len f) holds S2[i,w . i] ) ) from FINSEQ_1:sch_5(A6); len w = len f by A7, FINSEQ_1:def_3; then reconsider w = w as len f -element FinSequence of RS by CARD_1:def_7; A8: now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_f)_holds_ w_/._i_=_(a_*_(g_/._i))_+_(b_*_(h_/._i)) let i be Nat; ::_thesis: ( i in Seg (len f) implies w /. i = (a * (g /. i)) + (b * (h /. i)) ) assume A9: i in Seg (len f) ; ::_thesis: w /. i = (a * (g /. i)) + (b * (h /. i)) hence w /. i = w . i by A7, PARTFUN1:def_6 .= (a * (g /. i)) + (b * (h /. i)) by A7, A9 ; ::_thesis: verum end; reconsider a0 = a as Element of REAL by NUMBERS:15, TARSKI:def_3; reconsider b0 = b as Element of REAL by NUMBERS:15, TARSKI:def_3; dom (a0 (#) g) = dom g by VFUNCT_1:def_4 .= Seg (len g) by FINSEQ_1:def_3 ; then A10: a0 (#) g is FinSequence-like by FINSEQ_1:def_2; rng (a0 (#) g) c= the carrier of RS ; then reconsider ag = a0 (#) g as FinSequence of RS by A10, FINSEQ_1:def_4; dom (b0 (#) h) = dom h by VFUNCT_1:def_4 .= Seg (len h) by FINSEQ_1:def_3 ; then A11: b0 (#) h is FinSequence-like by FINSEQ_1:def_2; rng (b0 (#) h) c= the carrier of RS ; then reconsider bh = b0 (#) h as FinSequence of RS by A11, FINSEQ_1:def_4; A12: dom (a0 (#) g) = dom g by VFUNCT_1:def_4 .= Seg (len g) by FINSEQ_1:def_3 .= Seg (len f) by CARD_1:def_7 ; then A13: len ag = len f by FINSEQ_1:def_3; A14: dom (b0 (#) h) = dom h by VFUNCT_1:def_4 .= Seg (len h) by FINSEQ_1:def_3 .= Seg (len f) by CARD_1:def_7 ; A15: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_ag_holds_ w_._i_=_(ag_/._i)_+_(bh_/._i) let i be Element of NAT ; ::_thesis: ( i in dom ag implies w . i = (ag /. i) + (bh /. i) ) assume A16: i in dom ag ; ::_thesis: w . i = (ag /. i) + (bh /. i) hence w . i = (a * (g /. i)) + (b * (h /. i)) by A7, A12 .= (ag /. i) + (b * (h /. i)) by A16, VFUNCT_1:def_4 .= (ag /. i) + (bh /. i) by A16, A14, A12, VFUNCT_1:def_4 ; ::_thesis: verum end; A17: ( len ag = len bh & len ag = len w ) by A7, A13, A14, FINSEQ_1:def_3; A18: for i being Nat st i in Seg (len f) holds w /. i = (u . i) * (f /. i) proof let i be Nat; ::_thesis: ( i in Seg (len f) implies w /. i = (u . i) * (f /. i) ) assume A19: i in Seg (len f) ; ::_thesis: w /. i = (u . i) * (f /. i) hence w /. i = (a * (g /. i)) + (b * (h /. i)) by A8 .= (a * ((s . i) * (f /. i))) + (b * (h /. i)) by A19, A2 .= (a * ((s . i) * (f /. i))) + (b * ((t . i) * (f /. i))) by A19, A3 .= ((a * (s . i)) * (f /. i)) + (b * ((t . i) * (f /. i))) by RLVECT_1:def_7 .= ((a * (s . i)) * (f /. i)) + ((b * (t . i)) * (f /. i)) by RLVECT_1:def_7 .= ((a * (s . i)) + (b * (t . i))) * (f /. i) by RLVECT_1:def_6 .= (u . i) * (f /. i) by A19, A5 ; ::_thesis: verum end; (a * x) + (b * y) = (Sum ag) + (b * (Sum h)) by A2, A3, Th3 .= (Sum ag) + (Sum bh) by Th3 .= Sum w by A15, A17, RLVECT_2:2 ; hence (a * x) + (b * y) in Z_Lin f by A18; ::_thesis: verum end; theorem Th28: :: RLVECT_X:28 for RS being RealLinearSpace for f being FinSequence of RS st f = (Seg (len f)) --> (0. RS) holds Sum f = 0. RS proof let RS be RealLinearSpace; ::_thesis: for f being FinSequence of RS st f = (Seg (len f)) --> (0. RS) holds Sum f = 0. RS let f be FinSequence of RS; ::_thesis: ( f = (Seg (len f)) --> (0. RS) implies Sum f = 0. RS ) assume A1: f = (Seg (len f)) --> (0. RS) ; ::_thesis: Sum f = 0. RS A2: now__::_thesis:_for_k_being_Element_of_NAT_ for_v_being_Element_of_RS_st_k_in_dom_f_&_v_=_f_._k_holds_ f_._k_=_-_v let k be Element of NAT ; ::_thesis: for v being Element of RS st k in dom f & v = f . k holds f . k = - v let v be Element of RS; ::_thesis: ( k in dom f & v = f . k implies f . k = - v ) assume A3: ( k in dom f & v = f . k ) ; ::_thesis: f . k = - v then k in Seg (len f) by FINSEQ_1:def_3; then f . k = 0. RS by A1, FUNCOP_1:7; hence f . k = - v by A3, RLVECT_1:12; ::_thesis: verum end; len f = len f ; then Sum f = - (Sum f) by A2, RLVECT_1:40; hence Sum f = 0. RS by RLVECT_1:19; ::_thesis: verum end; theorem Th29: :: RLVECT_X:29 for RS being RealLinearSpace for f being FinSequence of RS for v being Element of RS for i being Nat st i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) holds Sum f = v proof let RS be RealLinearSpace; ::_thesis: for f being FinSequence of RS for v being Element of RS for i being Nat st i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) holds Sum f = v let f be FinSequence of RS; ::_thesis: for v being Element of RS for i being Nat st i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) holds Sum f = v let v be Element of RS; ::_thesis: for i being Nat st i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) holds Sum f = v let i be Nat; ::_thesis: ( i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) implies Sum f = v ) defpred S1[ Nat] means for g being FinSequence of RS st len g = \$1 & i in Seg (len g) & g = ((Seg (len g)) --> (0. RS)) +* ({i} --> v) holds Sum g = v; A1: S1[ 0 ] ; A2: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A3: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_for_f_being_FinSequence_of_RS_st_len_f_=_n_+_1_&_i_in_Seg_(len_f)_&_f_=_((Seg_(len_f))_-->_(0._RS))_+*_({i}_-->_v)_holds_ for_f1_being_Function_st_f1_=_(Seg_(len_f))_-->_(0._RS)_holds_ for_f2_being_Function_st_f2_=_{i}_-->_v_holds_ Sum_f_=_v let f be FinSequence of RS; ::_thesis: ( len f = n + 1 & i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) implies for f1 being Function st f1 = (Seg (len f)) --> (0. RS) holds for f2 being Function st f2 = {i} --> v holds Sum b3 = v ) assume A4: ( len f = n + 1 & i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) ) ; ::_thesis: for f1 being Function st f1 = (Seg (len f)) --> (0. RS) holds for f2 being Function st f2 = {i} --> v holds Sum b3 = v reconsider g = f | n as FinSequence of RS ; n + 1 in Seg (n + 1) by FINSEQ_1:4; then A5: n + 1 in dom f by A4, FINSEQ_1:def_3; A6: len g = n by A4, FINSEQ_1:59, NAT_1:11; f = (f | n) ^ <*(f . (n + 1))*> by A4, FINSEQ_3:55 .= g ^ <*(f /. (n + 1))*> by A5, PARTFUN1:def_6 ; then A7: Sum f = (Sum g) + (Sum <*(f /. (n + 1))*>) by RLVECT_1:41; A8: dom ({i} --> v) = {i} by FUNCOP_1:13; let f1 be Function; ::_thesis: ( f1 = (Seg (len f)) --> (0. RS) implies for f2 being Function st f2 = {i} --> v holds Sum b2 = v ) assume A9: f1 = (Seg (len f)) --> (0. RS) ; ::_thesis: for f2 being Function st f2 = {i} --> v holds Sum b2 = v let f2 be Function; ::_thesis: ( f2 = {i} --> v implies Sum b1 = v ) assume A10: f2 = {i} --> v ; ::_thesis: Sum b1 = v percases ( i = n + 1 or i <> n + 1 ) ; supposeA11: i = n + 1 ; ::_thesis: Sum b1 = v then dom f2 = {(n + 1)} by A10, FUNCOP_1:13; then g = f1 | (Seg n) by A4, A9, A10, FINSEQ_3:14, FUNCT_4:72 .= ((Seg (len f)) /\ (Seg n)) --> (0. RS) by A9, FUNCOP_1:12 ; then A12: g = (Seg n) --> (0. RS) by A4, FINSEQ_1:7, NAT_1:11; A13: n + 1 in {(n + 1)} by ZFMISC_1:31; then n + 1 in dom f2 by A10, A11, FUNCOP_1:13; then f . (n + 1) = f2 . (n + 1) by A4, A10, FUNCT_4:13 .= v by A10, A11, A13, FUNCOP_1:7 ; then A14: f /. (n + 1) = v by A5, PARTFUN1:def_6; Sum g = 0. RS by A6, A12, Th28; hence Sum f = (0. RS) + v by A7, A14, RLVECT_1:44 .= v by RLVECT_1:4 ; ::_thesis: verum end; supposeA15: i <> n + 1 ; ::_thesis: Sum b1 = v then ( i < n + 1 or i > n + 1 ) by XXREAL_0:1; then ( 1 <= i & i <= n ) by A4, FINSEQ_1:1, NAT_1:13; then A16: i in Seg (len g) by A6, FINSEQ_1:1; g = (f1 | (Seg n)) +* (f2 | (Seg n)) by A4, A9, A10, FUNCT_4:71 .= (((Seg (len f)) /\ (Seg n)) --> (0. RS)) +* (f2 | (Seg n)) by A9, FUNCOP_1:12 .= ((Seg (len g)) --> (0. RS)) +* (f2 | (Seg n)) by A4, A6, FINSEQ_1:7, NAT_1:11 .= ((Seg (len g)) --> (0. RS)) +* (({i} /\ (Seg n)) --> v) by A10, FUNCOP_1:12 ; then A17: g = ((Seg (len g)) --> (0. RS)) +* ({i} --> v) by A6, A16, ZFMISC_1:46; not {(n + 1)} c= dom f2 by A8, A10, A15, ZFMISC_1:3; then not n + 1 in dom f2 by ZFMISC_1:31; then f . (n + 1) = f1 . (n + 1) by A4, A9, A10, FUNCT_4:11 .= 0. RS by A4, A9, FINSEQ_1:4, FUNCOP_1:7 ; then A18: f /. (n + 1) = 0. RS by A5, PARTFUN1:def_6; Sum g = v by A16, A17, A6, A3; hence Sum f = v + (0. RS) by A7, A18, RLVECT_1:44 .= v by RLVECT_1:4 ; ::_thesis: verum end; end; end; hence S1[n + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence ( i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) implies Sum f = v ) ; ::_thesis: verum end; theorem Th30: :: RLVECT_X:30 for RS being RealLinearSpace for f being FinSequence of RS for i being Nat st i in Seg (len f) holds f /. i in Z_Lin f proof let RS be RealLinearSpace; ::_thesis: for f being FinSequence of RS for i being Nat st i in Seg (len f) holds f /. i in Z_Lin f let f be FinSequence of RS; ::_thesis: for i being Nat st i in Seg (len f) holds f /. i in Z_Lin f let i be Nat; ::_thesis: ( i in Seg (len f) implies f /. i in Z_Lin f ) assume A1: i in Seg (len f) ; ::_thesis: f /. i in Z_Lin f set s = ((Seg (len f)) --> 0) +* ({i} --> 1); A2: dom (((Seg (len f)) --> 0) +* ({i} --> 1)) = Seg (len f) proof dom (((Seg (len f)) --> 0) +* ({i} --> 1)) = (dom ((Seg (len f)) --> 0)) \/ (dom ({i} --> 1)) by FUNCT_4:def_1 .= (Seg (len f)) \/ (dom ({i} --> 1)) by FUNCOP_1:13 .= (Seg (len f)) \/ {i} by FUNCOP_1:13 ; hence dom (((Seg (len f)) --> 0) +* ({i} --> 1)) = Seg (len f) by A1, ZFMISC_1:40; ::_thesis: verum end; then A3: ((Seg (len f)) --> 0) +* ({i} --> 1) is FinSequence-like by FINSEQ_1:def_2; rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= INT proof rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= (rng ((Seg (len f)) --> 0)) \/ (rng ({i} --> 1)) by FUNCT_4:17; hence rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= INT by XBOOLE_1:1; ::_thesis: verum end; then reconsider s = ((Seg (len f)) --> 0) +* ({i} --> 1) as FinSequence of INT by A3, FINSEQ_1:def_4; len s = len f by A2, FINSEQ_1:def_3; then reconsider s = s as INT -valued len f -element FinSequence by CARD_1:def_7; defpred S1[ Nat, set ] means \$2 = (s . \$1) * (f /. \$1); A6: for k being Nat st k in Seg (len f) holds ex x being Element of RS st S1[k,x] ; consider w being FinSequence of RS such that A7: ( dom w = Seg (len f) & ( for i being Nat st i in Seg (len f) holds S1[i,w . i] ) ) from FINSEQ_1:sch_5(A6); A8: len w = len f by A7, FINSEQ_1:def_3; then reconsider w = w as len f -element FinSequence of RS by CARD_1:def_7; now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_f)_holds_ w_/._i_=_(s_._i)_*_(f_/._i) let i be Nat; ::_thesis: ( i in Seg (len f) implies w /. i = (s . i) * (f /. i) ) assume A9: i in Seg (len f) ; ::_thesis: w /. i = (s . i) * (f /. i) hence w /. i = w . i by A7, PARTFUN1:def_6 .= (s . i) * (f /. i) by A7, A9 ; ::_thesis: verum end; then A10: Sum w in Z_Lin f ; A11: w = ((Seg (len w)) --> (0. RS)) +* ({i} --> (f /. i)) proof consider w1 being Function such that A12: w1 = (Seg (len f)) --> (0. RS) ; A13: dom w1 = Seg (len f) by A12, FUNCOP_1:13; consider w2 being Function such that A14: w2 = {i} --> (f /. i) ; A15: dom w2 = {i} by A14, FUNCOP_1:13; consider ww being Function such that A16: ww = w1 +* w2 ; A17: dom ww = (Seg (len f)) \/ {i} by A13, A15, A16, FUNCT_4:def_1 .= Seg (len f) by A1, ZFMISC_1:40 ; then reconsider ww = ww as FinSequence by FINSEQ_1:def_2; rng w1 c= {(0. RS)} by A12, FUNCOP_1:13; then A18: rng w1 c= the carrier of RS by XBOOLE_1:1; rng w2 c= {(f /. i)} by A14, FUNCOP_1:13; then A19: rng w2 c= the carrier of RS by XBOOLE_1:1; A20: rng ww c= (rng w1) \/ (rng w2) by A16, FUNCT_4:17; (rng w1) \/ (rng w2) c= the carrier of RS by A18, A19, XBOOLE_1:8; then rng ww c= the carrier of RS by A20, XBOOLE_1:1; then reconsider ww = ww as FinSequence of RS by FINSEQ_1:def_4; for j being Nat st j in dom w holds w /. j = ww /. j proof let j be Nat; ::_thesis: ( j in dom w implies w /. j = ww /. j ) assume A21: j in dom w ; ::_thesis: w /. j = ww /. j A22: dom ({i} --> 1) = {i} by FUNCOP_1:13; percases ( j in dom w2 or not j in dom w2 ) ; supposeA23: j in dom w2 ; ::_thesis: w /. j = ww /. j then A24: j = i by A15, TARSKI:def_1; then w /. j = w . i by A21, PARTFUN1:def_6; then A25: w /. j = (s . i) * (f /. i) by A7, A21, A24; A26: i in {i} by TARSKI:def_1; then A27: s . i = ({i} --> 1) . i by A22, FUNCT_4:13 .= 1 by A26, FUNCOP_1:7 ; ww /. j = ww . j by A7, A17, A21, PARTFUN1:def_6 .= w2 . j by A16, A23, FUNCT_4:13 .= f /. i by A14, A15, A23, FUNCOP_1:7 ; hence w /. j = ww /. j by A25, A27, RLVECT_1:def_8; ::_thesis: verum end; supposeA28: not j in dom w2 ; ::_thesis: w /. j = ww /. j w /. j = w . j by A21, PARTFUN1:def_6; then A29: w /. j = (s . j) * (f /. j) by A7, A21; not j in dom ({i} --> 1) by A15, A28; then A30: s . j = ((Seg (len f)) --> 0) . j by FUNCT_4:11 .= 0 by A7, A21, FUNCOP_1:7 ; ww /. j = ww . j by A7, A17, A21, PARTFUN1:def_6 .= w1 . j by A16, A28, FUNCT_4:11 .= 0. RS by A7, A12, A21, FUNCOP_1:7 ; hence w /. j = ww /. j by A29, A30, RLVECT_1:10; ::_thesis: verum end; end; end; hence w = ((Seg (len w)) --> (0. RS)) +* ({i} --> (f /. i)) by A7, A8, A12, A14, A16, A17, FINSEQ_5:12; ::_thesis: verum end; i in Seg (len w) by A7, A1, FINSEQ_1:def_3; hence f /. i in Z_Lin f by A10, A11, Th29; ::_thesis: verum end; theorem Th31: :: RLVECT_X:31 for RS being RealLinearSpace for f being FinSequence of RS holds rng f c= Z_Lin f proof let RS be RealLinearSpace; ::_thesis: for f being FinSequence of RS holds rng f c= Z_Lin f let f be FinSequence of RS; ::_thesis: rng f c= Z_Lin f let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Z_Lin f ) assume y in rng f ; ::_thesis: y in Z_Lin f then consider x being set such that A1: ( x in dom f & y = f . x ) by FUNCT_1:def_3; A2: x in Seg (len f) by A1, FINSEQ_1:def_3; reconsider i = x as Nat by A1; y = f /. i by A1, PARTFUN1:def_6; hence y in Z_Lin f by A2, Th30; ::_thesis: verum end; theorem Th32: :: RLVECT_X:32 for RS being RealLinearSpace for f being non empty FinSequence of RS for g, h being FinSequence of RS for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) holds Sum h in Z_Lin f proof let RS be RealLinearSpace; ::_thesis: for f being non empty FinSequence of RS for g, h being FinSequence of RS for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) holds Sum h in Z_Lin f let f be non empty FinSequence of RS; ::_thesis: for g, h being FinSequence of RS for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) holds Sum h in Z_Lin f ( 1 <= 1 & 1 <= len f ) by FINSEQ_1:20; then 1 in Seg (len f) ; then A1: f /. 1 in Z_Lin f by Th30; reconsider z0 = 0 as Element of INT by NUMBERS:17, TARSKI:def_3; reconsider z1 = 1 as Element of INT by NUMBERS:17, TARSKI:def_3; (z0 * (f /. 1)) + (z0 * (f /. 1)) in Z_Lin f by Th27, A1; then (z0 * (f /. 1)) + (0. RS) in Z_Lin f by RLVECT_1:10; then A2: (0. RS) + (0. RS) in Z_Lin f by RLVECT_1:10; defpred S1[ Nat] means for g, h being FinSequence of RS for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = \$1 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) holds Sum h in Z_Lin f; A3: S1[ 0 ] proof let g, h be FinSequence of RS; ::_thesis: for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = 0 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) holds Sum h in Z_Lin f let s be INT -valued FinSequence; ::_thesis: ( rng g c= Z_Lin f & len g = 0 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) implies Sum h in Z_Lin f ) assume A4: ( rng g c= Z_Lin f & len g = 0 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) ) ; ::_thesis: Sum h in Z_Lin f Sum h = Sum (<*> the carrier of RS) by A4, FINSEQ_1:20 .= 0. RS by RLVECT_1:43 ; hence Sum h in Z_Lin f by A2, RLVECT_1:4; ::_thesis: verum end; A5: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A6: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_for_g,_h_being_FinSequence_of_RS for_s_being_INT_-valued_FinSequence_st_rng_g_c=_Z_Lin_f_&_len_g_=_n_+_1_&_len_g_=_len_s_&_len_g_=_len_h_&_(_for_i_being_Nat_st_i_in_Seg_(len_g)_holds_ h_/._i_=_(s_._i)_*_(g_/._i)_)_holds_ Sum_h_in_Z_Lin_f let g, h be FinSequence of RS; ::_thesis: for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = n + 1 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) holds Sum h in Z_Lin f let s be INT -valued FinSequence; ::_thesis: ( rng g c= Z_Lin f & len g = n + 1 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) implies Sum h in Z_Lin f ) assume A7: ( rng g c= Z_Lin f & len g = n + 1 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) ) ; ::_thesis: Sum h in Z_Lin f reconsider gn = g | n as FinSequence of RS ; reconsider hn = h | n as FinSequence of RS ; reconsider sn = s | n as INT -valued FinSequence ; A8: ( rng gn c= Z_Lin f & len gn = n & len gn = len sn & len gn = len hn & ( for i being Nat st i in Seg (len gn) holds hn /. i = (sn . i) * (gn /. i) ) ) proof A9: rng gn c= rng g by RELAT_1:70; A10: n <= len g by A7, NAT_1:11; A11: n <= len h by A7, NAT_1:11; A12: len hn = n by A7, FINSEQ_1:59, NAT_1:11; A13: len sn = n by A7, FINSEQ_1:59, NAT_1:11; for i being Nat st i in Seg (len gn) holds hn /. i = (sn . i) * (gn /. i) proof percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: for i being Nat st i in Seg (len gn) holds hn /. i = (sn . i) * (gn /. i) hence for i being Nat st i in Seg (len gn) holds hn /. i = (sn . i) * (gn /. i) ; ::_thesis: verum end; suppose n <> 0 ; ::_thesis: for i being Nat st i in Seg (len gn) holds hn /. i = (sn . i) * (gn /. i) then A14: n >= 1 by NAT_1:14; let i be Nat; ::_thesis: ( i in Seg (len gn) implies hn /. i = (sn . i) * (gn /. i) ) assume i in Seg (len gn) ; ::_thesis: hn /. i = (sn . i) * (gn /. i) then A15: i in Seg n by A7, FINSEQ_1:59, NAT_1:11; n in Seg (len g) by A10, A14, FINSEQ_1:1; then n in dom g by FINSEQ_1:def_3; then A16: gn /. i = g /. i by A15, FINSEQ_4:71; n in Seg (len h) by A11, A14, FINSEQ_1:1; then n in dom h by FINSEQ_1:def_3; then A17: hn /. i = h /. i by A15, FINSEQ_4:71; i <= n by A15, FINSEQ_1:1; then sn . i = s . i by FINSEQ_3:112; hence hn /. i = (sn . i) * (gn /. i) by A7, A15, A16, A17, FINSEQ_2:8; ::_thesis: verum end; end; end; hence ( rng gn c= Z_Lin f & len gn = n & len gn = len sn & len gn = len hn & ( for i being Nat st i in Seg (len gn) holds hn /. i = (sn . i) * (gn /. i) ) ) by A9, A10, A12, A13, A7, FINSEQ_1:59, XBOOLE_1:1; ::_thesis: verum end; A18: Sum hn in Z_Lin f by A8, A6; A19: n + 1 in Seg (len g) by A7, FINSEQ_1:4; A20: h /. (n + 1) = (s . (n + 1)) * (g /. (n + 1)) by A7, FINSEQ_1:4; A21: h = hn ^ <*((s . (n + 1)) * (g /. (n + 1)))*> by A7, A20, FINSEQ_5:21; A22: n + 1 in dom g by A19, FINSEQ_1:def_3; then g /. (n + 1) = g . (n + 1) by PARTFUN1:def_6; then g /. (n + 1) in rng g by A22, FUNCT_1:3; then ((z1 * (s . (n + 1))) * (g /. (n + 1))) + (z0 * (g /. (n + 1))) in Z_Lin f by A7, Th27; then ((z1 * (s . (n + 1))) * (g /. (n + 1))) + (0. RS) in Z_Lin f by RLVECT_1:10; then (z1 * (s . (n + 1))) * (g /. (n + 1)) in Z_Lin f by RLVECT_1:4; then (z1 * (Sum hn)) + (z1 * ((s . (n + 1)) * (g /. (n + 1)))) in Z_Lin f by A18, Th27; then A23: (z1 * (Sum hn)) + ((s . (n + 1)) * (g /. (n + 1))) in Z_Lin f by RLVECT_1:def_8; Sum h = (Sum hn) + (Sum <*((s . (n + 1)) * (g /. (n + 1)))*>) by A21, RLVECT_1:41 .= (Sum hn) + ((s . (n + 1)) * (g /. (n + 1))) by RLVECT_1:44 ; hence Sum h in Z_Lin f by A23, RLVECT_1:def_8; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A5); hence for g, h being FinSequence of RS for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds h /. i = (s . i) * (g /. i) ) holds Sum h in Z_Lin f ; ::_thesis: verum end; theorem :: RLVECT_X:33 for RS being RealLinearSpace for f being non empty FinSequence of RS holds Z_Lin (rng f) = Z_Lin f proof let RS be RealLinearSpace; ::_thesis: for f being non empty FinSequence of RS holds Z_Lin (rng f) = Z_Lin f let f be non empty FinSequence of RS; ::_thesis: Z_Lin (rng f) = Z_Lin f for x being set holds ( x in Z_Lin (rng f) iff x in Z_Lin f ) proof let x be set ; ::_thesis: ( x in Z_Lin (rng f) iff x in Z_Lin f ) hereby ::_thesis: ( x in Z_Lin f implies x in Z_Lin (rng f) ) assume x in Z_Lin (rng f) ; ::_thesis: x in Z_Lin f then consider g, h being FinSequence of RS, a being INT -valued FinSequence such that A1: ( x = Sum h & rng g c= rng f & len g = len h & len g = len a & ( for i being Nat st i in Seg (len g) holds h /. i = (a . i) * (g /. i) ) ) by Lm2; rng f c= Z_Lin f by Th31; hence x in Z_Lin f by A1, Th32, XBOOLE_1:1; ::_thesis: verum end; assume x in Z_Lin f ; ::_thesis: x in Z_Lin (rng f) then consider g being len f -element FinSequence of RS, a being INT -valued len f -element FinSequence such that A2: ( x = Sum g & ( for i being Nat st i in Seg (len f) holds g /. i = (a . i) * (f /. i) ) ) by Th26; ( len f = len g & len a = len f ) by CARD_1:def_7; hence x in Z_Lin (rng f) by A2, Lm1; ::_thesis: verum end; hence Z_Lin (rng f) = Z_Lin f by TARSKI:1; ::_thesis: verum end; theorem Th34: :: RLVECT_X:34 for V being RealLinearSpace for A being Subset of V holds Lin (Z_Lin A) = Lin A proof let V be RealLinearSpace; ::_thesis: for A being Subset of V holds Lin (Z_Lin A) = Lin A let A be Subset of V; ::_thesis: Lin (Z_Lin A) = Lin A for x being set st x in A holds x in Z_Lin A by Th12; then A c= Z_Lin A by TARSKI:def_3; then A1: Lin A is Subspace of Lin (Z_Lin A) by RLVECT_3:20; reconsider W = the carrier of (Lin A) as Subset of V by RLSUB_1:def_2; Lin (Z_Lin A) is Subspace of Lin W by Th8, RLVECT_3:20; then Lin (Z_Lin A) is Subspace of Lin A by RLVECT_3:18; hence Lin (Z_Lin A) = Lin A by A1, RLSUB_1:26; ::_thesis: verum end; theorem Th35: :: RLVECT_X:35 for V being RealLinearSpace for A being Subset of V for x being set for g1, h1 being FinSequence of V for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) holds x in Z_Lin A proof let V be RealLinearSpace; ::_thesis: for A being Subset of V for x being set for g1, h1 being FinSequence of V for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) holds x in Z_Lin A let A be Subset of V; ::_thesis: for x being set for g1, h1 being FinSequence of V for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) holds x in Z_Lin A reconsider z0 = 0 as Element of INT by NUMBERS:17, TARSKI:def_3; reconsider z1 = 1 as Element of INT by NUMBERS:17, TARSKI:def_3; defpred S1[ Nat] means for x being set for g1, h1 being FinSequence of V for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = \$1 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) holds x in Z_Lin A; A1: S1[ 0 ] proof let x be set ; ::_thesis: for g1, h1 being FinSequence of V for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = 0 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) holds x in Z_Lin A let g1, h1 be FinSequence of V; ::_thesis: for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = 0 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) holds x in Z_Lin A let a1 be INT -valued FinSequence; ::_thesis: ( x = Sum h1 & rng g1 c= Z_Lin A & len g1 = 0 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) implies x in Z_Lin A ) assume A2: ( x = Sum h1 & rng g1 c= Z_Lin A & len g1 = 0 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) ) ; ::_thesis: x in Z_Lin A Sum h1 = Sum (<*> the carrier of V) by A2, FINSEQ_1:20 .= 0. V by RLVECT_1:43 ; hence x in Z_Lin A by A2, Th11; ::_thesis: verum end; A3: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A4: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_for_x_being_set_ for_g1,_h1_being_FinSequence_of_V for_a1_being_INT_-valued_FinSequence_st_x_=_Sum_h1_&_rng_g1_c=_Z_Lin_A_&_len_g1_=_n_+_1_&_len_g1_=_len_h1_&_len_g1_=_len_a1_&_(_for_i_being_Nat_st_i_in_Seg_(len_g1)_holds_ h1_/._i_=_(a1_._i)_*_(g1_/._i)_)_holds_ Sum_h1_in_Z_Lin_A let x be set ; ::_thesis: for g1, h1 being FinSequence of V for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = n + 1 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) holds Sum h1 in Z_Lin A let g1, h1 be FinSequence of V; ::_thesis: for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = n + 1 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) holds Sum h1 in Z_Lin A let a1 be INT -valued FinSequence; ::_thesis: ( x = Sum h1 & rng g1 c= Z_Lin A & len g1 = n + 1 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) implies Sum h1 in Z_Lin A ) assume A5: ( x = Sum h1 & rng g1 c= Z_Lin A & len g1 = n + 1 & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) ) ; ::_thesis: Sum h1 in Z_Lin A reconsider gn = g1 | n as FinSequence of V ; reconsider hn = h1 | n as FinSequence of V ; reconsider an = a1 | n as INT -valued FinSequence ; A6: ( rng gn c= Z_Lin A & len gn = n & len gn = len an & len gn = len hn & ( for i being Nat st i in Seg (len gn) holds hn /. i = (an . i) * (gn /. i) ) ) proof A7: rng gn c= rng g1 by RELAT_1:70; A8: n <= len g1 by A5, NAT_1:11; A9: n <= len h1 by A5, NAT_1:11; A10: len hn = n by A5, FINSEQ_1:59, NAT_1:11; A11: len an = n by A5, FINSEQ_1:59, NAT_1:11; for i being Nat st i in Seg (len gn) holds hn /. i = (an . i) * (gn /. i) proof percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: for i being Nat st i in Seg (len gn) holds hn /. i = (an . i) * (gn /. i) hence for i being Nat st i in Seg (len gn) holds hn /. i = (an . i) * (gn /. i) ; ::_thesis: verum end; suppose n <> 0 ; ::_thesis: for i being Nat st i in Seg (len gn) holds hn /. i = (an . i) * (gn /. i) then A12: n >= 1 by NAT_1:14; let i be Nat; ::_thesis: ( i in Seg (len gn) implies hn /. i = (an . i) * (gn /. i) ) assume i in Seg (len gn) ; ::_thesis: hn /. i = (an . i) * (gn /. i) then A13: i in Seg n by A5, FINSEQ_1:59, NAT_1:11; n in Seg (len g1) by A8, A12, FINSEQ_1:1; then n in dom g1 by FINSEQ_1:def_3; then A14: gn /. i = g1 /. i by A13, FINSEQ_4:71; n in Seg (len h1) by A9, A12, FINSEQ_1:1; then n in dom h1 by FINSEQ_1:def_3; then A15: hn /. i = h1 /. i by A13, FINSEQ_4:71; i <= n by A13, FINSEQ_1:1; then an . i = a1 . i by FINSEQ_3:112; hence hn /. i = (an . i) * (gn /. i) by A5, A13, A14, A15, FINSEQ_2:8; ::_thesis: verum end; end; end; hence ( rng gn c= Z_Lin A & len gn = n & len gn = len an & len gn = len hn & ( for i being Nat st i in Seg (len gn) holds hn /. i = (an . i) * (gn /. i) ) ) by A5, A7, A8, A10, A11, FINSEQ_1:59, XBOOLE_1:1; ::_thesis: verum end; A16: n + 1 in Seg (len g1) by A5, FINSEQ_1:4; A17: h1 /. (n + 1) = (a1 . (n + 1)) * (g1 /. (n + 1)) by A5, FINSEQ_1:4; A18: h1 = hn ^ <*((a1 . (n + 1)) * (g1 /. (n + 1)))*> by A5, A17, FINSEQ_5:21; A19: n + 1 in dom g1 by A16, FINSEQ_1:def_3; then g1 /. (n + 1) = g1 . (n + 1) by PARTFUN1:def_6; then g1 /. (n + 1) in rng g1 by A19, FUNCT_1:3; then ( (z1 * (a1 . (n + 1))) * (g1 /. (n + 1)) in Z_Lin A & z0 * (g1 /. (n + 1)) in Z_Lin A ) by A5, Th10; then ((z1 * (a1 . (n + 1))) * (g1 /. (n + 1))) + (z0 * (g1 /. (n + 1))) in Z_Lin A by Th9; then ((z1 * (a1 . (n + 1))) * (g1 /. (n + 1))) + (0. V) in Z_Lin A by RLVECT_1:10; then A20: (z1 * (a1 . (n + 1))) * (g1 /. (n + 1)) in Z_Lin A by RLVECT_1:4; z1 * (Sum hn) in Z_Lin A by A4, A6, Th10; then A21: (z1 * (Sum hn)) + ((z1 * (a1 . (n + 1))) * (g1 /. (n + 1))) in Z_Lin A by A20, Th9; Sum h1 = (Sum hn) + (Sum <*((a1 . (n + 1)) * (g1 /. (n + 1)))*>) by A18, RLVECT_1:41 .= (Sum hn) + ((a1 . (n + 1)) * (g1 /. (n + 1))) by RLVECT_1:44 ; hence Sum h1 in Z_Lin A by A21, RLVECT_1:def_8; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A3); hence for x being set for g1, h1 being FinSequence of V for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) holds x in Z_Lin A ; ::_thesis: verum end; theorem :: RLVECT_X:36 for V being RealLinearSpace for A being Subset of V holds Z_Lin (Z_Lin A) = Z_Lin A proof let V be RealLinearSpace; ::_thesis: for A being Subset of V holds Z_Lin (Z_Lin A) = Z_Lin A let A be Subset of V; ::_thesis: Z_Lin (Z_Lin A) = Z_Lin A for x being set st x in A holds x in Z_Lin A by Th12; then A c= Z_Lin A by TARSKI:def_3; then A1: Z_Lin A c= Z_Lin (Z_Lin A) by Th13; Z_Lin (Z_Lin A) c= Z_Lin A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z_Lin (Z_Lin A) or x in Z_Lin A ) assume x in Z_Lin (Z_Lin A) ; ::_thesis: x in Z_Lin A then consider g1, h1 being FinSequence of V, a1 being INT -valued FinSequence such that A2: ( x = Sum h1 & rng g1 c= Z_Lin A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds h1 /. i = (a1 . i) * (g1 /. i) ) ) by Lm2; thus x in Z_Lin A by A2, Th35; ::_thesis: verum end; hence Z_Lin (Z_Lin A) = Z_Lin A by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: RLVECT_X:37 for V being RealLinearSpace for A, B being Subset of V st Z_Lin A = Z_Lin B holds Lin A = Lin B proof let V be RealLinearSpace; ::_thesis: for A, B being Subset of V st Z_Lin A = Z_Lin B holds Lin A = Lin B let A, B be Subset of V; ::_thesis: ( Z_Lin A = Z_Lin B implies Lin A = Lin B ) assume Z_Lin A = Z_Lin B ; ::_thesis: Lin A = Lin B hence Lin A = Lin (Z_Lin B) by Th34 .= Lin B by Th34 ; ::_thesis: verum end;