let V be RealLinearSpace; :: thesis: 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_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) )
let x, y, u, v, u1, v1 be VECTOR of V; :: thesis: ( Gen x,y implies ( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) ) )
assume A1:
Gen x,y
; :: thesis: ( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) )
( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) )
proof
A2:
(
u,
v // u1,
v1 implies ex
u2,
v2 being
VECTOR of
V st
(
u2 <> v2 &
u2,
v2,
u,
v are_COrtm_wrt x,
y &
u2,
v2,
u1,
v1 are_COrtm_wrt x,
y ) )
proof
assume A3:
u,
v // u1,
v1
;
:: thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )
A4:
now assume A5:
(
u = v &
u1 = v1 )
;
:: thesis: ex u2 being M2(the carrier of V) ex v2, u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )take u2 =
0. V;
:: thesis: ex v2, u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )take v2 =
x;
:: thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )
(
Ortm x,
y,
u2,
Ortm x,
y,
v2 // u,
v &
Ortm x,
y,
u2,
Ortm x,
y,
v2 // u1,
v1 )
by A5, ANALOAF:18;
then A6:
(
u2,
v2,
u1,
v1 are_COrtm_wrt x,
y &
u2,
v2,
u,
v are_COrtm_wrt x,
y )
by Def4;
u2 <> v2
by A1, Lm4;
hence
ex
u2,
v2 being
VECTOR of
V st
(
u2 <> v2 &
u2,
v2,
u,
v are_COrtm_wrt x,
y &
u2,
v2,
u1,
v1 are_COrtm_wrt x,
y )
by A6;
:: thesis: verum end;
A7:
now assume A8:
u <> v
;
:: thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )consider u2 being
VECTOR of
V such that A9:
Ortm x,
y,
u2 = u
by A1, Th8;
consider v2 being
VECTOR of
V such that A10:
Ortm x,
y,
v2 = v
by A1, Th8;
Ortm x,
y,
u2,
Ortm x,
y,
v2 // u,
v
by A9, A10, ANALOAF:17;
then A11:
u2,
v2,
u,
v are_COrtm_wrt x,
y
by Def4;
u2,
v2,
u1,
v1 are_COrtm_wrt x,
y
by A3, A9, A10, Def4;
hence
ex
u2,
v2 being
VECTOR of
V st
(
u2 <> v2 &
u2,
v2,
u,
v are_COrtm_wrt x,
y &
u2,
v2,
u1,
v1 are_COrtm_wrt x,
y )
by A8, A9, A10, A11;
:: thesis: verum end;
now assume A12:
u1 <> v1
;
:: thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )consider u2 being
VECTOR of
V such that A13:
Ortm x,
y,
u2 = u1
by A1, Th8;
consider v2 being
VECTOR of
V such that A14:
Ortm x,
y,
v2 = v1
by A1, Th8;
Ortm x,
y,
u2,
Ortm x,
y,
v2 // u1,
v1
by A13, A14, ANALOAF:17;
then A15:
u2,
v2,
u1,
v1 are_COrtm_wrt x,
y
by Def4;
Ortm x,
y,
u2,
Ortm x,
y,
v2 // u,
v
by A3, A13, A14, ANALOAF:21;
then
u2,
v2,
u,
v are_COrtm_wrt x,
y
by Def4;
hence
ex
u2,
v2 being
VECTOR of
V st
(
u2 <> v2 &
u2,
v2,
u,
v are_COrtm_wrt x,
y &
u2,
v2,
u1,
v1 are_COrtm_wrt x,
y )
by A12, A13, A14, A15;
:: thesis: verum end;
hence
ex
u2,
v2 being
VECTOR of
V st
(
u2 <> v2 &
u2,
v2,
u,
v are_COrtm_wrt x,
y &
u2,
v2,
u1,
v1 are_COrtm_wrt x,
y )
by A4, A7;
:: thesis: verum
end;
( ex
u2,
v2 being
VECTOR of
V st
(
u2 <> v2 &
u2,
v2,
u,
v are_COrtm_wrt x,
y &
u2,
v2,
u1,
v1 are_COrtm_wrt x,
y ) implies
u,
v // u1,
v1 )
proof
given u2,
v2 being
VECTOR of
V such that A16:
(
u2 <> v2 &
u2,
v2,
u,
v are_COrtm_wrt x,
y &
u2,
v2,
u1,
v1 are_COrtm_wrt x,
y )
;
:: thesis: u,v // u1,v1
(
Ortm x,
y,
u2,
Ortm x,
y,
v2 // u,
v &
Ortm x,
y,
u2,
Ortm x,
y,
v2 // u1,
v1 )
by A16, Def4;
hence
u,
v // u1,
v1
by A1, A16, Th6, ANALOAF:20;
:: thesis: verum
end;
hence
(
u,
v // u1,
v1 iff ex
u2,
v2 being
VECTOR of
V st
(
u2 <> v2 &
u2,
v2,
u,
v are_COrtm_wrt x,
y &
u2,
v2,
u1,
v1 are_COrtm_wrt x,
y ) )
by A2;
:: thesis: verum
end;
hence
( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) )
; :: thesis: verum