thus
for a being Real
for v, w being Element of (RealVS V) holds a * (v + w) = (a * v) + (a * w)
RLVECT_1:def 5 ( RealVS V is scalar-distributive & RealVS V is scalar-associative & RealVS V is scalar-unital )proof
let a be
Real;
for v, w being Element of (RealVS V) holds a * (v + w) = (a * v) + (a * w)
reconsider a =
a as
Real ;
let v,
w be
Element of
(RealVS V);
a * (v + w) = (a * v) + (a * w)
set a1 =
[**a,0**];
A1:
addLoopStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V #)
= addLoopStr(# the
carrier of
(RealVS V), the
addF of
(RealVS V), the
ZeroF of
(RealVS V) #)
by Def17;
then reconsider v1 =
v,
w1 =
w as
Element of
V ;
a * (v + w) =
[**a,0**] * (v1 + w1)
by A1, Def17
.=
([**a,0**] * v1) + ([**a,0**] * w1)
by VECTSP_1:def 14
.=
the
addF of
V . [( the Mult of (RealVS V) . (a,v1)),([**a,0**] * w1)]
by Def17
.=
(a * v) + (a * w)
by A1, Def17
;
hence
a * (v + w) = (a * v) + (a * w)
;
verum
end;
thus
for a, b being Real
for v being Element of (RealVS V) holds (a + b) * v = (a * v) + (b * v)
RLVECT_1:def 6 ( RealVS V is scalar-associative & RealVS V is scalar-unital )proof
let a,
b be
Real;
for v being Element of (RealVS V) holds (a + b) * v = (a * v) + (b * v)
reconsider a =
a,
b =
b as
Real ;
let v be
Element of
(RealVS V);
(a + b) * v = (a * v) + (b * v)
set a1 =
[**a,0**];
set b1 =
[**b,0**];
A2:
addLoopStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V #)
= addLoopStr(# the
carrier of
(RealVS V), the
addF of
(RealVS V), the
ZeroF of
(RealVS V) #)
by Def17;
then reconsider v1 =
v as
Element of
V ;
[**a,0**] + [**b,0**] = [**(a + b),0**]
;
then (a + b) * v =
([**a,0**] + [**b,0**]) * v1
by Def17
.=
([**a,0**] * v1) + ([**b,0**] * v1)
by VECTSP_1:def 15
.=
the
addF of
(RealVS V) . [( the Mult of (RealVS V) . (a,v)),([**b,0**] * v1)]
by A2, Def17
.=
(a * v) + (b * v)
by Def17
;
hence
(a + b) * v = (a * v) + (b * v)
;
verum
end;
thus
for a, b being Real
for v being Element of (RealVS V) holds (a * b) * v = a * (b * v)
RLVECT_1:def 7 RealVS V is scalar-unital proof
let a,
b be
Real;
for v being Element of (RealVS V) holds (a * b) * v = a * (b * v)
reconsider a =
a,
b =
b as
Real ;
let v be
Element of
(RealVS V);
(a * b) * v = a * (b * v)
addLoopStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V #)
= addLoopStr(# the
carrier of
(RealVS V), the
addF of
(RealVS V), the
ZeroF of
(RealVS V) #)
by Def17;
then reconsider v1 =
v as
Element of
V ;
[**(a * b),0**] = [**a,0**] * [**b,0**]
;
then (a * b) * v =
([**a,0**] * [**b,0**]) * v1
by Def17
.=
[**a,0**] * ([**b,0**] * v1)
by VECTSP_1:def 16
.=
the
Mult of
(RealVS V) . (
a,
([**b,0**] * v1))
by Def17
.=
a * (b * v)
by Def17
;
hence
(a * b) * v = a * (b * v)
;
verum
end;
let v be Element of (RealVS V); RLVECT_1:def 8 1 * v = v
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #)
by Def17;
then reconsider v1 = v as Element of V ;
thus 1 * v =
[**1,0**] * v1
by Def17
.=
v
by COMPLFLD:8, VECTSP_1:def 17
; verum