let V be RealLinearSpace; for u, u1, v, v1, w, y 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 u, u1, v, v1, w, y be VECTOR of V; ( 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
; ( 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,u # v,u1 # v1 are_Ort_wrt w,y
by A2;
A4:
(u # v1) # (v # u1) = (u # v) # (u1 # v1)
by Th6;
then
u # v,u1 # v1 // u # v,(u # v1) # (v # u1)
by Th12;
then A5:
u # v,u1 # v1 '||' u # v,(u # v1) # (v # u1)
;
u,v // u1,v1
by A2;
then A6:
u,v '||' u # v1,v # u1
by Lm2;
then A7:
( u,v // u # v1,v # u1 or u,v // v # u1,u # v1 )
;
per cases
( u = v or u <> v )
;
suppose
u = v
;
( u,v,u # v1,v # u1 are_DTr_wrt w,y or u,v,v # u1,u # v1 are_DTr_wrt w,y )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, Th26;
verum end; suppose A8:
u <> v
;
( u,v,u # v1,v # u1 are_DTr_wrt w,y or u,v,v # u1,u # v1 are_DTr_wrt w,y )per cases
( u # v = u1 # v1 or u # v <> u1 # v1 )
;
suppose A9:
u # v = u1 # v1
;
( u,v,u # v1,v # u1 are_DTr_wrt w,y or u,v,v # u1,u # v1 are_DTr_wrt w,y )then A10:
v # u1,
u # v1,
u # v,
(v # u1) # (u # v1) are_Ort_wrt w,
y
by A1, A4, Lm9;
(
u,
v,
u # v,
(u # v1) # (v # u1) are_Ort_wrt w,
y &
u # v1,
v # u1,
u # v,
(u # v1) # (v # u1) are_Ort_wrt w,
y )
by A1, A4, A9, Lm9;
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, A10;
verum end; suppose
u # v <> u1 # v1
;
( 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
by A1, A3, A5, Lm10;
then
u # v,
(u # v1) # (v # u1),
u # v1,
v # u1 are_Ort_wrt w,
y
by A1, A6, A8, Lm10;
then
u # v,
(u # v1) # (v # u1),
v # u1,
u # v1 are_Ort_wrt w,
y
by Lm4;
then A12:
v # u1,
u # v1,
u # v,
(v # u1) # (u # v1) are_Ort_wrt w,
y
by Lm5;
u # v1,
v # u1,
u # v,
(u # v1) # (v # u1) are_Ort_wrt w,
y
by A1, A6, A8, A11, Lm10;
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, A12;
verum end;