let V be RealLinearSpace; for x, y being VECTOR of V st Gen x,y holds
ex u, v, w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
let x, y be VECTOR of V; ( Gen x,y implies ex u, v, w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) ) )
assume A1:
Gen x,y
; ex u, v, w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
take u = (0 * x) + (0 * y); ex v, w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
take v = (1 * x) + (1 * y); ex w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
take w = (1 * x) + ((- 1) * y); ( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
A2:
pr1 (x,y,u) = 0
by A1, Lm6;
A3:
pr2 (x,y,u) = 0
by A1, Lm6;
A4:
pr1 (x,y,v) = 1
by A1, Lm6;
pr2 (x,y,v) = 1
by A1, Lm6;
then A5:
Ortm (x,y,u), Ortm (x,y,v) // u,w
by A2, A3, A4, ANALOAF:8;
for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
proof
let v1,
w1 be
VECTOR of
V;
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
assume
v1,
w1,
u,
v are_COrtm_wrt x,
y
;
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
then A6:
Ortm (
x,
y,
v1),
Ortm (
x,
y,
w1)
// u,
v
;
now ( v1 <> w1 & ( v1,w1,u,w are_COrtm_wrt x,y or v1,w1,w,u are_COrtm_wrt x,y ) implies ex a, b being Real st
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) )assume A7:
v1 <> w1
;
( ( v1,w1,u,w are_COrtm_wrt x,y or v1,w1,w,u are_COrtm_wrt x,y ) implies ex a, b being Real st
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) )assume
(
v1,
w1,
u,
w are_COrtm_wrt x,
y or
v1,
w1,
w,
u are_COrtm_wrt x,
y )
;
ex a, b being Real st
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )then
(
Ortm (
x,
y,
v1),
Ortm (
x,
y,
w1)
// u,
w or
Ortm (
x,
y,
v1),
Ortm (
x,
y,
w1)
// w,
u )
;
then
(
u,
v // u,
w or
u,
v // w,
u )
by A1, A6, A7, Th6, ANALOAF:11;
then consider a,
b being
Real such that A8:
a * (v - u) = b * (w - u)
and A9:
(
a <> 0 or
b <> 0 )
by ANALMETR:14;
take a =
a;
ex b being Real st
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )take b =
b;
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )u =
(0. V) + (0 * y)
by RLVECT_1:10
.=
(0. V) + (0. V)
by RLVECT_1:10
.=
0. V
by RLVECT_1:4
;
then
a * v = b * (w - (0. V))
by A8, RLVECT_1:13;
then A10:
a * v = b * w
by RLVECT_1:13;
A11:
now ( not a <> 0 or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )assume A12:
a <> 0
;
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
((a ") * a) * v = (a ") * (b * w)
by A10, RLVECT_1:def 7;
then
((a ") * a) * v = ((a ") * b) * w
by RLVECT_1:def 7;
then
1
* v = ((a ") * b) * w
by A12, XCMPLX_0:def 7;
then
1
* v = ((((a ") * b) * 1) * x) + ((((a ") * b) * (- 1)) * y)
by Lm2;
then A13:
((1 * 1) * x) + ((1 * 1) * y) = ((((a ") * b) * 1) * x) + ((((a ") * b) * (- 1)) * y)
by Lm2;
then
a * 1
= a * ((a ") * (b * 1))
by A1, Lm3;
then A14:
a * 1
= (a * (a ")) * (b * 1)
;
1
= ((a ") * b) * (- 1)
by A1, A13, Lm3;
then
1
= ((a ") * a) * (- 1)
by A12, A14, XCMPLX_0:def 7;
hence
( ( not
v1,
w1,
u,
w are_COrtm_wrt x,
y & not
v1,
w1,
w,
u are_COrtm_wrt x,
y ) or
v1 = w1 )
by A12, XCMPLX_0:def 7;
verum end; now ( not b <> 0 or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )assume A15:
b <> 0
;
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
((b ") * a) * v = (b ") * (b * w)
by A10, RLVECT_1:def 7;
then
((b ") * a) * v = ((b ") * b) * w
by RLVECT_1:def 7;
then
((b ") * a) * v = 1
* w
by A15, XCMPLX_0:def 7;
then
((((b ") * a) * 1) * x) + ((((b ") * a) * 1) * y) = 1
* w
by Lm2;
then A16:
((((b ") * a) * 1) * x) + ((((b ") * a) * 1) * y) = ((1 * 1) * x) + ((1 * (- 1)) * y)
by Lm2;
then
b * 1
= b * ((b ") * (a * 1))
by A1, Lm3;
then A17:
b * 1
= (b * (b ")) * (a * 1)
;
- 1
= ((b ") * a) * 1
by A1, A16, Lm3;
then
- 1
= ((b ") * b) * 1
by A15, A17, XCMPLX_0:def 7;
hence
( ( not
v1,
w1,
u,
w are_COrtm_wrt x,
y & not
v1,
w1,
w,
u are_COrtm_wrt x,
y ) or
v1 = w1 )
by A15, XCMPLX_0:def 7;
verum end; hence
( ( not
v1,
w1,
u,
w are_COrtm_wrt x,
y & not
v1,
w1,
w,
u are_COrtm_wrt x,
y ) or
v1 = w1 )
by A9, A11;
verum end;
hence
( ( not
v1,
w1,
u,
w are_COrtm_wrt x,
y & not
v1,
w1,
w,
u are_COrtm_wrt x,
y ) or
v1 = w1 )
;
verum
end;
hence
( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
by A5; verum