let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for u, u', u1, u2, t1, t2 being VECTOR of V
for A1, A2 being Real st u <> u' & A1 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) & A2 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) * ((PProJ w,y,(u - u'),(u - u')) " ) & t1 = u1 + (A1 * (u - u')) & t2 = u2 + (A2 * (u - u')) holds
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u')) & A2 - A1 = ((- 2) * (PProJ w,y,(u - u'),(u2 - u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) )
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, u', u1, u2, t1, t2 being VECTOR of V
for A1, A2 being Real st u <> u' & A1 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) & A2 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) * ((PProJ w,y,(u - u'),(u - u')) " ) & t1 = u1 + (A1 * (u - u')) & t2 = u2 + (A2 * (u - u')) holds
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u')) & A2 - A1 = ((- 2) * (PProJ w,y,(u - u'),(u2 - u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) ) )
assume A1:
Gen w,y
; :: thesis: for u, u', u1, u2, t1, t2 being VECTOR of V
for A1, A2 being Real st u <> u' & A1 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) & A2 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) * ((PProJ w,y,(u - u'),(u - u')) " ) & t1 = u1 + (A1 * (u - u')) & t2 = u2 + (A2 * (u - u')) holds
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u')) & A2 - A1 = ((- 2) * (PProJ w,y,(u - u'),(u2 - u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) )
let u, u', u1, u2, t1, t2 be VECTOR of V; :: thesis: for A1, A2 being Real st u <> u' & A1 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) & A2 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) * ((PProJ w,y,(u - u'),(u - u')) " ) & t1 = u1 + (A1 * (u - u')) & t2 = u2 + (A2 * (u - u')) holds
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u')) & A2 - A1 = ((- 2) * (PProJ w,y,(u - u'),(u2 - u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) )
let A1, A2 be Real; :: thesis: ( u <> u' & A1 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) & A2 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) * ((PProJ w,y,(u - u'),(u - u')) " ) & t1 = u1 + (A1 * (u - u')) & t2 = u2 + (A2 * (u - u')) implies ( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u')) & A2 - A1 = ((- 2) * (PProJ w,y,(u - u'),(u2 - u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) ) )
assume that
u <> u'
and
A2:
A1 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) * ((PProJ w,y,(u - u'),(u - u')) " )
and
A3:
A2 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) * ((PProJ w,y,(u - u'),(u - u')) " )
and
A4:
( t1 = u1 + (A1 * (u - u')) & t2 = u2 + (A2 * (u - u')) )
; :: thesis: ( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u')) & A2 - A1 = ((- 2) * (PProJ w,y,(u - u'),(u2 - u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) )
thus
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u')) & A2 - A1 = ((- 2) * (PProJ w,y,(u - u'),(u2 - u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) )
:: thesis: verumproof
set uu =
((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) - ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1)));
((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) - ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) = (- 2) * (PProJ w,y,(u - u'),(u2 - u1))
proof
A5:
((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) - ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) =
((PProJ w,y,(u - u'),(u + u')) - (PProJ w,y,(u - u'),(2 * u2))) - ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1)))
by A1, Th33
.=
((PProJ w,y,(u - u'),(u + u')) - (PProJ w,y,(u - u'),(2 * u2))) - ((PProJ w,y,(u - u'),(u + u')) - (PProJ w,y,(u - u'),(2 * u1)))
by A1, Th33
.=
(PProJ w,y,(u - u'),(2 * u1)) - (PProJ w,y,(u - u'),(2 * u2))
.=
PProJ w,
y,
(u - u'),
((2 * u1) - (2 * u2))
by A1, Th32
;
(2 * u1) - (2 * u2) =
- ((2 * u2) - (2 * u1))
by RLVECT_1:47
.=
- (2 * (u2 - u1))
by RLVECT_1:48
.=
2
* (- (u2 - u1))
by RLVECT_1:39
.=
(- 2) * (u2 - u1)
by RLVECT_1:38
;
hence
((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) - ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) = (- 2) * (PProJ w,y,(u - u'),(u2 - u1))
by A1, A5, Th33;
:: thesis: verum
end;
hence
(
t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u')) &
A2 - A1 = ((- 2) * (PProJ w,y,(u - u'),(u2 - u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) )
by A2, A3, A4, Lm19, XCMPLX_1:40;
:: thesis: verum
end;