let X be RealLinearSpace; :: thesis: LinearFunctionals X is linearly-closed

set W = LinearFunctionals X;

A1: for v, u being VECTOR of (RealVectSpace the carrier of X) st v in LinearFunctionals X & u in LinearFunctionals X holds

v + u in LinearFunctionals X

for v being VECTOR of (RealVectSpace the carrier of X) st v in LinearFunctionals X holds

a * v in LinearFunctionals X

set W = LinearFunctionals X;

A1: for v, u being VECTOR of (RealVectSpace the carrier of X) st v in LinearFunctionals X & u in LinearFunctionals X holds

v + u in LinearFunctionals X

proof

for a being Real
let v, u be VECTOR of (RealVectSpace the carrier of X); :: thesis: ( v in LinearFunctionals X & u in LinearFunctionals X implies v + u in LinearFunctionals X )

assume A2: ( v in LinearFunctionals X & u in LinearFunctionals X ) ; :: thesis: v + u in LinearFunctionals X

reconsider f = v + u as Functional of X by FUNCT_2:66;

A3: f is additive

end;assume A2: ( v in LinearFunctionals X & u in LinearFunctionals X ) ; :: thesis: v + u in LinearFunctionals X

reconsider f = v + u as Functional of X by FUNCT_2:66;

A3: f is additive

proof

f is homogeneous
let x, y be VECTOR of X; :: according to HAHNBAN:def 2 :: thesis: f . (x + y) = K55((f . x),(f . y))

reconsider vZ1 = v, uZ1 = u as Element of Funcs ( the carrier of X,REAL) ;

A4: uZ1 is linear-Functional of X by A2, Def7;

reconsider uZ11 = uZ1 as additive homogeneous Functional of X by A2, Def7;

reconsider x1 = x, y1 = y as Element of X ;

A5: vZ1 is linear-Functional of X by A2, Def7;

f . (x + y) = (uZ1 . (x + y)) + (vZ1 . (x + y)) by FUNCSDOM:1

.= ((uZ1 . x) + (uZ1 . y)) + (vZ1 . (x + y)) by A4, HAHNBAN:def 2

.= ((uZ1 . x) + (uZ1 . y)) + ((vZ1 . x) + (vZ1 . y)) by A5, HAHNBAN:def 2

.= (((uZ1 . x) + (vZ1 . x)) + (uZ1 . y)) + (vZ1 . y)

.= ((f . x) + (uZ1 . y)) + (vZ1 . y) by FUNCSDOM:1

.= (f . x) + ((uZ1 . y) + (vZ1 . y)) ;

hence f . (x + y) = (f . x) + (f . y) by FUNCSDOM:1; :: thesis: verum

end;reconsider vZ1 = v, uZ1 = u as Element of Funcs ( the carrier of X,REAL) ;

A4: uZ1 is linear-Functional of X by A2, Def7;

reconsider uZ11 = uZ1 as additive homogeneous Functional of X by A2, Def7;

reconsider x1 = x, y1 = y as Element of X ;

A5: vZ1 is linear-Functional of X by A2, Def7;

f . (x + y) = (uZ1 . (x + y)) + (vZ1 . (x + y)) by FUNCSDOM:1

.= ((uZ1 . x) + (uZ1 . y)) + (vZ1 . (x + y)) by A4, HAHNBAN:def 2

.= ((uZ1 . x) + (uZ1 . y)) + ((vZ1 . x) + (vZ1 . y)) by A5, HAHNBAN:def 2

.= (((uZ1 . x) + (vZ1 . x)) + (uZ1 . y)) + (vZ1 . y)

.= ((f . x) + (uZ1 . y)) + (vZ1 . y) by FUNCSDOM:1

.= (f . x) + ((uZ1 . y) + (vZ1 . y)) ;

hence f . (x + y) = (f . x) + (f . y) by FUNCSDOM:1; :: thesis: verum

proof

hence
v + u in LinearFunctionals X
by A3, Def7; :: thesis: verum
let x be VECTOR of X; :: according to HAHNBAN:def 3 :: thesis: for b_{1} being object holds f . (b_{1} * x) = b_{1} * (f . x)

let s be Real; :: thesis: f . (s * x) = s * (f . x)

reconsider v1 = v, u1 = u as Element of Funcs ( the carrier of X,REAL) ;

A6: ( u1 is linear-Functional of X & v1 is linear-Functional of X ) by A2, Def7;

f . (s * x) = (u1 . (s * x)) + (v1 . (s * x)) by FUNCSDOM:1

.= (s * (u1 . x)) + (v1 . (s * x)) by A6, HAHNBAN:def 3

.= (s * (u1 . x)) + (s * (v1 . x)) by A6, HAHNBAN:def 3

.= s * ((u1 . x) + (v1 . x)) ;

hence f . (s * x) = s * (f . x) by FUNCSDOM:1; :: thesis: verum

end;let s be Real; :: thesis: f . (s * x) = s * (f . x)

reconsider v1 = v, u1 = u as Element of Funcs ( the carrier of X,REAL) ;

A6: ( u1 is linear-Functional of X & v1 is linear-Functional of X ) by A2, Def7;

f . (s * x) = (u1 . (s * x)) + (v1 . (s * x)) by FUNCSDOM:1

.= (s * (u1 . x)) + (v1 . (s * x)) by A6, HAHNBAN:def 3

.= (s * (u1 . x)) + (s * (v1 . x)) by A6, HAHNBAN:def 3

.= s * ((u1 . x) + (v1 . x)) ;

hence f . (s * x) = s * (f . x) by FUNCSDOM:1; :: thesis: verum

for v being VECTOR of (RealVectSpace the carrier of X) st v in LinearFunctionals X holds

a * v in LinearFunctionals X

proof

hence
LinearFunctionals X is linearly-closed
by A1; :: thesis: verum
let a be Real; :: thesis: for v being VECTOR of (RealVectSpace the carrier of X) st v in LinearFunctionals X holds

a * v in LinearFunctionals X

let v be VECTOR of (RealVectSpace the carrier of X); :: thesis: ( v in LinearFunctionals X implies a * v in LinearFunctionals X )

assume A8: v in LinearFunctionals X ; :: thesis: a * v in LinearFunctionals X

reconsider f = a * v as Functional of X by FUNCT_2:66;

A9: f is additive

end;a * v in LinearFunctionals X

let v be VECTOR of (RealVectSpace the carrier of X); :: thesis: ( v in LinearFunctionals X implies a * v in LinearFunctionals X )

assume A8: v in LinearFunctionals X ; :: thesis: a * v in LinearFunctionals X

reconsider f = a * v as Functional of X by FUNCT_2:66;

A9: f is additive

proof

f is homogeneous
let x, y be VECTOR of X; :: according to HAHNBAN:def 2 :: thesis: f . (x + y) = K55((f . x),(f . y))

reconsider vZ1 = v as Element of Funcs ( the carrier of X,REAL) ;

A10: vZ1 is linear-Functional of X by Def7, A8;

f . (x + y) = a * (vZ1 . (x + y)) by FUNCSDOM:4

.= a * ((vZ1 . x) + (vZ1 . y)) by A10, HAHNBAN:def 2

.= (a * (vZ1 . x)) + (a * (vZ1 . y))

.= (f . x) + (a * (vZ1 . y)) by FUNCSDOM:4 ;

hence f . (x + y) = (f . x) + (f . y) by FUNCSDOM:4; :: thesis: verum

end;reconsider vZ1 = v as Element of Funcs ( the carrier of X,REAL) ;

A10: vZ1 is linear-Functional of X by Def7, A8;

f . (x + y) = a * (vZ1 . (x + y)) by FUNCSDOM:4

.= a * ((vZ1 . x) + (vZ1 . y)) by A10, HAHNBAN:def 2

.= (a * (vZ1 . x)) + (a * (vZ1 . y))

.= (f . x) + (a * (vZ1 . y)) by FUNCSDOM:4 ;

hence f . (x + y) = (f . x) + (f . y) by FUNCSDOM:4; :: thesis: verum

proof

hence
a * v in LinearFunctionals X
by A9, Def7; :: thesis: verum
let x be VECTOR of X; :: according to HAHNBAN:def 3 :: thesis: for b_{1} being object holds f . (b_{1} * x) = b_{1} * (f . x)

let s be Real; :: thesis: f . (s * x) = s * (f . x)

reconsider vZ1 = v as Element of Funcs ( the carrier of X,REAL) ;

A11: vZ1 is linear-Functional of X by Def7, A8;

f . (s * x) = a * (vZ1 . (s * x)) by FUNCSDOM:4

.= a * (s * (vZ1 . x)) by A11, HAHNBAN:def 3

.= s * (a * (vZ1 . x)) ;

hence f . (s * x) = s * (f . x) by FUNCSDOM:4; :: thesis: verum

end;let s be Real; :: thesis: f . (s * x) = s * (f . x)

reconsider vZ1 = v as Element of Funcs ( the carrier of X,REAL) ;

A11: vZ1 is linear-Functional of X by Def7, A8;

f . (s * x) = a * (vZ1 . (s * x)) by FUNCSDOM:4

.= a * (s * (vZ1 . x)) by A11, HAHNBAN:def 3

.= s * (a * (vZ1 . x)) ;

hence f . (s * x) = s * (f . x) by FUNCSDOM:4; :: thesis: verum