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