let V be RealLinearSpace; for w, y being VECTOR of V st Gen w,y holds
for u, u9, u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,w1 are_DTr_wrt w,y & u,u9,v2,w2 are_DTr_wrt w,y & u1,u2,v1,v2 are_Ort_wrt w,y holds
t1,t2,w1,w2 are_Ort_wrt w,y
let w, y be VECTOR of V; ( Gen w,y implies for u, u9, u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,w1 are_DTr_wrt w,y & u,u9,v2,w2 are_DTr_wrt w,y & u1,u2,v1,v2 are_Ort_wrt w,y holds
t1,t2,w1,w2 are_Ort_wrt w,y )
assume A1:
Gen w,y
; for u, u9, u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,w1 are_DTr_wrt w,y & u,u9,v2,w2 are_DTr_wrt w,y & u1,u2,v1,v2 are_Ort_wrt w,y holds
t1,t2,w1,w2 are_Ort_wrt w,y
let u, u9, u1, u2, v1, v2, t1, t2, w1, w2 be VECTOR of V; ( u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,w1 are_DTr_wrt w,y & u,u9,v2,w2 are_DTr_wrt w,y & u1,u2,v1,v2 are_Ort_wrt w,y implies t1,t2,w1,w2 are_Ort_wrt w,y )
assume that
A2:
u <> u9
and
A3:
( u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y )
and
A4:
( u,u9,v1,w1 are_DTr_wrt w,y & u,u9,v2,w2 are_DTr_wrt w,y )
and
A5:
u1,u2,v1,v2 are_Ort_wrt w,y
; t1,t2,w1,w2 are_Ort_wrt w,y
set A1 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ");
set A2 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ");
set A3 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ");
set A4 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ");
( u1 + ((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) * (u - u9)) = t1 & u2 + ((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) * (u - u9)) = t2 )
by A1, A2, A3, Th36;
then A6:
t2 - t1 = (u2 - u1) + (((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9))
by A1, Lm21;
A7:
( t1 = u1 + ((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) * (u - u9)) & t2 = u2 + ((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) * (u - u9)) )
by A1, A2, A3, Th36;
A8:
( v1 + ((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) * (u - u9)) = w1 & v2 + ((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) * (u - u9)) = w2 )
by A1, A2, A4, Th36;
then
w2 - w1 = (v2 - v1) + (((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9))
by A1, Lm21;
then A9: PProJ (w,y,(t2 - t1),(w2 - w1)) =
(PProJ (w,y,(u2 - u1),((v2 - v1) + (((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9))))) + (PProJ (w,y,(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)),((v2 - v1) + (((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)))))
by A1, A6, Th30
.=
((PProJ (w,y,(u2 - u1),(v2 - v1))) + (PProJ (w,y,(u2 - u1),(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9))))) + (PProJ (w,y,(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)),((v2 - v1) + (((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)))))
by A1, Th30
.=
(0 + (PProJ (w,y,(u2 - u1),(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9))))) + (PProJ (w,y,(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)),((v2 - v1) + (((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)))))
by A1, A5, Th33
.=
(PProJ (w,y,(u2 - u1),(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)))) + ((PProJ (w,y,(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)),(v2 - v1))) + (PProJ (w,y,(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)),(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)))))
by A1, Th30
;
set aa = ((PProJ (w,y,(u - u9),(u - u9))) ") * ((PProJ (w,y,(u - u9),(u2 - u1))) * (PProJ (w,y,(u - u9),(v2 - v1))));
A10: PProJ (w,y,(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)),(v2 - v1)) =
PProJ (w,y,(v2 - v1),(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)))
.=
(PProJ (w,y,(v2 - v1),(u - u9))) * ((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")))
by A1, Th31
.=
(PProJ (w,y,(v2 - v1),(u - u9))) * (((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))
by A1, A7, Lm21
.=
(- 2) * (((PProJ (w,y,(u - u9),(u - u9))) ") * ((PProJ (w,y,(u - u9),(u2 - u1))) * (PProJ (w,y,(u - u9),(v2 - v1)))))
;
A11:
PProJ (w,y,(u - u9),(u - u9)) <> 0
by A1, A2, Th35;
A12: PProJ (w,y,(u2 - u1),(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9))) =
(PProJ (w,y,(u2 - u1),(u - u9))) * ((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")))
by A1, Th31
.=
(PProJ (w,y,(u2 - u1),(u - u9))) * (((- 2) * (PProJ (w,y,(u - u9),(v2 - v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))
by A1, A8, Lm21
.=
(- 2) * (((PProJ (w,y,(u - u9),(u - u9))) ") * ((PProJ (w,y,(u - u9),(u2 - u1))) * (PProJ (w,y,(u - u9),(v2 - v1)))))
;
PProJ (w,y,(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)),(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9))) =
((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((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),(((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9))))
by A1, Th31
.=
((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((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),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (PProJ (w,y,(u - u9),(u - u9))))
by A1, Th31
.=
((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * ((((- 2) * (PProJ (w,y,(u - u9),(v2 - v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) * (PProJ (w,y,(u - u9),(u - u9))))
by A1, A8, Lm21
.=
((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (((- 2) * (PProJ (w,y,(u - u9),(v2 - v1)))) * (((PProJ (w,y,(u - u9),(u - u9))) ") * (PProJ (w,y,(u - u9),(u - u9)))))
.=
((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (((- 2) * (PProJ (w,y,(u - u9),(v2 - v1)))) * 1)
by A11, XCMPLX_0:def 7
.=
((- 2) * ((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((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),(v2 - v1)))
.=
((- 2) * (((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (PProJ (w,y,(u - u9),(v2 - v1)))
by A1, A7, Lm21
.=
4 * (((PProJ (w,y,(u - u9),(u - u9))) ") * ((PProJ (w,y,(u - u9),(u2 - u1))) * (PProJ (w,y,(u - u9),(v2 - v1)))))
;
hence
t1,t2,w1,w2 are_Ort_wrt w,y
by A1, A9, A12, A10, Th33; verum