let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for u, u', u1, u2, t1, t2 being VECTOR of V st u <> u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y holds
u,u',u1 # u2,t1 # t2 are_DTr_wrt w,y
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, u', u1, u2, t1, t2 being VECTOR of V st u <> u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y holds
u,u',u1 # u2,t1 # t2 are_DTr_wrt w,y )
assume A1:
Gen w,y
; :: thesis: for u, u', u1, u2, t1, t2 being VECTOR of V st u <> u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y holds
u,u',u1 # u2,t1 # t2 are_DTr_wrt w,y
let u, u', u1, u2, t1, t2 be VECTOR of V; :: thesis: ( u <> u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y implies u,u',u1 # u2,t1 # t2 are_DTr_wrt w,y )
assume that
A2:
u <> u'
and
A3:
( u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y )
; :: thesis: u,u',u1 # u2,t1 # t2 are_DTr_wrt w,y
( u1,t1,u2,t2 are_DTr_wrt w,y & u2,t2,u1,t1 are_DTr_wrt w,y )
by A1, A2, A3, Th21;
then A4:
( u1,t1,u1 # u2,t1 # t2 are_DTr_wrt w,y & u2,t2,u2 # u1,t2 # t1 are_DTr_wrt w,y )
by A1, Th28;
A5:
now assume A6:
u1 <> t1
;
:: thesis: u,u',u1 # u2,t1 # t2 are_DTr_wrt w,y
u1,
t1,
u,
u' are_DTr_wrt w,
y
by A1, A3, Th23;
hence
u,
u',
u1 # u2,
t1 # t2 are_DTr_wrt w,
y
by A1, A4, A6, Th21;
:: thesis: verum end;
A7:
now assume A8:
u2 <> t2
;
:: thesis: u,u',u1 # u2,t1 # t2 are_DTr_wrt w,y
u2,
t2,
u,
u' are_DTr_wrt w,
y
by A1, A3, Th23;
hence
u,
u',
u1 # u2,
t1 # t2 are_DTr_wrt w,
y
by A1, A4, A8, Th21;
:: thesis: verum end;
now assume A9:
(
u1 = t1 &
u2 = t2 )
;
:: thesis: u,u',u1 # u2,t1 # t2 are_DTr_wrt w,ythen A10:
u,
u' // u1 # u2,
t1 # t2
by ANALOAF:18;
u # u',
(u1 # u2) # (t1 # t2),
u1 # u2,
t1 # t2 are_Ort_wrt w,
y
by A1, A9, Lm5;
then A11:
u1 # u2,
t1 # t2,
u # u',
(u1 # u2) # (t1 # t2) are_Ort_wrt w,
y
by A1, Lm4A;
u,
u',
u # u',
u1 # u2 are_Ort_wrt w,
y
proof
set uu' =
u # u';
(
u,
u',
u # u',
u1 # t1 are_Ort_wrt w,
y &
u,
u',
u # u',
u2 # t2 are_Ort_wrt w,
y )
by A3, Def3;
then A12:
(
u' - u,
u1 - (u # u') are_Ort_wrt w,
y &
u' - u,
u2 - (u # u') are_Ort_wrt w,
y )
by A9, ANALMETR:def 3;
A13:
(u1 # u2) - (u # u') = ((2 " ) * (u1 - (u # u'))) + ((2 " ) * (u2 - (u # u')))
(
u' - u,
(2 " ) * (u1 - (u # u')) are_Ort_wrt w,
y &
u' - u,
(2 " ) * (u2 - (u # u')) are_Ort_wrt w,
y )
by A12, ANALMETR:11;
then
u' - u,
(u1 # u2) - (u # u') are_Ort_wrt w,
y
by A1, A13, ANALMETR:14;
hence
u,
u',
u # u',
u1 # u2 are_Ort_wrt w,
y
by ANALMETR:def 3;
:: thesis: verum
end; hence
u,
u',
u1 # u2,
t1 # t2 are_DTr_wrt w,
y
by A9, A10, A11, Def3;
:: thesis: verum end;
hence
u,u',u1 # u2,t1 # t2 are_DTr_wrt w,y
by A5, A7; :: thesis: verum