A1: for a being Real
for u1, u2 being VECTOR of (Prod_of_RLS (X,Y)) holds a * (u1 + u2) = (a * u1) + (a * u2)
proof
let a be Real; :: thesis: for u1, u2 being VECTOR of (Prod_of_RLS (X,Y)) holds a * (u1 + u2) = (a * u1) + (a * u2)
reconsider a = a as Real ;
let u1, u2 be VECTOR of (Prod_of_RLS (X,Y)); :: thesis: a * (u1 + u2) = (a * u1) + (a * u2)
consider x1, y1 being object such that
A2: x1 in the carrier of X and
A3: y1 in the carrier of Y and
A4: u1 = [x1,y1] by ZFMISC_1:def 2;
reconsider x1 = x1 as VECTOR of X by A2;
consider x2, y2 being object such that
A5: x2 in the carrier of X and
A6: y2 in the carrier of Y and
A7: u2 = [x2,y2] by ZFMISC_1:def 2;
reconsider y2 = y2 as VECTOR of Y by A6;
reconsider x2 = x2 as VECTOR of X by A5;
reconsider y1 = y1 as VECTOR of Y by A3;
A8: a * (x1 + x2) = (a * x1) + (a * x2) by RLVECT_1:def 5;
u1 + u2 = [(x1 + x2),(y1 + y2)] by A4, A7, Def1;
then A9: a * (u1 + u2) = [(a * (x1 + x2)),(a * (y1 + y2))] by Def2;
A10: a * (y1 + y2) = (a * y1) + (a * y2) by RLVECT_1:def 5;
A11: a * u2 = [(a * x2),(a * y2)] by ;
a * u1 = [(a * x1),(a * y1)] by ;
hence a * (u1 + u2) = (a * u1) + (a * u2) by A9, A11, A8, A10, Def1; :: thesis: verum
end;
A12: for a, b being Real
for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a * b) * u = a * (b * u)
proof
let a, b be Real; :: thesis: for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a * b) * u = a * (b * u)
reconsider a = a, b = b as Real ;
let u be VECTOR of (Prod_of_RLS (X,Y)); :: thesis: (a * b) * u = a * (b * u)
consider x, y being object such that
A13: x in the carrier of X and
A14: y in the carrier of Y and
A15: u = [x,y] by ZFMISC_1:def 2;
reconsider y = y as VECTOR of Y by A14;
reconsider x = x as VECTOR of X by A13;
b * u = [(b * x),(b * y)] by ;
then A16: a * (b * u) = [(a * (b * x)),(a * (b * y))] by Def2;
A17: (a * b) * y = a * (b * y) by RLVECT_1:def 7;
(a * b) * x = a * (b * x) by RLVECT_1:def 7;
hence (a * b) * u = a * (b * u) by ; :: thesis: verum
end;
A18: for a, b being Real
for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a + b) * u = (a * u) + (b * u)
proof
let a, b be Real; :: thesis: for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a + b) * u = (a * u) + (b * u)
reconsider a = a, b = b as Real ;
let u be VECTOR of (Prod_of_RLS (X,Y)); :: thesis: (a + b) * u = (a * u) + (b * u)
consider x, y being object such that
A19: x in the carrier of X and
A20: y in the carrier of Y and
A21: u = [x,y] by ZFMISC_1:def 2;
reconsider y = y as VECTOR of Y by A20;
reconsider x = x as VECTOR of X by A19;
A22: b * u = [(b * x),(b * y)] by ;
a * u = [(a * x),(a * y)] by ;
then A23: (a * u) + (b * u) = [((a * x) + (b * x)),((a * y) + (b * y))] by ;
A24: (a + b) * y = (a * y) + (b * y) by RLVECT_1:def 6;
(a + b) * x = (a * x) + (b * x) by RLVECT_1:def 6;
hence (a + b) * u = (a * u) + (b * u) by ; :: thesis: verum
end;
for u being VECTOR of (Prod_of_RLS (X,Y)) holds 1 * u = u
proof
let u be VECTOR of (Prod_of_RLS (X,Y)); :: thesis: 1 * u = u
consider x, y being object such that
A25: x in the carrier of X and
A26: y in the carrier of Y and
A27: u = [x,y] by ZFMISC_1:def 2;
reconsider y = y as VECTOR of Y by A26;
reconsider x = x as VECTOR of X by A25;
A28: 1 * y = y by RLVECT_1:def 8;
1 * x = x by RLVECT_1:def 8;
hence 1 * u = u by ; :: thesis: verum
end;
hence ( Prod_of_RLS (X,Y) is vector-distributive & Prod_of_RLS (X,Y) is scalar-distributive & Prod_of_RLS (X,Y) is scalar-associative & Prod_of_RLS (X,Y) is scalar-unital ) by A1, A18, A12; :: thesis: verum