let AS be Oriented_Orthogonality_Space; :: thesis: ( AS is left_transitive implies AS is bach_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 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & 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 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & 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 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
A2: ( AS is left_transitive implies AS is right_transitive ) by Th15;
then A3: ( u,u1 '//' v,v1 & v,v1 '//' w1,w & u2,v2 '//' w1,w & u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) by A1;
assume that
A4: u,u1 '//' v,v1 and
A5: w,w1 '//' v,v1 and
A6: w,w1 '//' u2,v2 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
A7: ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
proof
A8: now :: thesis: ( u,u1 '//' v2,u2 & u <> u1 & v <> v1 & w <> w1 & ( v = v1 or w = w1 or u,u1 '//' u2,v2 or u,u1 '//' v2,u2 ) & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A9: u,u1 '//' v2,u2 and
A10: u <> u1 and
A11: v <> v1 and
w <> w1 ; :: thesis: ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
A12: now :: thesis: ( not u2,v2 '//' u,u1 or ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
assume A13: u2,v2 '//' u,u1 ; :: thesis: ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
then A14: u2,v2 '//' w,w1 by A2, A1, A4, A5, A10, A11;
A15: now :: thesis: ( not u2,v2 '//' w1,w or ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
assume u2,v2 '//' w1,w ; :: thesis: ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
then ( w = w1 or u2 = v2 ) by A14, Def1;
hence ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) ; :: thesis: verum
end;
w1,w '//' v2,u2 by A6, Def1;
then ( u2,v2 '//' w1,w or u2 = v2 ) by A2, A1, A9, A10, A13;
hence ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A15; :: thesis: verum
end;
A16: now :: thesis: ( not u2,v2 '//' u1,u or ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
A17: w1,w '//' v1,v by A5, Def1;
assume A18: u2,v2 '//' u1,u ; :: thesis: ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
u1,u '//' v1,v by A4, Def1;
then A19: u2,v2 '//' w1,w by A2, A1, A10, A11, A18, A17;
A20: now :: thesis: ( not u2,v2 '//' w,w1 or ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
assume u2,v2 '//' w,w1 ; :: thesis: ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
then ( w = w1 or u2 = v2 ) by A19, Def1;
hence ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) ; :: thesis: verum
end;
u1,u '//' u2,v2 by A9, Def1;
then ( u2,v2 '//' w,w1 or u2 = v2 ) by A2, A1, A6, A10, A18;
hence ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A20; :: thesis: verum
end;
( v2,u2 '//' u,u1 or v2,u2 '//' u1,u ) by A9, Def1;
hence ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A16, A12, Def1; :: thesis: verum
end;
assume ( v = v1 or w = w1 or u,u1 '//' u2,v2 or u,u1 '//' v2,u2 ) ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A8, Def1; :: thesis: verum
end;
A21: now :: thesis: ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w1,w & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A22: u,u1 '//' v,v1 and
A23: v,v1 '//' w,w1 and
A24: u2,v2 '//' w1,w ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
v2,u2 '//' w,w1 by A24, Def1;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A2, A1, A7, A22, A23; :: thesis: verum
end;
A25: now :: thesis: ( u,u1 '//' v,v1 & v,v1 '//' w1,w & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A26: u,u1 '//' v,v1 and
A27: v,v1 '//' w1,w and
A28: u2,v2 '//' w,w1 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
v2,u2 '//' w1,w by A28, Def1;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A2, A1, A7, A26, A27; :: thesis: verum
end;
( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) by A2, A1;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A4, A5, A6, A21, A3, A25, Def1; :: thesis: verum
end;
hence ( AS is left_transitive implies AS is bach_transitive ) ; :: thesis: verum