let OAS be OAffinSpace; :: thesis: for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is translation & a <> f . a & LIN a,f . a,b holds
a,b // f . a,f . b
let a, b be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is translation & a <> f . a & LIN a,f . a,b holds
a,b // f . a,f . b
let f be Permutation of the carrier of OAS; :: thesis: ( f is translation & a <> f . a & LIN a,f . a,b implies a,b // f . a,f . b )
assume that
A1: f is translation and
A2: a <> f . a and
A3: LIN a,f . a,b ; :: thesis: a,b // f . a,f . b
f <> id the carrier of OAS by A2, FUNCT_1:35;
then A4: b <> f . b by A1, Def9;
A5: f is dilatation by A1, Def9;
now
assume A6: a <> b ; :: thesis: a,b // f . a,f . b
A7: now
assume A8: Mid f . a,a,b ; :: thesis: a,b // f . a,f . b
A9: now
assume Mid f . b,b,a ; :: thesis: a,b // f . a,f . b
then Mid a,b,f . b by DIRAF:13;
then a,b // b,f . b by DIRAF:def 3;
then A10: a,b // a,f . b by ANALOAF:def 5;
Mid b,a,f . a by A8, DIRAF:13;
then b,a // a,f . a by DIRAF:def 3;
then A11: a,b // f . a,a by ANALOAF:def 5;
then f . a,a // a,f . b by A6, A10, ANALOAF:def 5;
then f . a,a // f . a,f . b by ANALOAF:def 5;
hence a,b // f . a,f . b by A10, A11, DIRAF:6; :: thesis: verum
end;
A12: now
A13: now
assume A14: a = f . b ; :: thesis: a,b // f . a,f . b
a,f . a // b,f . b by A1, A2, A3, Lm6;
hence a,b // f . a,f . b by A14, DIRAF:5; :: thesis: verum
end;
assume Mid b,a,f . b ; :: thesis: a,b // f . a,f . b
then ( b,a // f . b,f . a or a = f . b ) by A1, A4, Lm8;
hence a,b // f . a,f . b by A13, DIRAF:5; :: thesis: verum
end;
A15: now
assume Mid b,f . b,a ; :: thesis: a,b // f . a,f . b
then b,a // f . b,f . a by A1, A4, Lm7;
hence a,b // f . a,f . b by DIRAF:5; :: thesis: verum
end;
( LIN a,f . a,f . b & LIN a,f . a,a ) by A3, A5, Th60, DIRAF:37;
hence a,b // f . a,f . b by A2, A3, A15, A12, A9, DIRAF:35, DIRAF:38; :: thesis: verum
end;
A16: now
assume A17: Mid a,b,f . a ; :: thesis: a,b // f . a,f . b
( b = f . a implies a,b // f . a,f . b ) by A1, A2, A3, Lm6;
hence a,b // f . a,f . b by A1, A2, A17, Lm8; :: thesis: verum
end;
( Mid a,f . a,b implies a,b // f . a,f . b ) by A1, A2, Lm7;
hence a,b // f . a,f . b by A3, A7, A16, DIRAF:35; :: thesis: verum
end;
hence a,b // f . a,f . b by DIRAF:7; :: thesis: verum