let X, Y, Z be RealLinearSpace; :: thesis: BilinearOperators (X,Y,Z) is linearly-closed

set W = BilinearOperators (X,Y,Z);

A1: for v, u being VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)) st v in BilinearOperators (X,Y,Z) & u in BilinearOperators (X,Y,Z) holds

v + u in BilinearOperators (X,Y,Z)

for v being VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)) st v in BilinearOperators (X,Y,Z) holds

b * v in BilinearOperators (X,Y,Z)

set W = BilinearOperators (X,Y,Z);

A1: for v, u being VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)) st v in BilinearOperators (X,Y,Z) & u in BilinearOperators (X,Y,Z) holds

v + u in BilinearOperators (X,Y,Z)

proof

for b being Real
let v, u be VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)); :: thesis: ( v in BilinearOperators (X,Y,Z) & u in BilinearOperators (X,Y,Z) implies v + u in BilinearOperators (X,Y,Z) )

assume that

A2: v in BilinearOperators (X,Y,Z) and

A3: u in BilinearOperators (X,Y,Z) ; :: thesis: v + u in BilinearOperators (X,Y,Z)

reconsider u1 = u as BilinearOperator of X,Y,Z by A3, Def6;

reconsider v1 = v as BilinearOperator of X,Y,Z by A2, Def6;

v + u is BilinearOperator of X,Y,Z

end;assume that

A2: v in BilinearOperators (X,Y,Z) and

A3: u in BilinearOperators (X,Y,Z) ; :: thesis: v + u in BilinearOperators (X,Y,Z)

reconsider u1 = u as BilinearOperator of X,Y,Z by A3, Def6;

reconsider v1 = v as BilinearOperator of X,Y,Z by A2, Def6;

v + u is BilinearOperator of X,Y,Z

proof

hence
v + u in BilinearOperators (X,Y,Z)
by Def6; :: thesis: verum
reconsider L = v + u as Function of [:X,Y:],Z by FUNCT_2:66;

A4: for x1, x2 being Point of X

for y being Point of Y holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))

for y being Point of Y

for a being Real holds L . ((a * x),y) = a * (L . (x,y))

for y1, y2 being Point of Y holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))

for y being Point of Y

for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

end;A4: for x1, x2 being Point of X

for y being Point of Y holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))

proof

A6:
for x being Point of X
let x1, x2 be Point of X; :: thesis: for y being Point of Y holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))

let y be Point of Y; :: thesis: L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))

A5: ( [x1,y] is Element of [:X,Y:] & [x2,y] is Element of [:X,Y:] & [(x1 + x2),y] is Element of [:X,Y:] ) ;

hence L . ((x1 + x2),y) = (v1 . ((x1 + x2),y)) + (u1 . ((x1 + x2),y)) by LOPBAN_1:1

.= ((v1 . (x1,y)) + (v1 . (x2,y))) + (u1 . ((x1 + x2),y)) by LOPBAN_8:11

.= ((v1 . (x1,y)) + (v1 . (x2,y))) + ((u1 . (x1,y)) + (u1 . (x2,y))) by LOPBAN_8:11

.= ((v1 . (x1,y)) + (u1 . (x1,y))) + ((v1 . (x2,y)) + (u1 . (x2,y))) by LM14

.= (L . (x1,y)) + ((v1 . (x2,y)) + (u1 . (x2,y))) by A5, LOPBAN_1:1

.= (L . (x1,y)) + (L . (x2,y)) by A5, LOPBAN_1:1 ;

:: thesis: verum

end;let y be Point of Y; :: thesis: L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))

A5: ( [x1,y] is Element of [:X,Y:] & [x2,y] is Element of [:X,Y:] & [(x1 + x2),y] is Element of [:X,Y:] ) ;

hence L . ((x1 + x2),y) = (v1 . ((x1 + x2),y)) + (u1 . ((x1 + x2),y)) by LOPBAN_1:1

.= ((v1 . (x1,y)) + (v1 . (x2,y))) + (u1 . ((x1 + x2),y)) by LOPBAN_8:11

.= ((v1 . (x1,y)) + (v1 . (x2,y))) + ((u1 . (x1,y)) + (u1 . (x2,y))) by LOPBAN_8:11

.= ((v1 . (x1,y)) + (u1 . (x1,y))) + ((v1 . (x2,y)) + (u1 . (x2,y))) by LM14

.= (L . (x1,y)) + ((v1 . (x2,y)) + (u1 . (x2,y))) by A5, LOPBAN_1:1

.= (L . (x1,y)) + (L . (x2,y)) by A5, LOPBAN_1:1 ;

:: thesis: verum

for y being Point of Y

for a being Real holds L . ((a * x),y) = a * (L . (x,y))

proof

A8:
for x being Point of X
let x be Point of X; :: thesis: for y being Point of Y

for a being Real holds L . ((a * x),y) = a * (L . (x,y))

let y be Point of Y; :: thesis: for a being Real holds L . ((a * x),y) = a * (L . (x,y))

let a be Real; :: thesis: L . ((a * x),y) = a * (L . (x,y))

A7: ( [x,y] is Element of [:X,Y:] & [(a * x),y] is Element of [:X,Y:] ) ;

hence L . ((a * x),y) = (v1 . ((a * x),y)) + (u1 . ((a * x),y)) by LOPBAN_1:1

.= (a * (v1 . (x,y))) + (u1 . ((a * x),y)) by LOPBAN_8:11

.= (a * (v1 . (x,y))) + (a * (u1 . (x,y))) by LOPBAN_8:11

.= a * ((v1 . (x,y)) + (u1 . (x,y))) by RLVECT_1:def 5

.= a * (L . (x,y)) by A7, LOPBAN_1:1 ;

:: thesis: verum

end;for a being Real holds L . ((a * x),y) = a * (L . (x,y))

let y be Point of Y; :: thesis: for a being Real holds L . ((a * x),y) = a * (L . (x,y))

let a be Real; :: thesis: L . ((a * x),y) = a * (L . (x,y))

A7: ( [x,y] is Element of [:X,Y:] & [(a * x),y] is Element of [:X,Y:] ) ;

hence L . ((a * x),y) = (v1 . ((a * x),y)) + (u1 . ((a * x),y)) by LOPBAN_1:1

.= (a * (v1 . (x,y))) + (u1 . ((a * x),y)) by LOPBAN_8:11

.= (a * (v1 . (x,y))) + (a * (u1 . (x,y))) by LOPBAN_8:11

.= a * ((v1 . (x,y)) + (u1 . (x,y))) by RLVECT_1:def 5

.= a * (L . (x,y)) by A7, LOPBAN_1:1 ;

:: thesis: verum

for y1, y2 being Point of Y holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))

proof

for x being Point of X
let x be Point of X; :: thesis: for y1, y2 being Point of Y holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))

let y1, y2 be Point of Y; :: thesis: L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))

A9: ( [x,y1] is Element of [:X,Y:] & [x,y2] is Element of [:X,Y:] & [x,(y1 + y2)] is Element of [:X,Y:] ) ;

hence L . (x,(y1 + y2)) = (v1 . (x,(y1 + y2))) + (u1 . (x,(y1 + y2))) by LOPBAN_1:1

.= ((v1 . (x,y1)) + (v1 . (x,y2))) + (u1 . (x,(y1 + y2))) by LOPBAN_8:11

.= ((v1 . (x,y1)) + (v1 . (x,y2))) + ((u1 . (x,y1)) + (u1 . (x,y2))) by LOPBAN_8:11

.= ((v1 . (x,y1)) + (u1 . (x,y1))) + ((v1 . (x,y2)) + (u1 . (x,y2))) by LM14

.= (L . (x,y1)) + ((v1 . (x,y2)) + (u1 . (x,y2))) by A9, LOPBAN_1:1

.= (L . (x,y1)) + (L . (x,y2)) by A9, LOPBAN_1:1 ;

:: thesis: verum

end;let y1, y2 be Point of Y; :: thesis: L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))

A9: ( [x,y1] is Element of [:X,Y:] & [x,y2] is Element of [:X,Y:] & [x,(y1 + y2)] is Element of [:X,Y:] ) ;

hence L . (x,(y1 + y2)) = (v1 . (x,(y1 + y2))) + (u1 . (x,(y1 + y2))) by LOPBAN_1:1

.= ((v1 . (x,y1)) + (v1 . (x,y2))) + (u1 . (x,(y1 + y2))) by LOPBAN_8:11

.= ((v1 . (x,y1)) + (v1 . (x,y2))) + ((u1 . (x,y1)) + (u1 . (x,y2))) by LOPBAN_8:11

.= ((v1 . (x,y1)) + (u1 . (x,y1))) + ((v1 . (x,y2)) + (u1 . (x,y2))) by LM14

.= (L . (x,y1)) + ((v1 . (x,y2)) + (u1 . (x,y2))) by A9, LOPBAN_1:1

.= (L . (x,y1)) + (L . (x,y2)) by A9, LOPBAN_1:1 ;

:: thesis: verum

for y being Point of Y

for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

proof

hence
v + u is BilinearOperator of X,Y,Z
by A4, A6, A8, LOPBAN_8:11; :: thesis: verum
let x be Point of X; :: thesis: for y being Point of Y

for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

let y be Point of Y; :: thesis: for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

let a be Real; :: thesis: L . (x,(a * y)) = a * (L . (x,y))

A10: ( [x,y] is Element of [:X,Y:] & [x,(a * y)] is Element of [:X,Y:] ) ;

hence L . (x,(a * y)) = (v1 . (x,(a * y))) + (u1 . (x,(a * y))) by LOPBAN_1:1

.= (a * (v1 . (x,y))) + (u1 . (x,(a * y))) by LOPBAN_8:11

.= (a * (v1 . (x,y))) + (a * (u1 . (x,y))) by LOPBAN_8:11

.= a * ((v1 . (x,y)) + (u1 . (x,y))) by RLVECT_1:def 5

.= a * (L . (x,y)) by A10, LOPBAN_1:1 ;

:: thesis: verum

end;for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

let y be Point of Y; :: thesis: for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

let a be Real; :: thesis: L . (x,(a * y)) = a * (L . (x,y))

A10: ( [x,y] is Element of [:X,Y:] & [x,(a * y)] is Element of [:X,Y:] ) ;

hence L . (x,(a * y)) = (v1 . (x,(a * y))) + (u1 . (x,(a * y))) by LOPBAN_1:1

.= (a * (v1 . (x,y))) + (u1 . (x,(a * y))) by LOPBAN_8:11

.= (a * (v1 . (x,y))) + (a * (u1 . (x,y))) by LOPBAN_8:11

.= a * ((v1 . (x,y)) + (u1 . (x,y))) by RLVECT_1:def 5

.= a * (L . (x,y)) by A10, LOPBAN_1:1 ;

:: thesis: verum

for v being VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)) st v in BilinearOperators (X,Y,Z) holds

b * v in BilinearOperators (X,Y,Z)

proof

hence
BilinearOperators (X,Y,Z) is linearly-closed
by A1, RLSUB_1:def 1; :: thesis: verum
let b be Real; :: thesis: for v being VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)) st v in BilinearOperators (X,Y,Z) holds

b * v in BilinearOperators (X,Y,Z)

let v be VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)); :: thesis: ( v in BilinearOperators (X,Y,Z) implies b * v in BilinearOperators (X,Y,Z) )

assume A11: v in BilinearOperators (X,Y,Z) ; :: thesis: b * v in BilinearOperators (X,Y,Z)

reconsider v1 = v as BilinearOperator of X,Y,Z by A11, Def6;

b * v is BilinearOperator of X,Y,Z

end;b * v in BilinearOperators (X,Y,Z)

let v be VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)); :: thesis: ( v in BilinearOperators (X,Y,Z) implies b * v in BilinearOperators (X,Y,Z) )

assume A11: v in BilinearOperators (X,Y,Z) ; :: thesis: b * v in BilinearOperators (X,Y,Z)

reconsider v1 = v as BilinearOperator of X,Y,Z by A11, Def6;

b * v is BilinearOperator of X,Y,Z

proof

hence
b * v in BilinearOperators (X,Y,Z)
by Def6; :: thesis: verum
reconsider L = b * v as Function of [:X,Y:],Z by FUNCT_2:66;

A12: for x1, x2 being Point of X

for y being Point of Y holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))

for y being Point of Y

for a being Real holds L . ((a * x),y) = a * (L . (x,y))

for y1, y2 being Point of Y holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))

for y being Point of Y

for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

end;A12: for x1, x2 being Point of X

for y being Point of Y holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))

proof

A14:
for x being Point of X
let x1, x2 be Point of X; :: thesis: for y being Point of Y holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))

let y be Point of Y; :: thesis: L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))

A13: ( [x1,y] is Element of [:X,Y:] & [x2,y] is Element of [:X,Y:] & [(x1 + x2),y] is Element of [:X,Y:] ) ;

hence L . ((x1 + x2),y) = b * (v1 . ((x1 + x2),y)) by LOPBAN_1:2

.= b * ((v1 . (x1,y)) + (v1 . (x2,y))) by LOPBAN_8:11

.= (b * (v1 . (x1,y))) + (b * (v1 . (x2,y))) by RLVECT_1:def 5

.= (L . (x1,y)) + (b * (v1 . (x2,y))) by A13, LOPBAN_1:2

.= (L . (x1,y)) + (L . (x2,y)) by A13, LOPBAN_1:2 ;

:: thesis: verum

end;let y be Point of Y; :: thesis: L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))

A13: ( [x1,y] is Element of [:X,Y:] & [x2,y] is Element of [:X,Y:] & [(x1 + x2),y] is Element of [:X,Y:] ) ;

hence L . ((x1 + x2),y) = b * (v1 . ((x1 + x2),y)) by LOPBAN_1:2

.= b * ((v1 . (x1,y)) + (v1 . (x2,y))) by LOPBAN_8:11

.= (b * (v1 . (x1,y))) + (b * (v1 . (x2,y))) by RLVECT_1:def 5

.= (L . (x1,y)) + (b * (v1 . (x2,y))) by A13, LOPBAN_1:2

.= (L . (x1,y)) + (L . (x2,y)) by A13, LOPBAN_1:2 ;

:: thesis: verum

for y being Point of Y

for a being Real holds L . ((a * x),y) = a * (L . (x,y))

proof

A16:
for x being Point of X
let x be Point of X; :: thesis: for y being Point of Y

for a being Real holds L . ((a * x),y) = a * (L . (x,y))

let y be Point of Y; :: thesis: for a being Real holds L . ((a * x),y) = a * (L . (x,y))

let a be Real; :: thesis: L . ((a * x),y) = a * (L . (x,y))

A15: ( [x,y] is Element of [:X,Y:] & [(a * x),y] is Element of [:X,Y:] ) ;

hence L . ((a * x),y) = b * (v1 . ((a * x),y)) by LOPBAN_1:2

.= b * (a * (v1 . (x,y))) by LOPBAN_8:11

.= (b * a) * (v1 . (x,y)) by RLVECT_1:def 7

.= a * (b * (v1 . (x,y))) by RLVECT_1:def 7

.= a * (L . (x,y)) by A15, LOPBAN_1:2 ;

:: thesis: verum

end;for a being Real holds L . ((a * x),y) = a * (L . (x,y))

let y be Point of Y; :: thesis: for a being Real holds L . ((a * x),y) = a * (L . (x,y))

let a be Real; :: thesis: L . ((a * x),y) = a * (L . (x,y))

A15: ( [x,y] is Element of [:X,Y:] & [(a * x),y] is Element of [:X,Y:] ) ;

hence L . ((a * x),y) = b * (v1 . ((a * x),y)) by LOPBAN_1:2

.= b * (a * (v1 . (x,y))) by LOPBAN_8:11

.= (b * a) * (v1 . (x,y)) by RLVECT_1:def 7

.= a * (b * (v1 . (x,y))) by RLVECT_1:def 7

.= a * (L . (x,y)) by A15, LOPBAN_1:2 ;

:: thesis: verum

for y1, y2 being Point of Y holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))

proof

for x being Point of X
let x be Point of X; :: thesis: for y1, y2 being Point of Y holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))

let y1, y2 be Point of Y; :: thesis: L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))

A17: ( [x,y1] is Element of [:X,Y:] & [x,y2] is Element of [:X,Y:] & [x,(y1 + y2)] is Element of [:X,Y:] ) ;

hence L . (x,(y1 + y2)) = b * (v1 . (x,(y1 + y2))) by LOPBAN_1:2

.= b * ((v1 . (x,y1)) + (v1 . (x,y2))) by LOPBAN_8:11

.= (b * (v1 . (x,y1))) + (b * (v1 . (x,y2))) by RLVECT_1:def 5

.= (L . (x,y1)) + (b * (v1 . (x,y2))) by A17, LOPBAN_1:2

.= (L . (x,y1)) + (L . (x,y2)) by A17, LOPBAN_1:2 ;

:: thesis: verum

end;let y1, y2 be Point of Y; :: thesis: L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))

A17: ( [x,y1] is Element of [:X,Y:] & [x,y2] is Element of [:X,Y:] & [x,(y1 + y2)] is Element of [:X,Y:] ) ;

hence L . (x,(y1 + y2)) = b * (v1 . (x,(y1 + y2))) by LOPBAN_1:2

.= b * ((v1 . (x,y1)) + (v1 . (x,y2))) by LOPBAN_8:11

.= (b * (v1 . (x,y1))) + (b * (v1 . (x,y2))) by RLVECT_1:def 5

.= (L . (x,y1)) + (b * (v1 . (x,y2))) by A17, LOPBAN_1:2

.= (L . (x,y1)) + (L . (x,y2)) by A17, LOPBAN_1:2 ;

:: thesis: verum

for y being Point of Y

for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

proof

hence
b * v is BilinearOperator of X,Y,Z
by A12, A14, A16, LOPBAN_8:11; :: thesis: verum
let x be Point of X; :: thesis: for y being Point of Y

for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

let y be Point of Y; :: thesis: for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

let a be Real; :: thesis: L . (x,(a * y)) = a * (L . (x,y))

A18: ( [x,y] is Element of [:X,Y:] & [x,(a * y)] is Element of [:X,Y:] ) ;

hence L . (x,(a * y)) = b * (v1 . (x,(a * y))) by LOPBAN_1:2

.= b * (a * (v1 . (x,y))) by LOPBAN_8:11

.= (b * a) * (v1 . (x,y)) by RLVECT_1:def 7

.= a * (b * (v1 . (x,y))) by RLVECT_1:def 7

.= a * (L . (x,y)) by A18, LOPBAN_1:2 ;

:: thesis: verum

end;for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

let y be Point of Y; :: thesis: for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

let a be Real; :: thesis: L . (x,(a * y)) = a * (L . (x,y))

A18: ( [x,y] is Element of [:X,Y:] & [x,(a * y)] is Element of [:X,Y:] ) ;

hence L . (x,(a * y)) = b * (v1 . (x,(a * y))) by LOPBAN_1:2

.= b * (a * (v1 . (x,y))) by LOPBAN_8:11

.= (b * a) * (v1 . (x,y)) by RLVECT_1:def 7

.= a * (b * (v1 . (x,y))) by RLVECT_1:def 7

.= a * (L . (x,y)) by A18, LOPBAN_1:2 ;

:: thesis: verum