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, Th35;
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, Th31
.= ((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, Th30
.= (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, Th34
.= ((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, Th34
.= ((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, Th30
.= (((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, Th30 ;
then q,p,p # q,v9 # u are_Ort_wrt w,y by A1, A7, Th33;
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:61;
1 * (v9 - u) = (u + (A * (p - q))) - u by A5, RLVECT_1:def 8
.= A * (p - q) by RLSUB_2:61 ;
then ( q,p // u,v9 or q,p // v9,u ) by ANALMETR:14;
then A10: ( p,q // u,v9 or p,q // v9,u ) by ANALOAF:12;
A11: PProJ (w,y,(A * (p - q)),(A * (p - q))) = A * (PProJ (w,y,(p - q),(A * (p - q)))) by A1, Th31
.= 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, Th31
.= 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, Th30
.= (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, Th34
.= ((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, Th34
.= ((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, Th30
.= (((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, Th30 ;
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, Th31
.= (((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, Th31
.= 0 ;
then u,v9,p # q,v9 # u are_Ort_wrt w,y by A1, Th33;
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, Th33;
then ( p,q,u,v9 are_DTr_wrt w,y or p,q,v9,u are_DTr_wrt w,y ) by A10;
hence v = v9 by A1, A2, A3, Th25; :: thesis: verum