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;
n -VectSp_over F is VectSp-like
proof
let x,
y 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) & (x + y) * b1 = (x * b1) + (y * b1) & (x * y) * b1 = x * (y * b1) & (1. F) * b1 = b1 )let v,
w be
Element of
(n -VectSp_over F);
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )
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
;
( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )
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
;
( (x * y) * v = x * (y * v) & (1. F) * v = v )
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
;
(1. F) * v = v
thus (1. F) * v =
(n -Mult_over F) . (1. F),
v9
by Def5
.=
the
multF of
F [;] (1. F),
v9
by Def4
.=
v
by A2, FINSEQOP:58
;
verum
thus
verum
;
verum
end;
hence
n -VectSp_over F is VectSp-like
; verum