let V be RealLinearSpace; :: thesis: for w, y being VECTOR of st Gen w,y holds
for p, q, u, v, v' being VECTOR of
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)) " ) & v' = u + (A * (p - q)) holds
v = v'
let w, y be VECTOR of ; :: thesis: ( Gen w,y implies for p, q, u, v, v' being VECTOR of
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)) " ) & v' = u + (A * (p - q)) holds
v = v' )
assume A1: Gen w,y ; :: thesis: for p, q, u, v, v' being VECTOR of
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)) " ) & v' = u + (A * (p - q)) holds
v = v'
let p, q, u, v, v' be VECTOR of ; :: 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)) " ) & v' = u + (A * (p - q)) holds
v = v'
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)) " ) & v' = u + (A * (p - q)) implies v = v' )
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: v' = u + (A * (p - q)) ; :: thesis: v = v'
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),((v' # u) - (p # q));
2 * (PProJ w,y,(p - q),((v' # u) - (p # q))) = 2 * ((PProJ w,y,(p - q),(v' # u)) - (PProJ w,y,(p - q),(p # q))) by A1, Th32
.= (2 * (PProJ w,y,(p - q),(v' # u))) - (2 * (PProJ w,y,(p - q),(p # q)))
.= ((PProJ w,y,(p - q),v') + (PProJ w,y,(p - q),u)) - (2 * (PProJ w,y,(p - q),(p # q))) by A1, Th36
.= ((PProJ w,y,(p - q),v') + (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,v' # u are_Ort_wrt w,y by A1, A7, Th35;
then p # q,v' # u,q,p are_Ort_wrt w,y by Lm5;
then A8: p # q,v' # u,p,q are_Ort_wrt w,y by Lm4;
set Y = PProJ w,y,(v' - u),((v' # u) - (p # q));
A9: v' - u = A * (p - q) by A5, RLSUB_2:78;
1 * (v' - u) = (u + (A * (p - q))) - u by A5, RLVECT_1:def 9
.= A * (p - q) by RLSUB_2:78 ;
then ( q,p // u,v' or q,p // v',u ) by ANALMETR:18;
then A10: ( p,q // u,v' or p,q // v',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,(v' - u),((v' # u) - (p # q))) = 2 * ((PProJ w,y,(v' - u),(v' # u)) - (PProJ w,y,(v' - u),(p # q))) by A1, Th32
.= (2 * (PProJ w,y,(v' - u),(v' # u))) - (2 * (PProJ w,y,(v' - u),(p # q)))
.= ((PProJ w,y,(v' - u),v') + (PProJ w,y,(v' - u),u)) - (2 * (PProJ w,y,(v' - u),(p # q))) by A1, Th36
.= ((PProJ w,y,(v' - u),v') + (PProJ w,y,(v' - u),u)) - ((PProJ w,y,(v' - u),p) + (PProJ w,y,(v' - u),q)) by A1, Th36
.= ((PProJ w,y,(v' - u),(u + (A * (p - q)))) + (PProJ w,y,(v' - u),u)) - (PProJ w,y,(v' - u),(p + q)) by A1, A5, Th32
.= (((PProJ w,y,(v' - u),u) + (PProJ w,y,(v' - u),(A * (p - q)))) + (PProJ w,y,(v' - u),u)) - (PProJ w,y,(v' - u),(p + q)) by A1, Th32 ;
then A12: 2 * (PProJ w,y,(v' - u),((v' # 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,v',p # q,v' # u are_Ort_wrt w,y by A1, Th35;
then p # q,v' # u,u,v' are_Ort_wrt w,y by Lm5;
then p # q,v' # u,v',u are_Ort_wrt w,y by Lm4;
then ( p,q,p # q,u # v' are_Ort_wrt w,y & u,v',p # q,u # v' are_Ort_wrt w,y & p,q,p # q,v' # u are_Ort_wrt w,y & v',u,p # q,v' # u are_Ort_wrt w,y ) by A1, A8, A12, Lm5, Th35;
then ( p,q,u,v' are_DTr_wrt w,y or p,q,v',u are_DTr_wrt w,y ) by A10, Def3;
hence v = v' by A1, A2, A3, Th27; :: thesis: verum