begin
Lm1:
for F being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b being Element of F holds - (a - b) = b - a
Lm2:
for F being Field
for a, b, c, d being Element of F holds ((a - b) * (c - d)) - ((b - a) * (d - c)) = 0. F
Lm3:
for F being Field
for a, b, c, d being Element of F holds (a * (b - b)) - ((c - c) * d) = 0. F
Lm4:
for F being Field
for a, e, d, b, c, h being Element of F st a <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F holds
(d * c) - (h * e) = 0. F
Lm5:
for F being Field
for a, b, c, d being Element of F st (a * b) - (c * d) = 0. F holds
(d * c) - (b * a) = 0. F
Lm6:
for F being Field
for b, a, e, d, c, h being Element of F st b <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F holds
(d * c) - (h * e) = 0. F
Lm7:
for F being Field
for c, d, a, b being Element of F holds (c * d) * (a * b) = ((a * c) * d) * b
Lm8:
for F being Field
for a, b, c, d, f, g being Element of F st (a * b) - (c * d) = 0. F holds
(((a * f) * g) * b) - (((c * f) * g) * d) = 0. F
Lm9:
for F being Field
for a, b, c, d being Element of F holds (a - b) * (c - d) = (a * c) + ((- (a * d)) + (- (b * (c - d))))
Lm10:
for F being Field
for a, b, c, d being Element of F holds (a + b) + (c + d) = (a + (b + c)) + d
Lm11:
for F being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b, c being Element of F holds (b + a) - (c + a) = b - c
Lm12:
for F being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b being Element of F holds a + b = - ((- b) + (- a))
Lm13:
for F being Field
for a, b, c, d, e, f being Element of F st ((a - b) * (c - d)) - ((a - e) * (c - f)) = 0. F holds
((b - a) * (f - d)) - ((b - e) * (f - c)) = 0. F
Lm14:
for F being Field
for a, b, c being Element of F holds a - ((a + b) + (- c)) = c - b
Lm15:
for F being Field
for a, b, c, h, g, e being Element of F holds ((a - b) * (c - ((c + h) + (- g)))) - ((e - ((e + b) + (- a))) * (g - h)) = 0. F
deffunc H1( Field) -> set = [: the carrier of $1, the carrier of $1, the carrier of $1:];
definition
let F be
Field;
existence
ex b1 being BinOp of [: the carrier of F, the carrier of F, the carrier of F:] st
for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b1 . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))]
uniqueness
for b1, b2 being BinOp of [: the carrier of F, the carrier of F, the carrier of F:] st ( for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b1 . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] ) & ( for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b2 . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] ) holds
b1 = b2
end;
theorem Th2:
for
F being
Field for
a,
b,
c,
f,
g,
h being
Element of
F holds
[a,b,c] + [f,g,h] = [(a + f),(b + g),(c + h)]
definition
let F be
Field;
existence
ex b1 being UnOp of [: the carrier of F, the carrier of F, the carrier of F:] st
for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b1 . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))]
uniqueness
for b1, b2 being UnOp of [: the carrier of F, the carrier of F, the carrier of F:] st ( for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b1 . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] ) & ( for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b2 . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] ) holds
b1 = b2
end;
definition
let F be
Field;
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( x = [a,b,c,d] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( x = [a,b,c,d] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) ) ) & ( for x being set holds
( x in b2 iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( x = [a,b,c,d] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) ) ) holds
b1 = b2
end;
theorem
for
F being
Field for
a,
b,
c,
d being
Element of
(MPS F) holds
(
[a,b,c,d] in PR F iff (
[a,b,c,d] in 4C_3 F & ex
e,
f,
g,
h being
Element of
[: the carrier of F, the carrier of F, the carrier of F:] st
(
[a,b,c,d] = [e,f,g,h] &
(((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F &
(((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F &
(((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) ) )
by Def9;
theorem Th9:
for
F being
Field for
a,
b,
c,
d being
Element of
(MPS F) holds
(
a,
b '||' c,
d iff (
[a,b,c,d] in 4C_3 F & ex
e,
f,
g,
h being
Element of
[: the carrier of F, the carrier of F, the carrier of F:] st
(
[a,b,c,d] = [e,f,g,h] &
(((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F &
(((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F &
(((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) ) )
theorem Th12:
for
F being
Field for
a,
b,
c,
d being
Element of
(MPS F) holds
(
a,
b '||' c,
d iff ex
e,
f,
g,
h being
Element of
[: the carrier of F, the carrier of F, the carrier of F:] st
(
[a,b,c,d] = [e,f,g,h] &
(((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F &
(((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F &
(((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) )
theorem Th15:
for
F being
Field for
a,
b,
p,
q,
r,
s being
Element of
(MPS F) st
a,
b '||' p,
q &
a,
b '||' r,
s & not
p,
q '||' r,
s holds
a = b
definition
let IT be non
empty ParStr ;
attr IT is
ParSp-like means :
Def12:
for
a,
b,
c,
d,
p,
q,
r,
s being
Element of
IT holds
(
a,
b '||' b,
a &
a,
b '||' c,
c & (
a,
b '||' p,
q &
a,
b '||' r,
s & not
p,
q '||' r,
s implies
a = b ) & (
a,
b '||' a,
c implies
b,
a '||' b,
c ) & ex
x being
Element of
IT st
(
a,
b '||' c,
x &
a,
c '||' b,
x ) );
end;
::
deftheorem Def12 defines
ParSp-like PARSP_1:def 12 :
for IT being non empty ParStr holds
( IT is ParSp-like iff for a, b, c, d, p, q, r, s being Element of IT holds
( a,b '||' b,a & a,b '||' c,c & ( a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s implies a = b ) & ( a,b '||' a,c implies b,a '||' b,c ) & ex x being Element of IT st
( a,b '||' c,x & a,c '||' b,x ) ) );
theorem Th23:
for
PS being
ParSp for
a,
b,
c,
d being
Element of
PS st
a,
b '||' c,
d holds
(
b,
a '||' c,
d &
a,
b '||' d,
c &
b,
a '||' d,
c &
c,
d '||' a,
b &
d,
c '||' a,
b &
c,
d '||' b,
a &
d,
c '||' b,
a )
theorem Th24:
for
PS being
ParSp for
a,
b,
c being
Element of
PS st
a,
b '||' a,
c holds
(
a,
c '||' a,
b &
b,
a '||' a,
c &
a,
b '||' c,
a &
a,
c '||' b,
a &
b,
a '||' c,
a &
c,
a '||' a,
b &
c,
a '||' b,
a &
b,
a '||' b,
c &
a,
b '||' b,
c &
b,
a '||' c,
b &
b,
c '||' b,
a &
a,
b '||' c,
b &
c,
b '||' b,
a &
b,
c '||' a,
b &
c,
b '||' a,
b &
c,
a '||' c,
b &
a,
c '||' c,
b &
c,
a '||' b,
c &
a,
c '||' b,
c &
c,
b '||' c,
a &
b,
c '||' c,
a &
c,
b '||' a,
c &
b,
c '||' a,
c )
theorem Th26:
for
PS being
ParSp for
a,
b,
p,
q,
r,
s being
Element of
PS st
a <> b &
p,
q '||' a,
b &
a,
b '||' r,
s holds
p,
q '||' r,
s
theorem Th29:
for
PS being
ParSp for
a,
b,
c being
Element of
PS st not
a,
b '||' a,
c holds
( not
a,
c '||' a,
b & not
b,
a '||' a,
c & not
a,
b '||' c,
a & not
a,
c '||' b,
a & not
b,
a '||' c,
a & not
c,
a '||' a,
b & not
c,
a '||' b,
a & not
b,
a '||' b,
c & not
a,
b '||' b,
c & not
b,
a '||' c,
b & not
b,
c '||' b,
a & not
b,
a '||' c,
b & not
c,
b '||' b,
a & not
b,
c '||' a,
b & not
c,
b '||' a,
b & not
c,
a '||' c,
b & not
a,
c '||' c,
b & not
c,
a '||' b,
c & not
a,
c '||' b,
c & not
c,
b '||' c,
a & not
b,
c '||' c,
a & not
c,
b '||' a,
c & not
b,
c '||' a,
c )
theorem Th30:
for
PS being
ParSp for
a,
b,
c,
d,
p,
q,
r,
s being
Element of
PS st not
a,
b '||' c,
d &
a,
b '||' p,
q &
c,
d '||' r,
s &
p <> q &
r <> s holds
not
p,
q '||' r,
s
theorem Th31:
for
PS being
ParSp for
a,
b,
c,
p,
q,
r being
Element of
PS st not
a,
b '||' a,
c &
a,
b '||' p,
q &
a,
c '||' p,
r &
b,
c '||' q,
r &
p <> q holds
not
p,
q '||' p,
r
theorem Th32:
for
PS being
ParSp for
a,
b,
c,
p,
r being
Element of
PS st not
a,
b '||' a,
c &
a,
c '||' p,
r &
b,
c '||' p,
r holds
p = r
theorem
for
PS being
ParSp for
a,
b,
c,
p,
q,
r,
s being
Element of
PS st not
a,
b '||' a,
c &
a,
b '||' p,
q &
a,
c '||' p,
r &
a,
c '||' p,
s &
b,
c '||' q,
r &
b,
c '||' q,
s holds
r = s
theorem
for
PS being
ParSp st ( for
a,
b being
Element of
PS holds
a = b ) holds
for
p,
q,
r,
s being
Element of
PS holds
p,
q '||' r,
s
theorem
for
PS being
ParSp for
a,
b,
c,
p,
q being
Element of
PS st not
a,
b '||' a,
c &
p <> q &
p,
q '||' p,
a &
p,
q '||' p,
b holds
not
p,
q '||' p,
c
:: 3. DEFINITION OF PARALLELITY SPACE
::