let AFP be AffinPlane; :: thesis: ( ( for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b ) ) implies AFP is Moufangian )
assume A1:
for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b )
; :: thesis: AFP is Moufangian
now let o be
Element of
AFP;
:: thesis: for K being Subset of AFP
for c, c', a, b, a', b' being Element of AFP st o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' holds
b,c // b',c'let K be
Subset of
AFP;
:: thesis: for c, c', a, b, a', b' being Element of AFP st o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' holds
b,c // b',c'let c,
c',
a,
b,
a',
b' be
Element of
AFP;
:: thesis: ( o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' implies b,c // b',c' )assume A2:
(
o in K &
c in K &
c' in K &
K is
being_line &
LIN o,
a,
a' &
LIN o,
b,
b' & not
a in K &
a,
b // K &
a',
b' // K &
a,
c // a',
c' )
;
:: thesis: b,c // b',c'then consider f being
Permutation of the
carrier of
AFP such that A3:
(
f is_Sc K &
f . a = b )
by A1;
A4:
f is
collineation
by A3, Def1;
A5:
a,
b // a',
b'
by A2, AFF_1:45;
A6:
(
f . c = c &
f . c' = c' )
by A2, A3, Def1;
f . a' = b'
proof
set x =
f . a';
A7:
now assume A8:
a <> b
;
:: thesis: f . a' = b'
a',
f . a' // K
by A3, Def1;
then A9:
a,
b // a',
f . a'
by A2, AFF_1:45;
f . o = o
by A2, A3, Def1;
then
LIN o,
b,
f . a'
by A2, A3, A4, TRANSGEO:108;
hence
f . a' = b'
by A2, A5, A8, A9, AFF_1:60, AFF_1:70;
:: thesis: verum end;
hence
f . a' = b'
by A7;
:: thesis: verum
end; hence
b,
c // b',
c'
by A2, A3, A4, A6, TRANSGEO:107;
:: thesis: verum end;
hence
AFP is Moufangian
by Lm2; :: thesis: verum