let V be RealLinearSpace; for u, u1, v, v1, x, y 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 u, u1, v, v1, x, y 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 ( u = v & u1 = v1 implies ex u2 being M3( 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 ) )assume that A5:
u = v
and A6:
u1 = v1
;
ex u2 being M3( 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
;
A9:
u2,
v2,
u,
v are_COrte_wrt x,
y
by A7;
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 ( u <> v 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 ) )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
;
u2,
v2,
u1,
v1 are_COrte_wrt x,
y
by A3, A12, A13;
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 ( 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 ) )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
;
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
;
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 )
by A1, Th13, ANALOAF:11;
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