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_COrte_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_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_COrte_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_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_COrte_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
( Gen x,y implies ex u, v being VECTOR of V st u <> v )
proof
assume A2: Gen x,y ; :: thesis: ex u, v being VECTOR of V st u <> v
take x ; :: thesis: ex v being VECTOR of V st x <> v
take 0. V ; :: thesis: x <> 0. V
thus x <> 0. V by A2, Lm4; :: thesis: verum
end;
then consider u, v being VECTOR of V such that
A3: u <> v by A1;
take u ; :: thesis: ex v, w being VECTOR of V st
( u,v,u,w are_COrte_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
take v ; :: thesis: ex w being VECTOR of V st
( u,v,u,w are_COrte_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
consider w being VECTOR of V such that
A4: w <> u and
A5: u,v,u,w are_COrte_wrt x,y by A1, Th40;
take w ; :: thesis: ( u,v,u,w are_COrte_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
thus u,v,u,w are_COrte_wrt x,y by A5; :: thesis: for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
A6: Orte (x,y,u), Orte (x,y,v) // u,w by A5;
let v1, w1 be VECTOR of V; :: thesis: ( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
assume v1,w1,u,v are_COrte_wrt x,y ; :: thesis: ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
then A7: Orte (x,y,v1), Orte (x,y,w1) // u,v ;
now :: thesis: ( v1 <> w1 & ( v1,w1,u,w are_COrte_wrt x,y or v1,w1,w,u are_COrte_wrt x,y ) implies ex a, b being Real st
( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) )
assume A8: v1 <> w1 ; :: thesis: ( ( v1,w1,u,w are_COrte_wrt x,y or v1,w1,w,u are_COrte_wrt x,y ) implies ex a, b being Real st
( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) )
assume ( v1,w1,u,w are_COrte_wrt x,y or v1,w1,w,u are_COrte_wrt x,y ) ; :: thesis: ex a, b being Real st
( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
then ( Orte (x,y,v1), Orte (x,y,w1) // u,w or Orte (x,y,v1), Orte (x,y,w1) // w,u ) ;
then ( u,v // u,w or u,v // w,u ) by A1, A7, A8, Th13, ANALOAF:11;
then ( Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u), Orte (x,y,w) or Orte (x,y,u), Orte (x,y,v) // Orte (x,y,w), Orte (x,y,u) ) by A1, Th16;
then ( u,w // Orte (x,y,u), Orte (x,y,w) or u,w // Orte (x,y,w), Orte (x,y,u) ) by A1, A3, A6, Th13, ANALOAF:11;
then consider a, b being Real such that
A9: a * (w - u) = b * ((Orte (x,y,w)) - (Orte (x,y,u))) and
A10: ( a <> 0 or b <> 0 ) by ANALMETR:14;
take a = a; :: thesis: ex b being Real st
( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
take b = b; :: thesis: ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
a * (w - u) = b * (Orte (x,y,(w - u))) by A1, A9, Th11;
then A11: a * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = b * (Orte (x,y,(w - u))) by A1, Lm5;
A12: now :: thesis: ( not a <> 0 or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
assume A13: a <> 0 ; :: thesis: ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
A14: pr2 (x,y,(w - u)) <> 0
proof
assume A15: not pr2 (x,y,(w - u)) <> 0 ; :: thesis: contradiction
then a * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = ((b * 0) * x) + ((b * (- (pr1 (x,y,(w - u))))) * y) by A11, Lm2;
then ((a * (pr1 (x,y,(w - u)))) * x) + ((a * (pr2 (x,y,(w - u)))) * y) = ((b * 0) * x) + ((b * (- (pr1 (x,y,(w - u))))) * y) by Lm2;
then a * (pr1 (x,y,(w - u))) = 0 by A1, Lm3;
then pr1 (x,y,(w - u)) = 0 by A13, XCMPLX_1:6;
then w - u = (0 * x) + (0 * y) by A1, A15, Lm5
.= (0. V) + (0 * y) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence contradiction by A4, RLVECT_1:21; :: thesis: verum
end;
((a ") * a) * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = (a ") * (b * (((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y))) by A11, RLVECT_1:def 7;
then ((a ") * a) * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = ((a ") * b) * (((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y)) by RLVECT_1:def 7;
then 1 * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = ((a ") * b) * (((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y)) by A13, XCMPLX_0:def 7;
then ((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y) = ((a ") * b) * (((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y)) by RLVECT_1:def 8;
then A16: ((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y) = ((((a ") * b) * (pr2 (x,y,(w - u)))) * x) + ((((a ") * b) * (- (pr1 (x,y,(w - u))))) * y) by Lm2;
then pr1 (x,y,(w - u)) = ((a ") * b) * (pr2 (x,y,(w - u))) by A1, Lm3;
then A17: pr2 (x,y,(w - u)) = - (((a ") * b) * (((a ") * b) * (pr2 (x,y,(w - u))))) by A1, A16, Lm3;
- (((pr2 (x,y,(w - u))) ") * (pr2 (x,y,(w - u)))) = ((pr2 (x,y,(w - u))) ") * (- (pr2 (x,y,(w - u))))
.= ((pr2 (x,y,(w - u))) ") * (((a ") * b) * (((a ") * b) * (pr2 (x,y,(w - u))))) by A17 ;
then - 1 = (((pr2 (x,y,(w - u))) ") * (pr2 (x,y,(w - u)))) * (((a ") * b) * ((a ") * b)) by A14, XCMPLX_0:def 7;
then - 1 = 1 * (((a ") * b) * ((a ") * b)) by A14, XCMPLX_0:def 7;
hence ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) by XREAL_1:63; :: thesis: verum
end;
now :: thesis: ( not b <> 0 or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
assume A18: b <> 0 ; :: thesis: ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
A19: pr2 (x,y,(w - u)) <> 0
proof
assume A20: not pr2 (x,y,(w - u)) <> 0 ; :: thesis: contradiction
then a * (((pr1 (x,y,(w - u))) * x) + (0 * y)) = ((b * 0) * x) + ((b * (- (pr1 (x,y,(w - u))))) * y) by A11, Lm2;
then ((a * (pr1 (x,y,(w - u)))) * x) + ((a * 0) * y) = ((b * 0) * x) + ((b * (- (pr1 (x,y,(w - u))))) * y) by Lm2;
then b * (- (pr1 (x,y,(w - u)))) = 0 by A1, Lm3;
then - (pr1 (x,y,(w - u))) = 0 by A18, XCMPLX_1:6;
then w - u = (0 * x) + ((- 0) * y) by A1, A20, Lm5
.= (0. V) + (0 * y) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence contradiction by A4, RLVECT_1:21; :: thesis: verum
end;
(b ") * (a * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y))) = ((b ") * b) * (((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y)) by A11, RLVECT_1:def 7;
then ((b ") * a) * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = ((b ") * b) * (((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y)) by RLVECT_1:def 7;
then ((b ") * a) * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = 1 * (((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y)) by A18, XCMPLX_0:def 7;
then ((b ") * a) * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = ((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y) by RLVECT_1:def 8;
then A21: ((((b ") * a) * (pr1 (x,y,(w - u)))) * x) + ((((b ") * a) * (pr2 (x,y,(w - u)))) * y) = ((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y) by Lm2;
then ((b ") * a) * (pr2 (x,y,(w - u))) = - (pr1 (x,y,(w - u))) by A1, Lm3;
then A22: pr2 (x,y,(w - u)) = ((b ") * a) * (- (((b ") * a) * (pr2 (x,y,(w - u))))) by A1, A21, Lm3;
- (((pr2 (x,y,(w - u))) ") * (pr2 (x,y,(w - u)))) = ((pr2 (x,y,(w - u))) ") * (- (pr2 (x,y,(w - u))))
.= ((pr2 (x,y,(w - u))) ") * (((b ") * a) * (((b ") * a) * (pr2 (x,y,(w - u))))) by A22 ;
then - 1 = (((pr2 (x,y,(w - u))) ") * (pr2 (x,y,(w - u)))) * (((b ") * a) * ((b ") * a)) by A19, XCMPLX_0:def 7;
then - 1 = 1 * (((b ") * a) * ((b ") * a)) by A19, XCMPLX_0:def 7;
hence ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) by XREAL_1:63; :: thesis: verum
end;
hence ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) by A10, A12; :: thesis: verum
end;
hence ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ; :: thesis: verum