let m be non zero Nat; for x, y being Element of REAL
for z being Element of REAL m
for i being Nat st 1 <= i & i <= m & y = (proj (i,m)) . z holds
( (Replace (z,i,x)) - z = (0* m) +* (i,(x - y)) & z - (Replace (z,i,x)) = (0* m) +* (i,(y - x)) )
let x, y be Element of REAL ; for z being Element of REAL m
for i being Nat st 1 <= i & i <= m & y = (proj (i,m)) . z holds
( (Replace (z,i,x)) - z = (0* m) +* (i,(x - y)) & z - (Replace (z,i,x)) = (0* m) +* (i,(y - x)) )
let z be Element of REAL m; for i being Nat st 1 <= i & i <= m & y = (proj (i,m)) . z holds
( (Replace (z,i,x)) - z = (0* m) +* (i,(x - y)) & z - (Replace (z,i,x)) = (0* m) +* (i,(y - x)) )
let i be Nat; ( 1 <= i & i <= m & y = (proj (i,m)) . z implies ( (Replace (z,i,x)) - z = (0* m) +* (i,(x - y)) & z - (Replace (z,i,x)) = (0* m) +* (i,(y - x)) ) )
assume that
A1:
( 1 <= i & i <= m )
and
A2:
y = (proj (i,m)) . z
; ( (Replace (z,i,x)) - z = (0* m) +* (i,(x - y)) & z - (Replace (z,i,x)) = (0* m) +* (i,(y - x)) )
reconsider xy = x - y, my = - y as Element of REAL ;
A3:
( len (Replace ((0* m),i,xy)) = m & len (Replace ((0* m),i,x)) = m & len (Replace ((0* m),i,my)) = m )
by Lm6;
A4:
dom (Replace (z,i,x)) = dom z
by FUNCT_7:30;
A5:
( dom (- z) = dom z & dom (- (Replace (z,i,x))) = dom (Replace (z,i,x)) )
by VALUED_1:def 5;
A6:
dom ((Replace (z,i,x)) - z) = (dom (Replace (z,i,x))) /\ (dom (- z))
by VALUED_1:def 1;
A7:
len (0* m) = m
by CARD_1:def 7;
dom ((Replace (z,i,x)) - z) = Seg m
by A4, A5, A6, FINSEQ_1:89;
then
len ((Replace (z,i,x)) - z) = len (0* m)
by A7, FINSEQ_1:def 3;
then A8:
len ((Replace (z,i,x)) - z) = len (Replace ((0* m),i,xy))
by FINSEQ_7:5;
for j being Nat st 1 <= j & j <= len ((Replace (z,i,x)) - z) holds
(Replace ((0* m),i,xy)) . j = ((Replace (z,i,x)) - z) . j
proof
let j be
Nat;
( 1 <= j & j <= len ((Replace (z,i,x)) - z) implies (Replace ((0* m),i,xy)) . j = ((Replace (z,i,x)) - z) . j )
assume A9:
( 1
<= j &
j <= len ((Replace (z,i,x)) - z) )
;
(Replace ((0* m),i,xy)) . j = ((Replace (z,i,x)) - z) . j
reconsider j =
j as
Nat ;
A10:
j in dom ((Replace (z,i,x)) - z)
by A9, FINSEQ_3:25;
(- z) . j = (- 1) * (z . j)
by RVSUM_1:44;
then
((Replace (z,i,x)) - z) . j = ((Replace (z,i,x)) . j) + (- (z . j))
by A10, VALUED_1:def 1;
then A11:
((Replace (z,i,x)) - z) . j = ((Replace (z,i,x)) . j) - (z . j)
;
A12:
( 1
<= i &
i <= len z implies
(Replace (z,i,x)) . i = x )
A13:
dom ((Replace ((0* m),i,x)) + (Replace ((0* m),i,my))) = (dom (Replace ((0* m),i,x))) /\ (dom (Replace ((0* m),i,my)))
by VALUED_1:def 1;
(
j in dom (Replace ((0* m),i,x)) &
j in dom (Replace ((0* m),i,my)) )
by A3, A9, A8, FINSEQ_3:25;
then
j in dom ((Replace ((0* m),i,x)) + (Replace ((0* m),i,my)))
by A13, XBOOLE_0:def 4;
then A14:
((Replace ((0* m),i,x)) + (Replace ((0* m),i,my))) . j = ((Replace ((0* m),i,x)) . j) + ((Replace ((0* m),i,my)) . j)
by VALUED_1:def 1;
per cases
( i = j or not i = j )
;
suppose A15:
i = j
;
(Replace ((0* m),i,xy)) . j = ((Replace (z,i,x)) - z) . jreconsider xmy =
x + my as
Real ;
(Replace ((0* m),i,xy)) . j =
(Replace ((0* m),i,xmy)) . j
.=
((Replace ((0* m),i,x)) + (Replace ((0* m),i,my))) . j
by A1, Th9
.=
x + ((Replace ((0* m),i,my)) . j)
by A1, A14, A15, Lm7
.=
x + (- y)
by A1, A15, Lm7
.=
x - ((proj (i,m)) . z)
by A2
;
hence
(Replace ((0* m),i,xy)) . j = ((Replace (z,i,x)) - z) . j
by A11, A9, A4, A5, A6, A12, A15, FINSEQ_3:29, PDIFF_1:def 1;
verum end; suppose A16:
not
i = j
;
(Replace ((0* m),i,xy)) . j = ((Replace (z,i,x)) - z) . jthen
(Replace ((0* m),i,xy)) . j = (z . j) - (z . j)
by A3, A9, A8, Lm7;
hence
(Replace ((0* m),i,xy)) . j = ((Replace (z,i,x)) - z) . j
by A11, A16, FUNCT_7:32;
verum end;
end;
hence A17:
(Replace (z,i,x)) - z = (0* m) +* (i,(x - y))
by A8; z - (Replace (z,i,x)) = (0* m) +* (i,(y - x))
reconsider a = - 1 as Element of REAL by XREAL_0:def 1;
reconsider axy = a * xy as Element of REAL ;
z - (Replace (z,i,x)) = - (Replace ((0* m),i,xy))
by A17, RVSUM_1:35;
then
z - (Replace (z,i,x)) = Replace ((0* m),i,axy)
by A1, Th10;
hence
z - (Replace (z,i,x)) = (0* m) +* (i,(y - x))
; verum