let j, n be Nat; :: thesis: for F being FinSequence of the carrier of (RealVectSpace (Seg n))
for Bn being Subset of (RealVectSpace (Seg n))
for v0 being Element of (RealVectSpace (Seg n))
for l being Linear_Combination of Bn st F is one-to-one & Bn is R-orthogonal & rng F = Carrier l & v0 in Bn & j in dom (l (#) F) & v0 = F . j holds
(Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0))
let F be FinSequence of the carrier of (RealVectSpace (Seg n)); :: thesis: for Bn being Subset of (RealVectSpace (Seg n))
for v0 being Element of (RealVectSpace (Seg n))
for l being Linear_Combination of Bn st F is one-to-one & Bn is R-orthogonal & rng F = Carrier l & v0 in Bn & j in dom (l (#) F) & v0 = F . j holds
(Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0))
let Bn be Subset of (RealVectSpace (Seg n)); :: thesis: for v0 being Element of (RealVectSpace (Seg n))
for l being Linear_Combination of Bn st F is one-to-one & Bn is R-orthogonal & rng F = Carrier l & v0 in Bn & j in dom (l (#) F) & v0 = F . j holds
(Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0))
let v0 be Element of (RealVectSpace (Seg n)); :: thesis: for l being Linear_Combination of Bn st F is one-to-one & Bn is R-orthogonal & rng F = Carrier l & v0 in Bn & j in dom (l (#) F) & v0 = F . j holds
(Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0))
let l be Linear_Combination of Bn; :: thesis: ( F is one-to-one & Bn is R-orthogonal & rng F = Carrier l & v0 in Bn & j in dom (l (#) F) & v0 = F . j implies (Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0)) )
assume that
A1: F is one-to-one and
A2: Bn is R-orthogonal and
A3: rng F = Carrier l and
A4: v0 in Bn and
A5: j in dom (l (#) F) and
A6: v0 = F . j ; :: thesis: (Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0))
A7: len (l (#) F) = len F by RLVECT_2:def 7;
then A8: dom (l (#) F) = Seg (len F) by FINSEQ_1:def 3
.= dom F by FINSEQ_1:def 3 ;
reconsider F2 = l (#) F as FinSequence of the carrier of (RealVectSpace (Seg n)) ;
reconsider rv0 = v0 as Element of REAL n by FINSEQ_2:93;
consider f being sequence of the carrier of (RealVectSpace (Seg n)) such that
A9: Sum F2 = f . (len F2) and
A10: f . 0 = 0. (RealVectSpace (Seg n)) and
A11: for j2 being Nat
for v being Element of (RealVectSpace (Seg n)) st j2 < len F2 & v = F2 . (j2 + 1) holds
f . (j2 + 1) = (f . j2) + v by RLVECT_1:def 12;
defpred S1[ Nat] means ( $1 >= j & $1 <= len F implies (Euclid_scalar n) . (v0,(f . $1)) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0)) );
defpred S2[ Nat] means ( $1 < j implies (Euclid_scalar n) . (v0,(f . $1)) = 0 );
(Euclid_scalar n) . (v0,(f . 0)) = |(rv0,(0* n))| by A10, REAL_NS1:def 5
.= 0 by EUCLID_4:18 ;
then A12: S2[ 0 ] ;
A13: dom (l (#) F) = Seg (len (l (#) F)) by FINSEQ_1:def 3;
then A14: j <= len F by A5, A7, FINSEQ_1:1;
A15: Carrier l c= Bn by RLVECT_2:def 6;
A16: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A17: S2[k] ; :: thesis: S2[k + 1]
now :: thesis: ( ( k < len F2 & S2[k + 1] ) or ( k >= len F2 & S2[k + 1] ) )
per cases ( k < len F2 or k >= len F2 ) ;
case A18: k < len F2 ; :: thesis: verum
A19: 1 <= k + 1 by NAT_1:11;
k + 1 <= len F2 by A18, NAT_1:13;
then k + 1 in Seg (len F2) by A19, FINSEQ_1:1;
then k + 1 in dom F2 by FINSEQ_1:def 3;
then F2 . (k + 1) in rng F2 by FUNCT_1:def 3;
then reconsider v = F2 . (k + 1) as Element of (RealVectSpace (Seg n)) ;
reconsider rv = v as Element of REAL n by FINSEQ_2:93;
reconsider fk = f . k as Element of REAL n by FINSEQ_2:93;
per cases ( k + 1 < j or k + 1 >= j ) ;
suppose A20: k + 1 < j ; :: thesis: S2[k + 1]
A21: 1 <= k + 1 by NAT_1:11;
k + 1 < len F by A14, A20, XXREAL_0:2;
then k + 1 in Seg (len F) by A21, FINSEQ_1:1;
then A22: k + 1 in dom F by FINSEQ_1:def 3;
then A23: F /. (k + 1) = F . (k + 1) by PARTFUN1:def 6;
then A24: rv0 <> F /. (k + 1) by A1, A5, A6, A8, A20, A22, FUNCT_1:def 4;
k < k + 1 by XREAL_1:29;
then A25: |(rv0,fk)| = 0 by A17, A20, REAL_NS1:def 5, XXREAL_0:2;
reconsider fk1 = F /. (k + 1) as Element of REAL n by FINSEQ_2:93;
A26: |(rv0,(fk + rv))| = |(rv0,fk)| + |(rv0,rv)| by EUCLID_4:28;
A27: F /. (k + 1) in rng F by A22, A23, FUNCT_1:def 3;
v = (l . (F /. (k + 1))) * (F /. (k + 1)) by A8, A22, RLVECT_2:def 7;
then |(rv0,rv)| = (l . (F /. (k + 1))) * |(rv0,fk1)| by EUCLID_4:22
.= (l . (F /. (k + 1))) * 0 by A2, A3, A4, A15, A27, A24
.= 0 ;
then (Euclid_scalar n) . (v0,((f . k) + v)) = 0 by A25, A26, REAL_NS1:def 5;
hence S2[k + 1] by A11, A18; :: thesis: verum
end;
suppose k + 1 >= j ; :: thesis: S2[k + 1]
hence S2[k + 1] ; :: thesis: verum
end;
end;
end;
end;
end;
hence S2[k + 1] ; :: thesis: verum
end;
A29: for i being Nat holds S2[i] from NAT_1:sch 2(A12, A16);
 A30: for i being Nat st i < j holds
(Euclid_scalar n) . (v0,(f . i)) = 0 by A29;
A31: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A32: S1[k] ; :: thesis: S1[k + 1]
per cases ( k + 1 < j or k + 1 >= j ) ;
suppose k + 1 < j ; :: thesis: S1[k + 1]
hence S1[k + 1] ; :: thesis: verum
end;
suppose A33: k + 1 >= j ; :: thesis: S1[k + 1]
per cases ( k + 1 > j or k + 1 = j ) by A33, XXREAL_0:1;
suppose A34: k + 1 > j ; :: thesis: S1[k + 1]
per cases ( k + 1 <= len F2 or k + 1 > len F2 ) ;
suppose A35: k + 1 <= len F2 ; :: thesis: S1[k + 1]
1 <= k + 1 by NAT_1:11;
then A36: k + 1 in Seg (len F2) by A35, FINSEQ_1:1;
then A37: k + 1 in dom F by A7, FINSEQ_1:def 3;
then A38: F /. (k + 1) = F . (k + 1) by PARTFUN1:def 6;
then A39: F /. (k + 1) in rng F by A37, FUNCT_1:def 3;
k + 1 in dom F2 by A36, FINSEQ_1:def 3;
then F2 . (k + 1) in rng F2 by FUNCT_1:def 3;
then reconsider v = F2 . (k + 1) as Element of (RealVectSpace (Seg n)) ;
reconsider rv = v as Element of REAL n by FINSEQ_2:93;
reconsider fk1 = F /. (k + 1) as Element of REAL n by FINSEQ_2:93;
reconsider fk = f . k as Element of REAL n by FINSEQ_2:93;
A40: |(rv0,(fk + rv))| = |(rv0,fk)| + |(rv0,rv)| by EUCLID_4:28;
A41: rv0 <> F /. (k + 1) by A1, A5, A6, A8, A34, A37, A38, FUNCT_1:def 4;
v = (l . (F /. (k + 1))) * (F /. (k + 1)) by A8, A37, RLVECT_2:def 7;
then A42: |(rv0,rv)| = (l . (F /. (k + 1))) * |(rv0,fk1)| by EUCLID_4:22
.= (l . (F /. (k + 1))) * 0 by A2, A3, A4, A15, A39, A41
.= 0 ;
k < k + 1 by XREAL_1:29;
then A43: k < len F2 by A35, XXREAL_0:2;
then |(rv0,fk)| = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0)) by A32, A34, NAT_1:13, REAL_NS1:def 5, RLVECT_2:def 7;
then (Euclid_scalar n) . (v0,((f . k) + v)) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0)) by A40, A42, REAL_NS1:def 5;
hence S1[k + 1] by A11, A43; :: thesis: verum
end;
suppose k + 1 > len F2 ; :: thesis: S1[k + 1]
hence S1[k + 1] by RLVECT_2:def 7; :: thesis: verum
end;
end;
end;
suppose A44: k + 1 = j ; :: thesis: S1[k + 1]
then F2 . (k + 1) in rng F2 by A5, FUNCT_1:def 3;
then reconsider v = F2 . (k + 1) as Element of (RealVectSpace (Seg n)) ;
A45: v = (l . (F /. (k + 1))) * (F /. (k + 1)) by A5, A44, RLVECT_2:def 7;
reconsider rv = v as Element of REAL n by FINSEQ_2:93;
k + 1 in dom F by A5, A13, A7, A44, FINSEQ_1:def 3;
then A46: |(rv0,rv)| = |(rv0,((l . (F /. j)) * rv0))| by A6, A44, A45, PARTFUN1:def 6
.= (Euclid_scalar n) . (v0,((l . (F /. j)) * v0)) by REAL_NS1:def 5 ;
reconsider fk = f . k as Element of REAL n by FINSEQ_2:93;
(Euclid_scalar n) . (v0,(f . k)) = 0 by A30, A44, XREAL_1:29;
then A47: |(rv0,fk)| = 0 by REAL_NS1:def 5;
k < k + 1 by XREAL_1:29;
then A48: k < len F2 by A7, A14, A44, XXREAL_0:2;
|(rv0,(fk + rv))| = |(rv0,fk)| + |(rv0,rv)| by EUCLID_4:28;
then (Euclid_scalar n) . (v0,((f . k) + v)) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0)) by A47, A46, REAL_NS1:def 5;
hence S1[k + 1] by A11, A48; :: thesis: verum
end;
end;
end;
end;
end;
A49: S1[ 0 ] by A5, A13, FINSEQ_1:1;
A50: for i being Nat holds S1[i] from NAT_1:sch 2(A49, A31);
 for i being Nat st i >= j & i <= len F holds
(Euclid_scalar n) . (v0,(f . i)) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0)) by A50;
hence (Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0)) by A9, A7, A14; :: thesis: verum