thus
for a being Real
for v, w being Element of (RealVS V) holds a * (v + w) = (a * v) + (a * w)
:: according to RLVECT_1:def 9 :: thesis: ( ( for b1, b2 being Element of REAL
for b3 being Element of the carrier of (RealVS V) holds (b1 + b2) * b3 = (b1 * b3) + (b2 * b3) ) & ( for b1, b2 being Element of REAL
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;
:: thesis: for v, w being Element of (RealVS V) holds a * (v + w) = (a * v) + (a * w)let v,
w be
Element of
(RealVS V);
:: thesis: a * (v + w) = (a * v) + (a * w)
A1:
addLoopStr(# the
carrier of
V,the
addF of
V,the
U2 of
V #)
= addLoopStr(# the
carrier of
(RealVS V),the
addF of
(RealVS V),the
U2 of
(RealVS V) #)
by Def22;
set a1 =
[**a,0 **];
reconsider v1 =
v,
w1 =
w as
Element of
V by A1;
thus 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
;
:: thesis: verum
end;
thus
for a, b being Real
for v being Element of (RealVS V) holds (a + b) * v = (a * v) + (b * v)
:: thesis: ( ( for b1, b2 being Element of REAL
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;
:: thesis: for v being Element of (RealVS V) holds (a + b) * v = (a * v) + (b * v)let v be
Element of
(RealVS V);
:: thesis: (a + b) * v = (a * v) + (b * v)
A2:
addLoopStr(# the
carrier of
V,the
addF of
V,the
U2 of
V #)
= addLoopStr(# the
carrier of
(RealVS V),the
addF of
(RealVS V),the
U2 of
(RealVS V) #)
by Def22;
set a1 =
[**a,0 **];
set b1 =
[**b,0 **];
A3:
[**a,0 **] + [**b,0 **] = [**(a + b),0 **]
;
reconsider v1 =
v as
Element of
V by A2;
thus (a + b) * v =
([**a,0 **] + [**b,0 **]) * v1
by A3, 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
;
:: thesis: verum
end;
thus
for a, b being Real
for v being Element of (RealVS V) holds (a * b) * v = a * (b * v)
:: thesis: for b1 being Element of the carrier of (RealVS V) holds 1 * b1 = b1proof
let a,
b be
Real;
:: thesis: for v being Element of (RealVS V) holds (a * b) * v = a * (b * v)let v be
Element of
(RealVS V);
:: thesis: (a * b) * v = a * (b * v)
A4:
addLoopStr(# the
carrier of
V,the
addF of
V,the
U2 of
V #)
= addLoopStr(# the
carrier of
(RealVS V),the
addF of
(RealVS V),the
U2 of
(RealVS V) #)
by Def22;
A5:
[**(a * b),0 **] = [**a,0 **] * [**b,0 **]
;
reconsider v1 =
v as
Element of
V by A4;
thus (a * b) * v =
([**a,0 **] * [**b,0 **]) * v1
by A5, 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
;
:: thesis: verum
end;
let v be Element of (RealVS V); :: thesis: 1 * v = v
addLoopStr(# the carrier of V,the addF of V,the U2 of V #) = addLoopStr(# the carrier of (RealVS V),the addF of (RealVS V),the U2 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
; :: thesis: verum