let V be RealLinearSpace; :: thesis: for w, y, v1, u, v2 being VECTOR of V st Gen w,y & v1,u,u,v2 are_DTr_wrt w,y holds
( v1 = u & u = v2 )
let w, y, v1, u, v2 be VECTOR of V; :: thesis: ( 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
; :: thesis: ( v1 = u & u = v2 )
set a = v1 # u;
set b = u # v2;
A3:
( v1,u // u,v2 & v1,u,v1 # u,u # v2 are_Ort_wrt w,y & u,v2,v1 # u,u # v2 are_Ort_wrt w,y )
by A2, Def3;
( v1 <> v2 implies ( v1 = u & u = v2 ) )
proof
assume
v1 <> v2
;
:: thesis: ( v1 = u & u = v2 )
then A4:
v1 # u <> u # v2
by Th9;
v1 # u,
u // u,
u # v2
by A3, Th15;
then
(
v1 # u,
u // v1 # u,
u # v2 &
u,
u # v2 // v1 # u,
u # v2 )
by Lm1;
then A5:
(
v1 # u,
u '||' v1 # u,
u # v2 &
u,
u # v2 '||' v1 # u,
u # v2 )
by Def1;
(
u,
v2 // u,
u # v2 &
v1,
u // v1 # u,
u )
by Th14;
then A6:
(
v1,
u '||' v1 # u,
u &
u,
v2 '||' u,
u # v2 )
by Def1;
A7:
v1 = u
proof
assume A8:
v1 <> u
;
:: thesis: contradiction
A9:
u <> v1 # u
v1 # u,
u,
v1 # u,
u # v2 are_Ort_wrt w,
y
by A1, A3, A6, A8, Lm9;
then
v1 # u,
u,
v1 # u,
u are_Ort_wrt w,
y
by A1, A4, A5, Lm9;
hence
contradiction
by A1, A9, Lm7;
:: thesis: verum
end;
u = v2
proof
assume A10:
u <> v2
;
:: thesis: contradiction
A11:
u <> u # v2
u,
u # v2,
v1 # u,
u # v2 are_Ort_wrt w,
y
by A1, A3, A6, A10, Lm9;
then
u,
u # v2,
u,
u # v2 are_Ort_wrt w,
y
by A1, A4, A5, Lm9;
hence
contradiction
by A1, A11, Lm7;
:: thesis: verum
end;
hence
(
v1 = u &
u = v2 )
by A7;
:: thesis: verum
end;
hence
( v1 = u & u = v2 )
by A2, Th19; :: thesis: verum