let V be RealLinearSpace; for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y holds
( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )
let x, y, u, v, u1, v1 be VECTOR of V; ( Gen x,y implies ( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) ) )
assume A1:
Gen x,y
; ( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )
A2:
( u,v // u1,v1 implies ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )
proof
assume A3:
u,
v // u1,
v1
;
ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )
A4:
now assume that A5:
u = v
and A6:
u1 = v1
;
ex u2 being M2( the carrier of V) ex v2, u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )take u2 =
0. V;
ex v2, u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )take v2 =
x;
ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )A7:
Orte (
x,
y,
u2),
Orte (
x,
y,
v2)
// u,
v
by A5, ANALOAF:9;
Orte (
x,
y,
u2),
Orte (
x,
y,
v2)
// u1,
v1
by A6, ANALOAF:9;
then A8:
u2,
v2,
u1,
v1 are_COrte_wrt x,
y
by Def3;
A9:
u2,
v2,
u,
v are_COrte_wrt x,
y
by A7, Def3;
u2 <> v2
by A1, Lm4;
hence
ex
u2,
v2 being
VECTOR of
V st
(
u2 <> v2 &
u2,
v2,
u,
v are_COrte_wrt x,
y &
u2,
v2,
u1,
v1 are_COrte_wrt x,
y )
by A8, A9;
verum end;
A10:
now assume A11:
u <> v
;
ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )consider u2 being
VECTOR of
V such that A12:
Orte (
x,
y,
u2)
= u
by A1, Th15;
consider v2 being
VECTOR of
V such that A13:
Orte (
x,
y,
v2)
= v
by A1, Th15;
Orte (
x,
y,
u2),
Orte (
x,
y,
v2)
// u,
v
by A12, A13, ANALOAF:8;
then A14:
u2,
v2,
u,
v are_COrte_wrt x,
y
by Def3;
u2,
v2,
u1,
v1 are_COrte_wrt x,
y
by A3, A12, A13, Def3;
hence
ex
u2,
v2 being
VECTOR of
V st
(
u2 <> v2 &
u2,
v2,
u,
v are_COrte_wrt x,
y &
u2,
v2,
u1,
v1 are_COrte_wrt x,
y )
by A11, A12, A13, A14;
verum end;
now assume A15:
u1 <> v1
;
ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )consider u2 being
VECTOR of
V such that A16:
Orte (
x,
y,
u2)
= u1
by A1, Th15;
consider v2 being
VECTOR of
V such that A17:
Orte (
x,
y,
v2)
= v1
by A1, Th15;
Orte (
x,
y,
u2),
Orte (
x,
y,
v2)
// u1,
v1
by A16, A17, ANALOAF:8;
then A18:
u2,
v2,
u1,
v1 are_COrte_wrt x,
y
by Def3;
Orte (
x,
y,
u2),
Orte (
x,
y,
v2)
// u,
v
by A3, A16, A17, ANALOAF:12;
then
u2,
v2,
u,
v are_COrte_wrt x,
y
by Def3;
hence
ex
u2,
v2 being
VECTOR of
V st
(
u2 <> v2 &
u2,
v2,
u,
v are_COrte_wrt x,
y &
u2,
v2,
u1,
v1 are_COrte_wrt x,
y )
by A15, A16, A17, A18;
verum end;
hence
ex
u2,
v2 being
VECTOR of
V st
(
u2 <> v2 &
u2,
v2,
u,
v are_COrte_wrt x,
y &
u2,
v2,
u1,
v1 are_COrte_wrt x,
y )
by A4, A10;
verum
end;
( ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) implies u,v // u1,v1 )
proof
given u2,
v2 being
VECTOR of
V such that A19:
u2 <> v2
and A20:
u2,
v2,
u,
v are_COrte_wrt x,
y
and A21:
u2,
v2,
u1,
v1 are_COrte_wrt x,
y
;
u,v // u1,v1
A22:
Orte (
x,
y,
u2),
Orte (
x,
y,
v2)
// u,
v
by A20, Def3;
Orte (
x,
y,
u2),
Orte (
x,
y,
v2)
// u1,
v1
by A21, Def3;
hence
u,
v // u1,
v1
by A1, A19, A22, Th13, ANALOAF:11;
verum
end;
hence
( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )
by A2; verum