A1:
( addLoopStr(# the carrier of (n -VectSp_over F), the addF of (n -VectSp_over F), the ZeroF of (n -VectSp_over F) #) = n -Group_over F & n -Group_over F = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) )
by Def3, Def5;
1_ F is_a_unity_wrt the multF of F
by Th11;
then A2:
( the multF of F is having_a_unity & the_unity_wrt the multF of F = 1_ F )
by BINOP_1:def 8, SETWISEO:def 2;
X1:
n -VectSp_over F is vector-distributive
proof
let x be
Element of
F;
VECTSP_1:def 26 for b1, b2 being Element of the carrier of (n -VectSp_over F) holds x * (b1 + b2) = (x * b1) + (x * b2)let v,
w be
Element of
(n -VectSp_over F);
x * (v + w) = (x * v) + (x * w)
reconsider v9 =
v,
w9 =
w as
Element of
n -tuples_on the
carrier of
F by A1;
thus x * (v + w) =
(n -Mult_over F) . (
x,
((product ( the addF of F,n)) . (v,w)))
by A1, Def5
.=
(n -Mult_over F) . (
x,
( the addF of F .: (v9,w9)))
by Def1
.=
the
multF of
F [;] (
x,
( the addF of F .: (v9,w9)))
by Def4
.=
the
addF of
F .: (
( the multF of F [;] (x,v9)),
( the multF of F [;] (x,w9)))
by Lm5, Th18
.=
(product ( the addF of F,n)) . (
( the multF of F [;] (x,v9)),
( the multF of F [;] (x,w9)))
by Def1
.=
(product ( the addF of F,n)) . (
((n -Mult_over F) . (x,v9)),
( the multF of F [;] (x,w9)))
by Def4
.=
(product ( the addF of F,n)) . (
((n -Mult_over F) . (x,v9)),
((n -Mult_over F) . (x,w9)))
by Def4
.=
(product ( the addF of F,n)) . (
( the lmult of (n -VectSp_over F) . (x,v)),
((n -Mult_over F) . (x,w9)))
by Def5
.=
(x * v) + (x * w)
by A1, Def5
;
verum
end;
X2:
n -VectSp_over F is scalar-distributive
proof
let x,
y be
Element of
F;
VECTSP_1:def 27 for b1 being Element of the carrier of (n -VectSp_over F) holds (x + y) * b1 = (x * b1) + (y * b1)let v be
Element of
(n -VectSp_over F);
(x + y) * v = (x * v) + (y * v)
reconsider v9 =
v as
Element of
n -tuples_on the
carrier of
F by A1;
thus (x + y) * v =
(n -Mult_over F) . (
(x + y),
v9)
by Def5
.=
the
multF of
F [;] (
( the addF of F . (x,y)),
v9)
by Def4
.=
the
addF of
F .: (
( the multF of F [;] (x,v9)),
( the multF of F [;] (y,v9)))
by Lm5, FINSEQOP:47
.=
(product ( the addF of F,n)) . (
( the multF of F [;] (x,v9)),
( the multF of F [;] (y,v9)))
by Def1
.=
(product ( the addF of F,n)) . (
((n -Mult_over F) . (x,v9)),
( the multF of F [;] (y,v9)))
by Def4
.=
(product ( the addF of F,n)) . (
((n -Mult_over F) . (x,v9)),
((n -Mult_over F) . (y,v9)))
by Def4
.=
(product ( the addF of F,n)) . (
( the lmult of (n -VectSp_over F) . (x,v)),
((n -Mult_over F) . (y,v9)))
by Def5
.=
(x * v) + (y * v)
by A1, Def5
;
verum
end;
X3:
n -VectSp_over F is scalar-associative
proof
let x,
y be
Element of
F;
VECTSP_1:def 28 for b1 being Element of the carrier of (n -VectSp_over F) holds (x * y) * b1 = x * (y * b1)let v be
Element of
(n -VectSp_over F);
(x * y) * v = x * (y * v)
reconsider v9 =
v as
Element of
n -tuples_on the
carrier of
F by A1;
thus (x * y) * v =
(n -Mult_over F) . (
(x * y),
v9)
by Def5
.=
the
multF of
F [;] (
(x * y),
v9)
by Def4
.=
the
multF of
F [;] (
x,
( the multF of F [;] (y,v9)))
by Lm4, FINSEQOP:32
.=
(n -Mult_over F) . (
x,
( the multF of F [;] (y,v9)))
by Def4
.=
(n -Mult_over F) . (
x,
((n -Mult_over F) . (y,v9)))
by Def4
.=
(n -Mult_over F) . (
x,
( the lmult of (n -VectSp_over F) . (y,v)))
by Def5
.=
x * (y * v)
by Def5
;
verum
end;
n -VectSp_over F is scalar-unital
hence
( n -VectSp_over F is vector-distributive & n -VectSp_over F is scalar-distributive & n -VectSp_over F is scalar-associative & n -VectSp_over F is scalar-unital )
by X1, X2, X3; verum