let X, Y be RealNormSpace; :: thesis: for v1, v2, v3 being Lipschitzian LinearOperator of X,Y
for a, b being Real holds
( v1 + v2 = v2 + v1 & (v1 + v2) + v3 = v1 + (v2 + v3) & a (#) (v1 + v2) = (a (#) v1) + (a (#) v2) & (a + b) (#) v1 = (a (#) v1) + (b (#) v1) & (a * b) (#) v1 = a (#) (b (#) v1) )
let v1, v2, v3 be Lipschitzian LinearOperator of X,Y; :: thesis: for a, b being Real holds
( v1 + v2 = v2 + v1 & (v1 + v2) + v3 = v1 + (v2 + v3) & a (#) (v1 + v2) = (a (#) v1) + (a (#) v2) & (a + b) (#) v1 = (a (#) v1) + (b (#) v1) & (a * b) (#) v1 = a (#) (b (#) v1) )
let a, b be Real; :: thesis: ( v1 + v2 = v2 + v1 & (v1 + v2) + v3 = v1 + (v2 + v3) & a (#) (v1 + v2) = (a (#) v1) + (a (#) v2) & (a + b) (#) v1 = (a (#) v1) + (b (#) v1) & (a * b) (#) v1 = a (#) (b (#) v1) )
reconsider w1 = v1, w2 = v2, w3 = v3 as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by LOPBAN_1:def 9;
A1: v1 + v2 = w1 + w2 by Th11;
A2: v2 + v3 = w2 + w3 by Th11;
A3: a (#) v1 = a * w1 by LOPBAN13:30;
A4: a (#) v2 = a * w2 by LOPBAN13:30;
A5: b (#) v1 = b * w1 by LOPBAN13:30;
A6: v1 + v2 is Lipschitzian LinearOperator of X,Y by A1, LOPBAN_1:def 9;
A7: v2 + v3 is Lipschitzian LinearOperator of X,Y by A2, LOPBAN_1:def 9;
A8: a (#) v1 is Lipschitzian LinearOperator of X,Y by A3, LOPBAN_1:def 9;
A9: a (#) v2 is Lipschitzian LinearOperator of X,Y by A4, LOPBAN_1:def 9;
A10: b (#) v1 is Lipschitzian LinearOperator of X,Y by A5, LOPBAN_1:def 9;
thus v1 + v2 = v2 + v1 ; :: thesis: ( (v1 + v2) + v3 = v1 + (v2 + v3) & a (#) (v1 + v2) = (a (#) v1) + (a (#) v2) & (a + b) (#) v1 = (a (#) v1) + (b (#) v1) & (a * b) (#) v1 = a (#) (b (#) v1) )
thus (v1 + v2) + v3 = (w1 + w2) + w3 by A1, A6, Th11
.= w1 + (w2 + w3) by RLVECT_1:def 3
.= v1 + (v2 + v3) by A2, A7, Th11 ; :: thesis: ( a (#) (v1 + v2) = (a (#) v1) + (a (#) v2) & (a + b) (#) v1 = (a (#) v1) + (b (#) v1) & (a * b) (#) v1 = a (#) (b (#) v1) )
thus a (#) (v1 + v2) = a * (w1 + w2) by A6, Th11, LOPBAN13:30
.= (a * w1) + (a * w2) by RLVECT_1:def 5
.= (a (#) v1) + (a (#) v2) by A3, A4, A8, A9, Th11 ; :: thesis: ( (a + b) (#) v1 = (a (#) v1) + (b (#) v1) & (a * b) (#) v1 = a (#) (b (#) v1) )
thus (a + b) (#) v1 = (a + b) * w1 by LOPBAN13:30
.= (a * w1) + (b * w1) by RLVECT_1:def 6
.= (a (#) v1) + (b (#) v1) by A3, A5, A8, A10, Th11 ; :: thesis: (a * b) (#) v1 = a (#) (b (#) v1)
thus (a * b) (#) v1 = (a * b) * w1 by LOPBAN13:30
.= a * (b * w1) by RLVECT_1:def 7
.= a (#) (b (#) v1) by A5, A10, LOPBAN13:30 ; :: thesis: verum