let i be Nat; :: thesis: for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 st i in dom b1 holds
(b1 /. i) |-- b1 = Line ((1. (K,(len b1))),i)
let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 st i in dom b1 holds
(b1 /. i) |-- b1 = Line ((1. (K,(len b1))),i)
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1 st i in dom b1 holds
(b1 /. i) |-- b1 = Line ((1. (K,(len b1))),i)
let b1 be OrdBasis of V1; :: thesis: ( i in dom b1 implies (b1 /. i) |-- b1 = Line ((1. (K,(len b1))),i) )
set ONE = 1. (K,(len b1));
set bb = (b1 /. i) |-- b1;
consider KL being Linear_Combination of V1 such that
A1: ( b1 /. i = Sum KL & Carrier KL c= rng b1 ) and
A2: for k being Nat st 1 <= k & k <= len ((b1 /. i) |-- b1) holds
((b1 /. i) |-- b1) /. k = KL . (b1 /. k) by MATRLIN:def 7;
reconsider rb1 = rng b1 as Basis of V1 by MATRLIN:def 2;
A3: rb1 is linearly-independent by VECTSP_7:def 3;
b1 /. i in {(b1 /. i)} by TARSKI:def 1;
then b1 /. i in Lin {(b1 /. i)} by VECTSP_7:8;
then consider Lb being Linear_Combination of {(b1 /. i)} such that
A4: b1 /. i = Sum Lb by VECTSP_7:7;
assume A5: i in dom b1 ; :: thesis: (b1 /. i) |-- b1 = Line ((1. (K,(len b1))),i)
then A6: b1 . i = b1 /. i by PARTFUN1:def 6;
then A7: Carrier Lb c= {(b1 . i)} by VECTSP_6:def 4;
A8: b1 . i in rb1 by A5, FUNCT_1:def 3;
then {(b1 . i)} c= rb1 by ZFMISC_1:31;
then Carrier Lb c= rb1 by A7;
then A9: Lb = KL by A4, A1, A3, MATRLIN:5;
A10: width (1. (K,(len b1))) = len b1 by MATRIX_0:24;
A11: Indices (1. (K,(len b1))) = [:(Seg (len b1)),(Seg (len b1)):] by MATRIX_0:24;
A12: len b1 = len ((b1 /. i) |-- b1) by MATRLIN:def 7;
A13: b1 /. i <> 0. V1 by A6, A3, A8, VECTSP_7:2;
A14: now :: thesis: for j being Nat st 1 <= j & j <= len ((b1 /. i) |-- b1) holds
(Line ((1. (K,(len b1))),i)) . j = ((b1 /. i) |-- b1) . j
let j be Nat; :: thesis: ( 1 <= j & j <= len ((b1 /. i) |-- b1) implies (Line ((1. (K,(len b1))),i)) . j = ((b1 /. i) |-- b1) . j )
assume A15: ( 1 <= j & j <= len ((b1 /. i) |-- b1) ) ; :: thesis: (Line ((1. (K,(len b1))),i)) . j = ((b1 /. i) |-- b1) . j
A16: j in Seg (len b1) by A12, A15;
i in Seg (len b1) by A5, FINSEQ_1:def 3;
then A17: [i,j] in Indices (1. (K,(len b1))) by A11, A16, ZFMISC_1:87;
A18: j in dom b1 by A12, A15, FINSEQ_3:25;
A19: dom ((b1 /. i) |-- b1) = dom b1 by A12, FINSEQ_3:29;
now :: thesis: (Line ((1. (K,(len b1))),i)) . j = ((b1 /. i) |-- b1) . j
per cases ( i = j or i <> j ) ;
suppose A20: i = j ; :: thesis: (Line ((1. (K,(len b1))),i)) . j = ((b1 /. i) |-- b1) . j
(Lb . (b1 /. i)) * (b1 /. i) = b1 /. i by A4, VECTSP_6:17
.= (1_ K) * (b1 /. i) by VECTSP_1:def 17 ;
then A21: 1_ K = KL . (b1 /. i) by A13, A9, VECTSP10:4
.= ((b1 /. i) |-- b1) /. j by A2, A15, A20 ;
1_ K = (1. (K,(len b1))) * (i,j) by A17, A20, MATRIX_1:def 3
.= (Line ((1. (K,(len b1))),i)) . j by A10, A16, MATRIX_0:def 7 ;
hence (Line ((1. (K,(len b1))),i)) . j = ((b1 /. i) |-- b1) . j by A18, A19, A21, PARTFUN1:def 6; :: thesis: verum
end;
suppose A22: i <> j ; :: thesis: (Line ((1. (K,(len b1))),i)) . j = ((b1 /. i) |-- b1) . j
b1 is one-to-one by MATRLIN:def 2;
then b1 . i <> b1 . j by A5, A18, A22;
then A23: not b1 . j in Carrier Lb by A7, TARSKI:def 1;
A24: 0. K = (1. (K,(len b1))) * (i,j) by A17, A22, MATRIX_1:def 3
.= (Line ((1. (K,(len b1))),i)) . j by A10, A16, MATRIX_0:def 7 ;
b1 . j = b1 /. j by A18, PARTFUN1:def 6;
then 0. K = KL . (b1 /. j) by A9, A23
.= ((b1 /. i) |-- b1) /. j by A2, A15 ;
hence (Line ((1. (K,(len b1))),i)) . j = ((b1 /. i) |-- b1) . j by A18, A19, A24, PARTFUN1:def 6; :: thesis: verum
end;
end;
end;
hence (Line ((1. (K,(len b1))),i)) . j = ((b1 /. i) |-- b1) . j ; :: thesis: verum
end;
len (Line ((1. (K,(len b1))),i)) = len b1 by A10, CARD_1:def 7;
hence (b1 /. i) |-- b1 = Line ((1. (K,(len b1))),i) by A12, A14; :: thesis: verum