thus
for a being real number
for v, w being Element of (RealVS V) holds a * (v + w) = (a * v) + (a * w)
RLVECT_1:def 9 ( ( for b1, b2 being set
for b3 being Element of the carrier of (RealVS V) holds (b1 + b2) * b3 = (b1 * b3) + (b2 * b3) ) & ( for b1, b2 being set
for b3 being Element of the carrier of (RealVS V) holds (b1 * b2) * b3 = b1 * (b2 * b3) ) & ( for b1 being Element of the carrier of (RealVS V) holds 1 * b1 = b1 ) )proof
let a be
real number ;
for v, w being Element of (RealVS V) holds a * (v + w) = (a * v) + (a * w)
reconsider a =
a as
Real by XREAL_0:def 1;
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 Def22;
then reconsider v1 =
v,
w1 =
w as
Element of
V ;
a * (v + w) =
[**a,0 **] * (v1 + w1)
by A1, Def22
.=
([**a,0 **] * v1) + ([**a,0 **] * w1)
by VECTSP_1:def 26
.=
the
addF of
V . [(the Mult of (RealVS V) . a,v1),([**a,0 **] * w1)]
by Def22
.=
(a * v) + (a * w)
by A1, Def22
;
hence
a * (v + w) = (a * v) + (a * w)
;
verum
end;
thus
for a, b being real number
for v being Element of (RealVS V) holds (a + b) * v = (a * v) + (b * v)
( ( for b1, b2 being set
for b3 being Element of the carrier of (RealVS V) holds (b1 * b2) * b3 = b1 * (b2 * b3) ) & ( for b1 being Element of the carrier of (RealVS V) holds 1 * b1 = b1 ) )proof
let a,
b be
real number ;
for v being Element of (RealVS V) holds (a + b) * v = (a * v) + (b * v)
reconsider a =
a,
b =
b as
Real by XREAL_0:def 1;
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 Def22;
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 Def22
.=
([**a,0 **] * v1) + ([**b,0 **] * v1)
by VECTSP_1:def 26
.=
the
addF of
(RealVS V) . [(the Mult of (RealVS V) . a,v),([**b,0 **] * v1)]
by A2, Def22
.=
(a * v) + (b * v)
by Def22
;
hence
(a + b) * v = (a * v) + (b * v)
;
verum
end;
thus
for a, b being real number
for v being Element of (RealVS V) holds (a * b) * v = a * (b * v)
for b1 being Element of the carrier of (RealVS V) holds 1 * b1 = b1proof
let a,
b be
real number ;
for v being Element of (RealVS V) holds (a * b) * v = a * (b * v)
reconsider a =
a,
b =
b as
Real by XREAL_0:def 1;
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 Def22;
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 Def22
.=
[**a,0 **] * ([**b,0 **] * v1)
by VECTSP_1:def 26
.=
the
Mult of
(RealVS V) . a,
([**b,0 **] * v1)
by Def22
.=
a * (b * v)
by Def22
;
hence
(a * b) * v = a * (b * v)
;
verum
end;
let v be Element of (RealVS V); 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 Def22;
then reconsider v1 = v as Element of V ;
thus 1 * v =
[**1,0 **] * v1
by Def22
.=
v
by COMPLFLD:10, VECTSP_1:def 26
; verum