let G be RealNormSpace-Sequence; for i being Element of dom G
for xi being Element of (G . i) holds ||.((reproj (i,(0. (product G)))) . xi).|| = ||.xi.||
let i be Element of dom G; for xi being Element of (G . i) holds ||.((reproj (i,(0. (product G)))) . xi).|| = ||.xi.||
let xi be Element of (G . i); ||.((reproj (i,(0. (product G)))) . xi).|| = ||.xi.||
set j = len G;
reconsider i0 = i as Element of NAT ;
Seg (len G) = dom G
by FINSEQ_1:def 3;
then A1:
( 1 <= i0 & i0 <= len G )
by FINSEQ_1:1;
set z = 0. (product G);
A3:
the carrier of (product G) = product (carr G)
by Th10;
then reconsider w = (0. (product G)) +* (i0,xi) as Element of product (carr G) by Th11;
A4:
||.((reproj (i,(0. (product G)))) . xi).|| = |.(normsequence (G,w)).|
by Def4, PRVECT_2:7;
reconsider q = ||.xi.|| as Element of REAL ;
set q1 = <*q*>;
set y = 0* (len G);
A5:
len (normsequence (G,w)) = len G
by PRVECT_2:def 11;
A6:
len (0* (len G)) = len G
by CARD_1:def 7;
then A7:
(((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0) = Replace ((0* (len G)),i0,q)
by A1, FINSEQ_7:def 1;
then A8:
len ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) = len (0* (len G))
by FINSEQ_7:5;
A9:
len (0* (len G)) = len (Replace ((0* (len G)),i0,q))
by FINSEQ_7:5;
for k being Nat st 1 <= k & k <= len (normsequence (G,w)) holds
(normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) . k
proof
let k be
Nat;
( 1 <= k & k <= len (normsequence (G,w)) implies (normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) . k )
assume A10:
( 1
<= k &
k <= len (normsequence (G,w)) )
;
(normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) . k
then reconsider k1 =
k as
Element of
dom G by A5, FINSEQ_3:25;
A11:
k1 in dom G
;
0. (product G) in the
carrier of
(product G)
;
then
0. (product G) in product (carr G)
by Th10;
then consider g being
Function such that A12:
(
0. (product G) = g &
dom g = dom (carr G) & ( for
y being
object st
y in dom (carr G) holds
g . y in (carr G) . y ) )
by CARD_3:def 5;
A13:
k in dom (0. (product G))
by A11, A12, Lm1;
A14:
(normsequence (G,w)) . k = the
normF of
(G . k1) . (w . k1)
by PRVECT_2:def 11;
per cases
( k = i0 or k <> i0 )
;
suppose A15:
k = i0
;
(normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) . kthen A16:
(normsequence (G,w)) . k = ||.xi.||
by A14, A13, FUNCT_7:31;
(Replace ((0* (len G)),i0,q)) /. k = q
by A15, A10, A5, A6, FINSEQ_7:8;
hence
(normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) . k
by A16, A7, A10, A5, A6, A9, FINSEQ_4:15;
verum end; suppose A17:
k <> i0
;
(normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) . kthen
w . k1 = (0. (product G)) . k1
by FUNCT_7:32;
then A18:
(normsequence (G,w)) . k = ||.(0. (G . k1)).||
by A14, Th14, A3;
(Replace ((0* (len G)),i0,q)) /. k = (0* (len G)) /. k
by A17, A10, A5, A6, FINSEQ_7:10;
then
(Replace ((0* (len G)),i0,q)) . k = (0* (len G)) /. k
by A10, A5, A6, A9, FINSEQ_4:15;
then
(Replace ((0* (len G)),i0,q)) . k = (0* (len G)) . k
by A10, A5, A6, FINSEQ_4:15;
hence
(normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) . k
by A18, A6, A1, FINSEQ_7:def 1;
verum end;
end;
then A19:
normsequence (G,w) = (((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)
by A6, A8, PRVECT_2:def 11;
sqrt (Sum (sqr ((0* (len G)) | (i0 -' 1)))) = |.(0* (i0 -' 1)).|
by A1, PDIFF_7:2;
then
sqrt (Sum (sqr ((0* (len G)) | (i0 -' 1)))) = 0
by EUCLID:7;
then A20:
Sum (sqr ((0* (len G)) | (i0 -' 1))) = 0
by RVSUM_1:86, SQUARE_1:24;
sqrt (Sum (sqr ((0* (len G)) /^ i0))) = |.(0* ((len G) -' i0)).|
by PDIFF_7:3;
then A21:
sqrt (Sum (sqr ((0* (len G)) /^ i0))) = 0
by EUCLID:7;
reconsider q2 = q ^2 as Element of REAL by XREAL_0:def 1;
sqr ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) =
(sqr (((0* (len G)) | (i0 -' 1)) ^ <*q*>)) ^ (sqr ((0* (len G)) /^ i0))
by RVSUM_1:144
.=
((sqr ((0* (len G)) | (i0 -' 1))) ^ (sqr <*q*>)) ^ (sqr ((0* (len G)) /^ i0))
by RVSUM_1:144
.=
((sqr ((0* (len G)) | (i0 -' 1))) ^ <*(q ^2)*>) ^ (sqr ((0* (len G)) /^ i0))
by RVSUM_1:55
;
then Sum (sqr ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0))) =
(Sum ((sqr ((0* (len G)) | (i0 -' 1))) ^ <*q2*>)) + (Sum (sqr ((0* (len G)) /^ i0)))
by RVSUM_1:75
.=
((Sum (sqr ((0* (len G)) | (i0 -' 1)))) + (q ^2)) + (Sum (sqr ((0* (len G)) /^ i0)))
by RVSUM_1:74
.=
q ^2
by A20, A21, RVSUM_1:86, SQUARE_1:24
;
then
||.((reproj (i,(0. (product G)))) . xi).|| = |.q.|
by A19, A4, COMPLEX1:72;
hence
||.((reproj (i,(0. (product G)))) . xi).|| = ||.xi.||
by COMPLEX1:43; verum