let V be RealLinearSpace; for w, y being VECTOR of V st Gen w,y holds
for u, u9, u1, u2, t1, t2 being VECTOR of V
for A1, A2 being Real st A1 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & A2 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & t1 = u1 + (A1 * (u - u9)) & t2 = u2 + (A2 * (u - u9)) holds
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") )
let w, y be VECTOR of V; ( Gen w,y implies for u, u9, u1, u2, t1, t2 being VECTOR of V
for A1, A2 being Real st A1 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & A2 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & t1 = u1 + (A1 * (u - u9)) & t2 = u2 + (A2 * (u - u9)) holds
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") ) )
assume A1:
Gen w,y
; for u, u9, u1, u2, t1, t2 being VECTOR of V
for A1, A2 being Real st A1 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & A2 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & t1 = u1 + (A1 * (u - u9)) & t2 = u2 + (A2 * (u - u9)) holds
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") )
let u, u9, u1, u2, t1, t2 be VECTOR of V; for A1, A2 being Real st A1 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & A2 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & t1 = u1 + (A1 * (u - u9)) & t2 = u2 + (A2 * (u - u9)) holds
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") )
let A1, A2 be Real; ( A1 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & A2 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & t1 = u1 + (A1 * (u - u9)) & t2 = u2 + (A2 * (u - u9)) implies ( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") ) )
assume A2:
( A1 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & A2 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & t1 = u1 + (A1 * (u - u9)) & t2 = u2 + (A2 * (u - u9)) )
; ( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") )
thus
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") )
verumproof
set uu =
((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) - ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1))));
A3:
(2 * u1) - (2 * u2) =
- ((2 * u2) - (2 * u1))
by RLVECT_1:33
.=
- (2 * (u2 - u1))
by RLVECT_1:34
.=
2
* (- (u2 - u1))
by RLVECT_1:25
.=
(- 2) * (u2 - u1)
by RLVECT_1:24
;
((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) - ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) =
((PProJ (w,y,(u - u9),(u + u9))) - (PProJ (w,y,(u - u9),(2 * u2)))) - ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1))))
by A1, Th31
.=
((PProJ (w,y,(u - u9),(u + u9))) - (PProJ (w,y,(u - u9),(2 * u2)))) - ((PProJ (w,y,(u - u9),(u + u9))) - (PProJ (w,y,(u - u9),(2 * u1))))
by A1, Th31
.=
(PProJ (w,y,(u - u9),(2 * u1))) - (PProJ (w,y,(u - u9),(2 * u2)))
.=
PProJ (
w,
y,
(u - u9),
((2 * u1) - (2 * u2)))
by A1, Th30
;
then
((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) - ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) = (- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))
by A1, A3, Th31;
hence
(
t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) &
A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") )
by A2, Lm20, XCMPLX_1:40;
verum
end;