let V be RealLinearSpace; :: thesis: ( ex p, q being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * p) + (b * q) = w implies for u, v, w, y being VECTOR of V st not u,v // w,y & not u,v // y,w holds
ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) )
given p, q being VECTOR of V such that A1: for w being VECTOR of V ex a, b being Real st (a * p) + (b * q) = w ; :: thesis: for u, v, w, y being VECTOR of V st not u,v // w,y & not u,v // y,w holds
ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) )
let u, v, w, y be VECTOR of V; :: thesis: ( not u,v // w,y & not u,v // y,w implies ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) )
assume that
A2: not u,v // w,y and
A3: not u,v // y,w ; :: thesis: ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) )
consider r1, s1 being Real such that
A4: (r1 * p) + (s1 * q) = v - u by A1;
consider r2, s2 being Real such that
A5: (r2 * p) + (s2 * q) = y - w by A1;
set r = (r1 * s2) - (r2 * s1);
A6: now :: thesis: not (r1 * s2) - (r2 * s1) = 0
assume A7: (r1 * s2) - (r2 * s1) = 0 ; :: thesis: contradiction
A8: now :: thesis: ( r1 <> 0 implies not r2 = 0 )
assume that
A9: r1 <> 0 and
A10: r2 = 0 ; :: thesis: contradiction
s2 <> 0
proof
assume s2 = 0 ; :: thesis: contradiction
then y - w = (0. V) + (0 * q) by A5, A10, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
then y = w by RLVECT_1:21;
hence contradiction by A2; :: thesis: verum
end;
hence contradiction by A7, A9, A10, XCMPLX_1:6; :: thesis: verum
end;
A11: now :: thesis: not r1 = 0
assume A12: r1 = 0 ; :: thesis: contradiction
A13: s1 <> 0
proof
assume s1 = 0 ; :: thesis: contradiction
then v - u = (0. V) + (0 * q) by A4, A12, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
then u = v by RLVECT_1:21;
hence contradiction by A2; :: thesis: verum
end;
then A14: r2 = 0 by A7, A12, XCMPLX_1:6;
A15: s2 <> 0
proof
assume s2 = 0 ; :: thesis: contradiction
then y - w = (0. V) + (0 * q) by A5, A14, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
then y = w by RLVECT_1:21;
hence contradiction by A2; :: thesis: verum
end;
y - w = (0. V) + (s2 * q) by A5, A14, RLVECT_1:10
.= s2 * q by RLVECT_1:4 ;
then A16: (s2 ") * (y - w) = ((s2 ") * s2) * q by RLVECT_1:def 7
.= 1 * q by A15, XCMPLX_0:def 7
.= q by RLVECT_1:def 8 ;
v - u = (0. V) + (s1 * q) by A4, A12, RLVECT_1:10
.= s1 * q by RLVECT_1:4 ;
then A17: (s1 ") * (v - u) = ((s1 ") * s1) * q by RLVECT_1:def 7
.= 1 * q by A13, XCMPLX_0:def 7
.= q by RLVECT_1:def 8 ;
s1 " <> 0 by A13, XCMPLX_1:202;
hence contradiction by A2, A3, A17, A16, Lm1; :: thesis: verum
end;
A18: now :: thesis: ( r1 <> 0 & r2 <> 0 implies not s1 = 0 )
assume that
A19: r1 <> 0 and
A20: r2 <> 0 and
A21: s1 = 0 ; :: thesis: contradiction
v - u = (r1 * p) + (0. V) by A4, A21, RLVECT_1:10
.= r1 * p by RLVECT_1:4 ;
then A22: (r1 ") * (v - u) = ((r1 ") * r1) * p by RLVECT_1:def 7
.= 1 * p by A19, XCMPLX_0:def 7
.= p by RLVECT_1:def 8 ;
s2 = 0 by A7, A19, A21, XCMPLX_1:6;
then y - w = (r2 * p) + (0. V) by A5, RLVECT_1:10
.= r2 * p by RLVECT_1:4 ;
then A23: (r2 ") * (y - w) = ((r2 ") * r2) * p by RLVECT_1:def 7
.= 1 * p by A20, XCMPLX_0:def 7
.= p by RLVECT_1:def 8 ;
r1 " <> 0 by A19, XCMPLX_1:202;
hence contradiction by A2, A3, A22, A23, Lm1; :: thesis: verum
end;
now :: thesis: ( r1 <> 0 & r2 <> 0 & s1 <> 0 implies not s2 <> 0 )
assume that
A24: r1 <> 0 and
r2 <> 0 and
s1 <> 0 and
s2 <> 0 ; :: thesis: contradiction
r2 * (v - u) = (r2 * (r1 * p)) + (r2 * (s1 * q)) by A4, RLVECT_1:def 5
.= ((r2 * r1) * p) + (r2 * (s1 * q)) by RLVECT_1:def 7
.= ((r1 * r2) * p) + ((r1 * s2) * q) by A7, RLVECT_1:def 7
.= (r1 * (r2 * p)) + ((r1 * s2) * q) by RLVECT_1:def 7
.= (r1 * (r2 * p)) + (r1 * (s2 * q)) by RLVECT_1:def 7
.= r1 * (y - w) by A5, RLVECT_1:def 5 ;
hence contradiction by A2, A3, A24, Lm1; :: thesis: verum
end;
hence contradiction by A7, A11, A8, A18, XCMPLX_1:6; :: thesis: verum
end;
consider r3, s3 being Real such that
A25: (r3 * p) + (s3 * q) = u - w by A1;
set a = (r2 * s3) - (r3 * s2);
set b = (r1 * s3) - (r3 * s1);
A26: ((r1 * s3) - (r3 * s1)) * r2 = (r1 * ((r2 * s3) - (r3 * s2))) + (r3 * ((r1 * s2) - (r2 * s1))) ;
set z = u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u));
A27: ((r1 * s2) - (r2 * s1)) * ((u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u))) - u) = (((r1 * s2) - (r2 * s1)) * (u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)))) - (((r1 * s2) - (r2 * s1)) * u) by RLVECT_1:34
.= ((((r1 * s2) - (r2 * s1)) * u) + (((r1 * s2) - (r2 * s1)) * (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)))) - (((r1 * s2) - (r2 * s1)) * u) by RLVECT_1:def 5
.= ((((r1 * s2) - (r2 * s1)) * u) + ((((r1 * s2) - (r2 * s1)) * ((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2)))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * u) by RLVECT_1:def 7
.= ((((r1 * s2) - (r2 * s1)) * u) + (((((r1 * s2) - (r2 * s1)) * (((r1 * s2) - (r2 * s1)) ")) * ((r2 * s3) - (r3 * s2))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * u)
.= ((((r1 * s2) - (r2 * s1)) * u) + ((1 * ((r2 * s3) - (r3 * s2))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * u) by A6, XCMPLX_0:def 7
.= (((r2 * s3) - (r3 * s2)) * (v - u)) + ((((r1 * s2) - (r2 * s1)) * u) - (((r1 * s2) - (r2 * s1)) * u)) by RLVECT_1:def 3
.= (((r2 * s3) - (r3 * s2)) * (v - u)) + (0. V) by RLVECT_1:15
.= ((r2 * s3) - (r3 * s2)) * (v - u) by RLVECT_1:4 ;
A28: ((r1 * s2) - (r2 * s1)) * ((u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u))) - w) = (((r1 * s2) - (r2 * s1)) * (u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)))) - (((r1 * s2) - (r2 * s1)) * w) by RLVECT_1:34
.= ((((r1 * s2) - (r2 * s1)) * u) + (((r1 * s2) - (r2 * s1)) * (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)))) - (((r1 * s2) - (r2 * s1)) * w) by RLVECT_1:def 5
.= ((((r1 * s2) - (r2 * s1)) * u) + ((((r1 * s2) - (r2 * s1)) * ((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2)))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * w) by RLVECT_1:def 7
.= ((((r1 * s2) - (r2 * s1)) * u) + (((((r1 * s2) - (r2 * s1)) * (((r1 * s2) - (r2 * s1)) ")) * ((r2 * s3) - (r3 * s2))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * w)
.= ((((r1 * s2) - (r2 * s1)) * u) + ((1 * ((r2 * s3) - (r3 * s2))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * w) by A6, XCMPLX_0:def 7
.= (((r2 * s3) - (r3 * s2)) * (v - u)) + ((((r1 * s2) - (r2 * s1)) * u) - (((r1 * s2) - (r2 * s1)) * w)) by RLVECT_1:def 3
.= (((r2 * s3) - (r3 * s2)) * ((r1 * p) + (s1 * q))) + (((r1 * s2) - (r2 * s1)) * ((r3 * p) + (s3 * q))) by A4, A25, RLVECT_1:34
.= ((((r2 * s3) - (r3 * s2)) * (r1 * p)) + (((r2 * s3) - (r3 * s2)) * (s1 * q))) + (((r1 * s2) - (r2 * s1)) * ((r3 * p) + (s3 * q))) by RLVECT_1:def 5
.= ((((r2 * s3) - (r3 * s2)) * (r1 * p)) + (((r2 * s3) - (r3 * s2)) * (s1 * q))) + ((((r1 * s2) - (r2 * s1)) * (r3 * p)) + (((r1 * s2) - (r2 * s1)) * (s3 * q))) by RLVECT_1:def 5
.= (((((r2 * s3) - (r3 * s2)) * r1) * p) + (((r2 * s3) - (r3 * s2)) * (s1 * q))) + ((((r1 * s2) - (r2 * s1)) * (r3 * p)) + (((r1 * s2) - (r2 * s1)) * (s3 * q))) by RLVECT_1:def 7
.= (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r2 * s3) - (r3 * s2)) * s1) * q)) + ((((r1 * s2) - (r2 * s1)) * (r3 * p)) + (((r1 * s2) - (r2 * s1)) * (s3 * q))) by RLVECT_1:def 7
.= (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r2 * s3) - (r3 * s2)) * s1) * q)) + (((((r1 * s2) - (r2 * s1)) * r3) * p) + (((r1 * s2) - (r2 * s1)) * (s3 * q))) by RLVECT_1:def 7
.= (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r2 * s3) - (r3 * s2)) * s1) * q)) + (((((r1 * s2) - (r2 * s1)) * s3) * q) + ((((r1 * s2) - (r2 * s1)) * r3) * p)) by RLVECT_1:def 7
.= ((((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r2 * s3) - (r3 * s2)) * s1) * q)) + ((((r1 * s2) - (r2 * s1)) * s3) * q)) + ((((r1 * s2) - (r2 * s1)) * r3) * p) by RLVECT_1:def 3
.= ((((((r2 * s3) - (r3 * s2)) * s1) * q) + ((((r1 * s2) - (r2 * s1)) * s3) * q)) + ((((r2 * s3) - (r3 * s2)) * r1) * p)) + ((((r1 * s2) - (r2 * s1)) * r3) * p) by RLVECT_1:def 3
.= (((((r2 * s3) - (r3 * s2)) * s1) * q) + ((((r1 * s2) - (r2 * s1)) * s3) * q)) + (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r1 * s2) - (r2 * s1)) * r3) * p)) by RLVECT_1:def 3
.= (((((r2 * s3) - (r3 * s2)) * s1) + (((r1 * s2) - (r2 * s1)) * s3)) * q) + (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r1 * s2) - (r2 * s1)) * r3) * p)) by RLVECT_1:def 6
.= ((((r1 * s3) - (r3 * s1)) * s2) * q) + ((((r1 * s3) - (r3 * s1)) * r2) * p) by A26, RLVECT_1:def 6
.= (((r1 * s3) - (r3 * s1)) * (s2 * q)) + ((((r1 * s3) - (r3 * s1)) * r2) * p) by RLVECT_1:def 7
.= (((r1 * s3) - (r3 * s1)) * (s2 * q)) + (((r1 * s3) - (r3 * s1)) * (r2 * p)) by RLVECT_1:def 7
.= ((r1 * s3) - (r3 * s1)) * (y - w) by A5, RLVECT_1:def 5 ;
A29: ((r1 * s3) - (r3 * s1)) * s2 = (s1 * ((r2 * s3) - (r3 * s2))) + (s3 * ((r1 * s2) - (r2 * s1))) ;
per cases ( ( (r2 * s3) - (r3 * s2) = 0 & (r1 * s3) - (r3 * s1) <> 0 ) or ( (r2 * s3) - (r3 * s2) = 0 & (r1 * s3) - (r3 * s1) = 0 ) or ( (r2 * s3) - (r3 * s2) <> 0 & (r1 * s3) - (r3 * s1) = 0 ) or ( (r2 * s3) - (r3 * s2) <> 0 & (r1 * s3) - (r3 * s1) <> 0 ) ) ;
suppose that A30: (r2 * s3) - (r3 * s2) = 0 and
A31: (r1 * s3) - (r3 * s1) <> 0 ; :: thesis: ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) )
((r1 * s2) - (r2 * s1)) * ((u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u))) - u) = 0. V by A27, A30, RLVECT_1:10;
then (u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u))) - u = 0. V by A6, RLVECT_1:11;
then u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) = u by RLVECT_1:21;
then A32: u,v // u,u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) ;
( w,y // w,u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) or w,y // u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)),w ) by A28, A31, Lm1;
hence ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) by A32; :: thesis: verum
end;
suppose ( (r2 * s3) - (r3 * s2) = 0 & (r1 * s3) - (r3 * s1) = 0 ) ; :: thesis: ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) )
then ( r3 = 0 & s3 = 0 ) by A6, A26, A29, XCMPLX_1:6;
then (0. V) + (0 * q) = u - w by A25, RLVECT_1:10;
then (0. V) + (0. V) = u - w by RLVECT_1:10;
then 0. V = u - w by RLVECT_1:4;
then u = w by RLVECT_1:21;
then A33: w,y // w,u ;
u,v // u,u ;
hence ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) by A33; :: thesis: verum
end;
suppose that A34: (r2 * s3) - (r3 * s2) <> 0 and
A35: (r1 * s3) - (r3 * s1) = 0 ; :: thesis: ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) )
((r1 * s2) - (r2 * s1)) * ((u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u))) - w) = 0. V by A28, A35, RLVECT_1:10;
then (u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u))) - w = 0. V by A6, RLVECT_1:11;
then u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) = w by RLVECT_1:21;
then A36: w,y // w,u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) ;
( u,v // u,u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) or u,v // u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)),u ) by A27, A34, Lm1;
hence ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) by A36; :: thesis: verum
end;
suppose that A37: (r2 * s3) - (r3 * s2) <> 0 and
A38: (r1 * s3) - (r3 * s1) <> 0 ; :: thesis: ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) )
A39: ( w,y // w,u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) or w,y // u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)),w ) by A28, A38, Lm1;
( u,v // u,u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) or u,v // u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)),u ) by A27, A37, Lm1;
hence ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) by A39; :: thesis: verum
end;
end;