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