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)

per cases ( ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) or v1 = v2 or v1 = v3 or v2 = v3 ) ;

suppose A2: ( 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)

per cases ( {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 Element of REAL by XREAL_0:def 1;

now :: thesis: x in Z_Lin {v1,v2,v3}

per cases ( v1 = v2 or v1 = v3 or v2 = v3 or ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ) ;

suppose A11: ( 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}

per cases ( 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;

suppose A12: 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;

suppose A14: 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;

suppose A16: ( 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 = H₁(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 object ; :: 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 object ; :: 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 object 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;

per cases ( 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; :: 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