let V be RealLinearSpace; :: thesis: for u, u1, v, v1 being VECTOR of V st u,v // u1,v1 holds
u,v // u # u1,v # v1
let u, u1, v, v1 be VECTOR of V; :: thesis: ( u,v // u1,v1 implies u,v // u # u1,v # v1 )
assume A1: u,v // u1,v1 ; :: thesis: u,v // u # u1,v # v1
per cases ( u = v or u1 = v1 or ( u <> v & u1 <> v1 ) ) ;
suppose ( u = v or u1 = v1 ) ; :: thesis: u,v // u # u1,v # v1
hence u,v // u # u1,v # v1 by Th8, ANALOAF:9; :: thesis: verum
end;
suppose A2: ( u <> v & u1 <> v1 ) ; :: thesis: u,v // u # u1,v # v1
set p = u # u1;
set q = v # v1;
consider a, b being Real such that
A3: ( 0 < a & 0 < b ) and
A4: a * (v - u) = b * (v1 - u1) by A1, A2, ANALOAF:def 1;
A5: ( 0 < a + b & 0 < b * 2 ) by A3, XREAL_1:34, XREAL_1:129;
(b * 2) * ((v # v1) - (u # u1)) = b * (2 * ((v # v1) - (u # u1))) by RLVECT_1:def 7
.= b * (((1 + 1) * (v # v1)) - (2 * (u # u1))) by RLVECT_1:34
.= b * (((1 * (v # v1)) + (1 * (v # v1))) - (2 * (u # u1))) by RLVECT_1:def 6
.= b * (((v # v1) + (1 * (v # v1))) - (2 * (u # u1))) by RLVECT_1:def 8
.= b * (((v # v1) + (v # v1)) - (2 * (u # u1))) by RLVECT_1:def 8
.= b * ((v + v1) - (2 * (u # u1))) by Def2
.= b * (v + (v1 - ((1 + 1) * (u # u1)))) by RLVECT_1:def 3
.= b * (v + (v1 - ((1 * (u # u1)) + (1 * (u # u1))))) by RLVECT_1:def 6
.= b * (v + (v1 - ((u # u1) + (1 * (u # u1))))) by RLVECT_1:def 8
.= b * (v + (v1 - ((u # u1) + (u # u1)))) by RLVECT_1:def 8
.= b * (v + (v1 - (u + u1))) by Def2
.= b * (v + ((v1 - u1) - u)) by RLVECT_1:27
.= b * ((v + (v1 - u1)) - u) by RLVECT_1:def 3
.= b * ((v1 - u1) + (v - u)) by RLVECT_1:def 3
.= (a * (v - u)) + (b * (v - u)) by A4, RLVECT_1:def 5
.= (a + b) * (v - u) by RLVECT_1:def 6 ;
hence u,v // u # u1,v # v1 by A5, ANALOAF:def 1; :: thesis: verum
end;
end;