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;
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));
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 A7, Def2;
a * u1 = [(a * x1),(a * y1)]
by A4, Def2;
hence
a * (u1 + u2) = (a * u1) + (a * u2)
by A9, A11, A8, A10, Def1;
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;
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));
(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 A15, Def2;
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 A15, A16, A17, Def2;
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;
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));
(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 A21, Def2;
a * u = [(a * x),(a * y)]
by A21, Def2;
then A23:
(a * u) + (b * u) = [((a * x) + (b * x)),((a * y) + (b * y))]
by A22, Def1;
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 A21, A23, A24, Def2;
verum
end;
for u being VECTOR of (Prod_of_RLS (X,Y)) holds 1 * u = u
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; verum