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 holds
u,v,u # u1,v # 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 implies u,v,u # u1,v # 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 # u1,v # v1 are_DTr_wrt w,y
set p = u # u1;
set q = v # v1;
set r = u # v;
set s = u1 # v1;
A3:
( u = v & u1 = v1 implies u # u1,v # v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y )
by A1, Lm9;
(u # u1) # (v # v1) = (u # v) # (u1 # v1)
by Th6;
then
u # v,u1 # v1 // u # v,(u # u1) # (v # v1)
by Th12;
then A4:
u # v,u1 # v1 '||' u # v,(u # u1) # (v # 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;
then A5:
( u # v <> u1 # v1 implies ( u1,v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y & u,v,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y ) )
by A1, A4, Lm10;
A6:
now ( u # v = u1 # v1 implies ( u1,v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y & u,v,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y ) )assume
u # v = u1 # v1
;
( u1,v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y & u,v,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y )then u # v =
(u # v) # (u1 # v1)
.=
(u # u1) # (v # v1)
by Th6
;
hence
(
u1,
v1,
u # v,
(u # u1) # (v # v1) are_Ort_wrt w,
y &
u,
v,
u # v,
(u # u1) # (v # v1) are_Ort_wrt w,
y )
by A1, Lm9;
verum end;
A7:
u,v // u1,v1
by A2;
then
u1,v1 // u,v
by ANALOAF:12;
then
u1,v1 // u1 # u,v1 # v
by Th14;
then
u1,v1 '||' u # u1,v # v1
;
then A8:
( u = v & u1 <> v1 implies u # u1,v # v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y )
by A1, A6, A5, Lm10;
A9:
u,v // u # u1,v # v1
by A7, Th14;
then
u,v '||' u # u1,v # v1
;
then
( u <> v implies u # u1,v # v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y )
by A1, A6, A5, Lm10;
hence
u,v,u # u1,v # v1 are_DTr_wrt w,y
by A9, A6, A5, A8, A3; verum