let m, i be Nat; for x being Element of REAL m
for r being Real holds
( ((reproj (i,x)) . r) - x = (reproj (i,(0* m))) . (r - ((proj (i,m)) . x)) & x - ((reproj (i,x)) . r) = (reproj (i,(0* m))) . (((proj (i,m)) . x) - r) )
let x be Element of REAL m; for r being Real holds
( ((reproj (i,x)) . r) - x = (reproj (i,(0* m))) . (r - ((proj (i,m)) . x)) & x - ((reproj (i,x)) . r) = (reproj (i,(0* m))) . (((proj (i,m)) . x) - r) )
let r1 be Real; ( ((reproj (i,x)) . r1) - x = (reproj (i,(0* m))) . (r1 - ((proj (i,m)) . x)) & x - ((reproj (i,x)) . r1) = (reproj (i,(0* m))) . (((proj (i,m)) . x) - r1) )
reconsider r = r1 as Element of REAL by XREAL_0:def 1;
reconsider rr = r - ((proj (i,m)) . x) as Element of REAL ;
reconsider rs = ((proj (i,m)) . x) - r as Element of REAL ;
reconsider p = ((reproj (i,x)) . r) - x as m -element FinSequence ;
reconsider q = (reproj (i,(0* m))) . rr as m -element FinSequence ;
reconsider s = x - ((reproj (i,x)) . r) as m -element FinSequence ;
reconsider t = (reproj (i,(0* m))) . rs as m -element FinSequence ;
A1:
( dom p = Seg m & dom q = Seg m & dom s = Seg m & dom t = Seg m & dom x = Seg m & dom (0* m) = Seg m )
by FINSEQ_1:89;
reconsider x1 = x as Element of m -tuples_on REAL ;
A2:
(reproj (i,x)) . r = Replace (x,i,r)
by PDIFF_1:def 5;
reconsider y1 = (reproj (i,x)) . r as Element of m -tuples_on REAL ;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A3:
( len x = mm & len (0* m) = mm )
by A1, FINSEQ_1:def 3;
then A4:
len (Replace (x,i,r)) = m
by FINSEQ_7:5;
for k being Nat st k in dom p holds
p . k = q . k
proof
let k be
Nat;
( k in dom p implies p . k = q . k )
assume A5:
k in dom p
;
p . k = q . k
then A6:
( 1
<= k &
k <= m )
by A1, FINSEQ_1:1;
then
k in dom (Replace (x,i,r))
by A4, FINSEQ_3:25;
then A7:
(Replace (x,i,r)) /. k = (Replace (x,i,r)) . k
by PARTFUN1:def 6;
A8:
p . k = (y1 . k) - (x1 . k)
by RVSUM_1:27;
q = Replace (
(0* m),
i,
rr)
by PDIFF_1:def 5;
then A9:
q . k = (Replace ((0* m),i,rr)) /. k
by A5, A1, PARTFUN1:def 6;
per cases
( k = i or k <> i )
;
suppose
k <> i
;
p . k = q . kthen
(
(Replace (x,i,r)) . k = x1 /. k &
q . k = (0* m) /. k )
by A3, A6, A7, A9, FINSEQ_7:10;
then
(
(Replace (x,i,r)) . k = x1 . k &
q . k = (m |-> 0) . k )
by A5, A1, PARTFUN1:def 6;
hence
p . k = q . k
by A2, A8;
verum end; end;
end;
then
((reproj (i,x)) . r) - x = (reproj (i,(0* m))) . (r - ((proj (i,m)) . x))
by A1, FINSEQ_1:13;
hence
((reproj (i,x)) . r1) - x = (reproj (i,(0* m))) . (r1 - ((proj (i,m)) . x))
; x - ((reproj (i,x)) . r1) = (reproj (i,(0* m))) . (((proj (i,m)) . x) - r1)
for k being Nat st k in dom s holds
s . k = t . k
proof
let k be
Nat;
( k in dom s implies s . k = t . k )
assume A11:
k in dom s
;
s . k = t . k
then A12:
( 1
<= k &
k <= m )
by A1, FINSEQ_1:1;
then
k in dom (Replace (x,i,r))
by A4, FINSEQ_3:25;
then A13:
(Replace (x,i,r)) /. k = (Replace (x,i,r)) . k
by PARTFUN1:def 6;
A14:
s . k = (x1 . k) - (y1 . k)
by RVSUM_1:27;
t = Replace (
(0* m),
i,
rs)
by PDIFF_1:def 5;
then A15:
t . k = (Replace ((0* m),i,rs)) /. k
by A1, A11, PARTFUN1:def 6;
per cases
( k = i or k <> i )
;
suppose
k <> i
;
s . k = t . kthen
(
(Replace (x,i,r)) . k = x1 /. k &
t . k = (0* m) /. k )
by A3, A12, A13, A15, FINSEQ_7:10;
then
(
(Replace (x,i,r)) . k = x1 . k &
t . k = (m |-> 0) . k )
by A1, A11, PARTFUN1:def 6;
hence
s . k = t . k
by A2, A14;
verum end; end;
end;
hence
x - ((reproj (i,x)) . r1) = (reproj (i,(0* m))) . (((proj (i,m)) . x) - r1)
by A1, FINSEQ_1:13; verum