let AS be Oriented_Orthogonality_Space; :: thesis: ( AS is left_transitive implies AS is right_transitive )
( ( for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds
u2,v2 '//' w,w1 ) implies for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2 )
proof
assume A1: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds
u2,v2 '//' w,w1 ; :: thesis: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; :: thesis: ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A2: u,u1 '//' v,v1 and
A3: v,v1 '//' w,w1 and
A4: u2,v2 '//' w,w1 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
A5: ( ( not w = w1 & not v = v1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
proof
now :: thesis: ( ( not w = w1 & not v = v1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
A6: now :: thesis: ( not v2,u2 '//' w,w1 or ( not w = w1 & not v = v1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
assume v2,u2 '//' w,w1 ; :: thesis: ( ( not w = w1 & not v = v1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
then u2,v2 '//' w1,w by Def1;
then ( u2 = v2 or w = w1 ) by A4, Def1;
hence ( ( not w = w1 & not v = v1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) ; :: thesis: verum
end;
( not u = u1 or ( not w = w1 & not v = v1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) by Def1;
hence ( ( not w = w1 & not v = v1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A1, A2, A3, A6; :: thesis: verum
end;
hence ( ( not w = w1 & not v = v1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) ; :: thesis: verum
end;
A7: now :: thesis: ( w,w1 '//' v,v1 & v,v1 '//' u,u1 & w,w1 '//' v2,u2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A8: w,w1 '//' v,v1 and
A9: v,v1 '//' u,u1 and
A10: w,w1 '//' v2,u2 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
( w = w1 or v = v1 or v2,u2 '//' u,u1 ) by A1, A8, A9, A10;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; :: thesis: verum
end;
A11: now :: thesis: ( w,w1 '//' v1,v & v,v1 '//' u,u1 & w,w1 '//' v2,u2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A12: w,w1 '//' v1,v and
A13: v,v1 '//' u,u1 and
A14: w,w1 '//' v2,u2 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
v1,v '//' u1,u by A13, Def1;
then ( w = w1 or v = v1 or v2,u2 '//' u1,u ) by A1, A12, A14;
then ( w = w1 or v = v1 or u2,v2 '//' u,u1 ) by Def1;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; :: thesis: verum
end;
A15: now :: thesis: ( w,w1 '//' v1,v & v,v1 '//' u,u1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A16: w,w1 '//' v1,v and
A17: v,v1 '//' u,u1 and
A18: w,w1 '//' u2,v2 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
v1,v '//' u1,u by A17, Def1;
then ( w = w1 or v = v1 or u2,v2 '//' u1,u ) by A1, A16, A18;
then ( w = w1 or v = v1 or v2,u2 '//' u,u1 ) by Def1;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; :: thesis: verum
end;
A19: now :: thesis: ( w,w1 '//' v1,v & v,v1 '//' u1,u & w,w1 '//' v2,u2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A20: w,w1 '//' v1,v and
A21: v,v1 '//' u1,u and
A22: w,w1 '//' v2,u2 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
v1,v '//' u,u1 by A21, Def1;
then ( w = w1 or v = v1 or v2,u2 '//' u,u1 ) by A1, A20, A22;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; :: thesis: verum
end;
A23: now :: thesis: ( w,w1 '//' v1,v & v,v1 '//' u1,u & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A24: w,w1 '//' v1,v and
A25: v,v1 '//' u1,u and
A26: w,w1 '//' u2,v2 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
v1,v '//' u,u1 by A25, Def1;
then ( w = w1 or v1 = v or u2,v2 '//' u,u1 ) by A1, A24, A26;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; :: thesis: verum
end;
A27: now :: thesis: ( w,w1 '//' v,v1 & v,v1 '//' u1,u & w,w1 '//' v2,u2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A28: w,w1 '//' v,v1 and
A29: v,v1 '//' u1,u and
A30: w,w1 '//' v2,u2 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
( w = w1 or v = v1 or v2,u2 '//' u1,u ) by A1, A28, A29, A30;
then ( w = w1 or v = v1 or u1,u '//' u2,v2 or u1,u '//' v2,u2 ) by Def1;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; :: thesis: verum
end;
A31: now :: thesis: ( w,w1 '//' v,v1 & v,v1 '//' u1,u & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A32: w,w1 '//' v,v1 and
A33: v,v1 '//' u1,u and
A34: w,w1 '//' u2,v2 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
( w = w1 or v = v1 or u2,v2 '//' u1,u ) by A1, A32, A33, A34;
then ( w = w1 or v = v1 or u1,u '//' u2,v2 or u1,u '//' v2,u2 ) by Def1;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; :: thesis: verum
end;
now :: thesis: ( w,w1 '//' v,v1 & v,v1 '//' u,u1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A35: w,w1 '//' v,v1 and
A36: v,v1 '//' u,u1 and
A37: w,w1 '//' u2,v2 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
( w = w1 or v = v1 or u2,v2 '//' u,u1 ) by A1, A35, A36, A37;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; :: thesis: verum
end;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A2, A3, A4, A7, A31, A27, A15, A11, A23, A19, Def1; :: thesis: verum
end;
hence ( AS is left_transitive implies AS is right_transitive ) ; :: thesis: verum