set V = R ^* n;
now for a, b being Element of R
for x being Vector of (R ^* n) holds (a + b) * x = (a * x) + (b * x)let a,
b be
Element of
R;
for x being Vector of (R ^* n) holds (a + b) * x = (a * x) + (b * x)let x be
Vector of
(R ^* n);
(a + b) * x = (a * x) + (b * x)reconsider u =
x as
Element of
n -tuples_on the
carrier of
R by DEF;
H1:
a * x =
the
lmult of
(R ^* n) . (
a,
u)
by VECTSP_1:def 12
.=
(vector_mult (n,R)) . (
a,
u)
by DEF
.=
a * u
by Defm
;
H2:
b * x =
the
lmult of
(R ^* n) . (
b,
u)
by VECTSP_1:def 12
.=
(vector_mult (n,R)) . (
b,
u)
by DEF
.=
b * u
by Defm
;
thus (a + b) * x =
the
lmult of
(R ^* n) . (
(a + b),
u)
by VECTSP_1:def 12
.=
(vector_mult (n,R)) . (
(a + b),
u)
by DEF
.=
(a + b) * u
by Defm
.=
(a * u) + (b * u)
by FVSUM_1:55
.=
(vector_add (n,R)) . (
(a * u),
(b * u))
by Defa
.=
(a * x) + (b * x)
by H1, H2, DEF
;
verum end;
hence
R ^* n is scalar-distributive
by VECTSP_1:def 15; ( R ^* n is scalar-associative & R ^* n is vector-distributive )
now for a, b being Element of R
for x being Vector of (R ^* n) holds (a * b) * x = a * (b * x)let a,
b be
Element of
R;
for x being Vector of (R ^* n) holds (a * b) * x = a * (b * x)let x be
Vector of
(R ^* n);
(a * b) * x = a * (b * x)reconsider u =
x as
Element of
n -tuples_on the
carrier of
R by DEF;
H:
b * x =
the
lmult of
(R ^* n) . (
b,
u)
by VECTSP_1:def 12
.=
(vector_mult (n,R)) . (
b,
u)
by DEF
.=
b * u
by Defm
;
thus (a * b) * x =
the
lmult of
(R ^* n) . (
(a * b),
u)
by VECTSP_1:def 12
.=
(vector_mult (n,R)) . (
(a * b),
u)
by DEF
.=
(a * b) * u
by Defm
.=
a * (b * u)
by FVSUM_1:54
.=
(vector_mult (n,R)) . (
a,
(b * u))
by Defm
.=
the
lmult of
(R ^* n) . (
a,
(b * u))
by DEF
.=
a * (b * x)
by H, VECTSP_1:def 12
;
verum end;
hence
R ^* n is scalar-associative
by VECTSP_1:def 16; R ^* n is vector-distributive
now for a being Element of R
for x, y being Vector of (R ^* n) holds a * (x + y) = (a * x) + (a * y)let a be
Element of
R;
for x, y being Vector of (R ^* n) holds a * (x + y) = (a * x) + (a * y)let x,
y be
Vector of
(R ^* n);
a * (x + y) = (a * x) + (a * y)reconsider u =
x,
v =
y as
Element of
n -tuples_on the
carrier of
R by DEF;
H1:
a * x =
the
lmult of
(R ^* n) . (
a,
u)
by VECTSP_1:def 12
.=
(vector_mult (n,R)) . (
a,
u)
by DEF
.=
a * u
by Defm
;
H2:
a * y =
the
lmult of
(R ^* n) . (
a,
v)
by VECTSP_1:def 12
.=
(vector_mult (n,R)) . (
a,
v)
by DEF
.=
a * v
by Defm
;
x + y =
(vector_add (n,R)) . (
u,
v)
by DEF
.=
u + v
by Defa
;
hence a * (x + y) =
the
lmult of
(R ^* n) . (
a,
(u + v))
by VECTSP_1:def 12
.=
(vector_mult (n,R)) . (
a,
(u + v))
by DEF
.=
a * (u + v)
by Defm
.=
(a * u) + (a * v)
by FVSUM_1:56
.=
(vector_add (n,R)) . (
(a * u),
(a * v))
by Defa
.=
(a * x) + (a * y)
by H1, H2, DEF
;
verum end;
hence
R ^* n is vector-distributive
by VECTSP_1:def 14; verum