let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for p, q, u, v, v9 being VECTOR of V
for A being Real st p,q,u,v are_DTr_wrt w,y & p <> q & A = ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " ) & v9 = u + (A * (p - q)) holds
v = v9
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for p, q, u, v, v9 being VECTOR of V
for A being Real st p,q,u,v are_DTr_wrt w,y & p <> q & A = ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " ) & v9 = u + (A * (p - q)) holds
v = v9 )
assume A1: Gen w,y ; :: thesis: for p, q, u, v, v9 being VECTOR of V
for A being Real st p,q,u,v are_DTr_wrt w,y & p <> q & A = ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " ) & v9 = u + (A * (p - q)) holds
v = v9
let p, q, u, v, v9 be VECTOR of V; :: thesis: for A being Real st p,q,u,v are_DTr_wrt w,y & p <> q & A = ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " ) & v9 = u + (A * (p - q)) holds
v = v9
let A be Real; :: thesis: ( p,q,u,v are_DTr_wrt w,y & p <> q & A = ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " ) & v9 = u + (A * (p - q)) implies v = v9 )
assume that
A2: p,q,u,v are_DTr_wrt w,y and
A3: p <> q and
A4: A = ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " ) and
A5: v9 = u + (A * (p - q)) ; :: thesis: v = v9
A6: PProJ w,y,(p - q),(p - q) <> 0 by A1, A3, Th37;
A7: PProJ w,y,(p - q),(A * (p - q)) = (((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " )) * (PProJ w,y,(p - q),(p - q)) by A1, A4, Th33
.= ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * (((PProJ w,y,(p - q),(p - q)) " ) * (PProJ w,y,(p - q),(p - q)))
.= ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * 1 by A6, XCMPLX_0:def 7
.= (PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u)) ;
set s = p # q;
set X = PProJ w,y,(p - q),((v9 # u) - (p # q));
2 * (PProJ w,y,(p - q),((v9 # u) - (p # q))) = 2 * ((PProJ w,y,(p - q),(v9 # u)) - (PProJ w,y,(p - q),(p # q))) by A1, Th32
.= (2 * (PProJ w,y,(p - q),(v9 # u))) - (2 * (PProJ w,y,(p - q),(p # q)))
.= ((PProJ w,y,(p - q),v9) + (PProJ w,y,(p - q),u)) - (2 * (PProJ w,y,(p - q),(p # q))) by A1, Th36
.= ((PProJ w,y,(p - q),v9) + (PProJ w,y,(p - q),u)) - ((PProJ w,y,(p - q),p) + (PProJ w,y,(p - q),q)) by A1, Th36
.= ((PProJ w,y,(p - q),(u + (A * (p - q)))) + (PProJ w,y,(p - q),u)) - (PProJ w,y,(p - q),(p + q)) by A1, A5, Th32
.= (((PProJ w,y,(p - q),u) + (PProJ w,y,(p - q),(A * (p - q)))) + (PProJ w,y,(p - q),u)) - (PProJ w,y,(p - q),(p + q)) by A1, Th32 ;
then q,p,p # q,v9 # u are_Ort_wrt w,y by A1, A7, Th35;
then p # q,v9 # u,q,p are_Ort_wrt w,y by Lm5;
then A8: p # q,v9 # u,p,q are_Ort_wrt w,y by Lm4;
set Y = PProJ w,y,(v9 - u),((v9 # u) - (p # q));
A9: v9 - u = A * (p - q) by A5, RLSUB_2:78;
1 * (v9 - u) = (u + (A * (p - q))) - u by A5, RLVECT_1:def 9
.= A * (p - q) by RLSUB_2:78 ;
then ( q,p // u,v9 or q,p // v9,u ) by ANALMETR:18;
then A10: ( p,q // u,v9 or p,q // v9,u ) by ANALOAF:21;
A11: PProJ w,y,(A * (p - q)),(A * (p - q)) = A * (PProJ w,y,(p - q),(A * (p - q))) by A1, Th33
.= A * ((((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " )) * (PProJ w,y,(p - q),(p - q))) by A1, A4, Th33
.= A * (((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * (((PProJ w,y,(p - q),(p - q)) " ) * (PProJ w,y,(p - q),(p - q))))
.= A * (((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * 1) by A6, XCMPLX_0:def 7
.= A * ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) ;
2 * (PProJ w,y,(v9 - u),((v9 # u) - (p # q))) = 2 * ((PProJ w,y,(v9 - u),(v9 # u)) - (PProJ w,y,(v9 - u),(p # q))) by A1, Th32
.= (2 * (PProJ w,y,(v9 - u),(v9 # u))) - (2 * (PProJ w,y,(v9 - u),(p # q)))
.= ((PProJ w,y,(v9 - u),v9) + (PProJ w,y,(v9 - u),u)) - (2 * (PProJ w,y,(v9 - u),(p # q))) by A1, Th36
.= ((PProJ w,y,(v9 - u),v9) + (PProJ w,y,(v9 - u),u)) - ((PProJ w,y,(v9 - u),p) + (PProJ w,y,(v9 - u),q)) by A1, Th36
.= ((PProJ w,y,(v9 - u),(u + (A * (p - q)))) + (PProJ w,y,(v9 - u),u)) - (PProJ w,y,(v9 - u),(p + q)) by A1, A5, Th32
.= (((PProJ w,y,(v9 - u),u) + (PProJ w,y,(v9 - u),(A * (p - q)))) + (PProJ w,y,(v9 - u),u)) - (PProJ w,y,(v9 - u),(p + q)) by A1, Th32 ;
then A12: 2 * (PProJ w,y,(v9 - u),((v9 # u) - (p # q))) = (((PProJ w,y,(A * (p - q)),u) + ((A * (PProJ w,y,(p - q),(p + q))) - (A * (2 * (PProJ w,y,(p - q),u))))) + (PProJ w,y,(A * (p - q)),u)) - (PProJ w,y,(A * (p - q)),(p + q)) by A9, A11
.= (((PProJ w,y,(A * (p - q)),u) + ((PProJ w,y,(A * (p - q)),(p + q)) - (2 * (A * (PProJ w,y,(p - q),u))))) + (PProJ w,y,(A * (p - q)),u)) - (PProJ w,y,(A * (p - q)),(p + q)) by A1, Th33
.= (((PProJ w,y,(A * (p - q)),u) + ((PProJ w,y,(A * (p - q)),(p + q)) - (2 * (PProJ w,y,(A * (p - q)),u)))) + (PProJ w,y,(A * (p - q)),u)) - (PProJ w,y,(A * (p - q)),(p + q)) by A1, Th33
.= 0 ;
then u,v9,p # q,v9 # u are_Ort_wrt w,y by A1, Th35;
then p # q,v9 # u,u,v9 are_Ort_wrt w,y by Lm5;
then p # q,v9 # u,v9,u are_Ort_wrt w,y by Lm4;
then ( p,q,p # q,u # v9 are_Ort_wrt w,y & u,v9,p # q,u # v9 are_Ort_wrt w,y & p,q,p # q,v9 # u are_Ort_wrt w,y & v9,u,p # q,v9 # u are_Ort_wrt w,y ) by A1, A8, A12, Lm5, Th35;
then ( p,q,u,v9 are_DTr_wrt w,y or p,q,v9,u are_DTr_wrt w,y ) by A10, Def3;
hence v = v9 by A1, A2, A3, Th27; :: thesis: verum