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 :
:: deftheorem defines + PARSP_1:def 2 :
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 :
:: deftheorem defines - PARSP_1:def 4 :
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem Def5 defines Relation4 PARSP_1:def 5 :
:: deftheorem Def6 defines '||' PARSP_1:def 6 :
:: deftheorem defines C3 PARSP_1:def 7 :
:: deftheorem defines 4C3 PARSP_1:def 8 :
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 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th13:
:: deftheorem defines PR PARSP_1:def 10 :
:: deftheorem defines MPS PARSP_1:def 11 :
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