let V be RealLinearSpace; for u, v1, v2, w, y being VECTOR of V st Gen w,y & v1,u,u,v2 are_DTr_wrt w,y holds
( v1 = u & u = v2 )
let u, v1, v2, w, y be VECTOR of V; ( Gen w,y & v1,u,u,v2 are_DTr_wrt w,y implies ( v1 = u & u = v2 ) )
assume that
A1:
Gen w,y
and
A2:
v1,u,u,v2 are_DTr_wrt w,y
; ( v1 = u & u = v2 )
set a = v1 # u;
set b = u # v2;
A3:
v1,u,v1 # u,u # v2 are_Ort_wrt w,y
by A2;
A4:
u,v2,v1 # u,u # v2 are_Ort_wrt w,y
by A2;
A5:
v1,u // u,v2
by A2;
per cases
( v1 = v2 or v1 <> v2 )
;
suppose
v1 <> v2
;
( v1 = u & u = v2 )then A6:
v1 # u <> u # v2
by Th7;
u,
v2 // u,
u # v2
by Th12;
then A7:
u,
v2 '||' u,
u # v2
;
A8:
v1 # u,
u // u,
u # v2
by A5, Th13;
then
u,
u # v2 // v1 # u,
u # v2
by Lm1;
then A9:
u,
u # v2 '||' v1 # u,
u # v2
;
A10:
u = v2
proof
assume A11:
u <> v2
;
contradiction
A12:
u <> u # v2
proof
assume
u = u # v2
;
contradiction
then
u # v2 = u # u
;
hence
contradiction
by A11, Th7;
verum
end;
u,
u # v2,
v1 # u,
u # v2 are_Ort_wrt w,
y
by A1, A4, A7, A11, Lm10;
then
u,
u # v2,
u,
u # v2 are_Ort_wrt w,
y
by A1, A6, A9, Lm10;
hence
contradiction
by A1, A12, Lm8;
verum
end;
v1,
u // v1 # u,
u
by Th12;
then A13:
v1,
u '||' v1 # u,
u
;
v1 # u,
u // v1 # u,
u # v2
by A8, Lm1;
then A14:
v1 # u,
u '||' v1 # u,
u # v2
;
v1 = u
proof
assume A15:
v1 <> u
;
contradiction
A16:
u <> v1 # u
proof
assume
u = v1 # u
;
contradiction
then
v1 # u = u # u
;
hence
contradiction
by A15, Th7;
verum
end;
v1 # u,
u,
v1 # u,
u # v2 are_Ort_wrt w,
y
by A1, A3, A13, A15, Lm10;
then
v1 # u,
u,
v1 # u,
u are_Ort_wrt w,
y
by A1, A6, A14, Lm10;
hence
contradiction
by A1, A16, Lm8;
verum
end; hence
(
v1 = u &
u = v2 )
by A10;
verum end;