let V be RealLinearSpace; :: thesis: for u1, u2, v, w, y being VECTOR of V st Gen w,y & v,u1,v,u2 are_DTr_wrt w,y holds
u1 = u2
let u1, u2, v, w, y be VECTOR of V; :: thesis: ( Gen w,y & v,u1,v,u2 are_DTr_wrt w,y implies u1 = u2 )
assume that
A1: Gen w,y and
A2: v,u1,v,u2 are_DTr_wrt w,y ; :: thesis: u1 = u2
A3: v,u1,v # u1,v # u2 are_Ort_wrt w,y by A2;
A4: v,u2,v # u1,v # u2 are_Ort_wrt w,y by A2;
v,u1 // v,u1 by ANALOAF:8;
then A5: v,u1 '||' v,u1 ;
set b = v # u1;
set c = v # u2;
A6: v,u1 // v,v # u1 by Th12;
then A7: v,u1 '||' v,v # u1 ;
A8: v,u1 // v,u2 by A2;
v,u2 // v,v # u1
proof
per cases ( v = v # u1 or v <> v # u1 ) ;
suppose v = v # u1 ; :: thesis: v,u2 // v,v # u1
hence v,u2 // v,v # u1 by ANALOAF:9; :: thesis: verum
end;
suppose v <> v # u1 ; :: thesis: v,u2 // v,v # u1
then v <> u1 ;
hence v,u2 // v,v # u1 by A8, A6, ANALOAF:11; :: thesis: verum
end;
end;
end;
then A9: v,u2 '||' v,v # u1 ;
v,u2 // v,v by ANALOAF:9;
then A10: v,u2 '||' v,v ;
A11: v,u2 // v,v # u2 by Th12;
then A12: v,u2 '||' v,v # u2 ;
A13: v,u2 // v,u1 by A8, ANALOAF:12;
v,u1 // v,v # u2
proof
per cases ( v = v # u2 or v <> v # u2 ) ;
suppose v = v # u2 ; :: thesis: v,u1 // v,v # u2
hence v,u1 // v,v # u2 by ANALOAF:9; :: thesis: verum
end;
suppose v <> v # u2 ; :: thesis: v,u1 // v,v # u2
then v <> u2 ;
hence v,u1 // v,v # u2 by A13, A11, ANALOAF:11; :: thesis: verum
end;
end;
end;
then A14: v,u1 '||' v,v # u2 ;
v,u2 // v,u2 by ANALOAF:8;
then A15: v,u2 '||' v,u2 ;
v,u1 // v,v by ANALOAF:9;
then A16: v,u1 '||' v,v ;
assume A17: u1 <> u2 ; :: thesis: contradiction
per cases ( v <> u1 or v <> u2 ) by A17;
suppose A18: v <> u1 ; :: thesis: contradiction
then v,u1 '||' v # u1,v # u2 by A1, A7, A5, A16, A14, Lm11;
then v # u1,v # u2,v # u1,v # u2 are_Ort_wrt w,y by A1, A3, A18, Lm10;
hence contradiction by A1, A17, Lm8, Th7; :: thesis: verum
end;
suppose A19: v <> u2 ; :: thesis: contradiction
then v,u2 '||' v # u1,v # u2 by A1, A12, A15, A10, A9, Lm11;
then v # u1,v # u2,v # u1,v # u2 are_Ort_wrt w,y by A1, A4, A19, Lm10;
hence contradiction by A1, A17, Lm8, Th7; :: thesis: verum
end;
end;