let V be RealLinearSpace; :: thesis: for x, y being VECTOR of V st Gen x,y holds
ex u, v, w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
let x, y be VECTOR of V; :: thesis: ( Gen x,y implies ex u, v, w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) ) )
assume A1: Gen x,y ; :: thesis: ex u, v, w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
take u = (0 * x) + (0 * y); :: thesis: ex v, w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
take v = (1 * x) + (1 * y); :: thesis: ex w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
take w = (1 * x) + ((- 1) * y); :: thesis: ( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
A2: pr1 (x,y,u) = 0 by A1, Lm6;
A3: pr2 (x,y,u) = 0 by A1, Lm6;
A4: pr1 (x,y,v) = 1 by A1, Lm6;
pr2 (x,y,v) = 1 by A1, Lm6;
then A5: Ortm (x,y,u), Ortm (x,y,v) // u,w by A2, A3, A4, ANALOAF:8;
for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
proof
let v1, w1 be VECTOR of V; :: thesis: ( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
assume v1,w1,u,v are_COrtm_wrt x,y ; :: thesis: ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
then A6: Ortm (x,y,v1), Ortm (x,y,w1) // u,v ;
now :: thesis: ( v1 <> w1 & ( v1,w1,u,w are_COrtm_wrt x,y or v1,w1,w,u are_COrtm_wrt x,y ) implies ex a, b being Real st
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) )
assume A7: v1 <> w1 ; :: thesis: ( ( v1,w1,u,w are_COrtm_wrt x,y or v1,w1,w,u are_COrtm_wrt x,y ) implies ex a, b being Real st
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) )
assume ( v1,w1,u,w are_COrtm_wrt x,y or v1,w1,w,u are_COrtm_wrt x,y ) ; :: thesis: ex a, b being Real st
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
then ( Ortm (x,y,v1), Ortm (x,y,w1) // u,w or Ortm (x,y,v1), Ortm (x,y,w1) // w,u ) ;
then ( u,v // u,w or u,v // w,u ) by A1, A6, A7, Th6, ANALOAF:11;
then consider a, b being Real such that
A8: a * (v - u) = b * (w - u) and
A9: ( a <> 0 or b <> 0 ) by ANALMETR:14;
take a = a; :: thesis: ex b being Real st
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
take b = b; :: thesis: ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
u = (0. V) + (0 * y) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
then a * v = b * (w - (0. V)) by A8, RLVECT_1:13;
then A10: a * v = b * w by RLVECT_1:13;
A11: now :: thesis: ( not a <> 0 or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
assume A12: a <> 0 ; :: thesis: ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
((a ") * a) * v = (a ") * (b * w) by A10, RLVECT_1:def 7;
then ((a ") * a) * v = ((a ") * b) * w by RLVECT_1:def 7;
then 1 * v = ((a ") * b) * w by A12, XCMPLX_0:def 7;
then 1 * v = ((((a ") * b) * 1) * x) + ((((a ") * b) * (- 1)) * y) by Lm2;
then A13: ((1 * 1) * x) + ((1 * 1) * y) = ((((a ") * b) * 1) * x) + ((((a ") * b) * (- 1)) * y) by Lm2;
then a * 1 = a * ((a ") * (b * 1)) by A1, Lm3;
then A14: a * 1 = (a * (a ")) * (b * 1) ;
1 = ((a ") * b) * (- 1) by A1, A13, Lm3;
then 1 = ((a ") * a) * (- 1) by A12, A14, XCMPLX_0:def 7;
hence ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) by A12, XCMPLX_0:def 7; :: thesis: verum
end;
now :: thesis: ( not b <> 0 or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
assume A15: b <> 0 ; :: thesis: ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
((b ") * a) * v = (b ") * (b * w) by A10, RLVECT_1:def 7;
then ((b ") * a) * v = ((b ") * b) * w by RLVECT_1:def 7;
then ((b ") * a) * v = 1 * w by A15, XCMPLX_0:def 7;
then ((((b ") * a) * 1) * x) + ((((b ") * a) * 1) * y) = 1 * w by Lm2;
then A16: ((((b ") * a) * 1) * x) + ((((b ") * a) * 1) * y) = ((1 * 1) * x) + ((1 * (- 1)) * y) by Lm2;
then b * 1 = b * ((b ") * (a * 1)) by A1, Lm3;
then A17: b * 1 = (b * (b ")) * (a * 1) ;
- 1 = ((b ") * a) * 1 by A1, A16, Lm3;
then - 1 = ((b ") * b) * 1 by A15, A17, XCMPLX_0:def 7;
hence ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) by A15, XCMPLX_0:def 7; :: thesis: verum
end;
hence ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) by A9, A11; :: thesis: verum
end;
hence ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ; :: thesis: verum
end;
hence ( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) ) by A5; :: thesis: verum