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;
func c3add F -> BinOp of
[: the carrier of F, the carrier of F, the carrier of F:] means :
Def1:
for
x,
y being
Element of
[: the carrier of F, the carrier of F, the carrier of F:] holds
it . (
x,
y)
= [((x `1) + (y `1)),((x `2) + (y `2)),((x `3) + (y `3))];
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) + (y `1)),((x `2) + (y `2)),((x `3) + (y `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) + (y `1)),((x `2) + (y `2)),((x `3) + (y `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) + (y `1)),((x `2) + (y `2)),((x `3) + (y `3))] ) holds
b1 = b2
end;
:: deftheorem Def1 defines c3add PARSP_1:def 1 :
for F being Field
for b2 being BinOp of [: the carrier of F, the carrier of F, the carrier of F:] holds
( b2 = c3add F iff for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b2 . (x,y) = [((x `1) + (y `1)),((x `2) + (y `2)),((x `3) + (y `3))] );
:: deftheorem defines + PARSP_1:def 2 :
for F being Field
for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds x + y = (c3add F) . (x,y);
theorem
canceled;
theorem
canceled;
theorem
theorem Th4:
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;
func c3compl F -> UnOp of
[: the carrier of F, the carrier of F, the carrier of F:] means :
Def3:
for
x being
Element of
[: the carrier of F, the carrier of F, the carrier of F:] holds
it . x = [(- (x `1)),(- (x `2)),(- (x `3))];
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)),(- (x `2)),(- (x `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)),(- (x `2)),(- (x `3))] ) & ( for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b2 . x = [(- (x `1)),(- (x `2)),(- (x `3))] ) holds
b1 = b2
end;
:: deftheorem Def3 defines c3compl PARSP_1:def 3 :
for F being Field
for b2 being UnOp of [: the carrier of F, the carrier of F, the carrier of F:] holds
( b2 = c3compl F iff for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b2 . x = [(- (x `1)),(- (x `2)),(- (x `3))] );
:: deftheorem defines - PARSP_1:def 4 :
for F being Field
for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds - x = (c3compl F) . x;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem Def5 defines Relation4 PARSP_1:def 5 :
for S, b2 being set holds
( b2 is Relation4 of S iff b2 c= [:S,S,S,S:] );
:: deftheorem Def6 defines '||' PARSP_1:def 6 :
for PS being non empty ParStr
for a, b, c, d being Element of PS holds
( a,b '||' c,d iff [a,b,c,d] in the 4_arg_relation of PS );
:: deftheorem defines C3 PARSP_1:def 7 :
for F being Field holds C3 F = [: the carrier of F, the carrier of F, the carrier of F:];
:: deftheorem defines 4C3 PARSP_1:def 8 :
for F being Field holds 4C3 F = [:(C3 F),(C3 F),(C3 F),(C3 F):];
definition
let F be
Field;
func PRs F -> set means :
Def9:
for
x being
set holds
(
x in it iff (
x in 4C3 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) - (b `1)) * ((c `2) - (d `2))) - (((c `1) - (d `1)) * ((a `2) - (b `2))) = 0. F &
(((a `1) - (b `1)) * ((c `3) - (d `3))) - (((c `1) - (d `1)) * ((a `3) - (b `3))) = 0. F &
(((a `2) - (b `2)) * ((c `3) - (d `3))) - (((c `2) - (d `2)) * ((a `3) - (b `3))) = 0. F ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in 4C3 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) - (b `1)) * ((c `2) - (d `2))) - (((c `1) - (d `1)) * ((a `2) - (b `2))) = 0. F & (((a `1) - (b `1)) * ((c `3) - (d `3))) - (((c `1) - (d `1)) * ((a `3) - (b `3))) = 0. F & (((a `2) - (b `2)) * ((c `3) - (d `3))) - (((c `2) - (d `2)) * ((a `3) - (b `3))) = 0. F ) ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in 4C3 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) - (b `1)) * ((c `2) - (d `2))) - (((c `1) - (d `1)) * ((a `2) - (b `2))) = 0. F & (((a `1) - (b `1)) * ((c `3) - (d `3))) - (((c `1) - (d `1)) * ((a `3) - (b `3))) = 0. F & (((a `2) - (b `2)) * ((c `3) - (d `3))) - (((c `2) - (d `2)) * ((a `3) - (b `3))) = 0. F ) ) ) ) & ( for x being set holds
( x in b2 iff ( x in 4C3 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) - (b `1)) * ((c `2) - (d `2))) - (((c `1) - (d `1)) * ((a `2) - (b `2))) = 0. F & (((a `1) - (b `1)) * ((c `3) - (d `3))) - (((c `1) - (d `1)) * ((a `3) - (b `3))) = 0. F & (((a `2) - (b `2)) * ((c `3) - (d `3))) - (((c `2) - (d `2)) * ((a `3) - (b `3))) = 0. F ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def9 defines PRs PARSP_1:def 9 :
for F being Field
for b2 being set holds
( b2 = PRs F iff for x being set holds
( x in b2 iff ( x in 4C3 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) - (b `1)) * ((c `2) - (d `2))) - (((c `1) - (d `1)) * ((a `2) - (b `2))) = 0. F & (((a `1) - (b `1)) * ((c `3) - (d `3))) - (((c `1) - (d `1)) * ((a `3) - (b `3))) = 0. F & (((a `2) - (b `2)) * ((c `3) - (d `3))) - (((c `2) - (d `2)) * ((a `3) - (b `3))) = 0. F ) ) ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th13:
:: deftheorem defines PR PARSP_1:def 10 :
for F being Field holds PR F = PRs F;
:: deftheorem defines MPS PARSP_1:def 11 :
for F being Field holds MPS F = ParStr(# (C3 F),(PR F) #);
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
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 4C3 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) - (f `1)) * ((g `2) - (h `2))) - (((g `1) - (h `1)) * ((e `2) - (f `2))) = 0. F &
(((e `1) - (f `1)) * ((g `3) - (h `3))) - (((g `1) - (h `1)) * ((e `3) - (f `3))) = 0. F &
(((e `2) - (f `2)) * ((g `3) - (h `3))) - (((g `2) - (h `2)) * ((e `3) - (f `3))) = 0. F ) ) )
by Def9;
theorem Th20:
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 4C3 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) - (f `1)) * ((g `2) - (h `2))) - (((g `1) - (h `1)) * ((e `2) - (f `2))) = 0. F &
(((e `1) - (f `1)) * ((g `3) - (h `3))) - (((g `1) - (h `1)) * ((e `3) - (f `3))) = 0. F &
(((e `2) - (f `2)) * ((g `3) - (h `3))) - (((g `2) - (h `2)) * ((e `3) - (f `3))) = 0. F ) ) )
theorem
theorem
theorem Th23:
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) - (f `1)) * ((g `2) - (h `2))) - (((g `1) - (h `1)) * ((e `2) - (f `2))) = 0. F &
(((e `1) - (f `1)) * ((g `3) - (h `3))) - (((g `1) - (h `1)) * ((e `3) - (f `3))) = 0. F &
(((e `2) - (f `2)) * ((g `3) - (h `3))) - (((g `2) - (h `2)) * ((e `3) - (f `3))) = 0. F ) )
theorem Th24:
theorem Th25:
theorem Th26:
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
theorem Th27:
theorem Th28:
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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
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 Th41:
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
theorem Th43:
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
theorem
theorem
canceled;
theorem Th47:
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 Th48:
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 Th49:
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 Th50:
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 Th51:
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 Th53:
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
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