let V1 be free finite-rank Z_Module; :: thesis: for b1 being OrdBasis of V1
for i, j being Nat st i in dom b1 & j in dom b1 holds
( ( i = j implies ((b1 /. i) |-- b1) . j = 1 ) & ( i <> j implies ((b1 /. i) |-- b1) . j = 0 ) )
let b1 be OrdBasis of V1; :: thesis: for i, j being Nat st i in dom b1 & j in dom b1 holds
( ( i = j implies ((b1 /. i) |-- b1) . j = 1 ) & ( i <> j implies ((b1 /. i) |-- b1) . j = 0 ) )
let i, j be Nat; :: thesis: ( i in dom b1 & j in dom b1 implies ( ( i = j implies ((b1 /. i) |-- b1) . j = 1 ) & ( i <> j implies ((b1 /. i) |-- b1) . j = 0 ) ) )
assume that
A5: i in dom b1 and
A18: j in dom b1 ; :: thesis: ( ( i = j implies ((b1 /. i) |-- b1) . j = 1 ) & ( i <> j implies ((b1 /. i) |-- b1) . j = 0 ) )
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 Def7;
reconsider rb1 = rng b1 as Basis of V1 by defOrdBasis;
b1 /. i in {(b1 /. i)} by TARSKI:def 1;
then b1 /. i in Lin {(b1 /. i)} by ZMODUL02:65;
then consider Lb being Linear_Combination of {(b1 /. i)} such that
A4: b1 /. i = Sum Lb by ZMODUL02:64;
A6: b1 . i = b1 /. i by A5, 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, Th5, VECTSP_7:def 3;
A12: len b1 = len ((b1 /. i) |-- b1) by Def7;
A13: b1 /. i <> 0. V1 by A6, A8, ZMODUL02:57, VECTSP_7:def 3;
j in Seg (len b1) by A18, FINSEQ_1:def 3;
then A15: ( 1 <= j & j <= len ((b1 /. i) |-- b1) ) by FINSEQ_1:1, A12;
A19: dom ((b1 /. i) |-- b1) = dom b1 by A12, FINSEQ_3:29;
set One = 1. INT.Ring;
reconsider KLi = KL . (b1 /. i) as Element of INT.Ring ;
now :: thesis: ( i = j implies 1 = ((b1 /. i) |-- b1) . j )
assume A20: i = j ; :: thesis: 1 = ((b1 /. i) |-- b1) . j
KLi * (b1 /. i) = b1 /. i by A4, A9, ZMODUL02:21
.= (1. INT.Ring) * (b1 /. i) by VECTSP_1:def 17 ;
then KLi = 1. INT.Ring by A13, ZMODUL01:11;
hence 1 = ((b1 /. i) |-- b1) /. j by A2, A15, A20
.= ((b1 /. i) |-- b1) . j by A18, A19, PARTFUN1:def 6 ;
:: thesis: verum
end;
hence ( i = j implies ((b1 /. i) |-- b1) . j = 1 ) ; :: thesis: ( i <> j implies ((b1 /. i) |-- b1) . j = 0 )
now :: thesis: ( i <> j implies 0 = ((b1 /. i) |-- b1) . j )
assume A22: i <> j ; :: thesis: 0 = ((b1 /. i) |-- b1) . j
b1 is one-to-one by defOrdBasis;
then b1 . i <> b1 . j by A5, A18, A22;
then A23: not b1 . j in Carrier Lb by A7, TARSKI:def 1;
b1 . j = b1 /. j by A18, PARTFUN1:def 6;
hence 0 = KL . (b1 /. j) by A9, A23
.= ((b1 /. i) |-- b1) /. j by A2, A15
.= ((b1 /. i) |-- b1) . j by A18, A19, PARTFUN1:def 6 ;
:: thesis: verum
end;
hence ( i <> j implies ((b1 /. i) |-- b1) . j = 0 ) ; :: thesis: verum