let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for a, b, c, d, a1, b1, c1, d1, p being Element of (DTrSpace (V,w,y)) st a,b // c,d & a # a1 = p & b # b1 = p & c # c1 = p & d # d1 = p holds
a1,b1 // c1,d1
let w, y be VECTOR of V; :: thesis: for a, b, c, d, a1, b1, c1, d1, p being Element of (DTrSpace (V,w,y)) st a,b // c,d & a # a1 = p & b # b1 = p & c # c1 = p & d # d1 = p holds
a1,b1 // c1,d1
let a, b, c, d, a1, b1, c1, d1, p be Element of (DTrSpace (V,w,y)); :: thesis: ( a,b // c,d & a # a1 = p & b # b1 = p & c # c1 = p & d # d1 = p implies a1,b1 // c1,d1 )
assume that
A1: ( a,b // c,d & a # a1 = p ) and
A2: ( b # b1 = p & c # c1 = p ) and
A3: d # d1 = p ; :: thesis: a1,b1 // c1,d1
reconsider u1 = a, u2 = b, v1 = c, v2 = d, u = p, t1 = a1, t2 = b1, w1 = c1, w2 = d1 as VECTOR of V ;
A4: ( u = u2 # t2 & u = v1 # w1 ) by A2, Def8;
A5: u = v2 # w2 by A3, Def8;
( u1,u2,v1,v2 are_DTr_wrt w,y & u = u1 # t1 ) by A1, Def8, Th44;
then t1,t2,w1,w2 are_DTr_wrt w,y by A4, A5, Th28;
hence a1,b1 // c1,d1 by Th44; :: thesis: verum