let K be Field; for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds (0. V1) |-- b1 = (len b1) |-> (0. K)
let V1 be finite-dimensional VectSp of K; for b1 being OrdBasis of V1 holds (0. V1) |-- b1 = (len b1) |-> (0. K)
let b1 be OrdBasis of V1; (0. V1) |-- b1 = (len b1) |-> (0. K)
per cases
( dom b1 = {} or dom b1 <> {} )
;
suppose
dom b1 <> {}
;
(0. V1) |-- b1 = (len b1) |-> (0. K)then consider x being
object such that A3:
x in dom b1
by XBOOLE_0:def 1;
A4:
width (1. (K,(len b1))) = len b1
by MATRIX_0:24;
reconsider x =
x as
Nat by A3;
0. V1 =
(b1 /. x) - (b1 /. x)
by VECTSP_1:16
.=
(b1 /. x) + ((- (1_ K)) * (b1 /. x))
by VECTSP_1:14
;
hence (0. V1) |-- b1 =
((b1 /. x) |-- b1) + (((- (1_ K)) * (b1 /. x)) |-- b1)
by Th17
.=
((b1 /. x) |-- b1) + ((- (1_ K)) * ((b1 /. x) |-- b1))
by Th18
.=
(Line ((1. (K,(len b1))),x)) + ((- (1_ K)) * ((b1 /. x) |-- b1))
by A3, Th19
.=
(Line ((1. (K,(len b1))),x)) + ((- (1_ K)) * (Line ((1. (K,(len b1))),x)))
by A3, Th19
.=
(Line ((1. (K,(len b1))),x)) + (- (Line ((1. (K,(len b1))),x)))
by FVSUM_1:59
.=
(len b1) |-> (0. K)
by A4, FVSUM_1:26
;
verum end; end;