let V be RealLinearSpace; :: thesis: for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y & u,v // u1,v1 holds
Ortm x,y,u, Ortm x,y,v // Ortm x,y,u1, Ortm x,y,v1
let x, y, u, v, u1, v1 be VECTOR of V; :: thesis: ( Gen x,y & u,v // u1,v1 implies Ortm x,y,u, Ortm x,y,v // Ortm x,y,u1, Ortm x,y,v1 )
assume A1:
Gen x,y
; :: thesis: ( not u,v // u1,v1 or Ortm x,y,u, Ortm x,y,v // Ortm x,y,u1, Ortm x,y,v1 )
assume A2:
u,v // u1,v1
; :: thesis: Ortm x,y,u, Ortm x,y,v // Ortm x,y,u1, Ortm x,y,v1
now assume A3:
u <> v
;
:: thesis: Ortm x,y,u, Ortm x,y,v // Ortm x,y,u1, Ortm x,y,v1now assume
u1 <> v1
;
:: thesis: Ortm x,y,u, Ortm x,y,v // Ortm x,y,u1, Ortm x,y,v1then consider a,
b being
Real such that A4:
(
0 < a &
0 < b )
and A5:
a * (v - u) = b * (v1 - u1)
by A2, A3, ANALOAF:def 1;
a * ((Ortm x,y,v) - (Ortm x,y,u)) =
a * (Ortm x,y,(v - u))
by A1, Th5
.=
Ortm x,
y,
(b * (v1 - u1))
by A1, A5, Th2
.=
b * (Ortm x,y,(v1 - u1))
by A1, Th2
.=
b * ((Ortm x,y,v1) - (Ortm x,y,u1))
by A1, Th5
;
hence
Ortm x,
y,
u,
Ortm x,
y,
v // Ortm x,
y,
u1,
Ortm x,
y,
v1
by A4, ANALOAF:def 1;
:: thesis: verum end; hence
Ortm x,
y,
u,
Ortm x,
y,
v // Ortm x,
y,
u1,
Ortm x,
y,
v1
by ANALOAF:18;
:: thesis: verum end;
hence
Ortm x,y,u, Ortm x,y,v // Ortm x,y,u1, Ortm x,y,v1
by ANALOAF:18; :: thesis: verum