let X, Y be ComplexLinearSpace; :: thesis: LinearOperators (X,Y) is linearly-closed

set W = LinearOperators (X,Y);

A1: for c being Complex

for v being VECTOR of (ComplexVectSpace ( the carrier of X,Y)) st v in LinearOperators (X,Y) holds

c * v in LinearOperators (X,Y)

v + u in LinearOperators (X,Y)

set W = LinearOperators (X,Y);

A1: for c being Complex

for v being VECTOR of (ComplexVectSpace ( the carrier of X,Y)) st v in LinearOperators (X,Y) holds

c * v in LinearOperators (X,Y)

proof

for v, u being VECTOR of (ComplexVectSpace ( the carrier of X,Y)) st v in LinearOperators (X,Y) & u in LinearOperators (X,Y) holds
let c be Complex; :: thesis: for v being VECTOR of (ComplexVectSpace ( the carrier of X,Y)) st v in LinearOperators (X,Y) holds

c * v in LinearOperators (X,Y)

let v be VECTOR of (ComplexVectSpace ( the carrier of X,Y)); :: thesis: ( v in LinearOperators (X,Y) implies c * v in LinearOperators (X,Y) )

assume A2: v in LinearOperators (X,Y) ; :: thesis: c * v in LinearOperators (X,Y)

c * v is LinearOperator of X,Y

end;c * v in LinearOperators (X,Y)

let v be VECTOR of (ComplexVectSpace ( the carrier of X,Y)); :: thesis: ( v in LinearOperators (X,Y) implies c * v in LinearOperators (X,Y) )

assume A2: v in LinearOperators (X,Y) ; :: thesis: c * v in LinearOperators (X,Y)

c * v is LinearOperator of X,Y

proof

hence
c * v in LinearOperators (X,Y)
by Def4; :: thesis: verum
reconsider f = c * v as Function of X,Y by FUNCT_2:66;

A3: f is homogeneous

end;A3: f is homogeneous

proof

f is additive
reconsider v9 = v as Element of Funcs ( the carrier of X, the carrier of Y) ;

let x be VECTOR of X; :: according to CLOPBAN1:def 3 :: thesis: for r being Complex holds f . (r * x) = r * (f . x)

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

A4: v9 is LinearOperator of X,Y by A2, Def4;

A5: f = (FuncExtMult ( the carrier of X,Y)) . [c,v9] by CLVECT_1:def 1;

hence f . (s * x) = c * (v9 . (s * x)) by Th2

.= c * (s * (v9 . x)) by A4, Def3

.= (c * s) * (v9 . x) by CLVECT_1:def 4

.= s * (c * (v9 . x)) by CLVECT_1:def 4

.= s * (f . x) by A5, Th2 ;

:: thesis: verum

end;let x be VECTOR of X; :: according to CLOPBAN1:def 3 :: thesis: for r being Complex holds f . (r * x) = r * (f . x)

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

A4: v9 is LinearOperator of X,Y by A2, Def4;

A5: f = (FuncExtMult ( the carrier of X,Y)) . [c,v9] by CLVECT_1:def 1;

hence f . (s * x) = c * (v9 . (s * x)) by Th2

.= c * (s * (v9 . x)) by A4, Def3

.= (c * s) * (v9 . x) by CLVECT_1:def 4

.= s * (c * (v9 . x)) by CLVECT_1:def 4

.= s * (f . x) by A5, Th2 ;

:: thesis: verum

proof

hence
c * v is LinearOperator of X,Y
by A3; :: thesis: verum
reconsider v9 = v as Element of Funcs ( the carrier of X, the carrier of Y) ;

let x, y be VECTOR of X; :: according to VECTSP_1:def 19 :: thesis: f . (x + y) = (f . x) + (f . y)

A6: v9 is LinearOperator of X,Y by A2, Def4;

A7: f = (FuncExtMult ( the carrier of X,Y)) . [c,v9] by CLVECT_1:def 1;

hence f . (x + y) = c * (v9 . (x + y)) by Th2

.= c * ((v9 . x) + (v9 . y)) by A6, VECTSP_1:def 20

.= (c * (v9 . x)) + (c * (v9 . y)) by CLVECT_1:def 2

.= (f . x) + (c * (v9 . y)) by A7, Th2

.= (f . x) + (f . y) by A7, Th2 ;

:: thesis: verum

end;let x, y be VECTOR of X; :: according to VECTSP_1:def 19 :: thesis: f . (x + y) = (f . x) + (f . y)

A6: v9 is LinearOperator of X,Y by A2, Def4;

A7: f = (FuncExtMult ( the carrier of X,Y)) . [c,v9] by CLVECT_1:def 1;

hence f . (x + y) = c * (v9 . (x + y)) by Th2

.= c * ((v9 . x) + (v9 . y)) by A6, VECTSP_1:def 20

.= (c * (v9 . x)) + (c * (v9 . y)) by CLVECT_1:def 2

.= (f . x) + (c * (v9 . y)) by A7, Th2

.= (f . x) + (f . y) by A7, Th2 ;

:: thesis: verum

v + u in LinearOperators (X,Y)

proof

hence
LinearOperators (X,Y) is linearly-closed
by A1, CLVECT_1:def 7; :: thesis: verum
let v, u be VECTOR of (ComplexVectSpace ( the carrier of X,Y)); :: thesis: ( v in LinearOperators (X,Y) & u in LinearOperators (X,Y) implies v + u in LinearOperators (X,Y) )

assume that

A8: v in LinearOperators (X,Y) and

A9: u in LinearOperators (X,Y) ; :: thesis: v + u in LinearOperators (X,Y)

v + u is LinearOperator of X,Y

end;assume that

A8: v in LinearOperators (X,Y) and

A9: u in LinearOperators (X,Y) ; :: thesis: v + u in LinearOperators (X,Y)

v + u is LinearOperator of X,Y

proof

hence
v + u in LinearOperators (X,Y)
by Def4; :: thesis: verum
reconsider f = v + u as Function of X,Y by FUNCT_2:66;

A10: f is homogeneous

end;A10: f is homogeneous

proof

f is additive
reconsider v9 = v, u9 = u as Element of Funcs ( the carrier of X, the carrier of Y) ;

let x be VECTOR of X; :: according to CLOPBAN1:def 3 :: thesis: for r being Complex holds f . (r * x) = r * (f . x)

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

A11: u9 is LinearOperator of X,Y by A9, Def4;

A12: v9 is LinearOperator of X,Y by A8, Def4;

thus f . (s * x) = (u9 . (s * x)) + (v9 . (s * x)) by LOPBAN_1:1

.= (s * (u9 . x)) + (v9 . (s * x)) by A11, Def3

.= (s * (u9 . x)) + (s * (v9 . x)) by A12, Def3

.= s * ((u9 . x) + (v9 . x)) by CLVECT_1:def 2

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

end;let x be VECTOR of X; :: according to CLOPBAN1:def 3 :: thesis: for r being Complex holds f . (r * x) = r * (f . x)

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

A11: u9 is LinearOperator of X,Y by A9, Def4;

A12: v9 is LinearOperator of X,Y by A8, Def4;

thus f . (s * x) = (u9 . (s * x)) + (v9 . (s * x)) by LOPBAN_1:1

.= (s * (u9 . x)) + (v9 . (s * x)) by A11, Def3

.= (s * (u9 . x)) + (s * (v9 . x)) by A12, Def3

.= s * ((u9 . x) + (v9 . x)) by CLVECT_1:def 2

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

proof

hence
v + u is LinearOperator of X,Y
by A10; :: thesis: verum
reconsider v9 = v, u9 = u as Element of Funcs ( the carrier of X, the carrier of Y) ;

let x, y be VECTOR of X; :: according to VECTSP_1:def 19 :: thesis: f . (x + y) = (f . x) + (f . y)

A13: u9 is LinearOperator of X,Y by A9, Def4;

A14: v9 is LinearOperator of X,Y by A8, Def4;

thus f . (x + y) = (u9 . (x + y)) + (v9 . (x + y)) by LOPBAN_1:1

.= ((u9 . x) + (u9 . y)) + (v9 . (x + y)) by A13, VECTSP_1:def 20

.= ((u9 . x) + (u9 . y)) + ((v9 . x) + (v9 . y)) by A14, VECTSP_1:def 20

.= (((u9 . x) + (u9 . y)) + (v9 . x)) + (v9 . y) by RLVECT_1:def 3

.= (((u9 . x) + (v9 . x)) + (u9 . y)) + (v9 . y) by RLVECT_1:def 3

.= ((f . x) + (u9 . y)) + (v9 . y) by LOPBAN_1:1

.= (f . x) + ((u9 . y) + (v9 . y)) by RLVECT_1:def 3

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

end;let x, y be VECTOR of X; :: according to VECTSP_1:def 19 :: thesis: f . (x + y) = (f . x) + (f . y)

A13: u9 is LinearOperator of X,Y by A9, Def4;

A14: v9 is LinearOperator of X,Y by A8, Def4;

thus f . (x + y) = (u9 . (x + y)) + (v9 . (x + y)) by LOPBAN_1:1

.= ((u9 . x) + (u9 . y)) + (v9 . (x + y)) by A13, VECTSP_1:def 20

.= ((u9 . x) + (u9 . y)) + ((v9 . x) + (v9 . y)) by A14, VECTSP_1:def 20

.= (((u9 . x) + (u9 . y)) + (v9 . x)) + (v9 . y) by RLVECT_1:def 3

.= (((u9 . x) + (v9 . x)) + (u9 . y)) + (v9 . y) by RLVECT_1:def 3

.= ((f . x) + (u9 . y)) + (v9 . y) by LOPBAN_1:1

.= (f . x) + ((u9 . y) + (v9 . y)) by RLVECT_1:def 3

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