let X, Y, Z be RealNormSpace; :: thesis: for v1, v2 being Lipschitzian LinearOperator of X,Y
for s1, s2 being Lipschitzian LinearOperator of Y,Z
for a being Real holds
( s1 * (v1 + v2) = (s1 * v1) + (s1 * v2) & (s1 + s2) * v1 = (s1 * v1) + (s2 * v1) & s1 * (a (#) v1) = a (#) (s1 * v1) )
let v1, v2 be Lipschitzian LinearOperator of X,Y; :: thesis: for s1, s2 being Lipschitzian LinearOperator of Y,Z
for a being Real holds
( s1 * (v1 + v2) = (s1 * v1) + (s1 * v2) & (s1 + s2) * v1 = (s1 * v1) + (s2 * v1) & s1 * (a (#) v1) = a (#) (s1 * v1) )
let s1, s2 be Lipschitzian LinearOperator of Y,Z; :: thesis: for a being Real holds
( s1 * (v1 + v2) = (s1 * v1) + (s1 * v2) & (s1 + s2) * v1 = (s1 * v1) + (s2 * v1) & s1 * (a (#) v1) = a (#) (s1 * v1) )
let a be Real; :: thesis: ( s1 * (v1 + v2) = (s1 * v1) + (s1 * v2) & (s1 + s2) * v1 = (s1 * v1) + (s2 * v1) & s1 * (a (#) v1) = a (#) (s1 * v1) )
reconsider pv1 = v1, pv2 = v2 as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by LOPBAN_1:def 9;
reconsider ps1 = s1, ps2 = s2 as Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) by LOPBAN_1:def 9;
A1: v1 + v2 = pv1 + pv2 by Th11;
A2: ps1 * pv1 = s1 * v1 by Th13;
A3: ps1 * pv2 = s1 * v2 by Th13;
A4: ps2 * pv1 = s2 * v1 by Th13;
A5: s1 + s2 = ps1 + ps2 by Th11;
A6: a (#) v1 = a * pv1 by LOPBAN13:30;
A7: v1 + v2 is Lipschitzian LinearOperator of X,Y by A1, LOPBAN_1:def 9;
A8: s1 * v1 is Lipschitzian LinearOperator of X,Z by A2, LOPBAN_1:def 9;
A9: s1 * v2 is Lipschitzian LinearOperator of X,Z by A3, LOPBAN_1:def 9;
A10: s1 + s2 is Lipschitzian LinearOperator of Y,Z by A5, LOPBAN_1:def 9;
A11: s2 * v1 is Lipschitzian LinearOperator of X,Z by A4, LOPBAN_1:def 9;
A12: a (#) v1 is Lipschitzian LinearOperator of X,Y by A6, LOPBAN_1:def 9;
thus s1 * (v1 + v2) = ps1 * (pv1 + pv2) by A1, A7, Th13
.= (ps1 * pv1) + (ps1 * pv2) by LOPBAN13:19
.= (s1 * v1) + (s1 * v2) by A2, A3, A8, A9, Th11 ; :: thesis: ( (s1 + s2) * v1 = (s1 * v1) + (s2 * v1) & s1 * (a (#) v1) = a (#) (s1 * v1) )
thus (s1 + s2) * v1 = (ps1 + ps2) * pv1 by A5, Th13, A10
.= (ps1 * pv1) + (ps2 * pv1) by LOPBAN13:20
.= (s1 * v1) + (s2 * v1) by A2, A4, A8, A11, Th11 ; :: thesis: s1 * (a (#) v1) = a (#) (s1 * v1)
thus s1 * (a (#) v1) = ps1 * (a * pv1) by A6, A12, Th13
.= (a * ps1) * pv1 by LOPBAN13:28
.= a * (ps1 * pv1) by LOPBAN13:28
.= a (#) (s1 * v1) by A8, Th13, LOPBAN13:30 ; :: thesis: verum