let V be RealLinearSpace; for u, u1, v, w, y being VECTOR of V st Gen w,y holds
ex t being VECTOR of V st
( u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y )
let u, u1, v, w, y be VECTOR of V; ( Gen w,y implies ex t being VECTOR of V st
( u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y ) )
assume A1:
Gen w,y
; ex t being VECTOR of V st
( u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y )
set a = u # v;
per cases
( u = v or u <> v )
;
suppose A2:
u = v
;
ex t being VECTOR of V st
( u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y )A3:
u1,
u1,
u # u,
u1 # u1 are_Ort_wrt w,
y
by A1, Lm5, Lm6;
(
u,
u // u1,
u1 &
u,
u,
u # u,
u1 # u1 are_Ort_wrt w,
y )
by A1, Lm5, Lm6, ANALOAF:9;
then
u,
u,
u1,
u1 are_DTr_wrt w,
y
by A3;
hence
ex
t being
VECTOR of
V st
(
u,
v,
u1,
t are_DTr_wrt w,
y or
u,
v,
t,
u1 are_DTr_wrt w,
y )
by A2;
verum end; suppose A4:
u <> v
;
ex t being VECTOR of V st
( u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y )
u # v <> u
proof
assume
u # v = u
;
contradiction
then
u # u = u # v
;
hence
contradiction
by A4, Th7;
verum
end; then
u - (u # v) <> 0. V
by RLVECT_1:21;
then consider r being
Real such that A5:
(u1 - (u # v)) - (r * (u - (u # v))),
u - (u # v) are_Ort_wrt w,
y
by A1, ANALMETR:13;
set b =
u1 - (r * (u - (u # v)));
set t =
(2 * (u1 - (r * (u - (u # v))))) - u1;
u1 + ((2 * (u1 - (r * (u - (u # v))))) - u1) =
(1 + 1) * (u1 - (r * (u - (u # v))))
by RLSUB_2:61
.=
(1 * (u1 - (r * (u - (u # v))))) + (1 * (u1 - (r * (u - (u # v)))))
by RLVECT_1:def 6
.=
(u1 - (r * (u - (u # v)))) + (1 * (u1 - (r * (u - (u # v)))))
by RLVECT_1:def 8
.=
(u1 - (r * (u - (u # v)))) + (u1 - (r * (u - (u # v))))
by RLVECT_1:def 8
;
then A6:
u1 # ((2 * (u1 - (r * (u - (u # v))))) - u1) = u1 - (r * (u - (u # v)))
by Def2;
u1 - (u1 - (r * (u - (u # v)))) =
(u1 - u1) + (r * (u - (u # v)))
by RLVECT_1:29
.=
(0. V) + (r * (u - (u # v)))
by RLVECT_1:15
.=
r * (u - (u # v))
by RLVECT_1:4
;
then A7:
u1 - ((2 * (u1 - (r * (u - (u # v))))) - u1) =
2
* (r * (u - (u # v)))
by A6, Th10
.=
(2 * r) * (u - (u # v))
by RLVECT_1:def 7
;
A8:
u1 - ((u # v) + (r * (u - (u # v)))) = (u1 - (r * (u - (u # v)))) - (u # v)
by RLVECT_1:27;
then
(u1 - (r * (u - (u # v)))) - (u # v),
u - (u # v) are_Ort_wrt w,
y
by A5, RLVECT_1:27;
then
(u1 - (r * (u - (u # v)))) - (u # v),
u1 - ((2 * (u1 - (r * (u - (u # v))))) - u1) are_Ort_wrt w,
y
by A7, ANALMETR:7;
then A9:
u # v,
u1 - (r * (u - (u # v))),
(2 * (u1 - (r * (u - (u # v))))) - u1,
u1 are_Ort_wrt w,
y
by ANALMETR:def 3;
then A10:
(2 * (u1 - (r * (u - (u # v))))) - u1,
u1,
u # v,
((2 * (u1 - (r * (u - (u # v))))) - u1) # u1 are_Ort_wrt w,
y
by A6, Lm5;
A11:
u - v = 2
* (u - (u # v))
by Th10;
then
u1 - ((2 * (u1 - (r * (u - (u # v))))) - u1) = r * (u - v)
by A7, RLVECT_1:def 7;
then
r * (u - v) = 1
* (u1 - ((2 * (u1 - (r * (u - (u # v))))) - u1))
by RLVECT_1:def 8;
then
(
v,
u // (2 * (u1 - (r * (u - (u # v))))) - u1,
u1 or
v,
u // u1,
(2 * (u1 - (r * (u - (u # v))))) - u1 )
by ANALMETR:14;
then A12:
(
u,
v // u1,
(2 * (u1 - (r * (u - (u # v))))) - u1 or
u,
v // (2 * (u1 - (r * (u - (u # v))))) - u1,
u1 )
by ANALOAF:12;
u # v,
u1 - (r * (u - (u # v))),
u1,
(2 * (u1 - (r * (u - (u # v))))) - u1 are_Ort_wrt w,
y
by A9, Lm4;
then A13:
u1,
(2 * (u1 - (r * (u - (u # v))))) - u1,
u # v,
u1 # ((2 * (u1 - (r * (u - (u # v))))) - u1) are_Ort_wrt w,
y
by A6, Lm5;
(u1 - (r * (u - (u # v)))) - (u # v) = (u1 - (u # v)) - (r * (u - (u # v)))
by A8, RLVECT_1:27;
then
(u1 - (r * (u - (u # v)))) - (u # v),
u - v are_Ort_wrt w,
y
by A5, A11, ANALMETR:7;
then
u # v,
u1 - (r * (u - (u # v))),
v,
u are_Ort_wrt w,
y
by ANALMETR:def 3;
then
u # v,
u1 - (r * (u - (u # v))),
u,
v are_Ort_wrt w,
y
by Lm4;
then
u,
v,
u # v,
u1 # ((2 * (u1 - (r * (u - (u # v))))) - u1) are_Ort_wrt w,
y
by A6, Lm5;
then
(
u,
v,
u1,
(2 * (u1 - (r * (u - (u # v))))) - u1 are_DTr_wrt w,
y or
u,
v,
(2 * (u1 - (r * (u - (u # v))))) - u1,
u1 are_DTr_wrt w,
y )
by A13, A10, A12;
hence
ex
t being
VECTOR of
V st
(
u,
v,
u1,
t are_DTr_wrt w,
y or
u,
v,
t,
u1 are_DTr_wrt w,
y )
;
verum end;