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 & w,u1,u,v are_COrtm_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 & w,u1,u,v are_COrtm_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 & w,u1,u,v are_COrtm_wrt x,y )
let u, v, w be VECTOR of V; ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_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 & w,u1,u,v are_COrtm_wrt x,y ) )assume A3:
u = v
;
ex u1 being M3( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )take u1 =
w + x;
ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )
Ortm (
x,
y,
w),
Ortm (
x,
y,
u1)
// u,
v
by A3, ANALOAF:9;
then A4:
w,
u1,
u,
v are_COrtm_wrt x,
y
;
hence
ex
u1 being
VECTOR of
V st
(
w <> u1 &
w,
u1,
u,
v are_COrtm_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 & w,u1,u,v are_COrtm_wrt x,y ) )assume A5:
u <> v
;
ex u1 being M3( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )consider u2 being
VECTOR of
V such that A6:
Ortm (
x,
y,
u2)
= u
by A1, Th8;
consider v2 being
VECTOR of
V such that A7:
Ortm (
x,
y,
v2)
= v
by A1, Th8;
take u1 =
(v2 + w) - u2;
ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )
u2,
v2 // w,
u1
by ANALOAF:16;
then
w,
u1 // u2,
v2
by ANALOAF:12;
then
Ortm (
x,
y,
w),
Ortm (
x,
y,
u1)
// Ortm (
x,
y,
u2),
Ortm (
x,
y,
v2)
by A1, Th17;
then A8:
w,
u1,
u,
v are_COrtm_wrt x,
y
by A6, A7;
hence
ex
u1 being
VECTOR of
V st
(
w <> u1 &
w,
u1,
u,
v are_COrtm_wrt x,
y )
by A8;
verum end;
hence
ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )
by A2; verum