A1:
1_ F is_a_unity_wrt the multF of F
by Th11;
then A2:
the multF of F is having_a_unity
by SETWISEO:def 2;
A3:
the_unity_wrt the multF of F = 1_ F
by A1, BINOP_1:def 8;
A4:
addLoopStr(# the carrier of (n -VectSp_over F),the addF of (n -VectSp_over F),the U2 of (n -VectSp_over F) #) = n -Group_over F
by Def5;
A5:
n -Group_over F = addLoopStr(# (n -tuples_on the carrier of F),(product the addF of F,n),(n .--> (0. F)) #)
by Def3;
n -VectSp_over F is VectSp-like
proof
let x,
y be
Element of
F;
:: according to VECTSP_1:def 26 :: thesis: 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);
:: thesis: ( 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 v' =
v,
w' =
w as
Element of
n -tuples_on the
carrier of
F by A4, A5;
thus x * (v + w) =
(n -Mult_over F) . x,
((product the addF of F,n) . v,w)
by A4, A5, Def5
.=
(n -Mult_over F) . x,
(the addF of F .: v',w')
by Def1
.=
the
multF of
F [;] x,
(the addF of F .: v',w')
by Def4
.=
the
addF of
F .: (the multF of F [;] x,v'),
(the multF of F [;] x,w')
by Lm5, Th18
.=
(product the addF of F,n) . (the multF of F [;] x,v'),
(the multF of F [;] x,w')
by Def1
.=
(product the addF of F,n) . ((n -Mult_over F) . x,v'),
(the multF of F [;] x,w')
by Def4
.=
(product the addF of F,n) . ((n -Mult_over F) . x,v'),
((n -Mult_over F) . x,w')
by Def4
.=
(product the addF of F,n) . (the lmult of (n -VectSp_over F) . x,v),
((n -Mult_over F) . x,w')
by Def5
.=
(x * v) + (x * w)
by A4, A5, Def5
;
:: thesis: ( (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),
v'
by Def5
.=
the
multF of
F [;] (the addF of F . x,y),
v'
by Def4
.=
the
addF of
F .: (the multF of F [;] x,v'),
(the multF of F [;] y,v')
by Lm5, FINSEQOP:47
.=
(product the addF of F,n) . (the multF of F [;] x,v'),
(the multF of F [;] y,v')
by Def1
.=
(product the addF of F,n) . ((n -Mult_over F) . x,v'),
(the multF of F [;] y,v')
by Def4
.=
(product the addF of F,n) . ((n -Mult_over F) . x,v'),
((n -Mult_over F) . y,v')
by Def4
.=
(product the addF of F,n) . (the lmult of (n -VectSp_over F) . x,v),
((n -Mult_over F) . y,v')
by Def5
.=
(x * v) + (y * v)
by A4, A5, Def5
;
:: thesis: ( (x * y) * v = x * (y * v) & (1. F) * v = v )
thus (x * y) * v =
(n -Mult_over F) . (x * y),
v'
by Def5
.=
the
multF of
F [;] (x * y),
v'
by Def4
.=
the
multF of
F [;] x,
(the multF of F [;] y,v')
by Lm4, FINSEQOP:32
.=
(n -Mult_over F) . x,
(the multF of F [;] y,v')
by Def4
.=
(n -Mult_over F) . x,
((n -Mult_over F) . y,v')
by Def4
.=
(n -Mult_over F) . x,
(the lmult of (n -VectSp_over F) . y,v)
by Def5
.=
x * (y * v)
by Def5
;
:: thesis: (1. F) * v = v
thus (1. F) * v =
(n -Mult_over F) . (1. F),
v'
by Def5
.=
the
multF of
F [;] (1. F),
v'
by Def4
.=
v
by A2, A3, FINSEQOP:58
;
:: thesis: verum
thus
verum
;
:: thesis: verum
end;
hence
n -VectSp_over F is VectSp-like
; :: thesis: verum