let V be RealLinearSpace; for x, y being VECTOR of V st Gen x,y holds
for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
let x, y be VECTOR of V; ( Gen x,y implies for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y ) )
assume A1:
Gen x,y
; for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
let u, v, w be VECTOR of V; ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
A2:
now ( u = v implies ex u1 being M3( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y ) )assume A3:
u = v
;
ex u1 being M3( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )take u1 =
w + x;
ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
Orte (
x,
y,
u),
Orte (
x,
y,
v)
// w,
u1
by A3, ANALOAF:9;
then A4:
u,
v,
w,
u1 are_COrte_wrt x,
y
;
hence
ex
u1 being
VECTOR of
V st
(
w <> u1 &
u,
v,
w,
u1 are_COrte_wrt x,
y )
by A4;
verum end;
now ( u <> v implies ex u1 being M3( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y ) )assume A5:
u <> v
;
ex u1 being M3( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )consider u2 being
VECTOR of
V such that A6:
Orte (
x,
y,
u2)
= u
by A1, Th15;
consider v2 being
VECTOR of
V such that A7:
Orte (
x,
y,
v2)
= v
by A1, Th15;
take u1 =
(u2 + w) - v2;
ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
v2,
u2 // w,
u1
by ANALOAF:16;
then
Orte (
x,
y,
v2),
Orte (
x,
y,
u2)
// Orte (
x,
y,
w),
Orte (
x,
y,
u1)
by A1, Th16;
then
Orte (
x,
y,
w),
Orte (
x,
y,
u1)
// v,
u
by A6, A7, ANALOAF:12;
then
Orte (
x,
y,
u1),
Orte (
x,
y,
w)
// u,
v
by ANALOAF:12;
then A8:
u1,
w,
u,
v are_COrte_wrt x,
y
;
hence
ex
u1 being
VECTOR of
V st
(
w <> u1 &
u,
v,
w,
u1 are_COrte_wrt x,
y )
by A1, A8, Th18;
verum end;
hence
ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
by A2; verum