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 holds
u,v,u # u1,v # 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 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
; :: thesis: 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 & 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;
(u # u1) # (v # v1) = (u # v) # (u1 # v1)
by Th8;
then
u # v,u1 # v1 // u # v,(u # u1) # (v # v1)
by Th14;
then A4:
u # v,u1 # v1 '||' u # v,(u # u1) # (v # v1)
by Def1;
A5:
u,v // u # u1,v # v1
by A3, Th16;
then A6:
u,v '||' u # u1,v # v1
by Def1;
u1,v1 // u,v
by A3, ANALOAF:21;
then
( u1,v1 // u1 # u,v1 # v & u # u1 = u1 # u & v # v1 = v1 # v )
by Th16;
then A7:
u1,v1 '||' u # u1,v # v1
by Def1;
A8:
now assume
u # v = u1 # v1
;
:: thesis: ( 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 Th8
;
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, Lm8;
:: thesis: verum end;
A9:
( 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, A3, A4, Lm9;
then A10:
( u <> v implies u # u1,v # v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y )
by A1, A6, A8, Lm9;
A11:
( u = v & u1 <> v1 implies u # u1,v # v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y )
by A1, A7, A8, A9, Lm9;
( u = v & u1 = v1 implies u # u1,v # v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y )
by A1, Lm8;
hence
u,v,u # u1,v # v1 are_DTr_wrt w,y
by A5, A8, A9, A10, A11, Def3; :: thesis: verum