let K be Field; for p being FinSequence of K holds (- (1_ K)) * p = - p
let p be FinSequence of K; (- (1_ K)) * p = - p
A1:
( Seg (len ((- (1_ K)) * p)) = Seg (len p) & dom ((- (1_ K)) * p) = Seg (len ((- (1_ K)) * p)) )
by FINSEQ_1:def 3, MATRIXR1:16;
A2:
dom p = Seg (len p)
by FINSEQ_1:def 3;
A3:
for i being Nat st i in dom p holds
((- (1_ K)) * p) . i = (- p) . i
proof
let i be
Nat;
( i in dom p implies ((- (1_ K)) * p) . i = (- p) . i )
A4:
rng p c= the
carrier of
K
by FINSEQ_1:def 4;
assume A5:
i in dom p
;
((- (1_ K)) * p) . i = (- p) . i
then A6:
p . i in dom ( the multF of K [;] ((- (1_ K)),(id the carrier of K)))
by A1, A2, FUNCT_1:11;
p . i in rng p
by A5, FUNCT_1:3;
then reconsider b =
p . i as
Element of
K by A4;
((- (1_ K)) * b) + b =
((- (1_ K)) * b) + ((1_ K) * b)
.=
((- (1_ K)) + (1_ K)) * b
by VECTSP_1:def 7
.=
(0. K) * b
by RLVECT_1:5
.=
0. K
;
then
((- (1_ K)) * b) + (b + (- b)) = (0. K) + (- b)
by RLVECT_1:def 3;
then (0. K) + (- b) =
((- (1_ K)) * b) + (0. K)
by RLVECT_1:5
.=
(- (1_ K)) * b
by RLVECT_1:4
;
then A7:
(- (1_ K)) * b = - b
by RLVECT_1:4;
((- (1_ K)) * p) . i =
((- (1_ K)) multfield) . (p . i)
by A5, FUNCT_1:13
.=
the
multF of
K . (
(- (1_ K)),
((id the carrier of K) . (p . i)))
by A6, FUNCOP_1:32
.=
the
multF of
K . (
(- (1_ K)),
b)
.=
(comp K) . b
by A7, VECTSP_1:def 13
.=
(- p) . i
by A5, FUNCT_1:13
;
hence
((- (1_ K)) * p) . i = (- p) . i
;
verum
end;
p is Element of (len p) -tuples_on the carrier of K
by FINSEQ_2:92;
then
- p is Element of (len p) -tuples_on the carrier of K
by FINSEQ_2:113;
then A8:
len (- p) = len p
by CARD_1:def 7;
( dom (- p) = Seg (len (- p)) & dom p = Seg (len p) )
by FINSEQ_1:def 3;
hence
(- (1_ K)) * p = - p
by A1, A3, A8, FINSEQ_1:13; verum