let MS be OrtAfPl; :: thesis: ( MS is Moufangian iff MS is satisfying_TDES )
set AS = AffinStruct(# the carrier of MS, the CONGR of MS #);
A1: now :: thesis: ( MS is satisfying_TDES implies MS is Moufangian )
assume A2: MS is satisfying_TDES ; :: thesis: MS is Moufangian
now :: thesis: for K being Subset of AffinStruct(# the carrier of MS, the CONGR of MS #)
for o, a, b, c, a9, b9, c9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K holds
b,c // b9,c9
let K be Subset of AffinStruct(# the carrier of MS, the CONGR of MS #); :: thesis: for o, a, b, c, a9, b9, c9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of AffinStruct(# the carrier of MS, the CONGR of MS #); :: thesis: ( K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K implies b,c // b9,c9 )
assume that
A3: K is being_line and
A4: o in K and
A5: c in K and
A6: c9 in K and
A7: not a in K and
A8: o <> c and
A9: a <> b and
A10: LIN o,a,a9 and
A11: LIN o,b,b9 and
A12: a,b // a9,b9 and
A13: a,c // a9,c9 and
A14: a,b // K ; :: thesis: b,c // b9,c9
reconsider o1 = o, a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of MS ;
A15: ( o1 <> b1 & a1,c1 // a19,c19 ) by A4, A7, A13, A14, AFF_1:35, ANALMETR:36;
A16: not LIN o,a,c
proof
assume LIN o,a,c ; :: thesis: contradiction
then LIN o,c,a by AFF_1:6;
hence contradiction by A3, A4, A5, A7, A8, AFF_1:25; :: thesis: verum
end;
A17: not LIN o,a,b
proof
set M = Line (a,b);
assume LIN o,a,b ; :: thesis: contradiction
then LIN a,b,o by AFF_1:6;
then A18: o in Line (a,b) by AFF_1:def 2;
( a in Line (a,b) & Line (a,b) // K ) by A9, A14, AFF_1:15, AFF_1:def 5;
then a in K by A4, A18, AFF_1:45;
hence contradiction by A3, A4, A5, A16, AFF_1:21; :: thesis: verum
end;
a,b // o,c by A3, A4, A5, A8, A14, AFF_1:27;
then b,a // o,c by AFF_1:4;
then A19: b1,a1 // o1,c1 by ANALMETR:36;
A20: ( LIN o1,a1,a19 & LIN o1,b1,b19 ) by A10, A11, ANALMETR:40;
a1,b1 // a19,b19 by A12, ANALMETR:36;
then A21: b1,a1 // b19,a19 by ANALMETR:59;
A22: LIN o,c,c9 by A3, A4, A5, A6, AFF_1:21;
then A23: LIN o1,c1,c19 by ANALMETR:40;
A24: now :: thesis: ( a9 <> o implies b,c // b9,c9 )
assume A25: a9 <> o ; :: thesis: b,c // b9,c9
A26: now :: thesis: ( a <> a9 implies b,c // b9,c9 )
assume A27: a <> a9 ; :: thesis: b,c // b9,c9
A28: not LIN a1,a19,c1
proof
assume LIN a1,a19,c1 ; :: thesis: contradiction
then A29: LIN a,a9,c by ANALMETR:40;
( LIN a,a9,o & LIN a,a9,a ) by A10, AFF_1:6, AFF_1:7;
hence contradiction by A16, A27, A29, AFF_1:8; :: thesis: verum
end;
A30: not LIN a1,a19,b1
proof
assume LIN a1,a19,b1 ; :: thesis: contradiction
then A31: LIN a,a9,b by ANALMETR:40;
( LIN a,a9,o & LIN a,a9,a ) by A10, AFF_1:6, AFF_1:7;
hence contradiction by A17, A27, A31, AFF_1:8; :: thesis: verum
end;
( c,a // c9,a9 & not LIN o,c,a ) by A13, A16, AFF_1:4, AFF_1:6;
then A32: o1 <> c19 by A10, A25, AFF_1:55;
( b,a // b9,a9 & not LIN o,b,a ) by A12, A17, AFF_1:4, AFF_1:6;
then o1 <> b19 by A10, A25, AFF_1:55;
then b1,c1 // b19,c19 by A2, A4, A7, A8, A20, A23, A21, A19, A15, A25, A32, A28, A30, CONMETR:def 5;
hence b,c // b9,c9 by ANALMETR:36; :: thesis: verum
end;
now :: thesis: ( a = a9 implies b,c // b9,c9 )
A33: LIN o,c,c by AFF_1:7;
assume A34: a = a9 ; :: thesis: b,c // b9,c9
then a,c // a9,c by AFF_1:2;
then A35: c = c9 by A10, A13, A22, A16, A33, AFF_1:56;
A36: LIN o,b,b by AFF_1:7;
a,b // a9,b by A34, AFF_1:2;
then b = b9 by A10, A11, A12, A17, A36, AFF_1:56;
hence b,c // b9,c9 by A35, AFF_1:2; :: thesis: verum
end;
hence b,c // b9,c9 by A26; :: thesis: verum
end;
now :: thesis: ( a9 = o implies b,c // b9,c9 )
assume a9 = o ; :: thesis: b,c // b9,c9
then ( b9 = o & c9 = o ) by A11, A12, A13, A22, A16, A17, AFF_1:55;
hence b,c // b9,c9 by AFF_1:3; :: thesis: verum
end;
hence b,c // b9,c9 by A24; :: thesis: verum
end;
then AffinStruct(# the carrier of MS, the CONGR of MS #) is Moufangian by AFF_2:def 7;
hence MS is Moufangian ; :: thesis: verum
end;
now :: thesis: ( MS is Moufangian implies MS is satisfying_TDES )
assume MS is Moufangian ; :: thesis: MS is satisfying_TDES
then A37: AffinStruct(# the carrier of MS, the CONGR of MS #) is Moufangian ;
now :: thesis: for o, a, a1, b, b1, c, c1 being Element of MS st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN b,b1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,b // o,c & b,c // b1,c1 holds
a,c // a1,c1
let o, a, a1, b, b1, c, c1 be Element of MS; :: thesis: ( o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN b,b1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,b // o,c & b,c // b1,c1 implies a,c // a1,c1 )
assume that
o <> a and
o <> a1 and
A38: o <> b and
o <> b1 and
A39: o <> c and
o <> c1 and
A40: not LIN b,b1,a and
A41: not LIN b,b1,c and
A42: LIN o,a,a1 and
A43: LIN o,b,b1 and
A44: LIN o,c,c1 and
A45: a,b // a1,b1 and
A46: a,b // o,c and
A47: b,c // b1,c1 ; :: thesis: a,c // a1,c1
reconsider o9 = o, a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1 as Element of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
set K = Line (o9,c9);
A48: Line (o9,c9) is being_line by A39, AFF_1:def 3;
a9,b9 // o9,c9 by A46, ANALMETR:36;
then a9,b9 // Line (o9,c9) by A39, AFF_1:def 4;
then A49: b9,a9 // Line (o9,c9) by AFF_1:34;
a9,b9 // a19,b19 by A45, ANALMETR:36;
then A50: b9,a9 // b19,a19 by AFF_1:4;
A51: c9 in Line (o9,c9) by AFF_1:15;
A52: ( LIN o9,a9,a19 & b9,c9 // b19,c19 ) by A42, A47, ANALMETR:36, ANALMETR:40;
A53: b9 <> a9 by A40, Th1;
A54: o9 in Line (o9,c9) by AFF_1:15;
A55: LIN o9,b9,b19 by A43, ANALMETR:40;
A56: not b9 in Line (o9,c9)
proof
assume A57: b9 in Line (o9,c9) ; :: thesis: contradiction
then b19 in Line (o9,c9) by A38, A48, A54, A55, AFF_1:25;
then LIN b9,b19,c9 by A48, A51, A57, AFF_1:21;
hence contradiction by A41, ANALMETR:40; :: thesis: verum
end;
LIN o9,c9,c19 by A44, ANALMETR:40;
then c19 in Line (o9,c9) by A39, A48, A54, A51, AFF_1:25;
then a9,c9 // a19,c19 by A37, A39, A48, A54, A51, A55, A56, A49, A50, A52, A53, AFF_2:def 7;
hence a,c // a1,c1 by ANALMETR:36; :: thesis: verum
end;
hence MS is satisfying_TDES by CONMETR:def 5; :: thesis: verum
end;
hence ( MS is Moufangian iff MS is satisfying_TDES ) by A1; :: thesis: verum