let V be RealLinearSpace; :: thesis: for w, y, u, v, u1, v1 being VECTOR of V st Gen w,y & u,v,u1,v1 are_DTr_wrt w,y & not u,v,u # v1,v # u1 are_DTr_wrt w,y holds
u,v,v # u1,u # v1 are_DTr_wrt w,y
let w, y, u, v, u1, v1 be VECTOR of V; :: thesis: ( Gen w,y & u,v,u1,v1 are_DTr_wrt w,y & not u,v,u # v1,v # u1 are_DTr_wrt w,y implies u,v,v # u1,u # v1 are_DTr_wrt w,y )
assume that
A1:
Gen w,y
and
A2:
u,v,u1,v1 are_DTr_wrt w,y
; :: thesis: ( u,v,u # v1,v # u1 are_DTr_wrt w,y or u,v,v # u1,u # v1 are_DTr_wrt w,y )
set p = u # v1;
set q = v # u1;
set r = u # v;
set s = u1 # v1;
A3:
( u,v // u1,v1 & u,v,u # v,u1 # v1 are_Ort_wrt w,y & u1,v1,u # v,u1 # v1 are_Ort_wrt w,y )
by A2, Def3;
A4:
(u # v1) # (v # u1) = (u # v) # (u1 # v1)
by Th8;
then
u # v,u1 # v1 // u # v,(u # v1) # (v # u1)
by Th14;
then A5:
u # v,u1 # v1 '||' u # v,(u # v1) # (v # u1)
by Def1;
A6:
u,v '||' u # v1,v # u1
by A3, Lm2;
then A7:
( u,v // u # v1,v # u1 or u,v // v # u1,u # v1 )
by Def1;
now assume A8:
(
u <> v &
u1 <> v1 )
;
:: thesis: ( u,v,u # v1,v # u1 are_DTr_wrt w,y or u,v,v # u1,u # v1 are_DTr_wrt w,y )A9:
now assume A10:
u # v = u1 # v1
;
:: thesis: ( u,v,u # v1,v # u1 are_DTr_wrt w,y or u,v,v # u1,u # v1 are_DTr_wrt w,y )then A11:
(
u,
v,
u # v,
(u # v1) # (v # u1) are_Ort_wrt w,
y &
u,
v,
u # v,
(v # u1) # (u # v1) are_Ort_wrt w,
y )
by A1, A4, Lm8;
(
u # v1,
v # u1,
u # v,
(u # v1) # (v # u1) are_Ort_wrt w,
y &
v # u1,
u # v1,
u # v,
(v # u1) # (u # v1) are_Ort_wrt w,
y )
by A1, A4, A10, Lm8;
hence
(
u,
v,
u # v1,
v # u1 are_DTr_wrt w,
y or
u,
v,
v # u1,
u # v1 are_DTr_wrt w,
y )
by A7, A11, Def3;
:: thesis: verum end; now assume
u # v <> u1 # v1
;
:: thesis: ( u,v,u # v1,v # u1 are_DTr_wrt w,y or u,v,v # u1,u # v1 are_DTr_wrt w,y )then A12:
u,
v,
u # v,
(u # v1) # (v # u1) are_Ort_wrt w,
y
by A1, A3, A5, Lm9;
then U:
u # v,
(u # v1) # (v # u1),
u # v1,
v # u1 are_Ort_wrt w,
y
by A1, A6, A8, Lm9;
then
u # v,
(u # v1) # (v # u1),
v # u1,
u # v1 are_Ort_wrt w,
y
by A1, Lm4;
then Y:
v # u1,
u # v1,
u # v,
(v # u1) # (u # v1) are_Ort_wrt w,
y
by A1, Lm4A;
u # v1,
v # u1,
u # v,
(u # v1) # (v # u1) are_Ort_wrt w,
y
by A1, Lm4A, U;
hence
(
u,
v,
u # v1,
v # u1 are_DTr_wrt w,
y or
u,
v,
v # u1,
u # v1 are_DTr_wrt w,
y )
by A7, A12, Def3, Y;
:: thesis: verum end; hence
(
u,
v,
u # v1,
v # u1 are_DTr_wrt w,
y or
u,
v,
v # u1,
u # v1 are_DTr_wrt w,
y )
by A9;
:: thesis: verum end;
hence
( u,v,u # v1,v # u1 are_DTr_wrt w,y or u,v,v # u1,u # v1 are_DTr_wrt w,y )
by A1, A2, Th28; :: thesis: verum