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