environ
vocabularies HIDDEN, REAL_1, RLVECT_1, RLSUB_1, XBOOLE_0, SUBSET_1, FUNCT_1, RLVECT_2, CARD_1, STRUCT_0, NUMBERS, FUNCT_2, TARSKI, ARYTM_3, ARYTM_1, SUPINF_2, RELAT_1, CARD_3, FINSEQ_1, VALUED_1, RLVECT_3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, FINSEQ_1, FUNCT_1, FUNCT_2, XCMPLX_0, XREAL_0, REAL_1, DOMAIN_1, FINSEQ_4, STRUCT_0, RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3;
definitions RLVECT_3, TARSKI, XBOOLE_0;
theorems ENUMSET1, FINSEQ_1, FINSEQ_3, RLSUB_1, RLSUB_2, RLVECT_1, RLVECT_2, RLVECT_3, SETWISEO, TARSKI, ZFMISC_1, FUNCT_2, XCMPLX_0, XCMPLX_1, FINSEQ_2, XREAL_0;
schemes FUNCT_2;
registrations RELSET_1, FINSET_1, NUMBERS, STRUCT_0, ORDINAL1, XREAL_0;
constructors HIDDEN, DOMAIN_1, REAL_1, FINSEQ_4, RLVECT_2, RLVECT_3, RELSET_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, RLVECT_1;
expansions RLVECT_3, TARSKI, XBOOLE_0;
Lm2:
now for V being RealLinearSpace
for v1, v2 being VECTOR of V
for a, b being Real st v1 <> v2 holds
ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b )
let V be
RealLinearSpace;
for v1, v2 being VECTOR of V
for a, b being Real st v1 <> v2 holds
ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b )let v1,
v2 be
VECTOR of
V;
for a, b being Real st v1 <> v2 holds
ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b )let a,
b be
Real;
( v1 <> v2 implies ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b ) )assume A1:
v1 <> v2
;
ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b )thus
ex
l being
Linear_Combination of
{v1,v2} st
(
l . v1 = a &
l . v2 = b )
verum
end;
Lm3:
now for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds
ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c )
let V be
RealLinearSpace;
for v1, v2, v3 being VECTOR of V
for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds
ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c )let v1,
v2,
v3 be
VECTOR of
V;
for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds
ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c )let a,
b,
c be
Real;
( v1 <> v2 & v1 <> v3 & v2 <> v3 implies ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c ) )assume that A1:
v1 <> v2
and A2:
v1 <> v3
and A3:
v2 <> v3
;
ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c )thus
ex
l being
Linear_Combination of
{v1,v2,v3} st
(
l . v1 = a &
l . v2 = b &
l . v3 = c )
verum
proof
reconsider zz =
0 ,
a =
a,
b =
b,
c =
c as
Element of
REAL by XREAL_0:def 1;
deffunc H1(
VECTOR of
V)
-> Element of
REAL =
zz;
consider f being
Function of the
carrier of
V,
REAL such that A4:
(
f . v1 = a &
f . v2 = b &
f . v3 = c )
and A5:
for
u being
VECTOR of
V st
u <> v1 &
u <> v2 &
u <> v3 holds
f . u = H1(
u)
from RLVECT_4:sch 1(A1, A2, A3);
reconsider f =
f as
Element of
Funcs ( the
carrier of
V,
REAL)
by FUNCT_2:8;
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 ;
TARSKI:def 3 ( not x in Carrier f or x in {v1,v2,v3} )
assume that A8:
x in Carrier f
and A9:
not
x in {v1,v2,v3}
;
contradiction
A10:
(
x <> v2 &
x <> v3 )
by A9, ENUMSET1:def 1;
(
f . x <> 0 &
x <> v1 )
by A8, A9, ENUMSET1:def 1, RLVECT_2:19;
hence
contradiction
by A5, A8, A10;
verum
end;
then reconsider f =
f as
Linear_Combination of
{v1,v2,v3} by RLVECT_2:def 6;
take
f
;
( f . v1 = a & f . v2 = b & f . v3 = c )
thus
(
f . v1 = a &
f . v2 = b &
f . v3 = c )
by A4;
verum
end;
end;
reconsider zz = 0 as Element of REAL by XREAL_0:def 1;